%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GRA002+2 : TPTP v5.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art01.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:51:48 EST 2010
% Result : Theorem 12.48s
% Output : CNFRefutation 12.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 11
% Syntax : Number of formulae : 116 ( 16 unt; 0 def)
% Number of atoms : 573 ( 136 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 771 ( 314 ~; 331 |; 107 &)
% ( 3 <=>; 15 =>; 1 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 2 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-5 aty)
% Number of variables : 422 ( 32 sgn 164 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X2,X3] :
( sequential(X2,X3)
<=> ( edge(X2)
& edge(X3)
& X2 != X3
& head_of(X2) = tail_of(X3) ) ),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',sequential_defn) ).
fof(3,axiom,
! [X1] :
( edge(X1)
=> head_of(X1) != tail_of(X1) ),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',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/tmpvCJmjN/sel_GRA002+2.p_1',shortest_path_defn) ).
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/tmpvCJmjN/sel_GRA002+2.p_1',precedes_defn) ).
fof(9,axiom,
( complete
=> ! [X4,X5,X2,X3,X7] :
( ( shortest_path(X4,X5,X7)
& precedes(X2,X3,X7) )
=> ? [X8] :
( edge(X8)
& tail_of(X8) = head_of(X3)
& head_of(X8) = tail_of(X2) ) ) ),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',back_edge) ).
fof(10,axiom,
! [X4,X5,X7] :
( path(X4,X5,X7)
=> length_of(X7) = number_of_in(edges,X7) ),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',length_defn) ).
fof(11,axiom,
! [X9,X10] : less_or_equal(number_of_in(X9,X10),number_of_in(X9,graph)),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',graph_has_them_all) ).
fof(12,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/tmpvCJmjN/sel_GRA002+2.p_1',sequential_pairs_and_triangles) ).
fof(13,axiom,
! [X4,X5,X7] :
( path(X4,X5,X7)
=> number_of_in(sequential_pairs,X7) = minus(length_of(X7),n1) ),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',path_length_sequential_pairs) ).
fof(14,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/tmpvCJmjN/sel_GRA002+2.p_1',triangle_defn) ).
fof(15,conjecture,
( complete
=> ! [X7,X4,X5] :
( shortest_path(X4,X5,X7)
=> less_or_equal(minus(length_of(X7),n1),number_of_in(triangles,graph)) ) ),
file('/tmp/tmpvCJmjN/sel_GRA002+2.p_1',maximal_path_length) ).
fof(16,negated_conjecture,
~ ( complete
=> ! [X7,X4,X5] :
( shortest_path(X4,X5,X7)
=> less_or_equal(minus(length_of(X7),n1),number_of_in(triangles,graph)) ) ),
inference(assume_negation,[status(cth)],[15]) ).
fof(20,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(26,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(27,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)],[26]) ).
fof(28,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)],[27]) ).
cnf(29,plain,
( sequential(X1,X2)
| X1 = X2
| head_of(X1) != tail_of(X2)
| ~ edge(X2)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[28]) ).
cnf(32,plain,
( edge(X2)
| ~ sequential(X1,X2) ),
inference(split_conjunct,[status(thm)],[28]) ).
cnf(33,plain,
( edge(X1)
| ~ sequential(X1,X2) ),
inference(split_conjunct,[status(thm)],[28]) ).
fof(34,plain,
! [X1] :
( ~ edge(X1)
| head_of(X1) != tail_of(X1) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(35,plain,
! [X2] :
( ~ edge(X2)
| head_of(X2) != tail_of(X2) ),
inference(variable_rename,[status(thm)],[34]) ).
cnf(36,plain,
( head_of(X1) != tail_of(X1)
| ~ edge(X1) ),
inference(split_conjunct,[status(thm)],[35]) ).
fof(37,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(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
| ? [X12] :
( path(X8,X9,X12)
& ~ less_or_equal(length_of(X10),length_of(X12)) )
| shortest_path(X8,X9,X10) ) ),
inference(variable_rename,[status(thm)],[37]) ).
fof(39,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)],[38]) ).
fof(40,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)],[39]) ).
fof(41,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)],[40]) ).
cnf(45,plain,
( path(X1,X2,X3)
| ~ shortest_path(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[41]) ).
fof(74,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)],[20]) ).
fof(75,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)],[74]) ).
fof(76,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)],[75]) ).
fof(77,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)],[76]) ).
cnf(78,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)],[77]) ).
fof(80,plain,
( ~ complete
| ! [X4,X5,X2,X3,X7] :
( ~ shortest_path(X4,X5,X7)
| ~ precedes(X2,X3,X7)
| ? [X8] :
( edge(X8)
& tail_of(X8) = head_of(X3)
& head_of(X8) = tail_of(X2) ) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(81,plain,
( ~ complete
| ! [X9,X10,X11,X12,X13] :
( ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ? [X14] :
( edge(X14)
& tail_of(X14) = head_of(X12)
& head_of(X14) = tail_of(X11) ) ) ),
inference(variable_rename,[status(thm)],[80]) ).
fof(82,plain,
( ~ complete
| ! [X9,X10,X11,X12,X13] :
( ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ( edge(esk4_5(X9,X10,X11,X12,X13))
& tail_of(esk4_5(X9,X10,X11,X12,X13)) = head_of(X12)
& head_of(esk4_5(X9,X10,X11,X12,X13)) = tail_of(X11) ) ) ),
inference(skolemize,[status(esa)],[81]) ).
fof(83,plain,
! [X9,X10,X11,X12,X13] :
( ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ( edge(esk4_5(X9,X10,X11,X12,X13))
& tail_of(esk4_5(X9,X10,X11,X12,X13)) = head_of(X12)
& head_of(esk4_5(X9,X10,X11,X12,X13)) = tail_of(X11) )
| ~ complete ),
inference(shift_quantors,[status(thm)],[82]) ).
fof(84,plain,
! [X9,X10,X11,X12,X13] :
( ( edge(esk4_5(X9,X10,X11,X12,X13))
| ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ~ complete )
& ( tail_of(esk4_5(X9,X10,X11,X12,X13)) = head_of(X12)
| ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ~ complete )
& ( head_of(esk4_5(X9,X10,X11,X12,X13)) = tail_of(X11)
| ~ shortest_path(X9,X10,X13)
| ~ precedes(X11,X12,X13)
| ~ complete ) ),
inference(distribute,[status(thm)],[83]) ).
cnf(85,plain,
( head_of(esk4_5(X4,X5,X1,X2,X3)) = tail_of(X1)
| ~ complete
| ~ precedes(X1,X2,X3)
| ~ shortest_path(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[84]) ).
cnf(86,plain,
( tail_of(esk4_5(X4,X5,X1,X2,X3)) = head_of(X2)
| ~ complete
| ~ precedes(X1,X2,X3)
| ~ shortest_path(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[84]) ).
cnf(87,plain,
( edge(esk4_5(X4,X5,X1,X2,X3))
| ~ complete
| ~ precedes(X1,X2,X3)
| ~ shortest_path(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[84]) ).
fof(88,plain,
! [X4,X5,X7] :
( ~ path(X4,X5,X7)
| length_of(X7) = number_of_in(edges,X7) ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(89,plain,
! [X8,X9,X10] :
( ~ path(X8,X9,X10)
| length_of(X10) = number_of_in(edges,X10) ),
inference(variable_rename,[status(thm)],[88]) ).
cnf(90,plain,
( length_of(X1) = number_of_in(edges,X1)
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[89]) ).
fof(91,plain,
! [X11,X12] : less_or_equal(number_of_in(X11,X12),number_of_in(X11,graph)),
inference(variable_rename,[status(thm)],[11]) ).
cnf(92,plain,
less_or_equal(number_of_in(X1,X2),number_of_in(X1,graph)),
inference(split_conjunct,[status(thm)],[91]) ).
fof(93,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)],[12]) ).
fof(94,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)],[93]) ).
fof(95,plain,
! [X9,X10,X11] :
( ~ path(X10,X11,X9)
| ( on_path(esk5_3(X9,X10,X11),X9)
& on_path(esk6_3(X9,X10,X11),X9)
& sequential(esk5_3(X9,X10,X11),esk6_3(X9,X10,X11))
& ! [X14] : ~ triangle(esk5_3(X9,X10,X11),esk6_3(X9,X10,X11),X14) )
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ),
inference(skolemize,[status(esa)],[94]) ).
fof(96,plain,
! [X9,X10,X11,X14] :
( ( ~ triangle(esk5_3(X9,X10,X11),esk6_3(X9,X10,X11),X14)
& on_path(esk5_3(X9,X10,X11),X9)
& on_path(esk6_3(X9,X10,X11),X9)
& sequential(esk5_3(X9,X10,X11),esk6_3(X9,X10,X11)) )
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ),
inference(shift_quantors,[status(thm)],[95]) ).
fof(97,plain,
! [X9,X10,X11,X14] :
( ( ~ triangle(esk5_3(X9,X10,X11),esk6_3(X9,X10,X11),X14)
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) )
& ( on_path(esk5_3(X9,X10,X11),X9)
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) )
& ( on_path(esk6_3(X9,X10,X11),X9)
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) )
& ( sequential(esk5_3(X9,X10,X11),esk6_3(X9,X10,X11))
| ~ path(X10,X11,X9)
| number_of_in(sequential_pairs,X9) = number_of_in(triangles,X9) ) ),
inference(distribute,[status(thm)],[96]) ).
cnf(98,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| sequential(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[97]) ).
cnf(99,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| on_path(esk6_3(X1,X2,X3),X1)
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[97]) ).
cnf(100,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| on_path(esk5_3(X1,X2,X3),X1)
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[97]) ).
cnf(101,plain,
( number_of_in(sequential_pairs,X1) = number_of_in(triangles,X1)
| ~ path(X2,X3,X1)
| ~ triangle(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3),X4) ),
inference(split_conjunct,[status(thm)],[97]) ).
fof(102,plain,
! [X4,X5,X7] :
( ~ path(X4,X5,X7)
| number_of_in(sequential_pairs,X7) = minus(length_of(X7),n1) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(103,plain,
! [X8,X9,X10] :
( ~ path(X8,X9,X10)
| number_of_in(sequential_pairs,X10) = minus(length_of(X10),n1) ),
inference(variable_rename,[status(thm)],[102]) ).
cnf(104,plain,
( number_of_in(sequential_pairs,X1) = minus(length_of(X1),n1)
| ~ path(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[103]) ).
fof(105,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)],[14]) ).
fof(106,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)],[105]) ).
fof(107,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)],[106]) ).
cnf(108,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)],[107]) ).
fof(115,negated_conjecture,
( complete
& ? [X7,X4,X5] :
( shortest_path(X4,X5,X7)
& ~ less_or_equal(minus(length_of(X7),n1),number_of_in(triangles,graph)) ) ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(116,negated_conjecture,
( complete
& ? [X8,X9,X10] :
( shortest_path(X9,X10,X8)
& ~ less_or_equal(minus(length_of(X8),n1),number_of_in(triangles,graph)) ) ),
inference(variable_rename,[status(thm)],[115]) ).
fof(117,negated_conjecture,
( complete
& shortest_path(esk8_0,esk9_0,esk7_0)
& ~ less_or_equal(minus(length_of(esk7_0),n1),number_of_in(triangles,graph)) ),
inference(skolemize,[status(esa)],[116]) ).
cnf(118,negated_conjecture,
~ less_or_equal(minus(length_of(esk7_0),n1),number_of_in(triangles,graph)),
inference(split_conjunct,[status(thm)],[117]) ).
cnf(119,negated_conjecture,
shortest_path(esk8_0,esk9_0,esk7_0),
inference(split_conjunct,[status(thm)],[117]) ).
cnf(120,negated_conjecture,
complete,
inference(split_conjunct,[status(thm)],[117]) ).
cnf(123,negated_conjecture,
path(esk8_0,esk9_0,esk7_0),
inference(spm,[status(thm)],[45,119,theory(equality)]) ).
cnf(126,plain,
( edge(esk4_5(X4,X5,X1,X2,X3))
| $false
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X1,X2,X3) ),
inference(rw,[status(thm)],[87,120,theory(equality)]) ).
cnf(127,plain,
( edge(esk4_5(X4,X5,X1,X2,X3))
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X1,X2,X3) ),
inference(cn,[status(thm)],[126,theory(equality)]) ).
cnf(131,plain,
( head_of(esk4_5(X4,X5,X1,X2,X3)) = tail_of(X1)
| $false
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X1,X2,X3) ),
inference(rw,[status(thm)],[85,120,theory(equality)]) ).
cnf(132,plain,
( head_of(esk4_5(X4,X5,X1,X2,X3)) = tail_of(X1)
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X1,X2,X3) ),
inference(cn,[status(thm)],[131,theory(equality)]) ).
cnf(134,plain,
( tail_of(X3) != tail_of(esk4_5(X1,X2,X3,X4,X5))
| ~ edge(esk4_5(X1,X2,X3,X4,X5))
| ~ precedes(X3,X4,X5)
| ~ shortest_path(X1,X2,X5) ),
inference(spm,[status(thm)],[36,132,theory(equality)]) ).
cnf(135,plain,
( esk4_5(X1,X2,X3,X4,X5) = X6
| sequential(esk4_5(X1,X2,X3,X4,X5),X6)
| tail_of(X6) != tail_of(X3)
| ~ edge(X6)
| ~ edge(esk4_5(X1,X2,X3,X4,X5))
| ~ precedes(X3,X4,X5)
| ~ shortest_path(X1,X2,X5) ),
inference(spm,[status(thm)],[29,132,theory(equality)]) ).
cnf(140,plain,
( tail_of(esk4_5(X4,X5,X1,X2,X3)) = head_of(X2)
| $false
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X1,X2,X3) ),
inference(rw,[status(thm)],[86,120,theory(equality)]) ).
cnf(141,plain,
( tail_of(esk4_5(X4,X5,X1,X2,X3)) = head_of(X2)
| ~ shortest_path(X4,X5,X3)
| ~ precedes(X1,X2,X3) ),
inference(cn,[status(thm)],[140,theory(equality)]) ).
cnf(143,plain,
( X1 = esk4_5(X2,X3,X4,X5,X6)
| sequential(X1,esk4_5(X2,X3,X4,X5,X6))
| head_of(X5) != head_of(X1)
| ~ edge(esk4_5(X2,X3,X4,X5,X6))
| ~ edge(X1)
| ~ precedes(X4,X5,X6)
| ~ shortest_path(X2,X3,X6) ),
inference(spm,[status(thm)],[29,141,theory(equality)]) ).
cnf(163,plain,
( edge(esk6_3(X1,X2,X3))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[32,98,theory(equality)]) ).
cnf(164,plain,
( edge(esk5_3(X1,X2,X3))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1) ),
inference(spm,[status(thm)],[33,98,theory(equality)]) ).
cnf(171,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2)
| ~ edge(X3)
| ~ edge(X2) ),
inference(csr,[status(thm)],[108,33]) ).
cnf(172,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2)
| ~ edge(X3) ),
inference(csr,[status(thm)],[171,33]) ).
cnf(173,plain,
( triangle(X1,X2,X3)
| ~ sequential(X3,X1)
| ~ sequential(X2,X3)
| ~ sequential(X1,X2) ),
inference(csr,[status(thm)],[172,33]) ).
cnf(180,plain,
( number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1)
| ~ sequential(X4,esk5_3(X1,X2,X3))
| ~ sequential(esk6_3(X1,X2,X3),X4)
| ~ sequential(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3)) ),
inference(spm,[status(thm)],[101,173,theory(equality)]) ).
cnf(183,negated_conjecture,
length_of(esk7_0) = number_of_in(edges,esk7_0),
inference(spm,[status(thm)],[90,123,theory(equality)]) ).
cnf(185,negated_conjecture,
minus(length_of(esk7_0),n1) = number_of_in(sequential_pairs,esk7_0),
inference(spm,[status(thm)],[104,123,theory(equality)]) ).
cnf(186,negated_conjecture,
( precedes(X1,X2,esk7_0)
| ~ on_path(X2,esk7_0)
| ~ on_path(X1,esk7_0)
| ~ sequential(X1,X2) ),
inference(spm,[status(thm)],[78,123,theory(equality)]) ).
cnf(189,negated_conjecture,
~ less_or_equal(minus(number_of_in(edges,esk7_0),n1),number_of_in(triangles,graph)),
inference(rw,[status(thm)],[118,183,theory(equality)]) ).
cnf(190,negated_conjecture,
minus(number_of_in(edges,esk7_0),n1) = number_of_in(sequential_pairs,esk7_0),
inference(rw,[status(thm)],[185,183,theory(equality)]) ).
cnf(191,negated_conjecture,
~ less_or_equal(number_of_in(sequential_pairs,esk7_0),number_of_in(triangles,graph)),
inference(rw,[status(thm)],[189,190,theory(equality)]) ).
cnf(208,negated_conjecture,
( precedes(X1,esk6_3(esk7_0,X2,X3),esk7_0)
| number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| ~ on_path(X1,esk7_0)
| ~ sequential(X1,esk6_3(esk7_0,X2,X3))
| ~ path(X2,X3,esk7_0) ),
inference(spm,[status(thm)],[186,99,theory(equality)]) ).
cnf(240,plain,
( tail_of(esk4_5(X1,X2,X3,X4,X5)) != tail_of(X3)
| ~ precedes(X3,X4,X5)
| ~ shortest_path(X1,X2,X5) ),
inference(csr,[status(thm)],[134,127]) ).
cnf(241,plain,
( head_of(X4) != tail_of(X3)
| ~ precedes(X3,X4,X5)
| ~ shortest_path(X1,X2,X5) ),
inference(spm,[status(thm)],[240,141,theory(equality)]) ).
cnf(253,plain,
( esk4_5(X1,X2,X3,X4,X5) = X6
| sequential(esk4_5(X1,X2,X3,X4,X5),X6)
| tail_of(X6) != tail_of(X3)
| ~ precedes(X3,X4,X5)
| ~ shortest_path(X1,X2,X5)
| ~ edge(X6) ),
inference(csr,[status(thm)],[135,127]) ).
cnf(279,negated_conjecture,
( number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| head_of(esk6_3(esk7_0,X1,X2)) != tail_of(X3)
| ~ shortest_path(X4,X5,esk7_0)
| ~ on_path(X3,esk7_0)
| ~ path(X1,X2,esk7_0)
| ~ sequential(X3,esk6_3(esk7_0,X1,X2)) ),
inference(spm,[status(thm)],[241,208,theory(equality)]) ).
cnf(356,plain,
( X1 = esk4_5(X2,X3,X4,X5,X6)
| sequential(X1,esk4_5(X2,X3,X4,X5,X6))
| head_of(X5) != head_of(X1)
| ~ precedes(X4,X5,X6)
| ~ shortest_path(X2,X3,X6)
| ~ edge(X1) ),
inference(csr,[status(thm)],[143,127]) ).
cnf(451,negated_conjecture,
( number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| head_of(esk6_3(esk7_0,X1,X2)) != tail_of(esk5_3(esk7_0,X1,X2))
| ~ on_path(esk5_3(esk7_0,X1,X2),esk7_0)
| ~ path(X1,X2,esk7_0)
| ~ shortest_path(X3,X4,esk7_0) ),
inference(spm,[status(thm)],[279,98,theory(equality)]) ).
cnf(453,negated_conjecture,
( number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| head_of(esk6_3(esk7_0,X1,X2)) != tail_of(esk5_3(esk7_0,X1,X2))
| ~ path(X1,X2,esk7_0)
| ~ shortest_path(X3,X4,esk7_0) ),
inference(csr,[status(thm)],[451,100]) ).
cnf(454,negated_conjecture,
( number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| head_of(esk6_3(esk7_0,X1,X2)) != tail_of(esk5_3(esk7_0,X1,X2))
| ~ path(X1,X2,esk7_0) ),
inference(spm,[status(thm)],[453,119,theory(equality)]) ).
cnf(455,plain,
( number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| ~ path(X2,X3,X1)
| ~ sequential(X4,esk5_3(X1,X2,X3))
| ~ sequential(esk6_3(X1,X2,X3),X4) ),
inference(csr,[status(thm)],[180,98]) ).
cnf(456,plain,
( number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| esk4_5(X4,X5,X6,X7,X8) = esk5_3(X1,X2,X3)
| ~ path(X2,X3,X1)
| ~ sequential(esk6_3(X1,X2,X3),esk4_5(X4,X5,X6,X7,X8))
| tail_of(esk5_3(X1,X2,X3)) != tail_of(X6)
| ~ precedes(X6,X7,X8)
| ~ shortest_path(X4,X5,X8)
| ~ edge(esk5_3(X1,X2,X3)) ),
inference(spm,[status(thm)],[455,253,theory(equality)]) ).
cnf(1520,plain,
( esk4_5(X4,X5,X6,X7,X8) = esk5_3(X1,X2,X3)
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| tail_of(esk5_3(X1,X2,X3)) != tail_of(X6)
| ~ precedes(X6,X7,X8)
| ~ path(X2,X3,X1)
| ~ shortest_path(X4,X5,X8)
| ~ sequential(esk6_3(X1,X2,X3),esk4_5(X4,X5,X6,X7,X8)) ),
inference(csr,[status(thm)],[456,164]) ).
cnf(1521,plain,
( esk4_5(X1,X2,X3,X4,X5) = esk5_3(X6,X7,X8)
| number_of_in(triangles,X6) = number_of_in(sequential_pairs,X6)
| esk6_3(X6,X7,X8) = esk4_5(X1,X2,X3,X4,X5)
| tail_of(esk5_3(X6,X7,X8)) != tail_of(X3)
| ~ precedes(X3,X4,X5)
| ~ path(X7,X8,X6)
| ~ shortest_path(X1,X2,X5)
| head_of(X4) != head_of(esk6_3(X6,X7,X8))
| ~ edge(esk6_3(X6,X7,X8)) ),
inference(spm,[status(thm)],[1520,356,theory(equality)]) ).
cnf(62909,plain,
( esk4_5(X1,X2,X3,X4,X5) = esk5_3(X6,X7,X8)
| esk6_3(X6,X7,X8) = esk4_5(X1,X2,X3,X4,X5)
| number_of_in(triangles,X6) = number_of_in(sequential_pairs,X6)
| tail_of(esk5_3(X6,X7,X8)) != tail_of(X3)
| head_of(X4) != head_of(esk6_3(X6,X7,X8))
| ~ precedes(X3,X4,X5)
| ~ path(X7,X8,X6)
| ~ shortest_path(X1,X2,X5) ),
inference(csr,[status(thm)],[1521,163]) ).
cnf(62910,plain,
( esk6_3(X1,X2,X3) = esk4_5(X4,X5,esk5_3(X1,X2,X3),X6,X7)
| esk4_5(X4,X5,esk5_3(X1,X2,X3),X6,X7) = esk5_3(X1,X2,X3)
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| head_of(X6) != head_of(esk6_3(X1,X2,X3))
| ~ precedes(esk5_3(X1,X2,X3),X6,X7)
| ~ path(X2,X3,X1)
| ~ shortest_path(X4,X5,X7) ),
inference(er,[status(thm)],[62909,theory(equality)]) ).
cnf(62975,plain,
( head_of(esk6_3(X3,X4,X5)) = tail_of(esk5_3(X3,X4,X5))
| esk4_5(X1,X2,esk5_3(X3,X4,X5),X6,X7) = esk5_3(X3,X4,X5)
| number_of_in(triangles,X3) = number_of_in(sequential_pairs,X3)
| ~ precedes(esk5_3(X3,X4,X5),X6,X7)
| ~ shortest_path(X1,X2,X7)
| head_of(X6) != head_of(esk6_3(X3,X4,X5))
| ~ path(X4,X5,X3) ),
inference(spm,[status(thm)],[132,62910,theory(equality)]) ).
cnf(63428,plain,
( head_of(esk6_3(X3,X4,X5)) = tail_of(esk5_3(X3,X4,X5))
| number_of_in(triangles,X3) = number_of_in(sequential_pairs,X3)
| ~ precedes(esk5_3(X3,X4,X5),X6,X7)
| ~ shortest_path(X1,X2,X7)
| head_of(X6) != head_of(esk6_3(X3,X4,X5))
| ~ path(X4,X5,X3) ),
inference(spm,[status(thm)],[240,62975,theory(equality)]) ).
cnf(63564,negated_conjecture,
( head_of(esk6_3(X1,X2,X3)) = tail_of(esk5_3(X1,X2,X3))
| number_of_in(triangles,X1) = number_of_in(sequential_pairs,X1)
| number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| head_of(esk6_3(esk7_0,X4,X5)) != head_of(esk6_3(X1,X2,X3))
| ~ path(X2,X3,X1)
| ~ shortest_path(X6,X7,esk7_0)
| ~ on_path(esk5_3(X1,X2,X3),esk7_0)
| ~ path(X4,X5,esk7_0)
| ~ sequential(esk5_3(X1,X2,X3),esk6_3(esk7_0,X4,X5)) ),
inference(spm,[status(thm)],[63428,208,theory(equality)]) ).
cnf(63639,negated_conjecture,
( head_of(esk6_3(esk7_0,X1,X2)) = tail_of(esk5_3(esk7_0,X1,X2))
| number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| ~ on_path(esk5_3(esk7_0,X1,X2),esk7_0)
| ~ path(X1,X2,esk7_0)
| ~ shortest_path(X3,X4,esk7_0) ),
inference(spm,[status(thm)],[63564,98,theory(equality)]) ).
cnf(63644,negated_conjecture,
( head_of(esk6_3(esk7_0,X1,X2)) = tail_of(esk5_3(esk7_0,X1,X2))
| number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| ~ path(X1,X2,esk7_0)
| ~ shortest_path(X3,X4,esk7_0) ),
inference(csr,[status(thm)],[63639,100]) ).
cnf(63645,negated_conjecture,
( number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| ~ path(X1,X2,esk7_0)
| ~ shortest_path(X3,X4,esk7_0) ),
inference(csr,[status(thm)],[63644,454]) ).
cnf(63646,negated_conjecture,
( number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0)
| ~ shortest_path(X1,X2,esk7_0) ),
inference(spm,[status(thm)],[63645,123,theory(equality)]) ).
cnf(63647,negated_conjecture,
number_of_in(triangles,esk7_0) = number_of_in(sequential_pairs,esk7_0),
inference(spm,[status(thm)],[63646,119,theory(equality)]) ).
cnf(63648,negated_conjecture,
less_or_equal(number_of_in(sequential_pairs,esk7_0),number_of_in(triangles,graph)),
inference(spm,[status(thm)],[92,63647,theory(equality)]) ).
cnf(63985,negated_conjecture,
$false,
inference(sr,[status(thm)],[63648,191,theory(equality)]) ).
cnf(63986,negated_conjecture,
$false,
63985,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/GRA/GRA002+2.p
% --creating new selector for [GRA001+0.ax]
% -running prover on /tmp/tmpvCJmjN/sel_GRA002+2.p_1 with time limit 29
% -prover status Theorem
% Problem GRA002+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/GRA/GRA002+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/GRA/GRA002+2.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
%
%------------------------------------------------------------------------------