%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : GRA006+1 : TPTP v5.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art09.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 : Wed Dec 29 05:40:48 EST 2010
% Result : Theorem 1.34s
% Output : Solution 1.34s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP28480/GRA006+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP28480/GRA006+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP28480/GRA006+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 28576
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(edge(X1)=>~(head_of(X1)=tail_of(X1))),file('/tmp/SRASS.s.p', no_loops)).
% fof(2, axiom,![X2]:![X3]:![X4]:![X5]:![X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))=>(~(?[X7]:(tail_of(X7)=tail_of(X4)&head_of(X7)=head_of(X5)))&~(precedes(X5,X4,X6)))),file('/tmp/SRASS.s.p', shortest_path_properties)).
% fof(3, axiom,(complete=>![X2]:![X3]:(((vertex(X2)&vertex(X3))&~(X2=X3))=>?[X1]:(edge(X1)&((X2=head_of(X1)&X3=tail_of(X1))<~>(X3=head_of(X1)&X2=tail_of(X1)))))),file('/tmp/SRASS.s.p', complete_properties)).
% fof(4, axiom,![X4]:![X5]:(sequential(X4,X5)<=>(((edge(X4)&edge(X5))&~(X4=X5))&head_of(X4)=tail_of(X5))),file('/tmp/SRASS.s.p', sequential_defn)).
% fof(6, axiom,![X2]:![X3]:![X6]:![X1]:((path(X2,X3,X6)&on_path(X1,X6))=>((edge(X1)&in_path(head_of(X1),X6))&in_path(tail_of(X1),X6))),file('/tmp/SRASS.s.p', on_path_properties)).
% fof(9, axiom,![X2]:![X3]:![X9]:(shortest_path(X2,X3,X9)<=>((path(X2,X3,X9)&~(X2=X3))&![X6]:(path(X2,X3,X6)=>less_or_equal(length_of(X9),length_of(X6))))),file('/tmp/SRASS.s.p', shortest_path_defn)).
% fof(10, axiom,![X6]:![X2]:![X3]:(path(X2,X3,X6)=>![X4]:![X5]:(precedes(X4,X5,X6)<=((on_path(X4,X6)&on_path(X5,X6))&(sequential(X4,X5)|?[X7]:(sequential(X4,X7)&precedes(X7,X5,X6)))))),file('/tmp/SRASS.s.p', precedes_defn)).
% fof(11, axiom,![X6]:![X2]:![X3]:(path(X2,X3,X6)=>![X4]:![X5]:(precedes(X4,X5,X6)=>((on_path(X4,X6)&on_path(X5,X6))&(sequential(X4,X5)<~>?[X7]:(sequential(X4,X7)&precedes(X7,X5,X6)))))),file('/tmp/SRASS.s.p', precedes_properties)).
% fof(13, axiom,![X2]:![X3]:![X6]:![X10]:((path(X2,X3,X6)&in_path(X10,X6))=>(vertex(X10)&?[X1]:(on_path(X1,X6)&(X10=head_of(X1)|X10=tail_of(X1))))),file('/tmp/SRASS.s.p', in_path_properties)).
% fof(18, conjecture,(complete=>![X2]:![X3]:![X4]:![X5]:![X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))=>(?[X7]:((edge(X7)&tail_of(X7)=tail_of(X4))&head_of(X7)=head_of(X5))<~>?[X7]:((edge(X7)&tail_of(X7)=head_of(X5))&head_of(X7)=tail_of(X4))))),file('/tmp/SRASS.s.p', edge_some_way)).
% fof(19, negated_conjecture,~((complete=>![X2]:![X3]:![X4]:![X5]:![X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))=>(?[X7]:((edge(X7)&tail_of(X7)=tail_of(X4))&head_of(X7)=head_of(X5))<~>?[X7]:((edge(X7)&tail_of(X7)=head_of(X5))&head_of(X7)=tail_of(X4)))))),inference(assume_negation,[status(cth)],[18])).
% fof(20, plain,![X2]:![X3]:![X4]:![X5]:![X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))=>(~(?[X7]:(tail_of(X7)=tail_of(X4)&head_of(X7)=head_of(X5)))&~(precedes(X5,X4,X6)))),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(21, plain,(complete=>![X2]:![X3]:(((vertex(X2)&vertex(X3))&~(X2=X3))=>?[X1]:(edge(X1)&~(((X2=head_of(X1)&X3=tail_of(X1))<=>(X3=head_of(X1)&X2=tail_of(X1))))))),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(24, plain,![X6]:![X2]:![X3]:(path(X2,X3,X6)=>![X4]:![X5]:(((on_path(X4,X6)&on_path(X5,X6))&(sequential(X4,X5)|?[X7]:(sequential(X4,X7)&precedes(X7,X5,X6))))=>precedes(X4,X5,X6))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(25, plain,![X6]:![X2]:![X3]:(path(X2,X3,X6)=>![X4]:![X5]:(precedes(X4,X5,X6)=>((on_path(X4,X6)&on_path(X5,X6))&~((sequential(X4,X5)<=>?[X7]:(sequential(X4,X7)&precedes(X7,X5,X6))))))),inference(fof_simplification,[status(thm)],[11,theory(equality)])).
% fof(26, negated_conjecture,~((complete=>![X2]:![X3]:![X4]:![X5]:![X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))=>~((?[X7]:((edge(X7)&tail_of(X7)=tail_of(X4))&head_of(X7)=head_of(X5))<=>?[X7]:((edge(X7)&tail_of(X7)=head_of(X5))&head_of(X7)=tail_of(X4))))))),inference(fof_simplification,[status(thm)],[19,theory(equality)])).
% fof(27, plain,![X1]:(~(edge(X1))|~(head_of(X1)=tail_of(X1))),inference(fof_nnf,[status(thm)],[1])).
% fof(28, plain,![X2]:(~(edge(X2))|~(head_of(X2)=tail_of(X2))),inference(variable_rename,[status(thm)],[27])).
% cnf(29,plain,(head_of(X1)!=tail_of(X1)|~edge(X1)),inference(split_conjunct,[status(thm)],[28])).
% fof(30, plain,![X2]:![X3]:![X4]:![X5]:![X6]:((~(shortest_path(X2,X3,X6))|~(precedes(X4,X5,X6)))|(![X7]:(~(tail_of(X7)=tail_of(X4))|~(head_of(X7)=head_of(X5)))&~(precedes(X5,X4,X6)))),inference(fof_nnf,[status(thm)],[20])).
% fof(31, plain,![X8]:![X9]:![X10]:![X11]:![X12]:((~(shortest_path(X8,X9,X12))|~(precedes(X10,X11,X12)))|(![X13]:(~(tail_of(X13)=tail_of(X10))|~(head_of(X13)=head_of(X11)))&~(precedes(X11,X10,X12)))),inference(variable_rename,[status(thm)],[30])).
% fof(32, plain,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:(((~(tail_of(X13)=tail_of(X10))|~(head_of(X13)=head_of(X11)))&~(precedes(X11,X10,X12)))|(~(shortest_path(X8,X9,X12))|~(precedes(X10,X11,X12)))),inference(shift_quantors,[status(thm)],[31])).
% fof(33, plain,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:(((~(tail_of(X13)=tail_of(X10))|~(head_of(X13)=head_of(X11)))|(~(shortest_path(X8,X9,X12))|~(precedes(X10,X11,X12))))&(~(precedes(X11,X10,X12))|(~(shortest_path(X8,X9,X12))|~(precedes(X10,X11,X12))))),inference(distribute,[status(thm)],[32])).
% cnf(34,plain,(~precedes(X1,X2,X3)|~shortest_path(X4,X5,X3)|~precedes(X2,X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(35,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)],[33])).
% fof(36, plain,(~(complete)|![X2]:![X3]:(((~(vertex(X2))|~(vertex(X3)))|X2=X3)|?[X1]:(edge(X1)&(((~(X2=head_of(X1))|~(X3=tail_of(X1)))|(~(X3=head_of(X1))|~(X2=tail_of(X1))))&((X2=head_of(X1)&X3=tail_of(X1))|(X3=head_of(X1)&X2=tail_of(X1))))))),inference(fof_nnf,[status(thm)],[21])).
% fof(37, plain,(~(complete)|![X4]:![X5]:(((~(vertex(X4))|~(vertex(X5)))|X4=X5)|?[X6]:(edge(X6)&(((~(X4=head_of(X6))|~(X5=tail_of(X6)))|(~(X5=head_of(X6))|~(X4=tail_of(X6))))&((X4=head_of(X6)&X5=tail_of(X6))|(X5=head_of(X6)&X4=tail_of(X6))))))),inference(variable_rename,[status(thm)],[36])).
% fof(38, plain,(~(complete)|![X4]:![X5]:(((~(vertex(X4))|~(vertex(X5)))|X4=X5)|(edge(esk1_2(X4,X5))&(((~(X4=head_of(esk1_2(X4,X5)))|~(X5=tail_of(esk1_2(X4,X5))))|(~(X5=head_of(esk1_2(X4,X5)))|~(X4=tail_of(esk1_2(X4,X5)))))&((X4=head_of(esk1_2(X4,X5))&X5=tail_of(esk1_2(X4,X5)))|(X5=head_of(esk1_2(X4,X5))&X4=tail_of(esk1_2(X4,X5)))))))),inference(skolemize,[status(esa)],[37])).
% fof(39, plain,![X4]:![X5]:((((~(vertex(X4))|~(vertex(X5)))|X4=X5)|(edge(esk1_2(X4,X5))&(((~(X4=head_of(esk1_2(X4,X5)))|~(X5=tail_of(esk1_2(X4,X5))))|(~(X5=head_of(esk1_2(X4,X5)))|~(X4=tail_of(esk1_2(X4,X5)))))&((X4=head_of(esk1_2(X4,X5))&X5=tail_of(esk1_2(X4,X5)))|(X5=head_of(esk1_2(X4,X5))&X4=tail_of(esk1_2(X4,X5)))))))|~(complete)),inference(shift_quantors,[status(thm)],[38])).
% fof(40, plain,![X4]:![X5]:(((edge(esk1_2(X4,X5))|((~(vertex(X4))|~(vertex(X5)))|X4=X5))|~(complete))&(((((~(X4=head_of(esk1_2(X4,X5)))|~(X5=tail_of(esk1_2(X4,X5))))|(~(X5=head_of(esk1_2(X4,X5)))|~(X4=tail_of(esk1_2(X4,X5)))))|((~(vertex(X4))|~(vertex(X5)))|X4=X5))|~(complete))&(((((X5=head_of(esk1_2(X4,X5))|X4=head_of(esk1_2(X4,X5)))|((~(vertex(X4))|~(vertex(X5)))|X4=X5))|~(complete))&(((X4=tail_of(esk1_2(X4,X5))|X4=head_of(esk1_2(X4,X5)))|((~(vertex(X4))|~(vertex(X5)))|X4=X5))|~(complete)))&((((X5=head_of(esk1_2(X4,X5))|X5=tail_of(esk1_2(X4,X5)))|((~(vertex(X4))|~(vertex(X5)))|X4=X5))|~(complete))&(((X4=tail_of(esk1_2(X4,X5))|X5=tail_of(esk1_2(X4,X5)))|((~(vertex(X4))|~(vertex(X5)))|X4=X5))|~(complete)))))),inference(distribute,[status(thm)],[39])).
% cnf(42,plain,(X1=X2|X2=tail_of(esk1_2(X1,X2))|X2=head_of(esk1_2(X1,X2))|~complete|~vertex(X2)|~vertex(X1)),inference(split_conjunct,[status(thm)],[40])).
% cnf(43,plain,(X1=X2|X1=head_of(esk1_2(X1,X2))|X1=tail_of(esk1_2(X1,X2))|~complete|~vertex(X2)|~vertex(X1)),inference(split_conjunct,[status(thm)],[40])).
% cnf(44,plain,(X1=X2|X1=head_of(esk1_2(X1,X2))|X2=head_of(esk1_2(X1,X2))|~complete|~vertex(X2)|~vertex(X1)),inference(split_conjunct,[status(thm)],[40])).
% cnf(46,plain,(X1=X2|edge(esk1_2(X1,X2))|~complete|~vertex(X2)|~vertex(X1)),inference(split_conjunct,[status(thm)],[40])).
% fof(47, 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(fof_nnf,[status(thm)],[4])).
% fof(48, plain,![X6]:![X7]:((~(sequential(X6,X7))|(((edge(X6)&edge(X7))&~(X6=X7))&head_of(X6)=tail_of(X7)))&((((~(edge(X6))|~(edge(X7)))|X6=X7)|~(head_of(X6)=tail_of(X7)))|sequential(X6,X7))),inference(variable_rename,[status(thm)],[47])).
% fof(49, plain,![X6]:![X7]:(((((edge(X6)|~(sequential(X6,X7)))&(edge(X7)|~(sequential(X6,X7))))&(~(X6=X7)|~(sequential(X6,X7))))&(head_of(X6)=tail_of(X7)|~(sequential(X6,X7))))&((((~(edge(X6))|~(edge(X7)))|X6=X7)|~(head_of(X6)=tail_of(X7)))|sequential(X6,X7))),inference(distribute,[status(thm)],[48])).
% cnf(50,plain,(sequential(X1,X2)|X1=X2|head_of(X1)!=tail_of(X2)|~edge(X2)|~edge(X1)),inference(split_conjunct,[status(thm)],[49])).
% fof(60, plain,![X2]:![X3]:![X6]:![X1]:((~(path(X2,X3,X6))|~(on_path(X1,X6)))|((edge(X1)&in_path(head_of(X1),X6))&in_path(tail_of(X1),X6))),inference(fof_nnf,[status(thm)],[6])).
% fof(61, plain,![X7]:![X8]:![X9]:![X10]:((~(path(X7,X8,X9))|~(on_path(X10,X9)))|((edge(X10)&in_path(head_of(X10),X9))&in_path(tail_of(X10),X9))),inference(variable_rename,[status(thm)],[60])).
% fof(62, plain,![X7]:![X8]:![X9]:![X10]:(((edge(X10)|(~(path(X7,X8,X9))|~(on_path(X10,X9))))&(in_path(head_of(X10),X9)|(~(path(X7,X8,X9))|~(on_path(X10,X9)))))&(in_path(tail_of(X10),X9)|(~(path(X7,X8,X9))|~(on_path(X10,X9))))),inference(distribute,[status(thm)],[61])).
% cnf(63,plain,(in_path(tail_of(X1),X2)|~on_path(X1,X2)|~path(X3,X4,X2)),inference(split_conjunct,[status(thm)],[62])).
% cnf(64,plain,(in_path(head_of(X1),X2)|~on_path(X1,X2)|~path(X3,X4,X2)),inference(split_conjunct,[status(thm)],[62])).
% cnf(65,plain,(edge(X1)|~on_path(X1,X2)|~path(X3,X4,X2)),inference(split_conjunct,[status(thm)],[62])).
% fof(86, plain,![X2]:![X3]:![X9]:((~(shortest_path(X2,X3,X9))|((path(X2,X3,X9)&~(X2=X3))&![X6]:(~(path(X2,X3,X6))|less_or_equal(length_of(X9),length_of(X6)))))&(((~(path(X2,X3,X9))|X2=X3)|?[X6]:(path(X2,X3,X6)&~(less_or_equal(length_of(X9),length_of(X6)))))|shortest_path(X2,X3,X9))),inference(fof_nnf,[status(thm)],[9])).
% fof(87, plain,![X10]:![X11]:![X12]:((~(shortest_path(X10,X11,X12))|((path(X10,X11,X12)&~(X10=X11))&![X13]:(~(path(X10,X11,X13))|less_or_equal(length_of(X12),length_of(X13)))))&(((~(path(X10,X11,X12))|X10=X11)|?[X14]:(path(X10,X11,X14)&~(less_or_equal(length_of(X12),length_of(X14)))))|shortest_path(X10,X11,X12))),inference(variable_rename,[status(thm)],[86])).
% fof(88, plain,![X10]:![X11]:![X12]:((~(shortest_path(X10,X11,X12))|((path(X10,X11,X12)&~(X10=X11))&![X13]:(~(path(X10,X11,X13))|less_or_equal(length_of(X12),length_of(X13)))))&(((~(path(X10,X11,X12))|X10=X11)|(path(X10,X11,esk4_3(X10,X11,X12))&~(less_or_equal(length_of(X12),length_of(esk4_3(X10,X11,X12))))))|shortest_path(X10,X11,X12))),inference(skolemize,[status(esa)],[87])).
% fof(89, plain,![X10]:![X11]:![X12]:![X13]:((((~(path(X10,X11,X13))|less_or_equal(length_of(X12),length_of(X13)))&(path(X10,X11,X12)&~(X10=X11)))|~(shortest_path(X10,X11,X12)))&(((~(path(X10,X11,X12))|X10=X11)|(path(X10,X11,esk4_3(X10,X11,X12))&~(less_or_equal(length_of(X12),length_of(esk4_3(X10,X11,X12))))))|shortest_path(X10,X11,X12))),inference(shift_quantors,[status(thm)],[88])).
% fof(90, plain,![X10]:![X11]:![X12]:![X13]:((((~(path(X10,X11,X13))|less_or_equal(length_of(X12),length_of(X13)))|~(shortest_path(X10,X11,X12)))&((path(X10,X11,X12)|~(shortest_path(X10,X11,X12)))&(~(X10=X11)|~(shortest_path(X10,X11,X12)))))&(((path(X10,X11,esk4_3(X10,X11,X12))|(~(path(X10,X11,X12))|X10=X11))|shortest_path(X10,X11,X12))&((~(less_or_equal(length_of(X12),length_of(esk4_3(X10,X11,X12))))|(~(path(X10,X11,X12))|X10=X11))|shortest_path(X10,X11,X12)))),inference(distribute,[status(thm)],[89])).
% cnf(94,plain,(path(X1,X2,X3)|~shortest_path(X1,X2,X3)),inference(split_conjunct,[status(thm)],[90])).
% fof(96, plain,![X6]:![X2]:![X3]:(~(path(X2,X3,X6))|![X4]:![X5]:(((~(on_path(X4,X6))|~(on_path(X5,X6)))|(~(sequential(X4,X5))&![X7]:(~(sequential(X4,X7))|~(precedes(X7,X5,X6)))))|precedes(X4,X5,X6))),inference(fof_nnf,[status(thm)],[24])).
% fof(97, plain,![X8]:![X9]:![X10]:(~(path(X9,X10,X8))|![X11]:![X12]:(((~(on_path(X11,X8))|~(on_path(X12,X8)))|(~(sequential(X11,X12))&![X13]:(~(sequential(X11,X13))|~(precedes(X13,X12,X8)))))|precedes(X11,X12,X8))),inference(variable_rename,[status(thm)],[96])).
% fof(98, plain,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:(((((~(sequential(X11,X13))|~(precedes(X13,X12,X8)))&~(sequential(X11,X12)))|(~(on_path(X11,X8))|~(on_path(X12,X8))))|precedes(X11,X12,X8))|~(path(X9,X10,X8))),inference(shift_quantors,[status(thm)],[97])).
% fof(99, plain,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:(((((~(sequential(X11,X13))|~(precedes(X13,X12,X8)))|(~(on_path(X11,X8))|~(on_path(X12,X8))))|precedes(X11,X12,X8))|~(path(X9,X10,X8)))&(((~(sequential(X11,X12))|(~(on_path(X11,X8))|~(on_path(X12,X8))))|precedes(X11,X12,X8))|~(path(X9,X10,X8)))),inference(distribute,[status(thm)],[98])).
% cnf(100,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)],[99])).
% fof(102, plain,![X6]:![X2]:![X3]:(~(path(X2,X3,X6))|![X4]:![X5]:(~(precedes(X4,X5,X6))|((on_path(X4,X6)&on_path(X5,X6))&((~(sequential(X4,X5))|![X7]:(~(sequential(X4,X7))|~(precedes(X7,X5,X6))))&(sequential(X4,X5)|?[X7]:(sequential(X4,X7)&precedes(X7,X5,X6))))))),inference(fof_nnf,[status(thm)],[25])).
% fof(103, plain,![X8]:![X9]:![X10]:(~(path(X9,X10,X8))|![X11]:![X12]:(~(precedes(X11,X12,X8))|((on_path(X11,X8)&on_path(X12,X8))&((~(sequential(X11,X12))|![X13]:(~(sequential(X11,X13))|~(precedes(X13,X12,X8))))&(sequential(X11,X12)|?[X14]:(sequential(X11,X14)&precedes(X14,X12,X8))))))),inference(variable_rename,[status(thm)],[102])).
% fof(104, plain,![X8]:![X9]:![X10]:(~(path(X9,X10,X8))|![X11]:![X12]:(~(precedes(X11,X12,X8))|((on_path(X11,X8)&on_path(X12,X8))&((~(sequential(X11,X12))|![X13]:(~(sequential(X11,X13))|~(precedes(X13,X12,X8))))&(sequential(X11,X12)|(sequential(X11,esk5_5(X8,X9,X10,X11,X12))&precedes(esk5_5(X8,X9,X10,X11,X12),X12,X8))))))),inference(skolemize,[status(esa)],[103])).
% fof(105, plain,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:((((((~(sequential(X11,X13))|~(precedes(X13,X12,X8)))|~(sequential(X11,X12)))&(sequential(X11,X12)|(sequential(X11,esk5_5(X8,X9,X10,X11,X12))&precedes(esk5_5(X8,X9,X10,X11,X12),X12,X8))))&(on_path(X11,X8)&on_path(X12,X8)))|~(precedes(X11,X12,X8)))|~(path(X9,X10,X8))),inference(shift_quantors,[status(thm)],[104])).
% fof(106, plain,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:((((((~(sequential(X11,X13))|~(precedes(X13,X12,X8)))|~(sequential(X11,X12)))|~(precedes(X11,X12,X8)))|~(path(X9,X10,X8)))&((((sequential(X11,esk5_5(X8,X9,X10,X11,X12))|sequential(X11,X12))|~(precedes(X11,X12,X8)))|~(path(X9,X10,X8)))&(((precedes(esk5_5(X8,X9,X10,X11,X12),X12,X8)|sequential(X11,X12))|~(precedes(X11,X12,X8)))|~(path(X9,X10,X8)))))&(((on_path(X11,X8)|~(precedes(X11,X12,X8)))|~(path(X9,X10,X8)))&((on_path(X12,X8)|~(precedes(X11,X12,X8)))|~(path(X9,X10,X8))))),inference(distribute,[status(thm)],[105])).
% cnf(107,plain,(on_path(X5,X3)|~path(X1,X2,X3)|~precedes(X4,X5,X3)),inference(split_conjunct,[status(thm)],[106])).
% cnf(108,plain,(on_path(X4,X3)|~path(X1,X2,X3)|~precedes(X4,X5,X3)),inference(split_conjunct,[status(thm)],[106])).
% fof(122, plain,![X2]:![X3]:![X6]:![X10]:((~(path(X2,X3,X6))|~(in_path(X10,X6)))|(vertex(X10)&?[X1]:(on_path(X1,X6)&(X10=head_of(X1)|X10=tail_of(X1))))),inference(fof_nnf,[status(thm)],[13])).
% fof(123, plain,![X11]:![X12]:![X13]:![X14]:((~(path(X11,X12,X13))|~(in_path(X14,X13)))|(vertex(X14)&?[X15]:(on_path(X15,X13)&(X14=head_of(X15)|X14=tail_of(X15))))),inference(variable_rename,[status(thm)],[122])).
% fof(124, plain,![X11]:![X12]:![X13]:![X14]:((~(path(X11,X12,X13))|~(in_path(X14,X13)))|(vertex(X14)&(on_path(esk6_4(X11,X12,X13,X14),X13)&(X14=head_of(esk6_4(X11,X12,X13,X14))|X14=tail_of(esk6_4(X11,X12,X13,X14)))))),inference(skolemize,[status(esa)],[123])).
% fof(125, plain,![X11]:![X12]:![X13]:![X14]:((vertex(X14)|(~(path(X11,X12,X13))|~(in_path(X14,X13))))&((on_path(esk6_4(X11,X12,X13,X14),X13)|(~(path(X11,X12,X13))|~(in_path(X14,X13))))&((X14=head_of(esk6_4(X11,X12,X13,X14))|X14=tail_of(esk6_4(X11,X12,X13,X14)))|(~(path(X11,X12,X13))|~(in_path(X14,X13)))))),inference(distribute,[status(thm)],[124])).
% cnf(128,plain,(vertex(X1)|~in_path(X1,X2)|~path(X3,X4,X2)),inference(split_conjunct,[status(thm)],[125])).
% fof(146, negated_conjecture,(complete&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))&((![X7]:((~(edge(X7))|~(tail_of(X7)=tail_of(X4)))|~(head_of(X7)=head_of(X5)))|?[X7]:((edge(X7)&tail_of(X7)=head_of(X5))&head_of(X7)=tail_of(X4)))&(![X7]:((~(edge(X7))|~(tail_of(X7)=head_of(X5)))|~(head_of(X7)=tail_of(X4)))|?[X7]:((edge(X7)&tail_of(X7)=tail_of(X4))&head_of(X7)=head_of(X5)))))),inference(fof_nnf,[status(thm)],[26])).
% fof(147, negated_conjecture,(complete&?[X8]:?[X9]:?[X10]:?[X11]:?[X12]:((shortest_path(X8,X9,X12)&precedes(X10,X11,X12))&((![X13]:((~(edge(X13))|~(tail_of(X13)=tail_of(X10)))|~(head_of(X13)=head_of(X11)))|?[X14]:((edge(X14)&tail_of(X14)=head_of(X11))&head_of(X14)=tail_of(X10)))&(![X15]:((~(edge(X15))|~(tail_of(X15)=head_of(X11)))|~(head_of(X15)=tail_of(X10)))|?[X16]:((edge(X16)&tail_of(X16)=tail_of(X10))&head_of(X16)=head_of(X11)))))),inference(variable_rename,[status(thm)],[146])).
% fof(148, negated_conjecture,(complete&((shortest_path(esk9_0,esk10_0,esk13_0)&precedes(esk11_0,esk12_0,esk13_0))&((![X13]:((~(edge(X13))|~(tail_of(X13)=tail_of(esk11_0)))|~(head_of(X13)=head_of(esk12_0)))|((edge(esk14_0)&tail_of(esk14_0)=head_of(esk12_0))&head_of(esk14_0)=tail_of(esk11_0)))&(![X15]:((~(edge(X15))|~(tail_of(X15)=head_of(esk12_0)))|~(head_of(X15)=tail_of(esk11_0)))|((edge(esk15_0)&tail_of(esk15_0)=tail_of(esk11_0))&head_of(esk15_0)=head_of(esk12_0)))))),inference(skolemize,[status(esa)],[147])).
% fof(149, negated_conjecture,![X13]:![X15]:((((((~(edge(X15))|~(tail_of(X15)=head_of(esk12_0)))|~(head_of(X15)=tail_of(esk11_0)))|((edge(esk15_0)&tail_of(esk15_0)=tail_of(esk11_0))&head_of(esk15_0)=head_of(esk12_0)))&(((~(edge(X13))|~(tail_of(X13)=tail_of(esk11_0)))|~(head_of(X13)=head_of(esk12_0)))|((edge(esk14_0)&tail_of(esk14_0)=head_of(esk12_0))&head_of(esk14_0)=tail_of(esk11_0))))&(shortest_path(esk9_0,esk10_0,esk13_0)&precedes(esk11_0,esk12_0,esk13_0)))&complete),inference(shift_quantors,[status(thm)],[148])).
% fof(150, negated_conjecture,![X13]:![X15]:((((((edge(esk15_0)|((~(edge(X15))|~(tail_of(X15)=head_of(esk12_0)))|~(head_of(X15)=tail_of(esk11_0))))&(tail_of(esk15_0)=tail_of(esk11_0)|((~(edge(X15))|~(tail_of(X15)=head_of(esk12_0)))|~(head_of(X15)=tail_of(esk11_0)))))&(head_of(esk15_0)=head_of(esk12_0)|((~(edge(X15))|~(tail_of(X15)=head_of(esk12_0)))|~(head_of(X15)=tail_of(esk11_0)))))&(((edge(esk14_0)|((~(edge(X13))|~(tail_of(X13)=tail_of(esk11_0)))|~(head_of(X13)=head_of(esk12_0))))&(tail_of(esk14_0)=head_of(esk12_0)|((~(edge(X13))|~(tail_of(X13)=tail_of(esk11_0)))|~(head_of(X13)=head_of(esk12_0)))))&(head_of(esk14_0)=tail_of(esk11_0)|((~(edge(X13))|~(tail_of(X13)=tail_of(esk11_0)))|~(head_of(X13)=head_of(esk12_0))))))&(shortest_path(esk9_0,esk10_0,esk13_0)&precedes(esk11_0,esk12_0,esk13_0)))&complete),inference(distribute,[status(thm)],[149])).
% cnf(151,negated_conjecture,(complete),inference(split_conjunct,[status(thm)],[150])).
% cnf(152,negated_conjecture,(precedes(esk11_0,esk12_0,esk13_0)),inference(split_conjunct,[status(thm)],[150])).
% cnf(153,negated_conjecture,(shortest_path(esk9_0,esk10_0,esk13_0)),inference(split_conjunct,[status(thm)],[150])).
% cnf(157,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|head_of(X1)!=tail_of(esk11_0)|tail_of(X1)!=head_of(esk12_0)|~edge(X1)),inference(split_conjunct,[status(thm)],[150])).
% cnf(158,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|head_of(X1)!=tail_of(esk11_0)|tail_of(X1)!=head_of(esk12_0)|~edge(X1)),inference(split_conjunct,[status(thm)],[150])).
% cnf(162,plain,(X1=X2|edge(esk1_2(X1,X2))|$false|~vertex(X2)|~vertex(X1)),inference(rw,[status(thm)],[46,151,theory(equality)])).
% cnf(163,plain,(X1=X2|edge(esk1_2(X1,X2))|~vertex(X2)|~vertex(X1)),inference(cn,[status(thm)],[162,theory(equality)])).
% cnf(164,plain,(X1=X2|head_of(esk1_2(X1,X2))=X2|head_of(esk1_2(X1,X2))=X1|$false|~vertex(X2)|~vertex(X1)),inference(rw,[status(thm)],[44,151,theory(equality)])).
% cnf(165,plain,(X1=X2|head_of(esk1_2(X1,X2))=X2|head_of(esk1_2(X1,X2))=X1|~vertex(X2)|~vertex(X1)),inference(cn,[status(thm)],[164,theory(equality)])).
% cnf(166,plain,(X1=X2|head_of(esk1_2(X1,X2))=X2|tail_of(esk1_2(X1,X2))=X2|$false|~vertex(X2)|~vertex(X1)),inference(rw,[status(thm)],[42,151,theory(equality)])).
% cnf(167,plain,(X1=X2|head_of(esk1_2(X1,X2))=X2|tail_of(esk1_2(X1,X2))=X2|~vertex(X2)|~vertex(X1)),inference(cn,[status(thm)],[166,theory(equality)])).
% cnf(168,plain,(X1=X2|head_of(esk1_2(X1,X2))=X1|tail_of(esk1_2(X1,X2))=X1|$false|~vertex(X2)|~vertex(X1)),inference(rw,[status(thm)],[43,151,theory(equality)])).
% cnf(169,plain,(X1=X2|head_of(esk1_2(X1,X2))=X1|tail_of(esk1_2(X1,X2))=X1|~vertex(X2)|~vertex(X1)),inference(cn,[status(thm)],[168,theory(equality)])).
% cnf(177,negated_conjecture,(path(esk9_0,esk10_0,esk13_0)),inference(spm,[status(thm)],[94,153,theory(equality)])).
% cnf(189,negated_conjecture,(~precedes(esk12_0,esk11_0,esk13_0)|~shortest_path(X1,X2,esk13_0)),inference(spm,[status(thm)],[34,152,theory(equality)])).
% cnf(193,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|X1=X2|tail_of(esk1_2(X1,X2))!=head_of(esk12_0)|tail_of(esk11_0)!=head_of(esk1_2(X1,X2))|~vertex(X2)|~vertex(X1)),inference(spm,[status(thm)],[157,163,theory(equality)])).
% cnf(196,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|X1=X2|tail_of(esk1_2(X1,X2))!=head_of(esk12_0)|tail_of(esk11_0)!=head_of(esk1_2(X1,X2))|~vertex(X2)|~vertex(X1)),inference(spm,[status(thm)],[158,163,theory(equality)])).
% cnf(197,negated_conjecture,(head_of(esk12_0)!=head_of(X1)|tail_of(esk11_0)!=tail_of(X1)|~shortest_path(X2,X3,esk13_0)),inference(spm,[status(thm)],[35,152,theory(equality)])).
% cnf(270,negated_conjecture,(~precedes(esk12_0,esk11_0,esk13_0)),inference(spm,[status(thm)],[189,153,theory(equality)])).
% fof(271, plain,(~(epred1_0)<=>![X1]:(~(tail_of(esk11_0)=tail_of(X1))|~(head_of(esk12_0)=head_of(X1)))),introduced(definition),['split']).
% cnf(272,plain,(epred1_0|tail_of(esk11_0)!=tail_of(X1)|head_of(esk12_0)!=head_of(X1)),inference(split_equiv,[status(thm)],[271])).
% fof(273, plain,(~(epred2_0)<=>![X3]:![X2]:~(shortest_path(X2,X3,esk13_0))),introduced(definition),['split']).
% cnf(274,plain,(epred2_0|~shortest_path(X2,X3,esk13_0)),inference(split_equiv,[status(thm)],[273])).
% cnf(275,negated_conjecture,(~epred2_0|~epred1_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[197,271,theory(equality)]),273,theory(equality)]),['split']).
% cnf(280,negated_conjecture,(edge(X1)|~on_path(X1,esk13_0)),inference(spm,[status(thm)],[65,177,theory(equality)])).
% cnf(281,negated_conjecture,(vertex(X1)|~in_path(X1,esk13_0)),inference(spm,[status(thm)],[128,177,theory(equality)])).
% cnf(282,negated_conjecture,(in_path(head_of(X1),esk13_0)|~on_path(X1,esk13_0)),inference(spm,[status(thm)],[64,177,theory(equality)])).
% cnf(283,negated_conjecture,(in_path(tail_of(X1),esk13_0)|~on_path(X1,esk13_0)),inference(spm,[status(thm)],[63,177,theory(equality)])).
% cnf(284,negated_conjecture,(on_path(X1,esk13_0)|~precedes(X2,X1,esk13_0)),inference(spm,[status(thm)],[107,177,theory(equality)])).
% cnf(285,negated_conjecture,(on_path(X1,esk13_0)|~precedes(X1,X2,esk13_0)),inference(spm,[status(thm)],[108,177,theory(equality)])).
% cnf(288,negated_conjecture,(precedes(X1,X2,esk13_0)|~on_path(X2,esk13_0)|~on_path(X1,esk13_0)|~sequential(X1,X2)),inference(spm,[status(thm)],[100,177,theory(equality)])).
% cnf(295,negated_conjecture,(epred2_0),inference(spm,[status(thm)],[274,153,theory(equality)])).
% cnf(296,negated_conjecture,($false|~epred1_0),inference(rw,[status(thm)],[275,295,theory(equality)])).
% cnf(297,negated_conjecture,(~epred1_0),inference(cn,[status(thm)],[296,theory(equality)])).
% cnf(299,negated_conjecture,(tail_of(esk11_0)!=tail_of(X1)|head_of(esk12_0)!=head_of(X1)),inference(sr,[status(thm)],[272,297,theory(equality)])).
% cnf(304,negated_conjecture,(head_of(esk1_2(X1,X2))=X1|X1=X2|tail_of(esk11_0)!=X1|head_of(esk12_0)!=head_of(esk1_2(X1,X2))|~vertex(X2)|~vertex(X1)),inference(spm,[status(thm)],[299,169,theory(equality)])).
% cnf(309,negated_conjecture,(on_path(esk12_0,esk13_0)),inference(spm,[status(thm)],[284,152,theory(equality)])).
% cnf(311,negated_conjecture,(edge(esk12_0)),inference(spm,[status(thm)],[280,309,theory(equality)])).
% cnf(315,negated_conjecture,(tail_of(esk12_0)!=head_of(esk12_0)),inference(spm,[status(thm)],[29,311,theory(equality)])).
% cnf(328,negated_conjecture,(on_path(esk11_0,esk13_0)),inference(spm,[status(thm)],[285,152,theory(equality)])).
% cnf(330,negated_conjecture,(edge(esk11_0)),inference(spm,[status(thm)],[280,328,theory(equality)])).
% cnf(336,negated_conjecture,(vertex(head_of(X1))|~on_path(X1,esk13_0)),inference(spm,[status(thm)],[281,282,theory(equality)])).
% cnf(346,negated_conjecture,(vertex(head_of(esk12_0))),inference(spm,[status(thm)],[336,309,theory(equality)])).
% cnf(351,negated_conjecture,(head_of(esk1_2(X1,head_of(esk12_0)))=head_of(esk12_0)|head_of(esk1_2(X1,head_of(esk12_0)))=X1|X1=head_of(esk12_0)|~vertex(X1)),inference(spm,[status(thm)],[165,346,theory(equality)])).
% cnf(366,negated_conjecture,(vertex(tail_of(X1))|~on_path(X1,esk13_0)),inference(spm,[status(thm)],[281,283,theory(equality)])).
% cnf(371,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|X1=X2|head_of(esk1_2(X1,X2))=X2|X2!=head_of(esk12_0)|head_of(esk1_2(X1,X2))!=tail_of(esk11_0)|~vertex(X2)|~vertex(X1)),inference(spm,[status(thm)],[193,167,theory(equality)])).
% cnf(380,negated_conjecture,(vertex(tail_of(esk11_0))),inference(spm,[status(thm)],[366,328,theory(equality)])).
% cnf(392,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|X1=X2|head_of(esk1_2(X1,X2))=X2|X2!=head_of(esk12_0)|head_of(esk1_2(X1,X2))!=tail_of(esk11_0)|~vertex(X2)|~vertex(X1)),inference(spm,[status(thm)],[196,167,theory(equality)])).
% cnf(413,negated_conjecture,(~on_path(esk11_0,esk13_0)|~on_path(esk12_0,esk13_0)|~sequential(esk12_0,esk11_0)),inference(spm,[status(thm)],[270,288,theory(equality)])).
% cnf(421,negated_conjecture,($false|~on_path(esk12_0,esk13_0)|~sequential(esk12_0,esk11_0)),inference(rw,[status(thm)],[413,328,theory(equality)])).
% cnf(422,negated_conjecture,($false|$false|~sequential(esk12_0,esk11_0)),inference(rw,[status(thm)],[421,309,theory(equality)])).
% cnf(423,negated_conjecture,(~sequential(esk12_0,esk11_0)),inference(cn,[status(thm)],[422,theory(equality)])).
% cnf(430,negated_conjecture,(esk12_0=esk11_0|tail_of(esk11_0)!=head_of(esk12_0)|~edge(esk11_0)|~edge(esk12_0)),inference(spm,[status(thm)],[423,50,theory(equality)])).
% cnf(431,negated_conjecture,(esk12_0=esk11_0|tail_of(esk11_0)!=head_of(esk12_0)|$false|~edge(esk12_0)),inference(rw,[status(thm)],[430,330,theory(equality)])).
% cnf(432,negated_conjecture,(esk12_0=esk11_0|tail_of(esk11_0)!=head_of(esk12_0)|$false|$false),inference(rw,[status(thm)],[431,311,theory(equality)])).
% cnf(433,negated_conjecture,(esk12_0=esk11_0|tail_of(esk11_0)!=head_of(esk12_0)),inference(cn,[status(thm)],[432,theory(equality)])).
% cnf(3885,negated_conjecture,(head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=tail_of(esk11_0)|tail_of(esk11_0)=head_of(esk12_0)),inference(spm,[status(thm)],[351,380,theory(equality)])).
% cnf(7220,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|~vertex(head_of(esk12_0))|~vertex(tail_of(esk11_0))),inference(spm,[status(thm)],[371,3885,theory(equality)])).
% cnf(7221,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|~vertex(head_of(esk12_0))|~vertex(tail_of(esk11_0))),inference(spm,[status(thm)],[392,3885,theory(equality)])).
% cnf(7231,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|$false|~vertex(tail_of(esk11_0))),inference(rw,[status(thm)],[7220,346,theory(equality)])).
% cnf(7232,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|$false|$false),inference(rw,[status(thm)],[7231,380,theory(equality)])).
% cnf(7233,negated_conjecture,(head_of(esk15_0)=head_of(esk12_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)),inference(cn,[status(thm)],[7232,theory(equality)])).
% cnf(7234,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|$false|~vertex(tail_of(esk11_0))),inference(rw,[status(thm)],[7221,346,theory(equality)])).
% cnf(7235,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)|$false|$false),inference(rw,[status(thm)],[7234,380,theory(equality)])).
% cnf(7236,negated_conjecture,(tail_of(esk15_0)=tail_of(esk11_0)|tail_of(esk11_0)=head_of(esk12_0)|head_of(esk1_2(tail_of(esk11_0),head_of(esk12_0)))=head_of(esk12_0)),inference(cn,[status(thm)],[7235,theory(equality)])).
% cnf(7298,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|head_of(esk15_0)=head_of(esk12_0)|~vertex(head_of(esk12_0))|~vertex(tail_of(esk11_0))),inference(spm,[status(thm)],[304,7233,theory(equality)])).
% cnf(7305,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|head_of(esk15_0)=head_of(esk12_0)|$false|~vertex(tail_of(esk11_0))),inference(rw,[status(thm)],[7298,346,theory(equality)])).
% cnf(7306,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|head_of(esk15_0)=head_of(esk12_0)|$false|$false),inference(rw,[status(thm)],[7305,380,theory(equality)])).
% cnf(7307,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|head_of(esk15_0)=head_of(esk12_0)),inference(cn,[status(thm)],[7306,theory(equality)])).
% cnf(7560,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|tail_of(esk15_0)=tail_of(esk11_0)|~vertex(head_of(esk12_0))|~vertex(tail_of(esk11_0))),inference(spm,[status(thm)],[304,7236,theory(equality)])).
% cnf(7567,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|tail_of(esk15_0)=tail_of(esk11_0)|$false|~vertex(tail_of(esk11_0))),inference(rw,[status(thm)],[7560,346,theory(equality)])).
% cnf(7568,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|tail_of(esk15_0)=tail_of(esk11_0)|$false|$false),inference(rw,[status(thm)],[7567,380,theory(equality)])).
% cnf(7569,negated_conjecture,(head_of(esk12_0)=tail_of(esk11_0)|tail_of(esk15_0)=tail_of(esk11_0)),inference(cn,[status(thm)],[7568,theory(equality)])).
% cnf(7580,negated_conjecture,(tail_of(esk11_0)=head_of(esk12_0)|head_of(esk12_0)!=head_of(esk15_0)),inference(spm,[status(thm)],[299,7569,theory(equality)])).
% cnf(7603,negated_conjecture,(tail_of(esk11_0)=head_of(esk12_0)),inference(csr,[status(thm)],[7580,7307])).
% cnf(7779,negated_conjecture,(esk12_0=esk11_0|$false),inference(rw,[status(thm)],[433,7603,theory(equality)])).
% cnf(7780,negated_conjecture,(esk12_0=esk11_0),inference(cn,[status(thm)],[7779,theory(equality)])).
% cnf(8121,negated_conjecture,(head_of(esk11_0)!=head_of(esk12_0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[315,7780,theory(equality)]),7603,theory(equality)]),7780,theory(equality)])).
% cnf(8122,negated_conjecture,($false),inference(rw,[status(thm)],[8121,7780,theory(equality)])).
% cnf(8123,negated_conjecture,($false),inference(cn,[status(thm)],[8122,theory(equality)])).
% cnf(8124,negated_conjecture,($false),8123,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1007
% # ...of these trivial : 94
% # ...subsumed : 274
% # ...remaining for further processing: 639
% # Other redundant clauses eliminated : 7
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 98
% # Backward-rewritten : 225
% # Generated clauses : 4762
% # ...of the previous two non-trivial : 4224
% # Contextual simplify-reflections : 251
% # Paramodulations : 4667
% # Factorizations : 60
% # Equation resolutions : 17
% # Current number of processed clauses: 241
% # Positive orientable unit clauses: 19
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 8
% # Non-unit-clauses : 214
% # Current number of unprocessed clauses: 772
% # ...number of literals in the above : 4307
% # Clause-clause subsumption calls (NU) : 9520
% # Rec. Clause-clause subsumption calls : 3069
% # Unit Clause-clause subsumption calls : 514
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 8
% # Indexed BW rewrite successes : 8
% # Backwards rewriting index: 218 leaves, 1.87+/-3.752 terms/leaf
% # Paramod-from index: 83 leaves, 1.10+/-0.333 terms/leaf
% # Paramod-into index: 174 leaves, 1.43+/-1.529 terms/leaf
% # -------------------------------------------------
% # User time : 0.285 s
% # System time : 0.012 s
% # Total time : 0.297 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.52 CPU 0.62 WC
% FINAL PrfWatch: 0.52 CPU 0.62 WC
% SZS output end Solution for /tmp/SystemOnTPTP28480/GRA006+1.tptp
%
%------------------------------------------------------------------------------