%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GRA011+1 : TPTP v5.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 09:57:29 EST 2010
% Result : Theorem 74.60s
% Output : CNFRefutation 74.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 16
% Syntax : Number of formulae : 348 ( 14 unt; 0 def)
% Number of atoms : 2072 ( 510 equ)
% Maximal formula atoms : 37 ( 5 avg)
% Number of connectives : 2929 (1205 ~;1524 |; 165 &)
% ( 10 <=>; 22 =>; 1 <=; 2 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 7 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-5 aty)
% Number of variables : 1309 ( 240 sgn 215 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1] :
( edge(X1)
=> ( vertex(head_of(X1))
& vertex(tail_of(X1)) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',edge_ends_are_vertices) ).
fof(2,axiom,
! [X2,X3] :
( sequential(X2,X3)
<=> ( edge(X2)
& edge(X3)
& X2 != X3
& head_of(X2) = tail_of(X3) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',sequential_defn) ).
fof(3,axiom,
! [X1] :
( edge(X1)
=> head_of(X1) != tail_of(X1) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',no_loops) ).
fof(4,axiom,
! [X4,X5,X6] :
( shortest_path(X4,X5,X6)
<=> ( path(X4,X5,X6)
& X4 != X5
& ! [X7] :
( path(X4,X5,X7)
=> less_or_equal(length_of(X6),length_of(X7)) ) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',shortest_path_defn) ).
fof(5,axiom,
( complete
=> ! [X4,X5] :
( ( vertex(X4)
& vertex(X5)
& X4 != X5 )
=> ? [X1] :
( edge(X1)
& ( ( X4 = head_of(X1)
& X5 = tail_of(X1) )
<~> ( X5 = head_of(X1)
& X4 = tail_of(X1) ) ) ) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',complete_properties) ).
fof(6,axiom,
! [X7,X4,X5] :
( path(X4,X5,X7)
=> ! [X2,X3] :
( precedes(X2,X3,X7)
=> ( on_path(X2,X7)
& on_path(X3,X7)
& ( sequential(X2,X3)
<~> ? [X8] :
( sequential(X2,X8)
& precedes(X8,X3,X7) ) ) ) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',precedes_properties) ).
fof(7,axiom,
! [X4,X5,X2,X3,X7] :
( ( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7) )
=> ( ~ ? [X8] :
( tail_of(X8) = tail_of(X2)
& head_of(X8) = head_of(X3) )
& ~ precedes(X3,X2,X7) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',shortest_path_properties) ).
fof(8,axiom,
! [X7,X4,X5] :
( path(X4,X5,X7)
=> ! [X2,X3] :
( precedes(X2,X3,X7)
<= ( on_path(X2,X7)
& on_path(X3,X7)
& ( sequential(X2,X3)
| ? [X8] :
( sequential(X2,X8)
& precedes(X8,X3,X7) ) ) ) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',precedes_defn) ).
fof(9,conjecture,
( complete
=> ! [X7,X4,X5] :
( shortest_path(X4,X5,X7)
=> number_of_in(sequential_pairs,X7) = number_of_in(triangles,X7) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',triangles_and_sequential_pairs) ).
fof(11,axiom,
! [X7,X4,X5] :
( ( path(X4,X5,X7)
& ! [X2,X3] :
( ( on_path(X2,X7)
& on_path(X3,X7)
& sequential(X2,X3) )
=> ? [X8] : triangle(X2,X3,X8) ) )
=> number_of_in(sequential_pairs,X7) = number_of_in(triangles,X7) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',sequential_pairs_and_triangles) ).
fof(13,axiom,
! [X2,X3,X8] :
( triangle(X2,X3,X8)
<=> ( edge(X2)
& edge(X3)
& edge(X8)
& sequential(X2,X3)
& sequential(X3,X8)
& sequential(X8,X2) ) ),
file('/tmp/tmpt82AUg/sel_GRA011+1.p_2',triangle_defn) ).
fof(15,negated_conjecture,
~ ( complete
=> ! [X7,X4,X5] :
( shortest_path(X4,X5,X7)
=> number_of_in(sequential_pairs,X7) = number_of_in(triangles,X7) ) ),
inference(assume_negation,[status(cth)],[9]) ).
fof(16,plain,
( complete
=> ! [X4,X5] :
( ( vertex(X4)
& vertex(X5)
& X4 != X5 )
=> ? [X1] :
( edge(X1)
& ~ ( ( X4 = head_of(X1)
& X5 = tail_of(X1) )
<=> ( X5 = head_of(X1)
& X4 = tail_of(X1) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[5,theory(equality)]) ).
fof(17,plain,
! [X7,X4,X5] :
( path(X4,X5,X7)
=> ! [X2,X3] :
( precedes(X2,X3,X7)
=> ( on_path(X2,X7)
& on_path(X3,X7)
& ~ ( sequential(X2,X3)
<=> ? [X8] :
( sequential(X2,X8)
& precedes(X8,X3,X7) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[6,theory(equality)]) ).
fof(18,plain,
! [X4,X5,X2,X3,X7] :
( ( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7) )
=> ( ~ ? [X8] :
( tail_of(X8) = tail_of(X2)
& head_of(X8) = head_of(X3) )
& ~ precedes(X3,X2,X7) ) ),
inference(fof_simplification,[status(thm)],[7,theory(equality)]) ).
fof(19,plain,
! [X7,X4,X5] :
( path(X4,X5,X7)
=> ! [X2,X3] :
( ( on_path(X2,X7)
& on_path(X3,X7)
& ( sequential(X2,X3)
| ? [X8] :
( sequential(X2,X8)
& precedes(X8,X3,X7) ) ) )
=> precedes(X2,X3,X7) ) ),
inference(fof_simplification,[status(thm)],[8,theory(equality)]) ).
fof(20,plain,
! [X1] :
( ~ edge(X1)
| ( vertex(head_of(X1))
& vertex(tail_of(X1)) ) ),
inference(fof_nnf,[status(thm)],[1]) ).
fof(21,plain,
! [X2] :
( ~ edge(X2)
| ( vertex(head_of(X2))
& vertex(tail_of(X2)) ) ),
inference(variable_rename,[status(thm)],[20]) ).
fof(22,plain,
! [X2] :
( ( vertex(head_of(X2))
| ~ edge(X2) )
& ( vertex(tail_of(X2))
| ~ edge(X2) ) ),
inference(distribute,[status(thm)],[21]) ).
cnf(23,plain,
( vertex(tail_of(X1))
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(24,plain,
( vertex(head_of(X1))
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[22]) ).
fof(25,plain,
! [X2,X3] :
( ( ~ sequential(X2,X3)
| ( edge(X2)
& edge(X3)
& X2 != X3
& head_of(X2) = tail_of(X3) ) )
& ( ~ edge(X2)
| ~ edge(X3)
| X2 = X3
| head_of(X2) != tail_of(X3)
| sequential(X2,X3) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(26,plain,
! [X4,X5] :
( ( ~ sequential(X4,X5)
| ( edge(X4)
& edge(X5)
& X4 != X5
& head_of(X4) = tail_of(X5) ) )
& ( ~ edge(X4)
| ~ edge(X5)
| X4 = X5
| head_of(X4) != tail_of(X5)
| sequential(X4,X5) ) ),
inference(variable_rename,[status(thm)],[25]) ).
fof(27,plain,
! [X4,X5] :
( ( edge(X4)
| ~ sequential(X4,X5) )
& ( edge(X5)
| ~ sequential(X4,X5) )
& ( X4 != X5
| ~ sequential(X4,X5) )
& ( head_of(X4) = tail_of(X5)
| ~ sequential(X4,X5) )
& ( ~ edge(X4)
| ~ edge(X5)
| X4 = X5
| head_of(X4) != tail_of(X5)
| sequential(X4,X5) ) ),
inference(distribute,[status(thm)],[26]) ).
cnf(28,plain,
( sequential(X1,X2)
| X1 = X2
| head_of(X1) != tail_of(X2)
| ~ edge(X2)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(29,plain,
( head_of(X1) = tail_of(X2)
| ~ sequential(X1,X2) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(30,plain,
( ~ sequential(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(31,plain,
( edge(X2)
| ~ sequential(X1,X2) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(32,plain,
( edge(X1)
| ~ sequential(X1,X2) ),
inference(split_conjunct,[status(thm)],[27]) ).
fof(33,plain,
! [X1] :
( ~ edge(X1)
| head_of(X1) != tail_of(X1) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(34,plain,
! [X2] :
( ~ edge(X2)
| head_of(X2) != tail_of(X2) ),
inference(variable_rename,[status(thm)],[33]) ).
cnf(35,plain,
( head_of(X1) != tail_of(X1)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[34]) ).
fof(36,plain,
! [X4,X5,X6] :
( ( ~ shortest_path(X4,X5,X6)
| ( path(X4,X5,X6)
& X4 != X5
& ! [X7] :
( ~ path(X4,X5,X7)
| less_or_equal(length_of(X6),length_of(X7)) ) ) )
& ( ~ path(X4,X5,X6)
| X4 = X5
| ? [X7] :
( path(X4,X5,X7)
& ~ less_or_equal(length_of(X6),length_of(X7)) )
| shortest_path(X4,X5,X6) ) ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(37,plain,
! [X8,X9,X10] :
( ( ~ shortest_path(X8,X9,X10)
| ( path(X8,X9,X10)
& X8 != X9
& ! [X11] :
( ~ path(X8,X9,X11)
| less_or_equal(length_of(X10),length_of(X11)) ) ) )
& ( ~ path(X8,X9,X10)
| X8 = X9
| ? [X12] :
( path(X8,X9,X12)
& ~ less_or_equal(length_of(X10),length_of(X12)) )
| shortest_path(X8,X9,X10) ) ),
inference(variable_rename,[status(thm)],[36]) ).
fof(38,plain,
! [X8,X9,X10] :
( ( ~ shortest_path(X8,X9,X10)
| ( path(X8,X9,X10)
& X8 != X9
& ! [X11] :
( ~ path(X8,X9,X11)
| less_or_equal(length_of(X10),length_of(X11)) ) ) )
& ( ~ path(X8,X9,X10)
| X8 = X9
| ( path(X8,X9,esk1_3(X8,X9,X10))
& ~ less_or_equal(length_of(X10),length_of(esk1_3(X8,X9,X10))) )
| shortest_path(X8,X9,X10) ) ),
inference(skolemize,[status(esa)],[37]) ).
fof(39,plain,
! [X8,X9,X10,X11] :
( ( ( ( ~ path(X8,X9,X11)
| less_or_equal(length_of(X10),length_of(X11)) )
& path(X8,X9,X10)
& X8 != X9 )
| ~ shortest_path(X8,X9,X10) )
& ( ~ path(X8,X9,X10)
| X8 = X9
| ( path(X8,X9,esk1_3(X8,X9,X10))
& ~ less_or_equal(length_of(X10),length_of(esk1_3(X8,X9,X10))) )
| shortest_path(X8,X9,X10) ) ),
inference(shift_quantors,[status(thm)],[38]) ).
fof(40,plain,
! [X8,X9,X10,X11] :
( ( ~ path(X8,X9,X11)
| less_or_equal(length_of(X10),length_of(X11))
| ~ shortest_path(X8,X9,X10) )
& ( path(X8,X9,X10)
| ~ shortest_path(X8,X9,X10) )
& ( X8 != X9
| ~ shortest_path(X8,X9,X10) )
& ( path(X8,X9,esk1_3(X8,X9,X10))
| ~ path(X8,X9,X10)
| X8 = X9
| shortest_path(X8,X9,X10) )
& ( ~ less_or_equal(length_of(X10),length_of(esk1_3(X8,X9,X10)))
| ~ path(X8,X9,X10)
| X8 = X9
| shortest_path(X8,X9,X10) ) ),
inference(distribute,[status(thm)],[39]) ).
cnf(44,plain,
( path(X1,X2,X3)
| ~ shortest_path(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[40]) ).
fof(46,plain,
( ~ complete
| ! [X4,X5] :
( ~ vertex(X4)
| ~ vertex(X5)
| X4 = X5
| ? [X1] :
( edge(X1)
& ( X4 != head_of(X1)
| X5 != tail_of(X1)
| X5 != head_of(X1)
| X4 != tail_of(X1) )
& ( ( X4 = head_of(X1)
& X5 = tail_of(X1) )
| ( X5 = head_of(X1)
& X4 = tail_of(X1) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(47,plain,
( ~ complete
| ! [X6,X7] :
( ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ? [X8] :
( edge(X8)
& ( X6 != head_of(X8)
| X7 != tail_of(X8)
| X7 != head_of(X8)
| X6 != tail_of(X8) )
& ( ( X6 = head_of(X8)
& X7 = tail_of(X8) )
| ( X7 = head_of(X8)
& X6 = tail_of(X8) ) ) ) ) ),
inference(variable_rename,[status(thm)],[46]) ).
fof(48,plain,
( ~ complete
| ! [X6,X7] :
( ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ( edge(esk2_2(X6,X7))
& ( X6 != head_of(esk2_2(X6,X7))
| X7 != tail_of(esk2_2(X6,X7))
| X7 != head_of(esk2_2(X6,X7))
| X6 != tail_of(esk2_2(X6,X7)) )
& ( ( X6 = head_of(esk2_2(X6,X7))
& X7 = tail_of(esk2_2(X6,X7)) )
| ( X7 = head_of(esk2_2(X6,X7))
& X6 = tail_of(esk2_2(X6,X7)) ) ) ) ) ),
inference(skolemize,[status(esa)],[47]) ).
fof(49,plain,
! [X6,X7] :
( ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ( edge(esk2_2(X6,X7))
& ( X6 != head_of(esk2_2(X6,X7))
| X7 != tail_of(esk2_2(X6,X7))
| X7 != head_of(esk2_2(X6,X7))
| X6 != tail_of(esk2_2(X6,X7)) )
& ( ( X6 = head_of(esk2_2(X6,X7))
& X7 = tail_of(esk2_2(X6,X7)) )
| ( X7 = head_of(esk2_2(X6,X7))
& X6 = tail_of(esk2_2(X6,X7)) ) ) )
| ~ complete ),
inference(shift_quantors,[status(thm)],[48]) ).
fof(50,plain,
! [X6,X7] :
( ( edge(esk2_2(X6,X7))
| ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ~ complete )
& ( X6 != head_of(esk2_2(X6,X7))
| X7 != tail_of(esk2_2(X6,X7))
| X7 != head_of(esk2_2(X6,X7))
| X6 != tail_of(esk2_2(X6,X7))
| ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ~ complete )
& ( X7 = head_of(esk2_2(X6,X7))
| X6 = head_of(esk2_2(X6,X7))
| ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ~ complete )
& ( X6 = tail_of(esk2_2(X6,X7))
| X6 = head_of(esk2_2(X6,X7))
| ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ~ complete )
& ( X7 = head_of(esk2_2(X6,X7))
| X7 = tail_of(esk2_2(X6,X7))
| ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ~ complete )
& ( X6 = tail_of(esk2_2(X6,X7))
| X7 = tail_of(esk2_2(X6,X7))
| ~ vertex(X6)
| ~ vertex(X7)
| X6 = X7
| ~ complete ) ),
inference(distribute,[status(thm)],[49]) ).
cnf(51,plain,
( X1 = X2
| X2 = tail_of(esk2_2(X1,X2))
| X1 = tail_of(esk2_2(X1,X2))
| ~ complete
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(split_conjunct,[status(thm)],[50]) ).
cnf(52,plain,
( X1 = X2
| X2 = tail_of(esk2_2(X1,X2))
| X2 = head_of(esk2_2(X1,X2))
| ~ complete
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(split_conjunct,[status(thm)],[50]) ).
cnf(53,plain,
( X1 = X2
| X1 = head_of(esk2_2(X1,X2))
| X1 = tail_of(esk2_2(X1,X2))
| ~ complete
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(split_conjunct,[status(thm)],[50]) ).
cnf(56,plain,
( X1 = X2
| edge(esk2_2(X1,X2))
| ~ complete
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(split_conjunct,[status(thm)],[50]) ).
fof(57,plain,
! [X7,X4,X5] :
( ~ path(X4,X5,X7)
| ! [X2,X3] :
( ~ precedes(X2,X3,X7)
| ( on_path(X2,X7)
& on_path(X3,X7)
& ( ~ sequential(X2,X3)
| ! [X8] :
( ~ sequential(X2,X8)
| ~ precedes(X8,X3,X7) ) )
& ( sequential(X2,X3)
| ? [X8] :
( sequential(X2,X8)
& precedes(X8,X3,X7) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(58,plain,
! [X9,X10,X11] :
( ~ path(X10,X11,X9)
| ! [X12,X13] :
( ~ precedes(X12,X13,X9)
| ( on_path(X12,X9)
& on_path(X13,X9)
& ( ~ sequential(X12,X13)
| ! [X14] :
( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9) ) )
& ( sequential(X12,X13)
| ? [X15] :
( sequential(X12,X15)
& precedes(X15,X13,X9) ) ) ) ) ),
inference(variable_rename,[status(thm)],[57]) ).
fof(59,plain,
! [X9,X10,X11] :
( ~ path(X10,X11,X9)
| ! [X12,X13] :
( ~ precedes(X12,X13,X9)
| ( on_path(X12,X9)
& on_path(X13,X9)
& ( ~ sequential(X12,X13)
| ! [X14] :
( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9) ) )
& ( sequential(X12,X13)
| ( sequential(X12,esk3_5(X9,X10,X11,X12,X13))
& precedes(esk3_5(X9,X10,X11,X12,X13),X13,X9) ) ) ) ) ),
inference(skolemize,[status(esa)],[58]) ).
fof(60,plain,
! [X9,X10,X11,X12,X13,X14] :
( ( ( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9)
| ~ sequential(X12,X13) )
& ( sequential(X12,X13)
| ( sequential(X12,esk3_5(X9,X10,X11,X12,X13))
& precedes(esk3_5(X9,X10,X11,X12,X13),X13,X9) ) )
& on_path(X12,X9)
& on_path(X13,X9) )
| ~ precedes(X12,X13,X9)
| ~ path(X10,X11,X9) ),
inference(shift_quantors,[status(thm)],[59]) ).
fof(61,plain,
! [X9,X10,X11,X12,X13,X14] :
( ( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9)
| ~ sequential(X12,X13)
| ~ precedes(X12,X13,X9)
| ~ path(X10,X11,X9) )
& ( sequential(X12,esk3_5(X9,X10,X11,X12,X13))
| sequential(X12,X13)
| ~ precedes(X12,X13,X9)
| ~ path(X10,X11,X9) )
& ( precedes(esk3_5(X9,X10,X11,X12,X13),X13,X9)
| sequential(X12,X13)
| ~ precedes(X12,X13,X9)
| ~ path(X10,X11,X9) )
& ( on_path(X12,X9)
| ~ precedes(X12,X13,X9)
| ~ path(X10,X11,X9) )
& ( on_path(X13,X9)
| ~ precedes(X12,X13,X9)
| ~ path(X10,X11,X9) ) ),
inference(distribute,[status(thm)],[60]) ).
cnf(62,plain,
( on_path(X5,X3)
| ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[61]) ).
cnf(63,plain,
( on_path(X4,X3)
| ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[61]) ).
cnf(64,plain,
( sequential(X4,X5)
| precedes(esk3_5(X3,X1,X2,X4,X5),X5,X3)
| ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[61]) ).
cnf(65,plain,
( sequential(X4,X5)
| sequential(X4,esk3_5(X3,X1,X2,X4,X5))
| ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[61]) ).
cnf(66,plain,
( ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3)
| ~ sequential(X4,X5)
| ~ precedes(X6,X5,X3)
| ~ sequential(X4,X6) ),
inference(split_conjunct,[status(thm)],[61]) ).
fof(67,plain,
! [X4,X5,X2,X3,X7] :
( ~ shortest_path(X4,X5,X7)
| ~ precedes(X2,X3,X7)
| ( ! [X8] :
( tail_of(X8) != tail_of(X2)
| head_of(X8) != head_of(X3) )
& ~ precedes(X3,X2,X7) ) ),
inference(fof_nnf,[status(thm)],[18]) ).
fof(68,plain,
! [X9,X10,X11,X12,X13] :
( ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ( ! [X14] :
( tail_of(X14) != tail_of(X11)
| head_of(X14) != head_of(X12) )
& ~ precedes(X12,X11,X13) ) ),
inference(variable_rename,[status(thm)],[67]) ).
fof(69,plain,
! [X9,X10,X11,X12,X13,X14] :
( ( ( tail_of(X14) != tail_of(X11)
| head_of(X14) != head_of(X12) )
& ~ precedes(X12,X11,X13) )
| ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13) ),
inference(shift_quantors,[status(thm)],[68]) ).
fof(70,plain,
! [X9,X10,X11,X12,X13,X14] :
( ( tail_of(X14) != tail_of(X11)
| head_of(X14) != head_of(X12)
| ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13) )
& ( ~ precedes(X12,X11,X13)
| ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13) ) ),
inference(distribute,[status(thm)],[69]) ).
cnf(71,plain,
( ~ precedes(X1,X2,X3)
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[70]) ).
cnf(72,plain,
( ~ precedes(X1,X2,X3)
| ~ shortest_path(X4,X5,X3)
| head_of(X6) != head_of(X2)
| tail_of(X6) != tail_of(X1) ),
inference(split_conjunct,[status(thm)],[70]) ).
fof(73,plain,
! [X7,X4,X5] :
( ~ path(X4,X5,X7)
| ! [X2,X3] :
( ~ on_path(X2,X7)
| ~ on_path(X3,X7)
| ( ~ sequential(X2,X3)
& ! [X8] :
( ~ sequential(X2,X8)
| ~ precedes(X8,X3,X7) ) )
| precedes(X2,X3,X7) ) ),
inference(fof_nnf,[status(thm)],[19]) ).
fof(74,plain,
! [X9,X10,X11] :
( ~ path(X10,X11,X9)
| ! [X12,X13] :
( ~ on_path(X12,X9)
| ~ on_path(X13,X9)
| ( ~ sequential(X12,X13)
& ! [X14] :
( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9) ) )
| precedes(X12,X13,X9) ) ),
inference(variable_rename,[status(thm)],[73]) ).
fof(75,plain,
! [X9,X10,X11,X12,X13,X14] :
( ( ( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9) )
& ~ sequential(X12,X13) )
| ~ on_path(X12,X9)
| ~ on_path(X13,X9)
| precedes(X12,X13,X9)
| ~ path(X10,X11,X9) ),
inference(shift_quantors,[status(thm)],[74]) ).
fof(76,plain,
! [X9,X10,X11,X12,X13,X14] :
( ( ~ sequential(X12,X14)
| ~ precedes(X14,X13,X9)
| ~ on_path(X12,X9)
| ~ on_path(X13,X9)
| precedes(X12,X13,X9)
| ~ path(X10,X11,X9) )
& ( ~ sequential(X12,X13)
| ~ on_path(X12,X9)
| ~ on_path(X13,X9)
| precedes(X12,X13,X9)
| ~ path(X10,X11,X9) ) ),
inference(distribute,[status(thm)],[75]) ).
cnf(77,plain,
( precedes(X4,X5,X3)
| ~ path(X1,X2,X3)
| ~ on_path(X5,X3)
| ~ on_path(X4,X3)
| ~ sequential(X4,X5) ),
inference(split_conjunct,[status(thm)],[76]) ).
cnf(78,plain,
( precedes(X4,X5,X3)
| ~ path(X1,X2,X3)
| ~ on_path(X5,X3)
| ~ on_path(X4,X3)
| ~ precedes(X6,X5,X3)
| ~ sequential(X4,X6) ),
inference(split_conjunct,[status(thm)],[76]) ).
fof(79,negated_conjecture,
( complete
& ? [X7,X4,X5] :
( shortest_path(X4,X5,X7)
& number_of_in(sequential_pairs,X7) != number_of_in(triangles,X7) ) ),
inference(fof_nnf,[status(thm)],[15]) ).
fof(80,negated_conjecture,
( complete
& ? [X8,X9,X10] :
( shortest_path(X9,X10,X8)
& number_of_in(sequential_pairs,X8) != number_of_in(triangles,X8) ) ),
inference(variable_rename,[status(thm)],[79]) ).
fof(81,negated_conjecture,
( complete
& shortest_path(esk5_0,esk6_0,esk4_0)
& number_of_in(sequential_pairs,esk4_0) != number_of_in(triangles,esk4_0) ),
inference(skolemize,[status(esa)],[80]) ).
cnf(82,negated_conjecture,
number_of_in(sequential_pairs,esk4_0) != number_of_in(triangles,esk4_0),
inference(split_conjunct,[status(thm)],[81]) ).
cnf(83,negated_conjecture,
shortest_path(esk5_0,esk6_0,esk4_0),
inference(split_conjunct,[status(thm)],[81]) ).
cnf(84,negated_conjecture,
complete,
inference(split_conjunct,[status(thm)],[81]) ).
fof(87,plain,
! [X7,X4,X5] :
( ~ path(X4,X5,X7)
| ? [X2,X3] :
( on_path(X2,X7)
& on_path(X3,X7)
& sequential(X2,X3)
& ! [X8] : ~ triangle(X2,X3,X8) )
| number_of_in(sequential_pairs,X7) = number_of_in(triangles,X7) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(88,plain,
! [X9,X10,X11] :
( ~ path(X10,X11,X9)
| ? [X12,X13] :
( on_path(X12,X9)
& on_path(X13,X9)
& sequential(X12,X13)
& ! [X14] : ~ triangle(X12,X13,X14) )
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ),
inference(variable_rename,[status(thm)],[87]) ).
fof(89,plain,
! [X9,X10,X11] :
( ~ path(X10,X11,X9)
| ( on_path(esk7_3(X9,X10,X11),X9)
& on_path(esk8_3(X9,X10,X11),X9)
& sequential(esk7_3(X9,X10,X11),esk8_3(X9,X10,X11))
& ! [X14] : ~ triangle(esk7_3(X9,X10,X11),esk8_3(X9,X10,X11),X14) )
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ),
inference(skolemize,[status(esa)],[88]) ).
fof(90,plain,
! [X9,X10,X11,X14] :
( ( ~ triangle(esk7_3(X9,X10,X11),esk8_3(X9,X10,X11),X14)
& on_path(esk7_3(X9,X10,X11),X9)
& on_path(esk8_3(X9,X10,X11),X9)
& sequential(esk7_3(X9,X10,X11),esk8_3(X9,X10,X11)) )
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ),
inference(shift_quantors,[status(thm)],[89]) ).
fof(91,plain,
! [X9,X10,X11,X14] :
( ( ~ triangle(esk7_3(X9,X10,X11),esk8_3(X9,X10,X11),X14)
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) )
& ( on_path(esk7_3(X9,X10,X11),X9)
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) )
& ( on_path(esk8_3(X9,X10,X11),X9)
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) )
& ( sequential(esk7_3(X9,X10,X11),esk8_3(X9,X10,X11))
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ) ),
inference(distribute,[status(thm)],[90]) ).
cnf(92,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| sequential(esk7_3(X1,X2,X3),esk8_3(X1,X2,X3))
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[91]) ).
cnf(93,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| on_path(esk8_3(X1,X2,X3),X1)
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[91]) ).
cnf(94,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| on_path(esk7_3(X1,X2,X3),X1)
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[91]) ).
cnf(95,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| ~ path(X2,X3,X1)
| ~ triangle(esk7_3(X1,X2,X3),esk8_3(X1,X2,X3),X4) ),
inference(split_conjunct,[status(thm)],[91]) ).
fof(99,plain,
! [X2,X3,X8] :
( ( ~ triangle(X2,X3,X8)
| ( edge(X2)
& edge(X3)
& edge(X8)
& sequential(X2,X3)
& sequential(X3,X8)
& sequential(X8,X2) ) )
& ( ~ edge(X2)
| ~ edge(X3)
| ~ edge(X8)
| ~ sequential(X2,X3)
| ~ sequential(X3,X8)
| ~ sequential(X8,X2)
| triangle(X2,X3,X8) ) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(100,plain,
! [X9,X10,X11] :
( ( ~ triangle(X9,X10,X11)
| ( edge(X9)
& edge(X10)
& edge(X11)
& sequential(X9,X10)
& sequential(X10,X11)
& sequential(X11,X9) ) )
& ( ~ edge(X9)
| ~ edge(X10)
| ~ edge(X11)
| ~ sequential(X9,X10)
| ~ sequential(X10,X11)
| ~ sequential(X11,X9)
| triangle(X9,X10,X11) ) ),
inference(variable_rename,[status(thm)],[99]) ).
fof(101,plain,
! [X9,X10,X11] :
( ( edge(X9)
| ~ triangle(X9,X10,X11) )
& ( edge(X10)
| ~ triangle(X9,X10,X11) )
& ( edge(X11)
| ~ triangle(X9,X10,X11) )
& ( sequential(X9,X10)
| ~ triangle(X9,X10,X11) )
& ( sequential(X10,X11)
| ~ triangle(X9,X10,X11) )
& ( sequential(X11,X9)
| ~ triangle(X9,X10,X11) )
& ( ~ edge(X9)
| ~ edge(X10)
| ~ edge(X11)
| ~ sequential(X9,X10)
| ~ sequential(X10,X11)
| ~ sequential(X11,X9)
| triangle(X9,X10,X11) ) ),
inference(distribute,[status(thm)],[100]) ).
cnf(102,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2)
| ~ edge(X3)
| ~ edge(X2)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[101]) ).
cnf(113,plain,
~ sequential(X1,X1),
inference(er,[status(thm)],[30,theory(equality)]) ).
cnf(114,negated_conjecture,
path(esk5_0,esk6_0,esk4_0),
inference(spm,[status(thm)],[44,83,theory(equality)]) ).
cnf(115,plain,
( X1 = X2
| edge(esk2_2(X1,X2))
| $false
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(rw,[status(thm)],[56,84,theory(equality)]) ).
cnf(116,plain,
( X1 = X2
| edge(esk2_2(X1,X2))
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[115,theory(equality)]) ).
cnf(120,plain,
( edge(esk8_3(X1,X2,X3))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[31,92,theory(equality)]) ).
cnf(121,plain,
( edge(esk7_3(X1,X2,X3))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[32,92,theory(equality)]) ).
cnf(128,plain,
( X1 = X2
| head_of(esk2_2(X1,X2)) = X2
| tail_of(esk2_2(X1,X2)) = X2
| $false
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(rw,[status(thm)],[52,84,theory(equality)]) ).
cnf(129,plain,
( X1 = X2
| head_of(esk2_2(X1,X2)) = X2
| tail_of(esk2_2(X1,X2)) = X2
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[128,theory(equality)]) ).
cnf(133,plain,
( X1 = X2
| head_of(esk2_2(X1,X2)) = X1
| tail_of(esk2_2(X1,X2)) = X1
| $false
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(rw,[status(thm)],[53,84,theory(equality)]) ).
cnf(134,plain,
( X1 = X2
| head_of(esk2_2(X1,X2)) = X1
| tail_of(esk2_2(X1,X2)) = X1
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[133,theory(equality)]) ).
cnf(137,plain,
( esk2_2(X1,X2) = X3
| sequential(esk2_2(X1,X2),X3)
| tail_of(esk2_2(X1,X2)) = X1
| X1 = X2
| tail_of(X3) != X1
| ~ edge(X3)
| ~ edge(esk2_2(X1,X2))
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(spm,[status(thm)],[28,134,theory(equality)]) ).
cnf(139,plain,
( X1 = X2
| tail_of(esk2_2(X1,X2)) = X2
| tail_of(esk2_2(X1,X2)) = X1
| $false
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(rw,[status(thm)],[51,84,theory(equality)]) ).
cnf(140,plain,
( X1 = X2
| tail_of(esk2_2(X1,X2)) = X2
| tail_of(esk2_2(X1,X2)) = X1
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[139,theory(equality)]) ).
cnf(141,plain,
( tail_of(esk2_2(X1,head_of(X2))) = X1
| tail_of(esk2_2(X1,head_of(X2))) = head_of(X2)
| X1 = head_of(X2)
| ~ vertex(X1)
| ~ edge(X2) ),
inference(spm,[status(thm)],[140,24,theory(equality)]) ).
cnf(143,plain,
( edge(esk3_5(X1,X2,X3,X4,X5))
| sequential(X4,X5)
| ~ precedes(X4,X5,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[31,65,theory(equality)]) ).
cnf(144,plain,
( edge(X1)
| sequential(X1,X5)
| ~ precedes(X1,X5,X2)
| ~ path(X3,X4,X2) ),
inference(spm,[status(thm)],[32,65,theory(equality)]) ).
cnf(145,plain,
( tail_of(esk3_5(X1,X2,X3,X4,X5)) = head_of(X4)
| sequential(X4,X5)
| ~ precedes(X4,X5,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[29,65,theory(equality)]) ).
cnf(146,plain,
( sequential(X4,X5)
| ~ precedes(X5,esk3_5(X1,X2,X3,X4,X5),X1)
| ~ shortest_path(X6,X7,X1)
| ~ precedes(X4,X5,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[71,64,theory(equality)]) ).
cnf(148,plain,
( on_path(esk3_5(X1,X2,X3,X4,X5),X1)
| sequential(X4,X5)
| ~ path(X6,X7,X1)
| ~ precedes(X4,X5,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[63,64,theory(equality)]) ).
cnf(151,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2)
| ~ edge(X3)
| ~ edge(X2) ),
inference(csr,[status(thm)],[102,32]) ).
cnf(152,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2)
| ~ edge(X3) ),
inference(csr,[status(thm)],[151,32]) ).
cnf(153,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2) ),
inference(csr,[status(thm)],[152,32]) ).
cnf(160,plain,
( number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1)
| ~ sequential(X4,esk7_3(X1,X2,X3))
| ~ sequential(esk8_3(X1,X2,X3),X4)
| ~ sequential(esk7_3(X1,X2,X3),esk8_3(X1,X2,X3)) ),
inference(spm,[status(thm)],[95,153,theory(equality)]) ).
cnf(161,plain,
( precedes(X4,X5,X3)
| ~ on_path(X4,X3)
| ~ precedes(X6,X5,X3)
| ~ path(X1,X2,X3)
| ~ sequential(X4,X6) ),
inference(csr,[status(thm)],[78,62]) ).
cnf(167,negated_conjecture,
( precedes(X1,X2,esk4_0)
| ~ on_path(X2,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,X2) ),
inference(spm,[status(thm)],[77,114,theory(equality)]) ).
cnf(168,negated_conjecture,
( precedes(X1,X2,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ precedes(X3,X2,esk4_0)
| ~ sequential(X1,X3) ),
inference(spm,[status(thm)],[161,114,theory(equality)]) ).
cnf(180,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,esk8_3(esk4_0,X2,X3))
| ~ path(X2,X3,esk4_0) ),
inference(spm,[status(thm)],[167,93,theory(equality)]) ).
cnf(182,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,esk8_3(esk4_0,X2,X3))
| ~ path(X2,X3,esk4_0) ),
inference(sr,[status(thm)],[180,82,theory(equality)]) ).
cnf(183,plain,
( edge(X1)
| ~ precedes(X1,X5,X2)
| ~ path(X3,X4,X2) ),
inference(csr,[status(thm)],[144,32]) ).
cnf(199,negated_conjecture,
( head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3)
| tail_of(X4) != tail_of(X3)
| ~ shortest_path(X5,X6,esk4_0)
| ~ on_path(X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(X4,esk8_3(esk4_0,X1,X2)) ),
inference(spm,[status(thm)],[72,182,theory(equality)]) ).
cnf(211,negated_conjecture,
( precedes(X1,X2,esk4_0)
| sequential(X5,X2)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,esk3_5(esk4_0,X3,X4,X5,X2))
| ~ precedes(X5,X2,esk4_0)
| ~ path(X3,X4,esk4_0) ),
inference(spm,[status(thm)],[168,64,theory(equality)]) ).
cnf(213,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,X4)
| ~ on_path(X4,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X4,esk8_3(esk4_0,X2,X3)) ),
inference(spm,[status(thm)],[168,182,theory(equality)]) ).
cnf(266,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ on_path(esk7_3(esk4_0,X2,X3),esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk7_3(esk4_0,X2,X3)) ),
inference(spm,[status(thm)],[213,92,theory(equality)]) ).
cnf(267,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| ~ on_path(X1,esk4_0)
| ~ on_path(esk7_3(esk4_0,X2,X3),esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk7_3(esk4_0,X2,X3)) ),
inference(sr,[status(thm)],[266,82,theory(equality)]) ).
cnf(268,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk7_3(esk4_0,X2,X3)) ),
inference(spm,[status(thm)],[267,94,theory(equality)]) ).
cnf(269,negated_conjecture,
( precedes(X1,esk8_3(esk4_0,X2,X3),esk4_0)
| ~ on_path(X1,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk7_3(esk4_0,X2,X3)) ),
inference(sr,[status(thm)],[268,82,theory(equality)]) ).
cnf(286,plain,
( vertex(head_of(X4))
| sequential(X4,X5)
| ~ edge(esk3_5(X1,X2,X3,X4,X5))
| ~ precedes(X4,X5,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[23,145,theory(equality)]) ).
cnf(287,plain,
( X1 = esk3_5(X2,X3,X4,X5,X6)
| sequential(X1,esk3_5(X2,X3,X4,X5,X6))
| sequential(X5,X6)
| head_of(X5) != head_of(X1)
| ~ edge(esk3_5(X2,X3,X4,X5,X6))
| ~ edge(X1)
| ~ precedes(X5,X6,X2)
| ~ path(X3,X4,X2) ),
inference(spm,[status(thm)],[28,145,theory(equality)]) ).
cnf(307,plain,
( tail_of(esk2_2(X1,X2)) = X1
| esk2_2(X1,X2) = X3
| X1 = X2
| sequential(esk2_2(X1,X2),X3)
| tail_of(X3) != X1
| ~ vertex(X2)
| ~ vertex(X1)
| ~ edge(X3) ),
inference(csr,[status(thm)],[137,116]) ).
cnf(308,plain,
( tail_of(esk2_2(tail_of(X1),X2)) = tail_of(X1)
| esk2_2(tail_of(X1),X2) = X1
| tail_of(X1) = X2
| sequential(esk2_2(tail_of(X1),X2),X1)
| ~ vertex(X2)
| ~ vertex(tail_of(X1))
| ~ edge(X1) ),
inference(er,[status(thm)],[307,theory(equality)]) ).
cnf(326,plain,
( tail_of(esk2_2(head_of(X1),head_of(X2))) = head_of(X2)
| tail_of(esk2_2(head_of(X1),head_of(X2))) = head_of(X1)
| head_of(X1) = head_of(X2)
| ~ edge(X2)
| ~ edge(X1) ),
inference(spm,[status(thm)],[141,24,theory(equality)]) ).
fof(330,plain,
( ~ epred9_0
<=> ! [X2,X3,X4,X1] :
( ~ sequential(X4,esk8_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ on_path(X4,esk4_0)
| tail_of(X4) != tail_of(X3)
| head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3) ) ),
introduced(definition),
[split] ).
cnf(331,plain,
( epred9_0
| ~ sequential(X4,esk8_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ on_path(X4,esk4_0)
| tail_of(X4) != tail_of(X3)
| head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3) ),
inference(split_equiv,[status(thm)],[330]) ).
fof(332,plain,
( ~ epred10_0
<=> ! [X6,X5] : ~ shortest_path(X5,X6,esk4_0) ),
introduced(definition),
[split] ).
cnf(333,plain,
( epred10_0
| ~ shortest_path(X5,X6,esk4_0) ),
inference(split_equiv,[status(thm)],[332]) ).
cnf(334,negated_conjecture,
( ~ epred10_0
| ~ epred9_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[199,330,theory(equality)]),332,theory(equality)]),
[split] ).
cnf(335,negated_conjecture,
epred10_0,
inference(spm,[status(thm)],[333,83,theory(equality)]) ).
cnf(337,negated_conjecture,
( $false
| ~ epred9_0 ),
inference(rw,[status(thm)],[334,335,theory(equality)]) ).
cnf(338,negated_conjecture,
~ epred9_0,
inference(cn,[status(thm)],[337,theory(equality)]) ).
cnf(342,negated_conjecture,
( ~ sequential(X4,esk8_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ on_path(X4,esk4_0)
| tail_of(X4) != tail_of(X3)
| head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3) ),
inference(sr,[status(thm)],[331,338,theory(equality)]) ).
cnf(343,negated_conjecture,
( number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3)
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(X3)
| ~ on_path(esk7_3(esk4_0,X1,X2),esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[342,92,theory(equality)]) ).
cnf(344,negated_conjecture,
( head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3)
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(X3)
| ~ on_path(esk7_3(esk4_0,X1,X2),esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(sr,[status(thm)],[343,82,theory(equality)]) ).
cnf(345,negated_conjecture,
( number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3)
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(X3)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[344,94,theory(equality)]) ).
cnf(346,negated_conjecture,
( head_of(esk8_3(esk4_0,X1,X2)) != head_of(X3)
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(X3)
| ~ path(X1,X2,esk4_0) ),
inference(sr,[status(thm)],[345,82,theory(equality)]) ).
cnf(348,negated_conjecture,
( tail_of(esk2_2(X3,X4)) = X4
| X3 = X4
| head_of(esk8_3(esk4_0,X1,X2)) != X4
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(esk2_2(X3,X4))
| ~ path(X1,X2,esk4_0)
| ~ vertex(X4)
| ~ vertex(X3) ),
inference(spm,[status(thm)],[346,129,theory(equality)]) ).
cnf(349,negated_conjecture,
( tail_of(esk2_2(X3,X4)) = X3
| X3 = X4
| head_of(esk8_3(esk4_0,X1,X2)) != X3
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(esk2_2(X3,X4))
| ~ path(X1,X2,esk4_0)
| ~ vertex(X4)
| ~ vertex(X3) ),
inference(spm,[status(thm)],[346,134,theory(equality)]) ).
cnf(351,plain,
( sequential(X4,X5)
| vertex(head_of(X4))
| ~ precedes(X4,X5,X1)
| ~ path(X2,X3,X1) ),
inference(csr,[status(thm)],[286,143]) ).
cnf(358,negated_conjecture,
( on_path(esk3_5(esk4_0,X1,X2,X3,X4),esk4_0)
| sequential(X3,X4)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[148,114,theory(equality)]) ).
cnf(360,plain,
( number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1)
| ~ sequential(X4,esk7_3(X1,X2,X3))
| ~ sequential(esk8_3(X1,X2,X3),X4) ),
inference(csr,[status(thm)],[160,92]) ).
cnf(372,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5))
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0) ),
inference(spm,[status(thm)],[167,358,theory(equality)]) ).
cnf(384,negated_conjecture,
( sequential(X4,X5)
| ~ precedes(esk3_5(esk4_0,X2,X3,X4,X5),X1,esk4_0)
| ~ shortest_path(X6,X7,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5)) ),
inference(spm,[status(thm)],[71,372,theory(equality)]) ).
cnf(387,negated_conjecture,
( sequential(X3,X4)
| head_of(esk3_5(esk4_0,X1,X2,X3,X4)) != head_of(X5)
| tail_of(X6) != tail_of(X5)
| ~ shortest_path(X7,X8,esk4_0)
| ~ on_path(X6,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(X6,esk3_5(esk4_0,X1,X2,X3,X4)) ),
inference(spm,[status(thm)],[72,372,theory(equality)]) ).
cnf(388,negated_conjecture,
( sequential(X4,X5)
| ~ precedes(X6,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(X6,X1)
| ~ sequential(X6,esk3_5(esk4_0,X2,X3,X4,X5))
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5)) ),
inference(spm,[status(thm)],[66,372,theory(equality)]) ).
cnf(389,negated_conjecture,
( sequential(X1,X2)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X5,X6,esk4_0)
| ~ on_path(X2,esk4_0)
| ~ sequential(X2,esk3_5(esk4_0,X3,X4,X1,X2)) ),
inference(spm,[status(thm)],[146,372,theory(equality)]) ).
cnf(391,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,X6)
| ~ on_path(X6,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X6,esk3_5(esk4_0,X2,X3,X4,X5)) ),
inference(spm,[status(thm)],[168,372,theory(equality)]) ).
cnf(400,negated_conjecture,
( sequential(X1,X2)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X5,X6,esk4_0)
| ~ sequential(X2,esk3_5(esk4_0,X3,X4,X1,X2)) ),
inference(csr,[status(thm)],[389,62]) ).
cnf(401,negated_conjecture,
( sequential(X1,X1)
| ~ precedes(X1,X1,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ shortest_path(X4,X5,esk4_0) ),
inference(spm,[status(thm)],[400,65,theory(equality)]) ).
cnf(402,negated_conjecture,
( ~ precedes(X1,X1,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ shortest_path(X4,X5,esk4_0) ),
inference(sr,[status(thm)],[401,113,theory(equality)]) ).
fof(404,plain,
( ~ epred13_0
<=> ! [X1] : ~ precedes(X1,X1,esk4_0) ),
introduced(definition),
[split] ).
cnf(405,plain,
( epred13_0
| ~ precedes(X1,X1,esk4_0) ),
inference(split_equiv,[status(thm)],[404]) ).
fof(406,plain,
( ~ epred14_0
<=> ! [X3,X2] : ~ path(X2,X3,esk4_0) ),
introduced(definition),
[split] ).
cnf(407,plain,
( epred14_0
| ~ path(X2,X3,esk4_0) ),
inference(split_equiv,[status(thm)],[406]) ).
fof(408,plain,
( ~ epred15_0
<=> ! [X5,X4] : ~ shortest_path(X4,X5,esk4_0) ),
introduced(definition),
[split] ).
cnf(409,plain,
( epred15_0
| ~ shortest_path(X4,X5,esk4_0) ),
inference(split_equiv,[status(thm)],[408]) ).
cnf(410,negated_conjecture,
( ~ epred15_0
| ~ epred14_0
| ~ epred13_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[402,404,theory(equality)]),406,theory(equality)]),408,theory(equality)]),
[split] ).
cnf(411,negated_conjecture,
epred15_0,
inference(spm,[status(thm)],[409,83,theory(equality)]) ).
cnf(413,negated_conjecture,
( $false
| ~ epred14_0
| ~ epred13_0 ),
inference(rw,[status(thm)],[410,411,theory(equality)]) ).
cnf(414,negated_conjecture,
( ~ epred14_0
| ~ epred13_0 ),
inference(cn,[status(thm)],[413,theory(equality)]) ).
cnf(417,negated_conjecture,
( epred13_0
| ~ on_path(esk8_3(esk4_0,X1,X2),esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk8_3(esk4_0,X1,X2),esk7_3(esk4_0,X1,X2)) ),
inference(spm,[status(thm)],[405,269,theory(equality)]) ).
cnf(419,negated_conjecture,
epred14_0,
inference(spm,[status(thm)],[407,114,theory(equality)]) ).
cnf(421,negated_conjecture,
( $false
| ~ epred13_0 ),
inference(rw,[status(thm)],[414,419,theory(equality)]) ).
cnf(422,negated_conjecture,
~ epred13_0,
inference(cn,[status(thm)],[421,theory(equality)]) ).
cnf(434,negated_conjecture,
( ~ on_path(esk8_3(esk4_0,X1,X2),esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk8_3(esk4_0,X1,X2),esk7_3(esk4_0,X1,X2)) ),
inference(sr,[status(thm)],[417,422,theory(equality)]) ).
cnf(454,negated_conjecture,
( sequential(X4,X5)
| ~ precedes(esk3_5(esk4_0,X2,X3,X4,X5),X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ shortest_path(X6,X7,esk4_0)
| ~ sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5)) ),
inference(csr,[status(thm)],[384,62]) ).
cnf(458,negated_conjecture,
( sequential(X1,X2)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X7,X8,esk4_0)
| ~ sequential(esk8_3(esk4_0,X5,X6),esk3_5(esk4_0,X3,X4,X1,X2))
| ~ on_path(esk3_5(esk4_0,X3,X4,X1,X2),esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ sequential(esk3_5(esk4_0,X3,X4,X1,X2),esk7_3(esk4_0,X5,X6)) ),
inference(spm,[status(thm)],[454,269,theory(equality)]) ).
cnf(466,negated_conjecture,
( tail_of(esk2_2(X1,head_of(esk8_3(esk4_0,X2,X3)))) = head_of(esk8_3(esk4_0,X2,X3))
| X1 = head_of(esk8_3(esk4_0,X2,X3))
| tail_of(esk7_3(esk4_0,X2,X3)) != tail_of(esk2_2(X1,head_of(esk8_3(esk4_0,X2,X3))))
| ~ path(X2,X3,esk4_0)
| ~ vertex(head_of(esk8_3(esk4_0,X2,X3)))
| ~ vertex(X1) ),
inference(er,[status(thm)],[348,theory(equality)]) ).
cnf(500,negated_conjecture,
( tail_of(esk2_2(head_of(esk8_3(esk4_0,X1,X2)),X3)) = head_of(esk8_3(esk4_0,X1,X2))
| head_of(esk8_3(esk4_0,X1,X2)) = X3
| tail_of(esk7_3(esk4_0,X1,X2)) != tail_of(esk2_2(head_of(esk8_3(esk4_0,X1,X2)),X3))
| ~ path(X1,X2,esk4_0)
| ~ vertex(X3)
| ~ vertex(head_of(esk8_3(esk4_0,X1,X2))) ),
inference(er,[status(thm)],[349,theory(equality)]) ).
cnf(503,plain,
( tail_of(esk2_2(head_of(X1),head_of(esk8_3(X2,X3,X4)))) = head_of(X1)
| tail_of(esk2_2(head_of(X1),head_of(esk8_3(X2,X3,X4)))) = head_of(esk8_3(X2,X3,X4))
| head_of(X1) = head_of(esk8_3(X2,X3,X4))
| number_of_in(triangles,X2) = number_of_in(sequential_pairs,X2)
| ~ edge(X1)
| ~ path(X3,X4,X2) ),
inference(spm,[status(thm)],[326,120,theory(equality)]) ).
cnf(528,plain,
( tail_of(esk2_2(tail_of(X1),X2)) = tail_of(X1)
| esk2_2(tail_of(X1),X2) = X1
| tail_of(X1) = X2
| sequential(esk2_2(tail_of(X1),X2),X1)
| ~ vertex(X2)
| ~ edge(X1) ),
inference(csr,[status(thm)],[308,23]) ).
cnf(529,plain,
( tail_of(esk2_2(tail_of(X1),head_of(X2))) = tail_of(X1)
| esk2_2(tail_of(X1),head_of(X2)) = X1
| tail_of(X1) = head_of(X2)
| sequential(esk2_2(tail_of(X1),head_of(X2)),X1)
| ~ edge(X1)
| ~ edge(X2) ),
inference(spm,[status(thm)],[528,24,theory(equality)]) ).
cnf(598,plain,
( tail_of(esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4))) = tail_of(esk7_3(X1,X2,X3))
| esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4)) = esk7_3(X1,X2,X3)
| tail_of(esk7_3(X1,X2,X3)) = head_of(X4)
| sequential(esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4)),esk7_3(X1,X2,X3))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ edge(X4)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[529,121,theory(equality)]) ).
cnf(604,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ on_path(X4,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[391,65,theory(equality)]) ).
cnf(612,negated_conjecture,
( sequential(X1,X2)
| head_of(esk3_5(esk4_0,X3,X4,X1,X2)) != head_of(X5)
| tail_of(X1) != tail_of(X5)
| ~ on_path(X1,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X6,X7,esk4_0) ),
inference(spm,[status(thm)],[387,65,theory(equality)]) ).
cnf(613,negated_conjecture,
( sequential(X1,X2)
| head_of(esk3_5(esk4_0,X3,X4,X1,X2)) != head_of(X5)
| tail_of(X1) != tail_of(X5)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X6,X7,esk4_0) ),
inference(csr,[status(thm)],[612,63]) ).
cnf(614,negated_conjecture,
( sequential(X1,X2)
| tail_of(X1) != tail_of(esk3_5(esk4_0,X3,X4,X1,X2))
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X5,X6,esk4_0) ),
inference(er,[status(thm)],[613,theory(equality)]) ).
cnf(618,negated_conjecture,
( sequential(X1,X2)
| head_of(X1) != tail_of(X1)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X5,X6,esk4_0) ),
inference(spm,[status(thm)],[614,145,theory(equality)]) ).
cnf(624,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(csr,[status(thm)],[604,63]) ).
cnf(629,negated_conjecture,
( sequential(X4,X5)
| ~ precedes(X6,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(X6,X1)
| ~ sequential(X6,esk3_5(esk4_0,X2,X3,X4,X5))
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[66,624,theory(equality)]) ).
cnf(632,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,X6)
| ~ on_path(X6,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X6,X4) ),
inference(spm,[status(thm)],[168,624,theory(equality)]) ).
cnf(638,negated_conjecture,
( epred13_0
| sequential(X3,X4)
| ~ on_path(esk3_5(esk4_0,X1,X2,X3,X4),esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk3_5(esk4_0,X1,X2,X3,X4),X3) ),
inference(spm,[status(thm)],[405,624,theory(equality)]) ).
cnf(641,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5))
| sequential(X4,X5)
| head_of(X1) != tail_of(X1)
| ~ path(X6,X7,esk4_0)
| ~ shortest_path(X8,X9,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[618,624,theory(equality)]) ).
cnf(645,negated_conjecture,
( sequential(X3,X4)
| ~ on_path(esk3_5(esk4_0,X1,X2,X3,X4),esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk3_5(esk4_0,X1,X2,X3,X4),X3) ),
inference(sr,[status(thm)],[638,422,theory(equality)]) ).
cnf(668,negated_conjecture,
( sequential(X3,X4)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk3_5(esk4_0,X1,X2,X3,X4),X3) ),
inference(csr,[status(thm)],[645,358]) ).
cnf(721,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5))
| sequential(X4,X5)
| head_of(X1) != tail_of(X1)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ shortest_path(X6,X7,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[641,114,theory(equality)]) ).
cnf(722,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X5))
| sequential(X4,X5)
| head_of(X1) != tail_of(X1)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[721,83,theory(equality)]) ).
cnf(743,plain,
( X1 = esk3_5(X2,X3,X4,X5,X6)
| sequential(X1,esk3_5(X2,X3,X4,X5,X6))
| sequential(X5,X6)
| head_of(X5) != head_of(X1)
| ~ precedes(X5,X6,X2)
| ~ path(X3,X4,X2)
| ~ edge(X1) ),
inference(csr,[status(thm)],[287,143]) ).
cnf(751,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| X6 = esk3_5(esk4_0,X2,X3,X4,X5)
| ~ on_path(X1,esk4_0)
| ~ on_path(X6,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X6)
| head_of(X4) != head_of(X6)
| ~ edge(X6) ),
inference(spm,[status(thm)],[391,743,theory(equality)]) ).
cnf(859,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk8_3(esk4_0,X6,X7))
| ~ sequential(esk8_3(esk4_0,X6,X7),X4)
| ~ path(X6,X7,esk4_0) ),
inference(spm,[status(thm)],[632,93,theory(equality)]) ).
cnf(861,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| sequential(X8,X9)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk3_5(esk4_0,X6,X7,X8,X9))
| ~ sequential(esk3_5(esk4_0,X6,X7,X8,X9),X4)
| ~ precedes(X8,X9,esk4_0)
| ~ path(X6,X7,esk4_0) ),
inference(spm,[status(thm)],[632,358,theory(equality)]) ).
cnf(863,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,esk8_3(esk4_0,X6,X7))
| ~ sequential(esk8_3(esk4_0,X6,X7),X4)
| ~ path(X6,X7,esk4_0) ),
inference(sr,[status(thm)],[859,82,theory(equality)]) ).
cnf(1069,negated_conjecture,
( precedes(esk7_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6),esk4_0)
| sequential(X5,X6)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ on_path(esk7_3(esk4_0,X1,X2),esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk8_3(esk4_0,X1,X2),X5) ),
inference(spm,[status(thm)],[863,92,theory(equality)]) ).
cnf(1070,negated_conjecture,
( precedes(esk7_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6),esk4_0)
| sequential(X5,X6)
| ~ on_path(esk7_3(esk4_0,X1,X2),esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk8_3(esk4_0,X1,X2),X5) ),
inference(sr,[status(thm)],[1069,82,theory(equality)]) ).
cnf(1076,negated_conjecture,
( sequential(X1,esk7_3(esk4_0,X2,X3))
| ~ precedes(X1,esk7_3(esk4_0,X2,X3),esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ shortest_path(X6,X7,esk4_0)
| ~ on_path(esk7_3(esk4_0,X2,X3),esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(esk8_3(esk4_0,X2,X3),X1) ),
inference(spm,[status(thm)],[146,1070,theory(equality)]) ).
cnf(1077,negated_conjecture,
( edge(esk7_3(esk4_0,X1,X2))
| sequential(X5,X6)
| ~ path(X7,X8,esk4_0)
| ~ on_path(esk7_3(esk4_0,X1,X2),esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk8_3(esk4_0,X1,X2),X5) ),
inference(spm,[status(thm)],[183,1070,theory(equality)]) ).
cnf(1090,negated_conjecture,
( sequential(X1,esk7_3(esk4_0,X2,X3))
| ~ precedes(X1,esk7_3(esk4_0,X2,X3),esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ shortest_path(X6,X7,esk4_0)
| ~ sequential(esk8_3(esk4_0,X2,X3),X1) ),
inference(csr,[status(thm)],[1076,62]) ).
cnf(1091,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5)),esk7_3(esk4_0,X4,X5))
| sequential(X3,esk7_3(esk4_0,X4,X5))
| ~ path(X6,X7,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ shortest_path(X8,X9,esk4_0)
| ~ sequential(esk8_3(esk4_0,X4,X5),esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5)))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[1090,64,theory(equality)]) ).
cnf(1097,negated_conjecture,
( sequential(X1,X2)
| ~ on_path(X3,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ sequential(X4,esk3_5(esk4_0,X5,X6,X1,X2))
| ~ sequential(X3,esk3_5(esk4_0,X5,X6,X1,X2))
| ~ sequential(X4,X3)
| ~ on_path(X4,esk4_0) ),
inference(spm,[status(thm)],[388,372,theory(equality)]) ).
cnf(1100,negated_conjecture,
( sequential(X1,X2)
| edge(esk7_3(esk4_0,X3,X4))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ sequential(esk8_3(esk4_0,X3,X4),X1) ),
inference(spm,[status(thm)],[1077,94,theory(equality)]) ).
cnf(1101,negated_conjecture,
( sequential(X1,X2)
| edge(esk7_3(esk4_0,X3,X4))
| ~ precedes(X1,X2,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ sequential(esk8_3(esk4_0,X3,X4),X1) ),
inference(sr,[status(thm)],[1100,82,theory(equality)]) ).
cnf(1102,negated_conjecture,
( sequential(esk3_5(X1,X2,X3,esk8_3(esk4_0,X4,X5),X6),X7)
| edge(esk7_3(esk4_0,X4,X5))
| sequential(esk8_3(esk4_0,X4,X5),X6)
| ~ precedes(esk3_5(X1,X2,X3,esk8_3(esk4_0,X4,X5),X6),X7,esk4_0)
| ~ path(X8,X9,esk4_0)
| ~ path(X10,X11,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ precedes(esk8_3(esk4_0,X4,X5),X6,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[1101,65,theory(equality)]) ).
cnf(1179,negated_conjecture,
( sequential(X1,X2)
| ~ on_path(X3,esk4_0)
| ~ on_path(X4,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(X3,esk3_5(esk4_0,X7,X8,X1,X2))
| ~ sequential(X4,X3)
| head_of(X4) != tail_of(X4)
| ~ sequential(X4,X1) ),
inference(spm,[status(thm)],[1097,722,theory(equality)]) ).
cnf(1313,negated_conjecture,
( sequential(X1,X2)
| head_of(X3) != tail_of(X3)
| ~ on_path(X1,esk4_0)
| ~ on_path(X3,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ sequential(X3,X1) ),
inference(spm,[status(thm)],[1179,65,theory(equality)]) ).
cnf(1321,negated_conjecture,
( sequential(X1,X2)
| head_of(X3) != tail_of(X3)
| ~ on_path(X3,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ sequential(X3,X1) ),
inference(csr,[status(thm)],[1313,63]) ).
cnf(1322,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X5) != tail_of(X5)
| ~ on_path(X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ path(X8,X9,esk4_0)
| ~ sequential(X5,esk3_5(esk4_0,X1,X2,X3,X4))
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[1321,64,theory(equality)]) ).
cnf(1398,negated_conjecture,
( sequential(X1,X2)
| ~ on_path(X3,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ sequential(X4,esk3_5(esk4_0,X5,X6,X1,X2))
| ~ sequential(X4,X3)
| ~ sequential(X3,X1)
| ~ on_path(X4,esk4_0) ),
inference(spm,[status(thm)],[629,372,theory(equality)]) ).
cnf(1443,negated_conjecture,
( sequential(X1,X2)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ shortest_path(X7,X8,esk4_0)
| ~ sequential(esk3_5(esk4_0,X3,X4,X1,X2),esk7_3(esk4_0,X5,X6))
| ~ sequential(esk8_3(esk4_0,X5,X6),esk3_5(esk4_0,X3,X4,X1,X2)) ),
inference(csr,[status(thm)],[458,148]) ).
cnf(1524,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X3) != tail_of(X3)
| ~ on_path(X3,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[1322,65,theory(equality)]) ).
cnf(1532,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X3) != tail_of(X3)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[1524,63]) ).
cnf(1533,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X3) != tail_of(X3)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[1532,114,theory(equality)]) ).
cnf(1534,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X3) != tail_of(X3)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[1533,114,theory(equality)]) ).
cnf(1547,negated_conjecture,
( precedes(esk3_5(esk4_0,X1,X2,X3,esk3_5(esk4_0,X4,X5,X6,X7)),X7,esk4_0)
| sequential(X6,X7)
| sequential(X3,esk3_5(esk4_0,X4,X5,X6,X7))
| ~ on_path(esk3_5(esk4_0,X1,X2,X3,esk3_5(esk4_0,X4,X5,X6,X7)),esk4_0)
| ~ precedes(X6,X7,esk4_0)
| ~ path(X4,X5,esk4_0)
| head_of(X3) != tail_of(X3)
| ~ precedes(X3,esk3_5(esk4_0,X4,X5,X6,X7),esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[211,1534,theory(equality)]) ).
cnf(2162,negated_conjecture,
( tail_of(esk2_2(head_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(X1)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| head_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(X1) ),
inference(spm,[status(thm)],[503,114,theory(equality)]) ).
cnf(2164,negated_conjecture,
( tail_of(esk2_2(head_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(X1)
| head_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(X1) ),
inference(sr,[status(thm)],[2162,82,theory(equality)]) ).
cnf(2165,negated_conjecture,
( tail_of(esk2_2(head_of(esk2_2(X1,X2)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(esk2_2(X1,X2)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk2_2(X1,X2))
| head_of(esk2_2(X1,X2)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| X1 = X2
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(spm,[status(thm)],[2164,116,theory(equality)]) ).
cnf(2928,negated_conjecture,
( X6 = esk3_5(esk4_0,X2,X3,X4,X5)
| precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X4,X5)
| head_of(X4) != head_of(X6)
| ~ on_path(X1,esk4_0)
| ~ on_path(X6,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X6) ),
inference(csr,[status(thm)],[751,31]) ).
cnf(2932,negated_conjecture,
( esk3_5(esk4_0,X1,X2,X3,X4) = esk3_5(esk4_0,X5,X6,X7,X8)
| precedes(X9,esk3_5(esk4_0,X5,X6,X7,X8),esk4_0)
| sequential(X7,X8)
| sequential(X3,X4)
| head_of(X7) != head_of(esk3_5(esk4_0,X1,X2,X3,X4))
| ~ on_path(X9,esk4_0)
| ~ precedes(X7,X8,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ sequential(X9,esk3_5(esk4_0,X1,X2,X3,X4))
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[2928,358,theory(equality)]) ).
cnf(5609,plain,
( edge(esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4)))
| tail_of(esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4))) = tail_of(esk7_3(X1,X2,X3))
| esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4)) = esk7_3(X1,X2,X3)
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| tail_of(esk7_3(X1,X2,X3)) = head_of(X4)
| ~ path(X2,X3,X1)
| ~ edge(X4) ),
inference(spm,[status(thm)],[32,598,theory(equality)]) ).
cnf(5619,plain,
( number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| tail_of(esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4))) = tail_of(esk7_3(X1,X2,X3))
| esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4)) = esk7_3(X1,X2,X3)
| tail_of(esk7_3(X1,X2,X3)) = head_of(X4)
| ~ path(X2,X3,X1)
| ~ sequential(esk8_3(X1,X2,X3),esk2_2(tail_of(esk7_3(X1,X2,X3)),head_of(X4)))
| ~ edge(X4) ),
inference(spm,[status(thm)],[360,598,theory(equality)]) ).
cnf(6969,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X1,X6)
| sequential(X4,X5)
| ~ on_path(X1,esk4_0)
| ~ precedes(X4,X5,esk4_0)
| ~ precedes(X1,X6,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(esk3_5(esk4_0,X7,X8,X1,X6),X4) ),
inference(spm,[status(thm)],[861,65,theory(equality)]) ).
cnf(6992,negated_conjecture,
( precedes(X1,esk3_5(esk4_0,X2,X3,X4,X5),esk4_0)
| sequential(X1,X6)
| sequential(X4,X5)
| ~ precedes(X4,X5,esk4_0)
| ~ precedes(X1,X6,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(esk3_5(esk4_0,X7,X8,X1,X6),X4) ),
inference(csr,[status(thm)],[6969,63]) ).
cnf(14878,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ shortest_path(X8,X9,esk4_0)
| ~ sequential(esk8_3(esk4_0,X4,X5),esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5))) ),
inference(csr,[status(thm)],[1091,1443]) ).
cnf(15180,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,esk8_3(esk4_0,X3,X4),X5),X5)
| sequential(esk8_3(esk4_0,X3,X4),X5)
| edge(esk7_3(esk4_0,X3,X4))
| ~ precedes(esk8_3(esk4_0,X3,X4),X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ path(X8,X9,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[1102,64,theory(equality)]) ).
cnf(15192,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,esk8_3(esk4_0,X3,X4),X5),X5)
| sequential(esk8_3(esk4_0,X3,X4),X5)
| edge(esk7_3(esk4_0,X3,X4))
| ~ precedes(esk8_3(esk4_0,X3,X4),X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[15180,114,theory(equality)]) ).
cnf(15193,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,esk8_3(esk4_0,X3,X4),X5),X5)
| sequential(esk8_3(esk4_0,X3,X4),X5)
| edge(esk7_3(esk4_0,X3,X4))
| ~ precedes(esk8_3(esk4_0,X3,X4),X5,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[15192,114,theory(equality)]) ).
cnf(15196,negated_conjecture,
( tail_of(X1) = head_of(esk3_5(esk4_0,X2,X3,esk8_3(esk4_0,X4,X5),X1))
| sequential(esk8_3(esk4_0,X4,X5),X1)
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(esk8_3(esk4_0,X4,X5),X1,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0) ),
inference(spm,[status(thm)],[29,15193,theory(equality)]) ).
cnf(15283,negated_conjecture,
( precedes(esk8_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6),esk4_0)
| sequential(X5,X6)
| sequential(esk8_3(esk4_0,X1,X2),X5)
| edge(esk7_3(esk4_0,X1,X2))
| ~ precedes(X5,X6,esk4_0)
| ~ precedes(esk8_3(esk4_0,X1,X2),X5,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[6992,15193,theory(equality)]) ).
cnf(15345,negated_conjecture,
( vertex(tail_of(X5))
| sequential(esk8_3(esk4_0,X3,X4),X5)
| edge(esk7_3(esk4_0,X3,X4))
| ~ edge(esk3_5(esk4_0,X1,X2,esk8_3(esk4_0,X3,X4),X5))
| ~ precedes(esk8_3(esk4_0,X3,X4),X5,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[24,15196,theory(equality)]) ).
cnf(15494,negated_conjecture,
( sequential(esk8_3(esk4_0,X3,X4),X5)
| vertex(tail_of(X5))
| edge(esk7_3(esk4_0,X3,X4))
| ~ precedes(esk8_3(esk4_0,X3,X4),X5,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[15345,143]) ).
cnf(15562,negated_conjecture,
( precedes(esk8_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6),esk4_0)
| sequential(X5,X6)
| edge(esk7_3(esk4_0,X1,X2))
| ~ precedes(esk8_3(esk4_0,X1,X2),X5,esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[15283,1101]) ).
cnf(15563,negated_conjecture,
( precedes(esk8_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6),esk4_0)
| sequential(X5,X6)
| edge(esk7_3(esk4_0,X1,X2))
| ~ precedes(esk8_3(esk4_0,X1,X2),X5,esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[15562,114,theory(equality)]) ).
cnf(15697,negated_conjecture,
( sequential(esk8_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6))
| vertex(tail_of(esk3_5(esk4_0,X3,X4,X5,X6)))
| edge(esk7_3(esk4_0,X1,X2))
| sequential(X5,X6)
| ~ path(X1,X2,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ precedes(esk8_3(esk4_0,X1,X2),X5,esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X3,X4,esk4_0) ),
inference(spm,[status(thm)],[15494,15563,theory(equality)]) ).
cnf(15893,negated_conjecture,
( sequential(esk8_3(esk4_0,X1,X2),esk3_5(esk4_0,X3,X4,X5,X6))
| sequential(X5,X6)
| vertex(tail_of(esk3_5(esk4_0,X3,X4,X5,X6)))
| edge(esk7_3(esk4_0,X1,X2))
| ~ precedes(esk8_3(esk4_0,X1,X2),X5,esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0) ),
inference(spm,[status(thm)],[15697,114,theory(equality)]) ).
cnf(15953,negated_conjecture,
( sequential(X1,esk7_3(esk4_0,X2,X3))
| vertex(tail_of(esk3_5(esk4_0,X6,X7,X1,esk7_3(esk4_0,X2,X3))))
| edge(esk7_3(esk4_0,X2,X3))
| ~ precedes(X1,esk7_3(esk4_0,X2,X3),esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ shortest_path(X8,X9,esk4_0)
| ~ precedes(esk8_3(esk4_0,X2,X3),X1,esk4_0) ),
inference(spm,[status(thm)],[14878,15893,theory(equality)]) ).
cnf(16160,negated_conjecture,
( vertex(tail_of(esk3_5(esk4_0,X6,X7,X1,esk7_3(esk4_0,X2,X3))))
| edge(esk7_3(esk4_0,X2,X3))
| ~ precedes(X1,esk7_3(esk4_0,X2,X3),esk4_0)
| ~ precedes(esk8_3(esk4_0,X2,X3),X1,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ shortest_path(X8,X9,esk4_0) ),
inference(csr,[status(thm)],[15953,31]) ).
cnf(16161,negated_conjecture,
( vertex(tail_of(esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5))))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ precedes(esk8_3(esk4_0,X4,X5),X3,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ shortest_path(X6,X7,esk4_0) ),
inference(spm,[status(thm)],[16160,114,theory(equality)]) ).
cnf(16162,negated_conjecture,
( vertex(tail_of(esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5))))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ precedes(esk8_3(esk4_0,X4,X5),X3,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[16161,83,theory(equality)]) ).
cnf(16167,negated_conjecture,
( vertex(head_of(X3))
| edge(esk7_3(esk4_0,X4,X5))
| sequential(X3,esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ precedes(esk8_3(esk4_0,X4,X5),X3,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[16162,145,theory(equality)]) ).
cnf(16216,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| vertex(head_of(X3))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ precedes(esk8_3(esk4_0,X4,X5),X3,esk4_0)
| ~ path(X4,X5,esk4_0) ),
inference(csr,[status(thm)],[16167,351]) ).
cnf(16217,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| vertex(head_of(X3))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X4,X5,esk4_0) ),
inference(csr,[status(thm)],[16216,351]) ).
cnf(16218,negated_conjecture,
( vertex(head_of(X3))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X4,X5,esk4_0) ),
inference(csr,[status(thm)],[16217,31]) ).
cnf(16219,negated_conjecture,
( vertex(head_of(esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5))))
| edge(esk7_3(esk4_0,X4,X5))
| sequential(X3,esk7_3(esk4_0,X4,X5))
| ~ path(X4,X5,esk4_0)
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[16218,64,theory(equality)]) ).
cnf(16224,negated_conjecture,
( vertex(head_of(esk3_5(esk4_0,X1,X2,X3,esk7_3(esk4_0,X4,X5))))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[16219,31]) ).
cnf(21114,negated_conjecture,
( tail_of(esk2_2(head_of(esk2_2(X1,tail_of(X2))),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(esk2_2(X1,tail_of(X2))),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk2_2(X1,tail_of(X2)))
| head_of(esk2_2(X1,tail_of(X2))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(X2)
| ~ vertex(X1)
| ~ edge(X2) ),
inference(spm,[status(thm)],[2165,23,theory(equality)]) ).
cnf(22345,negated_conjecture,
( head_of(esk2_2(X1,tail_of(X2))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(esk2_2(X1,tail_of(X2))),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(X2)
| head_of(esk2_2(X1,tail_of(X2))) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ path(esk5_0,esk6_0,esk4_0)
| ~ vertex(head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ vertex(head_of(esk2_2(X1,tail_of(X2))))
| ~ vertex(X1)
| ~ edge(X2) ),
inference(spm,[status(thm)],[466,21114,theory(equality)]) ).
cnf(22472,negated_conjecture,
( head_of(esk2_2(X1,tail_of(X2))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(esk2_2(X1,tail_of(X2))),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(X2)
| head_of(esk2_2(X1,tail_of(X2))) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| $false
| ~ vertex(head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ vertex(head_of(esk2_2(X1,tail_of(X2))))
| ~ vertex(X1)
| ~ edge(X2) ),
inference(rw,[status(thm)],[22345,114,theory(equality)]) ).
cnf(22473,negated_conjecture,
( head_of(esk2_2(X1,tail_of(X2))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(esk2_2(X1,tail_of(X2))),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(X2)
| head_of(esk2_2(X1,tail_of(X2))) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ vertex(head_of(esk2_2(X1,tail_of(X2))))
| ~ vertex(X1)
| ~ edge(X2) ),
inference(cn,[status(thm)],[22472,theory(equality)]) ).
cnf(31635,negated_conjecture,
( precedes(esk3_5(esk4_0,X1,X2,X3,esk3_5(esk4_0,X4,X5,X6,X7)),X7,esk4_0)
| sequential(X3,esk3_5(esk4_0,X4,X5,X6,X7))
| sequential(X6,X7)
| head_of(X3) != tail_of(X3)
| ~ precedes(X3,esk3_5(esk4_0,X4,X5,X6,X7),esk4_0)
| ~ precedes(X6,X7,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[1547,148]) ).
cnf(88212,negated_conjecture,
( tail_of(esk2_2(tail_of(X2),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X2) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(X2)
| tail_of(esk2_2(X1,tail_of(X2))) = tail_of(X2)
| tail_of(X2) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ vertex(tail_of(X2))
| ~ vertex(X1)
| ~ edge(X2) ),
inference(spm,[status(thm)],[22473,129,theory(equality)]) ).
cnf(88510,negated_conjecture,
( tail_of(esk2_2(tail_of(X2),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X2) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X1,tail_of(X2))) = tail_of(X2)
| X1 = tail_of(X2)
| tail_of(X2) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ vertex(X1)
| ~ edge(X2) ),
inference(csr,[status(thm)],[88212,23]) ).
cnf(88511,negated_conjecture,
( tail_of(esk2_2(tail_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X2,tail_of(X1))) = tail_of(X1)
| X2 = tail_of(X1)
| tail_of(X1) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X2)
| ~ edge(X1)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[88510,24,theory(equality)]) ).
cnf(88512,negated_conjecture,
( tail_of(esk2_2(tail_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X2,tail_of(X1))) = tail_of(X1)
| X2 = tail_of(X1)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| tail_of(X1) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X2)
| ~ edge(X1)
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[88511,120,theory(equality)]) ).
cnf(88513,negated_conjecture,
( tail_of(esk2_2(tail_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X2,tail_of(X1))) = tail_of(X1)
| X2 = tail_of(X1)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| tail_of(X1) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X2)
| ~ edge(X1)
| $false ),
inference(rw,[status(thm)],[88512,114,theory(equality)]) ).
cnf(88514,negated_conjecture,
( tail_of(esk2_2(tail_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X2,tail_of(X1))) = tail_of(X1)
| X2 = tail_of(X1)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| tail_of(X1) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X2)
| ~ edge(X1) ),
inference(cn,[status(thm)],[88513,theory(equality)]) ).
cnf(88515,negated_conjecture,
( tail_of(esk2_2(tail_of(X1),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(X1) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X2,tail_of(X1))) = tail_of(X1)
| X2 = tail_of(X1)
| tail_of(X1) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X2)
| ~ edge(X1) ),
inference(sr,[status(thm)],[88514,82,theory(equality)]) ).
cnf(88582,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X1,tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X1)
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(er,[status(thm)],[88515,theory(equality)]) ).
cnf(88653,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X1,tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ vertex(X1)
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[88582,121,theory(equality)]) ).
cnf(88654,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X1,tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ vertex(X1)
| $false ),
inference(rw,[status(thm)],[88653,114,theory(equality)]) ).
cnf(88655,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X1,tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[88654,theory(equality)]) ).
cnf(88656,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(X1,tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| X1 = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ vertex(X1) ),
inference(sr,[status(thm)],[88655,82,theory(equality)]) ).
cnf(88657,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(X1),tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(X1) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ edge(X1) ),
inference(spm,[status(thm)],[88656,24,theory(equality)]) ).
cnf(88670,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(head_of(esk8_3(X1,X2,X3)),tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(X1,X2,X3)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[88657,120,theory(equality)]) ).
cnf(89219,negated_conjecture,
( tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,X1,X2))
| tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ vertex(head_of(esk8_3(esk4_0,X1,X2)))
| ~ vertex(tail_of(esk7_3(esk4_0,esk5_0,esk6_0))) ),
inference(spm,[status(thm)],[500,88670,theory(equality)]) ).
cnf(89398,negated_conjecture,
( head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ vertex(head_of(esk8_3(esk4_0,X1,X2)))
| ~ vertex(tail_of(esk7_3(esk4_0,esk5_0,esk6_0))) ),
inference(sr,[status(thm)],[89219,82,theory(equality)]) ).
cnf(104291,negated_conjecture,
( esk3_5(esk4_0,X1,X2,X3,X4) = esk3_5(esk4_0,X5,X6,X7,X8)
| precedes(X3,esk3_5(esk4_0,X5,X6,X7,X8),esk4_0)
| sequential(X3,X4)
| sequential(X7,X8)
| head_of(X7) != head_of(esk3_5(esk4_0,X1,X2,X3,X4))
| ~ on_path(X3,esk4_0)
| ~ precedes(X7,X8,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[2932,65,theory(equality)]) ).
cnf(107644,negated_conjecture,
( esk3_5(esk4_0,X1,X2,X3,X4) = esk3_5(esk4_0,X5,X6,X7,X8)
| precedes(X3,esk3_5(esk4_0,X5,X6,X7,X8),esk4_0)
| sequential(X3,X4)
| sequential(X7,X8)
| head_of(X7) != head_of(esk3_5(esk4_0,X1,X2,X3,X4))
| ~ precedes(X7,X8,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[104291,63]) ).
cnf(107645,negated_conjecture,
( esk3_5(esk4_0,X1,X2,X3,X4) = esk3_5(esk4_0,X5,X6,esk3_5(esk4_0,X1,X2,X3,X4),X7)
| precedes(X3,esk3_5(esk4_0,X5,X6,esk3_5(esk4_0,X1,X2,X3,X4),X7),esk4_0)
| sequential(esk3_5(esk4_0,X1,X2,X3,X4),X7)
| sequential(X3,X4)
| ~ precedes(esk3_5(esk4_0,X1,X2,X3,X4),X7,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(er,[status(thm)],[107644,theory(equality)]) ).
cnf(107894,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X3)
| esk3_5(esk4_0,X5,X6,esk3_5(esk4_0,X1,X2,X3,X4),X3) = esk3_5(esk4_0,X1,X2,X3,X4)
| sequential(X3,X4)
| ~ precedes(esk3_5(esk4_0,X1,X2,X3,X4),X3,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ shortest_path(X7,X8,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[146,107645,theory(equality)]) ).
cnf(108272,negated_conjecture,
( esk3_5(esk4_0,X5,X6,esk3_5(esk4_0,X1,X2,X3,X4),X3) = esk3_5(esk4_0,X1,X2,X3,X4)
| sequential(X3,X4)
| ~ precedes(esk3_5(esk4_0,X1,X2,X3,X4),X3,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ shortest_path(X7,X8,esk4_0) ),
inference(csr,[status(thm)],[107894,668]) ).
cnf(108273,negated_conjecture,
( esk3_5(esk4_0,X1,X2,esk3_5(esk4_0,X3,X4,X5,X6),X5) = esk3_5(esk4_0,X3,X4,X5,X6)
| sequential(X5,X6)
| ~ precedes(esk3_5(esk4_0,X3,X4,X5,X6),X5,esk4_0)
| ~ precedes(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ path(X3,X4,esk4_0) ),
inference(spm,[status(thm)],[108272,83,theory(equality)]) ).
cnf(108285,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),esk3_5(esk4_0,X1,X2,X3,X4))
| sequential(esk3_5(esk4_0,X1,X2,X3,X4),X3)
| sequential(X3,X4)
| ~ precedes(esk3_5(esk4_0,X1,X2,X3,X4),X3,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[65,108273,theory(equality)]) ).
cnf(108807,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X3)
| sequential(X3,X4)
| ~ precedes(esk3_5(esk4_0,X1,X2,X3,X4),X3,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(sr,[status(thm)],[108285,113,theory(equality)]) ).
cnf(108808,negated_conjecture,
( sequential(X3,X4)
| ~ precedes(esk3_5(esk4_0,X1,X2,X3,X4),X3,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(csr,[status(thm)],[108807,668]) ).
cnf(108819,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X1))
| sequential(X4,X1)
| ~ precedes(X1,esk3_5(esk4_0,X2,X3,X4,X1),esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X5,X6,esk4_0)
| head_of(X1) != tail_of(X1)
| ~ precedes(X4,X1,esk4_0)
| ~ path(X2,X3,esk4_0) ),
inference(spm,[status(thm)],[108808,31635,theory(equality)]) ).
cnf(108957,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X1))
| sequential(X4,X1)
| head_of(X1) != tail_of(X1)
| ~ precedes(X4,X1,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ on_path(X1,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[108819,624,theory(equality)]) ).
cnf(108970,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X1))
| sequential(X4,X1)
| head_of(X1) != tail_of(X1)
| ~ precedes(X4,X1,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(csr,[status(thm)],[108957,62]) ).
cnf(108971,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X1))
| sequential(X4,X1)
| head_of(X1) != tail_of(X1)
| ~ precedes(X4,X1,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[108970,114,theory(equality)]) ).
cnf(108972,negated_conjecture,
( sequential(X1,esk3_5(esk4_0,X2,X3,X4,X1))
| sequential(X4,X1)
| head_of(X1) != tail_of(X1)
| ~ precedes(X4,X1,esk4_0)
| ~ path(X2,X3,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[108971,114,theory(equality)]) ).
cnf(108988,negated_conjecture,
( sequential(X1,X2)
| ~ on_path(X3,esk4_0)
| ~ on_path(X2,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ sequential(X2,X3)
| ~ sequential(X3,X1)
| head_of(X2) != tail_of(X2)
| ~ sequential(X2,X1) ),
inference(spm,[status(thm)],[1398,108972,theory(equality)]) ).
cnf(108992,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X4) != tail_of(X4)
| ~ on_path(X4,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(X4,X3) ),
inference(spm,[status(thm)],[1322,108972,theory(equality)]) ).
cnf(110608,negated_conjecture,
( sequential(X1,X2)
| head_of(X2) != tail_of(X2)
| ~ on_path(X3,esk4_0)
| ~ on_path(X2,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ sequential(X2,X1)
| ~ sequential(X2,X3) ),
inference(csr,[status(thm)],[108988,1321]) ).
cnf(110609,negated_conjecture,
( sequential(X1,X2)
| head_of(X2) != tail_of(X2)
| ~ on_path(X3,esk4_0)
| ~ on_path(X2,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ sequential(X2,X1) ),
inference(csr,[status(thm)],[110608,1321]) ).
cnf(110610,negated_conjecture,
( sequential(X1,X2)
| head_of(X2) != tail_of(X2)
| ~ on_path(X3,esk4_0)
| ~ precedes(X1,X2,esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X6,X7,esk4_0)
| ~ sequential(X2,X1) ),
inference(csr,[status(thm)],[110609,62]) ).
cnf(111070,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X4) != tail_of(X4)
| ~ on_path(X4,esk4_0)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(X4,X3) ),
inference(csr,[status(thm)],[108992,110610]) ).
cnf(111071,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X4) != tail_of(X4)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ path(X7,X8,esk4_0)
| ~ sequential(X4,X3) ),
inference(csr,[status(thm)],[111070,62]) ).
cnf(111072,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X4) != tail_of(X4)
| ~ precedes(X3,X4,esk4_0)
| ~ path(X5,X6,esk4_0)
| ~ sequential(X4,X3) ),
inference(spm,[status(thm)],[111071,114,theory(equality)]) ).
cnf(111073,negated_conjecture,
( sequential(esk3_5(esk4_0,X1,X2,X3,X4),X4)
| sequential(X3,X4)
| head_of(X4) != tail_of(X4)
| ~ precedes(X3,X4,esk4_0)
| ~ sequential(X4,X3) ),
inference(spm,[status(thm)],[111072,114,theory(equality)]) ).
cnf(111076,negated_conjecture,
( tail_of(X1) = head_of(esk3_5(esk4_0,X2,X3,X4,X1))
| sequential(X4,X1)
| head_of(X1) != tail_of(X1)
| ~ precedes(X4,X1,esk4_0)
| ~ sequential(X1,X4) ),
inference(spm,[status(thm)],[29,111073,theory(equality)]) ).
cnf(111596,negated_conjecture,
( vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| edge(esk7_3(esk4_0,X4,X5))
| sequential(X3,esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0)
| head_of(esk7_3(esk4_0,X4,X5)) != tail_of(esk7_3(esk4_0,X4,X5))
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(spm,[status(thm)],[16224,111076,theory(equality)]) ).
cnf(121534,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ path(X1,X2,esk4_0)
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(csr,[status(thm)],[111596,32]) ).
cnf(121535,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ path(X4,X5,esk4_0)
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(csr,[status(thm)],[121534,32]) ).
cnf(121536,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| edge(esk7_3(esk4_0,X4,X5))
| ~ precedes(X3,esk7_3(esk4_0,X4,X5),esk4_0)
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(csr,[status(thm)],[121535,32]) ).
cnf(121537,negated_conjecture,
( sequential(X3,esk7_3(esk4_0,X4,X5))
| vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| edge(esk7_3(esk4_0,X4,X5))
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(csr,[status(thm)],[121536,32]) ).
cnf(121538,negated_conjecture,
( vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| edge(esk7_3(esk4_0,X4,X5))
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(csr,[status(thm)],[121537,32]) ).
cnf(121539,negated_conjecture,
( vertex(tail_of(esk7_3(esk4_0,X4,X5)))
| ~ sequential(esk7_3(esk4_0,X4,X5),X3) ),
inference(csr,[status(thm)],[121538,23]) ).
cnf(121540,negated_conjecture,
( vertex(tail_of(esk7_3(esk4_0,X1,X2)))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[121539,92,theory(equality)]) ).
cnf(121574,negated_conjecture,
( vertex(tail_of(esk7_3(esk4_0,X1,X2)))
| ~ path(X1,X2,esk4_0) ),
inference(sr,[status(thm)],[121540,82,theory(equality)]) ).
cnf(204585,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ vertex(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)))
| ~ edge(esk8_3(esk4_0,X1,X2)) ),
inference(spm,[status(thm)],[89398,24,theory(equality)]) ).
cnf(205255,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ edge(esk8_3(esk4_0,X1,X2))
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[204585,121574,theory(equality)]) ).
cnf(205256,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ edge(esk8_3(esk4_0,X1,X2))
| $false ),
inference(rw,[status(thm)],[205255,114,theory(equality)]) ).
cnf(205257,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0)
| ~ edge(esk8_3(esk4_0,X1,X2)) ),
inference(cn,[status(thm)],[205256,theory(equality)]) ).
cnf(205258,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[205257,120,theory(equality)]) ).
cnf(205259,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,X1,X2)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) != tail_of(esk7_3(esk4_0,X1,X2))
| ~ path(X1,X2,esk4_0) ),
inference(sr,[status(thm)],[205258,82,theory(equality)]) ).
cnf(205260,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[205259,114,theory(equality)]) ).
cnf(205262,negated_conjecture,
( X1 = esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| sequential(X1,esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) != head_of(X1)
| ~ edge(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| ~ edge(X1) ),
inference(spm,[status(thm)],[28,205260,theory(equality)]) ).
cnf(205387,negated_conjecture,
( head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| edge(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| ~ path(esk5_0,esk6_0,esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[5609,205260,theory(equality)]) ).
cnf(205553,negated_conjecture,
( head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| edge(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| $false
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(rw,[status(thm)],[205387,114,theory(equality)]) ).
cnf(205554,negated_conjecture,
( head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| edge(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(cn,[status(thm)],[205553,theory(equality)]) ).
cnf(205555,negated_conjecture,
( head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| edge(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(sr,[status(thm)],[205554,82,theory(equality)]) ).
cnf(209378,negated_conjecture,
( X1 = esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| sequential(X1,esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) != head_of(X1)
| ~ edge(X1)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[205262,205555,theory(equality)]) ).
cnf(210383,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| esk8_3(esk4_0,esk5_0,esk6_0) = esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ path(esk5_0,esk6_0,esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[5619,209378,theory(equality)]) ).
cnf(210394,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| esk8_3(esk4_0,esk5_0,esk6_0) = esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| $false
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(rw,[status(thm)],[210383,114,theory(equality)]) ).
cnf(210395,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| esk8_3(esk4_0,esk5_0,esk6_0) = esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(cn,[status(thm)],[210394,theory(equality)]) ).
cnf(210396,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0)))) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk8_3(esk4_0,esk5_0,esk6_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(sr,[status(thm)],[210395,82,theory(equality)]) ).
cnf(210689,negated_conjecture,
( tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk8_3(esk4_0,esk5_0,esk6_0)
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[205260,210396,theory(equality)]) ).
cnf(210943,negated_conjecture,
( tail_of(esk8_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[205260,210689,theory(equality)]) ).
cnf(212274,negated_conjecture,
( esk2_2(tail_of(esk7_3(esk4_0,esk5_0,esk6_0)),head_of(esk8_3(esk4_0,esk5_0,esk6_0))) = esk7_3(esk4_0,esk5_0,esk6_0)
| head_of(esk8_3(esk4_0,esk5_0,esk6_0)) = tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(csr,[status(thm)],[210943,35]) ).
cnf(212466,negated_conjecture,
( tail_of(esk7_3(esk4_0,esk5_0,esk6_0)) = head_of(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[205260,212274,theory(equality)]) ).
cnf(212481,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = X1
| sequential(esk8_3(esk4_0,esk5_0,esk6_0),X1)
| tail_of(X1) != tail_of(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ edge(X1)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[28,212466,theory(equality)]) ).
cnf(213329,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| sequential(esk8_3(esk4_0,esk5_0,esk6_0),esk7_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(er,[status(thm)],[212481,theory(equality)]) ).
cnf(213443,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ on_path(esk8_3(esk4_0,esk5_0,esk6_0),esk4_0)
| ~ path(esk5_0,esk6_0,esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(spm,[status(thm)],[434,213329,theory(equality)]) ).
cnf(213648,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ on_path(esk8_3(esk4_0,esk5_0,esk6_0),esk4_0)
| $false
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(rw,[status(thm)],[213443,114,theory(equality)]) ).
cnf(213649,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ on_path(esk8_3(esk4_0,esk5_0,esk6_0),esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(cn,[status(thm)],[213648,theory(equality)]) ).
cnf(214024,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[213649,93,theory(equality)]) ).
cnf(214026,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0))
| $false ),
inference(rw,[status(thm)],[214024,114,theory(equality)]) ).
cnf(214027,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(cn,[status(thm)],[214026,theory(equality)]) ).
cnf(214028,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ edge(esk8_3(esk4_0,esk5_0,esk6_0))
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(sr,[status(thm)],[214027,82,theory(equality)]) ).
cnf(214031,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0))
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[214028,120,theory(equality)]) ).
cnf(214032,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0))
| $false ),
inference(rw,[status(thm)],[214031,114,theory(equality)]) ).
cnf(214033,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(cn,[status(thm)],[214032,theory(equality)]) ).
cnf(214034,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| ~ edge(esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(sr,[status(thm)],[214033,82,theory(equality)]) ).
cnf(214452,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[214034,121,theory(equality)]) ).
cnf(214453,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| $false ),
inference(rw,[status(thm)],[214452,114,theory(equality)]) ).
cnf(214454,negated_conjecture,
( esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0)
| number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0) ),
inference(cn,[status(thm)],[214453,theory(equality)]) ).
cnf(214455,negated_conjecture,
esk8_3(esk4_0,esk5_0,esk6_0) = esk7_3(esk4_0,esk5_0,esk6_0),
inference(sr,[status(thm)],[214454,82,theory(equality)]) ).
cnf(214457,negated_conjecture,
( number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| sequential(esk7_3(esk4_0,esk5_0,esk6_0),esk7_3(esk4_0,esk5_0,esk6_0))
| ~ path(esk5_0,esk6_0,esk4_0) ),
inference(spm,[status(thm)],[92,214455,theory(equality)]) ).
cnf(216906,negated_conjecture,
( number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| sequential(esk7_3(esk4_0,esk5_0,esk6_0),esk7_3(esk4_0,esk5_0,esk6_0))
| $false ),
inference(rw,[status(thm)],[214457,114,theory(equality)]) ).
cnf(216907,negated_conjecture,
( number_of_in(triangles,esk4_0) = number_of_in(sequential_pairs,esk4_0)
| sequential(esk7_3(esk4_0,esk5_0,esk6_0),esk7_3(esk4_0,esk5_0,esk6_0)) ),
inference(cn,[status(thm)],[216906,theory(equality)]) ).
cnf(216908,negated_conjecture,
sequential(esk7_3(esk4_0,esk5_0,esk6_0),esk7_3(esk4_0,esk5_0,esk6_0)),
inference(sr,[status(thm)],[216907,82,theory(equality)]) ).
cnf(216909,negated_conjecture,
$false,
inference(sr,[status(thm)],[216908,113,theory(equality)]) ).
cnf(216910,negated_conjecture,
$false,
216909,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/GRA/GRA011+1.p
% --creating new selector for [GRA001+0.ax]
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpt82AUg/sel_GRA011+1.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpt82AUg/sel_GRA011+1.p_2 with time limit 81
% -prover status Theorem
% Problem GRA011+1.p solved in phase 1.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/GRA/GRA011+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/GRA/GRA011+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------