%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GRA006+1 : TPTP v5.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.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:54:39 EST 2010
% Result : Theorem 239.72s
% Output : CNFRefutation 239.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 12
% Syntax : Number of formulae : 153 ( 20 unt; 0 def)
% Number of atoms : 831 ( 309 equ)
% Maximal formula atoms : 37 ( 5 avg)
% Number of connectives : 1075 ( 397 ~; 454 |; 189 &)
% ( 7 <=>; 23 =>; 1 <=; 4 <~>)
% Maximal formula depth : 15 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 4 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-5 aty)
% Number of variables : 358 ( 30 sgn 221 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X2,X3] :
( sequential(X2,X3)
<=> ( edge(X2)
& edge(X3)
& X2 != X3
& head_of(X2) = tail_of(X3) ) ),
file('/tmp/tmpR4QDPL/sel_GRA006+1.p_5',sequential_defn) ).
fof(3,axiom,
! [X1] :
( edge(X1)
=> head_of(X1) != tail_of(X1) ),
file('/tmp/tmpR4QDPL/sel_GRA006+1.p_5',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/tmpR4QDPL/sel_GRA006+1.p_5',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/tmpR4QDPL/sel_GRA006+1.p_5',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/tmpR4QDPL/sel_GRA006+1.p_5',precedes_properties) ).
fof(7,axiom,
! [X4,X5,X7,X9] :
( ( path(X4,X5,X7)
& in_path(X9,X7) )
=> ( vertex(X9)
& ? [X1] :
( on_path(X1,X7)
& ( X9 = head_of(X1)
| X9 = tail_of(X1) ) ) ) ),
file('/tmp/tmpR4QDPL/sel_GRA006+1.p_5',in_path_properties) ).
fof(8,axiom,
! [X4,X5,X7,X1] :
( ( path(X4,X5,X7)
& on_path(X1,X7) )
=> ( edge(X1)
& in_path(head_of(X1),X7)
& in_path(tail_of(X1),X7) ) ),
file('/tmp/tmpR4QDPL/sel_GRA006+1.p_5',on_path_properties) ).
fof(9,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/tmpR4QDPL/sel_GRA006+1.p_5',shortest_path_properties) ).
fof(10,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/tmpR4QDPL/sel_GRA006+1.p_5',precedes_defn) ).
fof(11,conjecture,
( complete
=> ! [X4,X5,X2,X3,X7] :
( ( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7) )
=> ( ? [X8] :
( edge(X8)
& tail_of(X8) = tail_of(X2)
& head_of(X8) = head_of(X3) )
<~> ? [X8] :
( edge(X8)
& tail_of(X8) = head_of(X3)
& head_of(X8) = tail_of(X2) ) ) ) ),
file('/tmp/tmpR4QDPL/sel_GRA006+1.p_5',edge_some_way) ).
fof(17,negated_conjecture,
~ ( complete
=> ! [X4,X5,X2,X3,X7] :
( ( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7) )
=> ( ? [X8] :
( edge(X8)
& tail_of(X8) = tail_of(X2)
& head_of(X8) = head_of(X3) )
<~> ? [X8] :
( edge(X8)
& tail_of(X8) = head_of(X3)
& head_of(X8) = tail_of(X2) ) ) ) ),
inference(assume_negation,[status(cth)],[11]) ).
fof(18,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(19,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(20,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)],[9,theory(equality)]) ).
fof(21,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)],[10,theory(equality)]) ).
fof(22,negated_conjecture,
~ ( complete
=> ! [X4,X5,X2,X3,X7] :
( ( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7) )
=> ~ ( ? [X8] :
( edge(X8)
& tail_of(X8) = tail_of(X2)
& head_of(X8) = head_of(X3) )
<=> ? [X8] :
( edge(X8)
& tail_of(X8) = head_of(X3)
& head_of(X8) = tail_of(X2) ) ) ) ),
inference(fof_simplification,[status(thm)],[17,theory(equality)]) ).
fof(28,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(29,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)],[28]) ).
fof(30,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)],[29]) ).
cnf(31,plain,
( sequential(X1,X2)
| X1 = X2
| head_of(X1) != tail_of(X2)
| ~ edge(X2)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[30]) ).
fof(36,plain,
! [X1] :
( ~ edge(X1)
| head_of(X1) != tail_of(X1) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(37,plain,
! [X2] :
( ~ edge(X2)
| head_of(X2) != tail_of(X2) ),
inference(variable_rename,[status(thm)],[36]) ).
cnf(38,plain,
( head_of(X1) != tail_of(X1)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[37]) ).
fof(39,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(40,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)],[39]) ).
fof(41,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)],[40]) ).
fof(42,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)],[41]) ).
fof(43,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)],[42]) ).
cnf(47,plain,
( path(X1,X2,X3)
| ~ shortest_path(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[43]) ).
fof(49,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)],[18]) ).
fof(50,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)],[49]) ).
fof(51,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)],[50]) ).
fof(52,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)],[51]) ).
fof(53,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)],[52]) ).
cnf(55,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)],[53]) ).
cnf(56,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)],[53]) ).
cnf(57,plain,
( X1 = X2
| X1 = head_of(esk2_2(X1,X2))
| X2 = head_of(esk2_2(X1,X2))
| ~ complete
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(split_conjunct,[status(thm)],[53]) ).
cnf(59,plain,
( X1 = X2
| edge(esk2_2(X1,X2))
| ~ complete
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(split_conjunct,[status(thm)],[53]) ).
fof(60,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)],[19]) ).
fof(61,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)],[60]) ).
fof(62,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)],[61]) ).
fof(63,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)],[62]) ).
fof(64,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)],[63]) ).
cnf(65,plain,
( on_path(X5,X3)
| ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[64]) ).
cnf(66,plain,
( on_path(X4,X3)
| ~ path(X1,X2,X3)
| ~ precedes(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[64]) ).
fof(70,plain,
! [X4,X5,X7,X9] :
( ~ path(X4,X5,X7)
| ~ in_path(X9,X7)
| ( vertex(X9)
& ? [X1] :
( on_path(X1,X7)
& ( X9 = head_of(X1)
| X9 = tail_of(X1) ) ) ) ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(71,plain,
! [X10,X11,X12,X13] :
( ~ path(X10,X11,X12)
| ~ in_path(X13,X12)
| ( vertex(X13)
& ? [X14] :
( on_path(X14,X12)
& ( X13 = head_of(X14)
| X13 = tail_of(X14) ) ) ) ),
inference(variable_rename,[status(thm)],[70]) ).
fof(72,plain,
! [X10,X11,X12,X13] :
( ~ path(X10,X11,X12)
| ~ in_path(X13,X12)
| ( vertex(X13)
& on_path(esk4_4(X10,X11,X12,X13),X12)
& ( X13 = head_of(esk4_4(X10,X11,X12,X13))
| X13 = tail_of(esk4_4(X10,X11,X12,X13)) ) ) ),
inference(skolemize,[status(esa)],[71]) ).
fof(73,plain,
! [X10,X11,X12,X13] :
( ( vertex(X13)
| ~ path(X10,X11,X12)
| ~ in_path(X13,X12) )
& ( on_path(esk4_4(X10,X11,X12,X13),X12)
| ~ path(X10,X11,X12)
| ~ in_path(X13,X12) )
& ( X13 = head_of(esk4_4(X10,X11,X12,X13))
| X13 = tail_of(esk4_4(X10,X11,X12,X13))
| ~ path(X10,X11,X12)
| ~ in_path(X13,X12) ) ),
inference(distribute,[status(thm)],[72]) ).
cnf(76,plain,
( vertex(X1)
| ~ in_path(X1,X2)
| ~ path(X3,X4,X2) ),
inference(split_conjunct,[status(thm)],[73]) ).
fof(77,plain,
! [X4,X5,X7,X1] :
( ~ path(X4,X5,X7)
| ~ on_path(X1,X7)
| ( edge(X1)
& in_path(head_of(X1),X7)
& in_path(tail_of(X1),X7) ) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(78,plain,
! [X8,X9,X10,X11] :
( ~ path(X8,X9,X10)
| ~ on_path(X11,X10)
| ( edge(X11)
& in_path(head_of(X11),X10)
& in_path(tail_of(X11),X10) ) ),
inference(variable_rename,[status(thm)],[77]) ).
fof(79,plain,
! [X8,X9,X10,X11] :
( ( edge(X11)
| ~ path(X8,X9,X10)
| ~ on_path(X11,X10) )
& ( in_path(head_of(X11),X10)
| ~ path(X8,X9,X10)
| ~ on_path(X11,X10) )
& ( in_path(tail_of(X11),X10)
| ~ path(X8,X9,X10)
| ~ on_path(X11,X10) ) ),
inference(distribute,[status(thm)],[78]) ).
cnf(80,plain,
( in_path(tail_of(X1),X2)
| ~ on_path(X1,X2)
| ~ path(X3,X4,X2) ),
inference(split_conjunct,[status(thm)],[79]) ).
cnf(81,plain,
( in_path(head_of(X1),X2)
| ~ on_path(X1,X2)
| ~ path(X3,X4,X2) ),
inference(split_conjunct,[status(thm)],[79]) ).
cnf(82,plain,
( edge(X1)
| ~ on_path(X1,X2)
| ~ path(X3,X4,X2) ),
inference(split_conjunct,[status(thm)],[79]) ).
fof(83,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)],[20]) ).
fof(84,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)],[83]) ).
fof(85,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)],[84]) ).
fof(86,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)],[85]) ).
cnf(87,plain,
( ~ precedes(X1,X2,X3)
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(88,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)],[86]) ).
fof(89,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)],[21]) ).
fof(90,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)],[89]) ).
fof(91,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)],[90]) ).
fof(92,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)],[91]) ).
cnf(93,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)],[92]) ).
fof(95,negated_conjecture,
( complete
& ? [X4,X5,X2,X3,X7] :
( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7)
& ( ! [X8] :
( ~ edge(X8)
| tail_of(X8) != tail_of(X2)
| head_of(X8) != head_of(X3) )
| ? [X8] :
( edge(X8)
& tail_of(X8) = head_of(X3)
& head_of(X8) = tail_of(X2) ) )
& ( ! [X8] :
( ~ edge(X8)
| tail_of(X8) != head_of(X3)
| head_of(X8) != tail_of(X2) )
| ? [X8] :
( edge(X8)
& tail_of(X8) = tail_of(X2)
& head_of(X8) = head_of(X3) ) ) ) ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(96,negated_conjecture,
( complete
& ? [X9,X10,X11,X12,X13] :
( shortest_path(X9,X10,X13)
& precedes(X11,X12,X13)
& ( ! [X14] :
( ~ edge(X14)
| tail_of(X14) != tail_of(X11)
| head_of(X14) != head_of(X12) )
| ? [X15] :
( edge(X15)
& tail_of(X15) = head_of(X12)
& head_of(X15) = tail_of(X11) ) )
& ( ! [X16] :
( ~ edge(X16)
| tail_of(X16) != head_of(X12)
| head_of(X16) != tail_of(X11) )
| ? [X17] :
( edge(X17)
& tail_of(X17) = tail_of(X11)
& head_of(X17) = head_of(X12) ) ) ) ),
inference(variable_rename,[status(thm)],[95]) ).
fof(97,negated_conjecture,
( complete
& shortest_path(esk5_0,esk6_0,esk9_0)
& precedes(esk7_0,esk8_0,esk9_0)
& ( ! [X14] :
( ~ edge(X14)
| tail_of(X14) != tail_of(esk7_0)
| head_of(X14) != head_of(esk8_0) )
| ( edge(esk10_0)
& tail_of(esk10_0) = head_of(esk8_0)
& head_of(esk10_0) = tail_of(esk7_0) ) )
& ( ! [X16] :
( ~ edge(X16)
| tail_of(X16) != head_of(esk8_0)
| head_of(X16) != tail_of(esk7_0) )
| ( edge(esk11_0)
& tail_of(esk11_0) = tail_of(esk7_0)
& head_of(esk11_0) = head_of(esk8_0) ) ) ),
inference(skolemize,[status(esa)],[96]) ).
fof(98,negated_conjecture,
! [X14,X16] :
( ( ~ edge(X16)
| tail_of(X16) != head_of(esk8_0)
| head_of(X16) != tail_of(esk7_0)
| ( edge(esk11_0)
& tail_of(esk11_0) = tail_of(esk7_0)
& head_of(esk11_0) = head_of(esk8_0) ) )
& ( ~ edge(X14)
| tail_of(X14) != tail_of(esk7_0)
| head_of(X14) != head_of(esk8_0)
| ( edge(esk10_0)
& tail_of(esk10_0) = head_of(esk8_0)
& head_of(esk10_0) = tail_of(esk7_0) ) )
& shortest_path(esk5_0,esk6_0,esk9_0)
& precedes(esk7_0,esk8_0,esk9_0)
& complete ),
inference(shift_quantors,[status(thm)],[97]) ).
fof(99,negated_conjecture,
! [X14,X16] :
( ( edge(esk11_0)
| ~ edge(X16)
| tail_of(X16) != head_of(esk8_0)
| head_of(X16) != tail_of(esk7_0) )
& ( tail_of(esk11_0) = tail_of(esk7_0)
| ~ edge(X16)
| tail_of(X16) != head_of(esk8_0)
| head_of(X16) != tail_of(esk7_0) )
& ( head_of(esk11_0) = head_of(esk8_0)
| ~ edge(X16)
| tail_of(X16) != head_of(esk8_0)
| head_of(X16) != tail_of(esk7_0) )
& ( edge(esk10_0)
| ~ edge(X14)
| tail_of(X14) != tail_of(esk7_0)
| head_of(X14) != head_of(esk8_0) )
& ( tail_of(esk10_0) = head_of(esk8_0)
| ~ edge(X14)
| tail_of(X14) != tail_of(esk7_0)
| head_of(X14) != head_of(esk8_0) )
& ( head_of(esk10_0) = tail_of(esk7_0)
| ~ edge(X14)
| tail_of(X14) != tail_of(esk7_0)
| head_of(X14) != head_of(esk8_0) )
& shortest_path(esk5_0,esk6_0,esk9_0)
& precedes(esk7_0,esk8_0,esk9_0)
& complete ),
inference(distribute,[status(thm)],[98]) ).
cnf(100,negated_conjecture,
complete,
inference(split_conjunct,[status(thm)],[99]) ).
cnf(101,negated_conjecture,
precedes(esk7_0,esk8_0,esk9_0),
inference(split_conjunct,[status(thm)],[99]) ).
cnf(102,negated_conjecture,
shortest_path(esk5_0,esk6_0,esk9_0),
inference(split_conjunct,[status(thm)],[99]) ).
cnf(106,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| head_of(X1) != tail_of(esk7_0)
| tail_of(X1) != head_of(esk8_0)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[99]) ).
cnf(107,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| head_of(X1) != tail_of(esk7_0)
| tail_of(X1) != head_of(esk8_0)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[99]) ).
cnf(138,negated_conjecture,
path(esk5_0,esk6_0,esk9_0),
inference(spm,[status(thm)],[47,102,theory(equality)]) ).
cnf(142,negated_conjecture,
( ~ precedes(esk8_0,esk7_0,esk9_0)
| ~ shortest_path(X1,X2,esk9_0) ),
inference(spm,[status(thm)],[87,101,theory(equality)]) ).
cnf(143,negated_conjecture,
( on_path(esk8_0,esk9_0)
| ~ path(X1,X2,esk9_0) ),
inference(spm,[status(thm)],[65,101,theory(equality)]) ).
cnf(144,negated_conjecture,
( on_path(esk7_0,esk9_0)
| ~ path(X1,X2,esk9_0) ),
inference(spm,[status(thm)],[66,101,theory(equality)]) ).
cnf(145,plain,
( X1 = X2
| edge(esk2_2(X1,X2))
| $false
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(rw,[status(thm)],[59,100,theory(equality)]) ).
cnf(146,plain,
( X1 = X2
| edge(esk2_2(X1,X2))
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[145,theory(equality)]) ).
cnf(150,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| X1 = X2
| head_of(esk8_0) != tail_of(esk2_2(X1,X2))
| head_of(esk2_2(X1,X2)) != tail_of(esk7_0)
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(spm,[status(thm)],[106,146,theory(equality)]) ).
cnf(153,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| X1 = X2
| head_of(esk8_0) != tail_of(esk2_2(X1,X2))
| head_of(esk2_2(X1,X2)) != tail_of(esk7_0)
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(spm,[status(thm)],[107,146,theory(equality)]) ).
cnf(154,plain,
( X1 = X2
| head_of(esk2_2(X1,X2)) = X2
| head_of(esk2_2(X1,X2)) = X1
| $false
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(rw,[status(thm)],[57,100,theory(equality)]) ).
cnf(155,plain,
( X1 = X2
| head_of(esk2_2(X1,X2)) = X2
| head_of(esk2_2(X1,X2)) = X1
| ~ vertex(X2)
| ~ vertex(X1) ),
inference(cn,[status(thm)],[154,theory(equality)]) ).
cnf(158,negated_conjecture,
( head_of(esk8_0) != head_of(X1)
| tail_of(esk7_0) != tail_of(X1)
| ~ shortest_path(X2,X3,esk9_0) ),
inference(spm,[status(thm)],[88,101,theory(equality)]) ).
cnf(159,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)],[55,100,theory(equality)]) ).
cnf(160,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)],[159,theory(equality)]) ).
cnf(162,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)],[56,100,theory(equality)]) ).
cnf(163,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)],[162,theory(equality)]) ).
cnf(204,negated_conjecture,
( edge(X1)
| ~ on_path(X1,esk9_0) ),
inference(spm,[status(thm)],[82,138,theory(equality)]) ).
cnf(205,negated_conjecture,
( vertex(X1)
| ~ in_path(X1,esk9_0) ),
inference(spm,[status(thm)],[76,138,theory(equality)]) ).
cnf(207,negated_conjecture,
( in_path(head_of(X1),esk9_0)
| ~ on_path(X1,esk9_0) ),
inference(spm,[status(thm)],[81,138,theory(equality)]) ).
cnf(208,negated_conjecture,
( in_path(tail_of(X1),esk9_0)
| ~ on_path(X1,esk9_0) ),
inference(spm,[status(thm)],[80,138,theory(equality)]) ).
cnf(211,negated_conjecture,
( precedes(X1,X2,esk9_0)
| ~ on_path(X2,esk9_0)
| ~ on_path(X1,esk9_0)
| ~ sequential(X1,X2) ),
inference(spm,[status(thm)],[93,138,theory(equality)]) ).
cnf(217,negated_conjecture,
~ precedes(esk8_0,esk7_0,esk9_0),
inference(spm,[status(thm)],[142,102,theory(equality)]) ).
fof(218,plain,
( ~ epred1_0
<=> ! [X1] :
( tail_of(esk7_0) != tail_of(X1)
| head_of(esk8_0) != head_of(X1) ) ),
introduced(definition),
[split] ).
cnf(219,plain,
( epred1_0
| tail_of(esk7_0) != tail_of(X1)
| head_of(esk8_0) != head_of(X1) ),
inference(split_equiv,[status(thm)],[218]) ).
fof(220,plain,
( ~ epred2_0
<=> ! [X3,X2] : ~ shortest_path(X2,X3,esk9_0) ),
introduced(definition),
[split] ).
cnf(221,plain,
( epred2_0
| ~ shortest_path(X2,X3,esk9_0) ),
inference(split_equiv,[status(thm)],[220]) ).
cnf(222,negated_conjecture,
( ~ epred2_0
| ~ epred1_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[158,218,theory(equality)]),220,theory(equality)]),
[split] ).
cnf(223,negated_conjecture,
epred2_0,
inference(spm,[status(thm)],[221,102,theory(equality)]) ).
cnf(225,negated_conjecture,
( $false
| ~ epred1_0 ),
inference(rw,[status(thm)],[222,223,theory(equality)]) ).
cnf(226,negated_conjecture,
~ epred1_0,
inference(cn,[status(thm)],[225,theory(equality)]) ).
cnf(232,negated_conjecture,
on_path(esk8_0,esk9_0),
inference(spm,[status(thm)],[143,138,theory(equality)]) ).
cnf(241,negated_conjecture,
edge(esk8_0),
inference(spm,[status(thm)],[204,232,theory(equality)]) ).
cnf(251,negated_conjecture,
on_path(esk7_0,esk9_0),
inference(spm,[status(thm)],[144,138,theory(equality)]) ).
cnf(258,negated_conjecture,
edge(esk7_0),
inference(spm,[status(thm)],[204,251,theory(equality)]) ).
cnf(260,negated_conjecture,
head_of(esk7_0) != tail_of(esk7_0),
inference(spm,[status(thm)],[38,258,theory(equality)]) ).
cnf(281,negated_conjecture,
( vertex(head_of(X1))
| ~ on_path(X1,esk9_0) ),
inference(spm,[status(thm)],[205,207,theory(equality)]) ).
cnf(294,negated_conjecture,
vertex(head_of(esk8_0)),
inference(spm,[status(thm)],[281,232,theory(equality)]) ).
cnf(304,negated_conjecture,
( head_of(esk2_2(X1,head_of(esk8_0))) = X1
| head_of(esk2_2(X1,head_of(esk8_0))) = head_of(esk8_0)
| X1 = head_of(esk8_0)
| ~ vertex(X1) ),
inference(spm,[status(thm)],[155,294,theory(equality)]) ).
cnf(310,negated_conjecture,
( vertex(tail_of(X1))
| ~ on_path(X1,esk9_0) ),
inference(spm,[status(thm)],[205,208,theory(equality)]) ).
cnf(319,negated_conjecture,
vertex(tail_of(esk7_0)),
inference(spm,[status(thm)],[310,251,theory(equality)]) ).
cnf(455,negated_conjecture,
( precedes(X1,esk7_0,esk9_0)
| ~ on_path(X1,esk9_0)
| ~ sequential(X1,esk7_0) ),
inference(spm,[status(thm)],[211,251,theory(equality)]) ).
cnf(467,negated_conjecture,
( precedes(esk8_0,esk7_0,esk9_0)
| ~ sequential(esk8_0,esk7_0) ),
inference(spm,[status(thm)],[455,232,theory(equality)]) ).
cnf(472,negated_conjecture,
~ sequential(esk8_0,esk7_0),
inference(sr,[status(thm)],[467,217,theory(equality)]) ).
cnf(473,negated_conjecture,
( esk8_0 = esk7_0
| tail_of(esk7_0) != head_of(esk8_0)
| ~ edge(esk7_0)
| ~ edge(esk8_0) ),
inference(spm,[status(thm)],[472,31,theory(equality)]) ).
cnf(474,negated_conjecture,
( esk8_0 = esk7_0
| tail_of(esk7_0) != head_of(esk8_0)
| $false
| ~ edge(esk8_0) ),
inference(rw,[status(thm)],[473,258,theory(equality)]) ).
cnf(475,negated_conjecture,
( esk8_0 = esk7_0
| tail_of(esk7_0) != head_of(esk8_0)
| $false
| $false ),
inference(rw,[status(thm)],[474,241,theory(equality)]) ).
cnf(476,negated_conjecture,
( esk8_0 = esk7_0
| tail_of(esk7_0) != head_of(esk8_0) ),
inference(cn,[status(thm)],[475,theory(equality)]) ).
cnf(843,negated_conjecture,
( head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = head_of(esk8_0)
| head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| tail_of(esk7_0) = head_of(esk8_0) ),
inference(spm,[status(thm)],[304,319,theory(equality)]) ).
cnf(1241,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0)
| head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| ~ vertex(head_of(esk8_0))
| ~ vertex(tail_of(esk7_0)) ),
inference(spm,[status(thm)],[163,843,theory(equality)]) ).
cnf(1242,negated_conjecture,
( epred1_0
| head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0)
| tail_of(esk7_0) != tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) ),
inference(spm,[status(thm)],[219,843,theory(equality)]) ).
cnf(1264,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0)
| head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| $false
| ~ vertex(tail_of(esk7_0)) ),
inference(rw,[status(thm)],[1241,294,theory(equality)]) ).
cnf(1265,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0)
| head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| $false
| $false ),
inference(rw,[status(thm)],[1264,319,theory(equality)]) ).
cnf(1266,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0)
| head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0) ),
inference(cn,[status(thm)],[1265,theory(equality)]) ).
cnf(1267,negated_conjecture,
( head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != tail_of(esk7_0) ),
inference(sr,[status(thm)],[1242,226,theory(equality)]) ).
cnf(1523,negated_conjecture,
( head_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0) ),
inference(csr,[status(thm)],[1267,1266]) ).
cnf(1525,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| ~ vertex(head_of(esk8_0))
| ~ vertex(tail_of(esk7_0)) ),
inference(spm,[status(thm)],[160,1523,theory(equality)]) ).
cnf(1531,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0)
| ~ vertex(head_of(esk8_0))
| ~ vertex(tail_of(esk7_0)) ),
inference(spm,[status(thm)],[150,1523,theory(equality)]) ).
cnf(1534,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0)
| ~ vertex(head_of(esk8_0))
| ~ vertex(tail_of(esk7_0)) ),
inference(spm,[status(thm)],[153,1523,theory(equality)]) ).
cnf(1542,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| $false
| ~ vertex(tail_of(esk7_0)) ),
inference(rw,[status(thm)],[1525,294,theory(equality)]) ).
cnf(1543,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| $false
| $false ),
inference(rw,[status(thm)],[1542,319,theory(equality)]) ).
cnf(1544,negated_conjecture,
( tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0) ),
inference(cn,[status(thm)],[1543,theory(equality)]) ).
cnf(1554,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0)
| $false
| ~ vertex(tail_of(esk7_0)) ),
inference(rw,[status(thm)],[1531,294,theory(equality)]) ).
cnf(1555,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0)
| $false
| $false ),
inference(rw,[status(thm)],[1554,319,theory(equality)]) ).
cnf(1556,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0) ),
inference(cn,[status(thm)],[1555,theory(equality)]) ).
cnf(1563,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0)
| $false
| ~ vertex(tail_of(esk7_0)) ),
inference(rw,[status(thm)],[1534,294,theory(equality)]) ).
cnf(1564,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0)
| $false
| $false ),
inference(rw,[status(thm)],[1563,319,theory(equality)]) ).
cnf(1565,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| tail_of(esk7_0) = head_of(esk8_0)
| tail_of(esk2_2(tail_of(esk7_0),head_of(esk8_0))) != head_of(esk8_0) ),
inference(cn,[status(thm)],[1564,theory(equality)]) ).
cnf(1642,negated_conjecture,
( head_of(esk11_0) = head_of(esk8_0)
| head_of(esk8_0) = tail_of(esk7_0) ),
inference(csr,[status(thm)],[1556,1544]) ).
cnf(1644,negated_conjecture,
( epred1_0
| head_of(esk8_0) = tail_of(esk7_0)
| tail_of(esk7_0) != tail_of(esk11_0) ),
inference(spm,[status(thm)],[219,1642,theory(equality)]) ).
cnf(1664,negated_conjecture,
( head_of(esk8_0) = tail_of(esk7_0)
| tail_of(esk11_0) != tail_of(esk7_0) ),
inference(sr,[status(thm)],[1644,226,theory(equality)]) ).
cnf(1760,negated_conjecture,
( tail_of(esk11_0) = tail_of(esk7_0)
| head_of(esk8_0) = tail_of(esk7_0) ),
inference(csr,[status(thm)],[1565,1544]) ).
cnf(1761,negated_conjecture,
head_of(esk8_0) = tail_of(esk7_0),
inference(csr,[status(thm)],[1760,1664]) ).
cnf(1840,negated_conjecture,
( esk8_0 = esk7_0
| $false ),
inference(rw,[status(thm)],[476,1761,theory(equality)]) ).
cnf(1841,negated_conjecture,
esk8_0 = esk7_0,
inference(cn,[status(thm)],[1840,theory(equality)]) ).
cnf(1893,negated_conjecture,
head_of(esk7_0) = tail_of(esk7_0),
inference(rw,[status(thm)],[1761,1841,theory(equality)]) ).
cnf(1894,negated_conjecture,
$false,
inference(sr,[status(thm)],[1893,260,theory(equality)]) ).
cnf(1895,negated_conjecture,
$false,
1894,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/GRA/GRA006+1.p
% --creating new selector for [GRA001+0.ax]
% eprover: CPU time limit exceeded, terminating
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpR4QDPL/sel_GRA006+1.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpR4QDPL/sel_GRA006+1.p_2 with time limit 81
% -prover status ResourceOut
% --creating new selector for [GRA001+0.ax]
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpR4QDPL/sel_GRA006+1.p_3 with time limit 74
% -prover status ResourceOut
% --creating new selector for [GRA001+0.ax]
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpR4QDPL/sel_GRA006+1.p_4 with time limit 55
% -prover status ResourceOut
% --creating new selector for [GRA001+0.ax]
% -running prover on /tmp/tmpR4QDPL/sel_GRA006+1.p_5 with time limit 54
% -prover status Theorem
% Problem GRA006+1.p solved in phase 4.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/GRA/GRA006+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/GRA/GRA006+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
%
%------------------------------------------------------------------------------