%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SYN550+1 : TPTP v5.0.0. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %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 : Thu Dec 30 09:58:11 EST 2010
% Result : Theorem 1.09s
% Output : Solution 1.09s
% 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/SystemOnTPTP13808/SYN550+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP13808/SYN550+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP13808/SYN550+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 13904
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.011 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:reachable(X1,X1),file('/tmp/SRASS.s.p', reflexivity_of_reachable)).
% fof(2, axiom,![X1]:![X2]:![X3]:((reachable(X1,X2)&reachable(X2,X3))=>reachable(X1,X3)),file('/tmp/SRASS.s.p', transitivity_of_reachable)).
% fof(3, conjecture,(?[X1]:(reachable(initial_world,X1)&![X2]:(reachable(X1,X2)=>p(X2)))<=>?[X1]:(reachable(initial_world,X1)&![X2]:(reachable(X1,X2)=>?[X3]:(reachable(X2,X3)&![X4]:(reachable(X3,X4)=>p(X4)))))),file('/tmp/SRASS.s.p', prove_this)).
% fof(4, negated_conjecture,~((?[X1]:(reachable(initial_world,X1)&![X2]:(reachable(X1,X2)=>p(X2)))<=>?[X1]:(reachable(initial_world,X1)&![X2]:(reachable(X1,X2)=>?[X3]:(reachable(X2,X3)&![X4]:(reachable(X3,X4)=>p(X4))))))),inference(assume_negation,[status(cth)],[3])).
% fof(5, plain,![X2]:reachable(X2,X2),inference(variable_rename,[status(thm)],[1])).
% cnf(6,plain,(reachable(X1,X1)),inference(split_conjunct,[status(thm)],[5])).
% fof(7, plain,![X1]:![X2]:![X3]:((~(reachable(X1,X2))|~(reachable(X2,X3)))|reachable(X1,X3)),inference(fof_nnf,[status(thm)],[2])).
% fof(8, plain,![X4]:![X5]:![X6]:((~(reachable(X4,X5))|~(reachable(X5,X6)))|reachable(X4,X6)),inference(variable_rename,[status(thm)],[7])).
% cnf(9,plain,(reachable(X1,X2)|~reachable(X3,X2)|~reachable(X1,X3)),inference(split_conjunct,[status(thm)],[8])).
% fof(10, negated_conjecture,((![X1]:(~(reachable(initial_world,X1))|?[X2]:(reachable(X1,X2)&~(p(X2))))|![X1]:(~(reachable(initial_world,X1))|?[X2]:(reachable(X1,X2)&![X3]:(~(reachable(X2,X3))|?[X4]:(reachable(X3,X4)&~(p(X4)))))))&(?[X1]:(reachable(initial_world,X1)&![X2]:(~(reachable(X1,X2))|p(X2)))|?[X1]:(reachable(initial_world,X1)&![X2]:(~(reachable(X1,X2))|?[X3]:(reachable(X2,X3)&![X4]:(~(reachable(X3,X4))|p(X4))))))),inference(fof_nnf,[status(thm)],[4])).
% fof(11, negated_conjecture,((![X5]:(~(reachable(initial_world,X5))|?[X6]:(reachable(X5,X6)&~(p(X6))))|![X7]:(~(reachable(initial_world,X7))|?[X8]:(reachable(X7,X8)&![X9]:(~(reachable(X8,X9))|?[X10]:(reachable(X9,X10)&~(p(X10)))))))&(?[X11]:(reachable(initial_world,X11)&![X12]:(~(reachable(X11,X12))|p(X12)))|?[X13]:(reachable(initial_world,X13)&![X14]:(~(reachable(X13,X14))|?[X15]:(reachable(X14,X15)&![X16]:(~(reachable(X15,X16))|p(X16))))))),inference(variable_rename,[status(thm)],[10])).
% fof(12, negated_conjecture,((![X5]:(~(reachable(initial_world,X5))|(reachable(X5,esk1_1(X5))&~(p(esk1_1(X5)))))|![X7]:(~(reachable(initial_world,X7))|(reachable(X7,esk2_1(X7))&![X9]:(~(reachable(esk2_1(X7),X9))|(reachable(X9,esk3_2(X7,X9))&~(p(esk3_2(X7,X9))))))))&((reachable(initial_world,esk4_0)&![X12]:(~(reachable(esk4_0,X12))|p(X12)))|(reachable(initial_world,esk5_0)&![X14]:(~(reachable(esk5_0,X14))|(reachable(X14,esk6_1(X14))&![X16]:(~(reachable(esk6_1(X14),X16))|p(X16))))))),inference(skolemize,[status(esa)],[11])).
% fof(13, negated_conjecture,![X5]:![X7]:![X9]:![X12]:![X14]:![X16]:((((((~(reachable(esk6_1(X14),X16))|p(X16))&reachable(X14,esk6_1(X14)))|~(reachable(esk5_0,X14)))&reachable(initial_world,esk5_0))|((~(reachable(esk4_0,X12))|p(X12))&reachable(initial_world,esk4_0)))&((((~(reachable(esk2_1(X7),X9))|(reachable(X9,esk3_2(X7,X9))&~(p(esk3_2(X7,X9)))))&reachable(X7,esk2_1(X7)))|~(reachable(initial_world,X7)))|(~(reachable(initial_world,X5))|(reachable(X5,esk1_1(X5))&~(p(esk1_1(X5))))))),inference(shift_quantors,[status(thm)],[12])).
% fof(14, negated_conjecture,![X5]:![X7]:![X9]:![X12]:![X14]:![X16]:((((((~(reachable(esk4_0,X12))|p(X12))|((~(reachable(esk6_1(X14),X16))|p(X16))|~(reachable(esk5_0,X14))))&(reachable(initial_world,esk4_0)|((~(reachable(esk6_1(X14),X16))|p(X16))|~(reachable(esk5_0,X14)))))&(((~(reachable(esk4_0,X12))|p(X12))|(reachable(X14,esk6_1(X14))|~(reachable(esk5_0,X14))))&(reachable(initial_world,esk4_0)|(reachable(X14,esk6_1(X14))|~(reachable(esk5_0,X14))))))&(((~(reachable(esk4_0,X12))|p(X12))|reachable(initial_world,esk5_0))&(reachable(initial_world,esk4_0)|reachable(initial_world,esk5_0))))&(((((reachable(X5,esk1_1(X5))|~(reachable(initial_world,X5)))|((reachable(X9,esk3_2(X7,X9))|~(reachable(esk2_1(X7),X9)))|~(reachable(initial_world,X7))))&((~(p(esk1_1(X5)))|~(reachable(initial_world,X5)))|((reachable(X9,esk3_2(X7,X9))|~(reachable(esk2_1(X7),X9)))|~(reachable(initial_world,X7)))))&(((reachable(X5,esk1_1(X5))|~(reachable(initial_world,X5)))|((~(p(esk3_2(X7,X9)))|~(reachable(esk2_1(X7),X9)))|~(reachable(initial_world,X7))))&((~(p(esk1_1(X5)))|~(reachable(initial_world,X5)))|((~(p(esk3_2(X7,X9)))|~(reachable(esk2_1(X7),X9)))|~(reachable(initial_world,X7))))))&(((reachable(X5,esk1_1(X5))|~(reachable(initial_world,X5)))|(reachable(X7,esk2_1(X7))|~(reachable(initial_world,X7))))&((~(p(esk1_1(X5)))|~(reachable(initial_world,X5)))|(reachable(X7,esk2_1(X7))|~(reachable(initial_world,X7))))))),inference(distribute,[status(thm)],[13])).
% cnf(15,negated_conjecture,(reachable(X1,esk2_1(X1))|~reachable(initial_world,X1)|~reachable(initial_world,X2)|~p(esk1_1(X2))),inference(split_conjunct,[status(thm)],[14])).
% cnf(16,negated_conjecture,(reachable(X1,esk2_1(X1))|reachable(X2,esk1_1(X2))|~reachable(initial_world,X1)|~reachable(initial_world,X2)),inference(split_conjunct,[status(thm)],[14])).
% cnf(17,negated_conjecture,(~reachable(initial_world,X1)|~reachable(esk2_1(X1),X2)|~p(esk3_2(X1,X2))|~reachable(initial_world,X3)|~p(esk1_1(X3))),inference(split_conjunct,[status(thm)],[14])).
% cnf(18,negated_conjecture,(reachable(X3,esk1_1(X3))|~reachable(initial_world,X1)|~reachable(esk2_1(X1),X2)|~p(esk3_2(X1,X2))|~reachable(initial_world,X3)),inference(split_conjunct,[status(thm)],[14])).
% cnf(19,negated_conjecture,(reachable(X2,esk3_2(X1,X2))|~reachable(initial_world,X1)|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X3)|~p(esk1_1(X3))),inference(split_conjunct,[status(thm)],[14])).
% cnf(20,negated_conjecture,(reachable(X2,esk3_2(X1,X2))|reachable(X3,esk1_1(X3))|~reachable(initial_world,X1)|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X3)),inference(split_conjunct,[status(thm)],[14])).
% cnf(21,negated_conjecture,(reachable(initial_world,esk5_0)|reachable(initial_world,esk4_0)),inference(split_conjunct,[status(thm)],[14])).
% cnf(22,negated_conjecture,(reachable(initial_world,esk5_0)|p(X1)|~reachable(esk4_0,X1)),inference(split_conjunct,[status(thm)],[14])).
% cnf(23,negated_conjecture,(reachable(X1,esk6_1(X1))|reachable(initial_world,esk4_0)|~reachable(esk5_0,X1)),inference(split_conjunct,[status(thm)],[14])).
% cnf(24,negated_conjecture,(reachable(X1,esk6_1(X1))|p(X2)|~reachable(esk5_0,X1)|~reachable(esk4_0,X2)),inference(split_conjunct,[status(thm)],[14])).
% cnf(25,negated_conjecture,(p(X2)|reachable(initial_world,esk4_0)|~reachable(esk5_0,X1)|~reachable(esk6_1(X1),X2)),inference(split_conjunct,[status(thm)],[14])).
% cnf(26,negated_conjecture,(p(X2)|p(X3)|~reachable(esk5_0,X1)|~reachable(esk6_1(X1),X2)|~reachable(esk4_0,X3)),inference(split_conjunct,[status(thm)],[14])).
% fof(27, plain,(~(epred1_0)<=>![X2]:(p(X2)|~(reachable(esk4_0,X2)))),introduced(definition),['split']).
% cnf(28,plain,(epred1_0|p(X2)|~reachable(esk4_0,X2)),inference(split_equiv,[status(thm)],[27])).
% fof(29, plain,(~(epred2_0)<=>![X1]:(reachable(X1,esk6_1(X1))|~(reachable(esk5_0,X1)))),introduced(definition),['split']).
% cnf(30,plain,(epred2_0|reachable(X1,esk6_1(X1))|~reachable(esk5_0,X1)),inference(split_equiv,[status(thm)],[29])).
% cnf(31,negated_conjecture,(~epred2_0|~epred1_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[24,27,theory(equality)]),29,theory(equality)]),['split']).
% fof(32, plain,(~(epred3_0)<=>![X1]:(reachable(X1,esk2_1(X1))|~(reachable(initial_world,X1)))),introduced(definition),['split']).
% cnf(33,plain,(epred3_0|reachable(X1,esk2_1(X1))|~reachable(initial_world,X1)),inference(split_equiv,[status(thm)],[32])).
% fof(34, plain,(~(epred4_0)<=>![X2]:(~(p(esk1_1(X2)))|~(reachable(initial_world,X2)))),introduced(definition),['split']).
% cnf(35,plain,(epred4_0|~reachable(initial_world,X2)|~p(esk1_1(X2))),inference(split_equiv,[status(thm)],[34])).
% cnf(36,negated_conjecture,(~epred4_0|~epred3_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[15,32,theory(equality)]),34,theory(equality)]),['split']).
% fof(37, plain,(~(epred5_0)<=>![X2]:(reachable(X2,esk1_1(X2))|~(reachable(initial_world,X2)))),introduced(definition),['split']).
% cnf(38,plain,(epred5_0|reachable(X2,esk1_1(X2))|~reachable(initial_world,X2)),inference(split_equiv,[status(thm)],[37])).
% cnf(39,negated_conjecture,(~epred5_0|~epred3_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[16,32,theory(equality)]),37,theory(equality)]),['split']).
% fof(40, plain,(~(epred6_0)<=>![X2]:![X1]:((p(X2)|~(reachable(esk6_1(X1),X2)))|~(reachable(esk5_0,X1)))),introduced(definition),['split']).
% cnf(41,plain,(epred6_0|p(X2)|~reachable(esk5_0,X1)|~reachable(esk6_1(X1),X2)),inference(split_equiv,[status(thm)],[40])).
% cnf(42,negated_conjecture,(~epred1_0|~epred6_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[26,40,theory(equality)]),27,theory(equality)]),['split']).
% fof(43, plain,(~(epred7_0)<=>![X2]:![X1]:((~(p(esk3_2(X1,X2)))|~(reachable(esk2_1(X1),X2)))|~(reachable(initial_world,X1)))),introduced(definition),['split']).
% cnf(44,plain,(epred7_0|~reachable(initial_world,X1)|~reachable(esk2_1(X1),X2)|~p(esk3_2(X1,X2))),inference(split_equiv,[status(thm)],[43])).
% cnf(45,negated_conjecture,(~epred4_0|~epred7_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[17,43,theory(equality)]),34,theory(equality)]),['split']).
% fof(46, plain,(~(epred8_0)<=>![X2]:![X1]:((reachable(X2,esk3_2(X1,X2))|~(reachable(esk2_1(X1),X2)))|~(reachable(initial_world,X1)))),introduced(definition),['split']).
% cnf(47,plain,(epred8_0|reachable(X2,esk3_2(X1,X2))|~reachable(initial_world,X1)|~reachable(esk2_1(X1),X2)),inference(split_equiv,[status(thm)],[46])).
% cnf(48,negated_conjecture,(~epred4_0|~epred8_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[19,46,theory(equality)]),34,theory(equality)]),['split']).
% cnf(49,negated_conjecture,(~epred7_0|~epred5_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[18,37,theory(equality)]),43,theory(equality)]),['split']).
% cnf(50,negated_conjecture,(~epred5_0|~epred8_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[20,46,theory(equality)]),37,theory(equality)]),['split']).
% cnf(51,negated_conjecture,(epred7_0|reachable(initial_world,esk5_0)|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X1)|~reachable(esk4_0,esk3_2(X1,X2))),inference(spm,[status(thm)],[44,22,theory(equality)])).
% cnf(55,negated_conjecture,(reachable(X1,esk6_1(X2))|reachable(initial_world,esk4_0)|~reachable(X1,X2)|~reachable(esk5_0,X2)),inference(spm,[status(thm)],[9,23,theory(equality)])).
% cnf(57,negated_conjecture,(epred7_0|epred1_0|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X1)|~reachable(esk4_0,esk3_2(X1,X2))),inference(spm,[status(thm)],[44,28,theory(equality)])).
% cnf(58,negated_conjecture,(epred4_0|reachable(initial_world,esk5_0)|~reachable(initial_world,X1)|~reachable(esk4_0,esk1_1(X1))),inference(spm,[status(thm)],[35,22,theory(equality)])).
% cnf(59,negated_conjecture,(epred4_0|epred1_0|~reachable(initial_world,X1)|~reachable(esk4_0,esk1_1(X1))),inference(spm,[status(thm)],[35,28,theory(equality)])).
% cnf(61,negated_conjecture,(reachable(X1,esk6_1(X2))|epred2_0|~reachable(X1,X2)|~reachable(esk5_0,X2)),inference(spm,[status(thm)],[9,30,theory(equality)])).
% cnf(64,negated_conjecture,(p(esk1_1(esk6_1(X1)))|reachable(initial_world,esk4_0)|epred5_0|~reachable(esk5_0,X1)|~reachable(initial_world,esk6_1(X1))),inference(spm,[status(thm)],[25,38,theory(equality)])).
% cnf(69,negated_conjecture,(epred6_0|p(esk1_1(esk6_1(X1)))|epred5_0|~reachable(esk5_0,X1)|~reachable(initial_world,esk6_1(X1))),inference(spm,[status(thm)],[41,38,theory(equality)])).
% cnf(71,negated_conjecture,(p(esk3_2(X1,esk6_1(X2)))|reachable(initial_world,esk4_0)|epred8_0|~reachable(esk5_0,X2)|~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)),inference(spm,[status(thm)],[25,47,theory(equality)])).
% cnf(72,negated_conjecture,(epred6_0|p(esk3_2(X1,esk6_1(X2)))|epred8_0|~reachable(esk5_0,X2)|~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)),inference(spm,[status(thm)],[41,47,theory(equality)])).
% cnf(73,negated_conjecture,(reachable(X1,esk3_2(X2,X3))|epred8_0|~reachable(X1,X3)|~reachable(esk2_1(X2),X3)|~reachable(initial_world,X2)),inference(spm,[status(thm)],[9,47,theory(equality)])).
% cnf(76,negated_conjecture,(epred4_0|epred1_0|epred5_0|~reachable(initial_world,esk4_0)),inference(spm,[status(thm)],[59,38,theory(equality)])).
% cnf(79,negated_conjecture,(epred4_0|reachable(initial_world,esk5_0)|epred5_0|~reachable(initial_world,esk4_0)),inference(spm,[status(thm)],[58,38,theory(equality)])).
% cnf(80,negated_conjecture,(epred5_0|epred4_0|reachable(initial_world,esk5_0)),inference(csr,[status(thm)],[79,21])).
% cnf(116,negated_conjecture,(epred4_0|epred5_0|reachable(initial_world,esk4_0)|~reachable(initial_world,esk6_1(X1))|~reachable(esk5_0,X1)),inference(spm,[status(thm)],[35,64,theory(equality)])).
% cnf(128,negated_conjecture,(epred5_0|epred4_0|reachable(initial_world,esk4_0)|~reachable(esk5_0,X1)|~reachable(initial_world,X1)),inference(spm,[status(thm)],[116,55,theory(equality)])).
% cnf(141,negated_conjecture,(epred5_0|epred4_0|reachable(initial_world,esk4_0)|~reachable(initial_world,esk5_0)),inference(spm,[status(thm)],[128,6,theory(equality)])).
% cnf(148,negated_conjecture,(epred5_0|epred4_0|reachable(initial_world,esk4_0)),inference(csr,[status(thm)],[141,80])).
% cnf(150,negated_conjecture,(epred5_0|epred4_0|epred1_0),inference(spm,[status(thm)],[76,148,theory(equality)])).
% cnf(151,negated_conjecture,(epred5_0|epred4_0|~epred2_0),inference(spm,[status(thm)],[31,150,theory(equality)])).
% cnf(152,negated_conjecture,(epred5_0|epred4_0|~epred6_0),inference(spm,[status(thm)],[42,150,theory(equality)])).
% cnf(180,negated_conjecture,(epred4_0|epred6_0|epred5_0|~reachable(initial_world,esk6_1(X1))|~reachable(esk5_0,X1)),inference(spm,[status(thm)],[35,69,theory(equality)])).
% cnf(181,negated_conjecture,(epred7_0|epred8_0|reachable(initial_world,esk4_0)|~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)|~reachable(esk5_0,X2)),inference(spm,[status(thm)],[44,71,theory(equality)])).
% cnf(182,negated_conjecture,(epred8_0|epred7_0|reachable(initial_world,esk4_0)|~reachable(initial_world,X1)|~reachable(esk5_0,esk2_1(X1))),inference(spm,[status(thm)],[181,23,theory(equality)])).
% cnf(186,negated_conjecture,(epred8_0|epred7_0|reachable(initial_world,esk4_0)|epred3_0|~reachable(initial_world,esk5_0)),inference(spm,[status(thm)],[182,33,theory(equality)])).
% cnf(188,negated_conjecture,(epred8_0|epred7_0|epred3_0|reachable(initial_world,esk4_0)),inference(csr,[status(thm)],[186,21])).
% cnf(195,negated_conjecture,(epred5_0|epred4_0|~reachable(initial_world,esk6_1(X1))|~reachable(esk5_0,X1)),inference(csr,[status(thm)],[180,152])).
% cnf(199,negated_conjecture,(epred5_0|epred4_0|epred2_0|~reachable(esk5_0,X1)|~reachable(initial_world,X1)),inference(spm,[status(thm)],[195,61,theory(equality)])).
% cnf(202,negated_conjecture,(epred5_0|epred4_0|~reachable(esk5_0,X1)|~reachable(initial_world,X1)),inference(csr,[status(thm)],[199,151])).
% cnf(215,negated_conjecture,(epred5_0|epred4_0|~reachable(initial_world,esk5_0)),inference(spm,[status(thm)],[202,6,theory(equality)])).
% cnf(220,negated_conjecture,(epred7_0|epred8_0|epred6_0|~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)|~reachable(esk5_0,X2)),inference(spm,[status(thm)],[44,72,theory(equality)])).
% cnf(228,negated_conjecture,(epred5_0|epred4_0),inference(csr,[status(thm)],[215,80])).
% cnf(229,negated_conjecture,(epred5_0|~epred7_0),inference(spm,[status(thm)],[45,228,theory(equality)])).
% cnf(230,negated_conjecture,(epred5_0|~epred8_0),inference(spm,[status(thm)],[48,228,theory(equality)])).
% cnf(231,negated_conjecture,(~epred7_0),inference(csr,[status(thm)],[229,49])).
% cnf(232,negated_conjecture,(epred8_0|epred3_0|reachable(initial_world,esk4_0)),inference(sr,[status(thm)],[188,231,theory(equality)])).
% cnf(233,negated_conjecture,(~epred8_0),inference(csr,[status(thm)],[230,50])).
% cnf(234,negated_conjecture,(epred3_0|reachable(initial_world,esk4_0)),inference(sr,[status(thm)],[232,233,theory(equality)])).
% cnf(236,negated_conjecture,(reachable(X1,esk3_2(X2,X3))|~reachable(X1,X3)|~reachable(esk2_1(X2),X3)|~reachable(initial_world,X2)),inference(sr,[status(thm)],[73,233,theory(equality)])).
% cnf(239,negated_conjecture,(epred7_0|epred1_0|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X1)|~reachable(esk4_0,X2)),inference(spm,[status(thm)],[57,236,theory(equality)])).
% cnf(240,negated_conjecture,(epred7_0|reachable(initial_world,esk5_0)|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X1)|~reachable(esk4_0,X2)),inference(spm,[status(thm)],[51,236,theory(equality)])).
% cnf(242,negated_conjecture,(epred1_0|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X1)|~reachable(esk4_0,X2)),inference(sr,[status(thm)],[239,231,theory(equality)])).
% cnf(243,negated_conjecture,(reachable(initial_world,esk5_0)|~reachable(esk2_1(X1),X2)|~reachable(initial_world,X1)|~reachable(esk4_0,X2)),inference(sr,[status(thm)],[240,231,theory(equality)])).
% cnf(264,negated_conjecture,(reachable(initial_world,esk5_0)|~reachable(initial_world,X1)|~reachable(esk4_0,esk2_1(X1))),inference(spm,[status(thm)],[243,6,theory(equality)])).
% cnf(268,negated_conjecture,(reachable(initial_world,esk5_0)|epred3_0|~reachable(initial_world,esk4_0)),inference(spm,[status(thm)],[264,33,theory(equality)])).
% cnf(270,negated_conjecture,(epred3_0|reachable(initial_world,esk5_0)),inference(csr,[status(thm)],[268,234])).
% cnf(295,negated_conjecture,(epred1_0|~reachable(initial_world,X1)|~reachable(esk4_0,esk2_1(X1))),inference(spm,[status(thm)],[242,6,theory(equality)])).
% cnf(299,negated_conjecture,(epred1_0|epred3_0|~reachable(initial_world,esk4_0)),inference(spm,[status(thm)],[295,33,theory(equality)])).
% cnf(301,negated_conjecture,(epred3_0|epred1_0),inference(csr,[status(thm)],[299,234])).
% cnf(302,negated_conjecture,(epred3_0|~epred2_0),inference(spm,[status(thm)],[31,301,theory(equality)])).
% cnf(303,negated_conjecture,(epred3_0|~epred6_0),inference(spm,[status(thm)],[42,301,theory(equality)])).
% cnf(304,negated_conjecture,(~epred4_0|~epred6_0),inference(spm,[status(thm)],[36,303,theory(equality)])).
% cnf(305,negated_conjecture,(~epred5_0|~epred6_0),inference(spm,[status(thm)],[39,303,theory(equality)])).
% cnf(323,negated_conjecture,(epred5_0|~epred6_0),inference(spm,[status(thm)],[304,228,theory(equality)])).
% cnf(324,negated_conjecture,(~epred6_0),inference(csr,[status(thm)],[323,305])).
% cnf(547,negated_conjecture,(epred8_0|epred6_0|~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)|~reachable(esk5_0,X2)),inference(sr,[status(thm)],[220,231,theory(equality)])).
% cnf(548,negated_conjecture,(epred6_0|~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)|~reachable(esk5_0,X2)),inference(sr,[status(thm)],[547,233,theory(equality)])).
% cnf(549,negated_conjecture,(~reachable(esk2_1(X1),esk6_1(X2))|~reachable(initial_world,X1)|~reachable(esk5_0,X2)),inference(sr,[status(thm)],[548,324,theory(equality)])).
% cnf(551,negated_conjecture,(epred2_0|~reachable(initial_world,X1)|~reachable(esk5_0,esk2_1(X1))),inference(spm,[status(thm)],[549,30,theory(equality)])).
% cnf(556,negated_conjecture,(epred2_0|epred3_0|~reachable(initial_world,esk5_0)),inference(spm,[status(thm)],[551,33,theory(equality)])).
% cnf(558,negated_conjecture,(epred3_0|epred2_0),inference(csr,[status(thm)],[556,270])).
% cnf(559,negated_conjecture,(epred3_0),inference(csr,[status(thm)],[558,302])).
% cnf(581,negated_conjecture,(~epred5_0|$false),inference(rw,[status(thm)],[39,559,theory(equality)])).
% cnf(582,negated_conjecture,(~epred5_0),inference(cn,[status(thm)],[581,theory(equality)])).
% cnf(583,negated_conjecture,(~epred4_0|$false),inference(rw,[status(thm)],[36,559,theory(equality)])).
% cnf(584,negated_conjecture,(~epred4_0),inference(cn,[status(thm)],[583,theory(equality)])).
% cnf(597,negated_conjecture,(epred4_0),inference(sr,[status(thm)],[228,582,theory(equality)])).
% cnf(598,negated_conjecture,($false),inference(sr,[status(thm)],[597,584,theory(equality)])).
% cnf(599,negated_conjecture,($false),598,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 208
% # ...of these trivial : 0
% # ...subsumed : 53
% # ...remaining for further processing: 155
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 33
% # Backward-rewritten : 25
% # Generated clauses : 359
% # ...of the previous two non-trivial : 358
% # Contextual simplify-reflections : 125
% # Paramodulations : 338
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 63
% # Positive orientable unit clauses: 3
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 6
% # Non-unit-clauses : 54
% # Current number of unprocessed clauses: 71
% # ...number of literals in the above : 422
% # Clause-clause subsumption calls (NU) : 2188
% # Rec. Clause-clause subsumption calls : 904
% # Unit Clause-clause subsumption calls : 115
% # Rewrite failures with RHS unbound: 0
% # Indexed BW rewrite attempts : 4
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 51 leaves, 1.31+/-0.641 terms/leaf
% # Paramod-from index: 12 leaves, 1.25+/-0.433 terms/leaf
% # Paramod-into index: 42 leaves, 1.21+/-0.513 terms/leaf
% # -------------------------------------------------
% # User time : 0.035 s
% # System time : 0.003 s
% # Total time : 0.038 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.15 CPU 0.22 WC
% FINAL PrfWatch: 0.15 CPU 0.22 WC
% SZS output end Solution for /tmp/SystemOnTPTP13808/SYN550+1.tptp
%
%------------------------------------------------------------------------------