S1 tolerates S2 by CIRCCOMB:47;
then InputVertices (S1 +* S2) is Subset of ((InputVertices S1) \/ (InputVertices S2)) by CIRCCOMB:11;
hence not InputVertices (S1 +* S2) is with_pair ; :: according to CIRCCMB3:def 11 :: thesis: verum