%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:27 AM UTC 2026
% Result : Theorem 0.69s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n009.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 02:06:06 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.28/0.51 start to proof:theBenchmark.p
% 0.69/0.62 % Version : CSI_E---1.1
% 0.69/0.62 % Problem : theBenchmark.p
% 0.69/0.62 % Proof found!
% 0.69/0.62 % SZS status Theorem for theBenchmark.p
% 0.69/0.62 % SZS output start Proof
% 0.69/0.62 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|p3(X2))))|~(((![X2]:((~(r1(X1,X2))|((((((((((((((((((~(![X1]:((~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1)))))))|~((~(p105(X2))&p104(X2))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1)))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1)))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1)))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1))|~(p105(X1))))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1)|~(p105(X1))))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1))|~(p104(X1))))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1)|~(p104(X1))))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1))|~(p103(X1))))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1)|~(p103(X1))))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1))|~(p102(X1))))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1)|~(p102(X1))))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1))|~(p101(X1))))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1)|~(p101(X1))))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1))|~(p100(X1))))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1)|~(p100(X1))))|~(p1(X2))))|~(p100(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2))))))&~(p101(X1)))&p100(X1))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 0.69/0.62 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 0.69/0.62 fof(transitivity, axiom, ![X1, X2, X3]:(((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', transitivity)).
% 0.69/0.62 fof(c_0_3, plain, ![X2]:((epred1_1(X2)<=>((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p106(X1))&p105(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p6(X1)&~p106(X1))&p105(X1)))))))|~((~p105(X2)&p104(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p105(X1))&p104(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p105(X1))&p104(X1)))))))|~((~p104(X2)&p103(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p104(X1))&p103(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p4(X1)&~p104(X1))&p103(X1)))))))|~((~p103(X2)&p102(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p103(X1))&p102(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p103(X1))&p102(X1)))))))|~((~p102(X2)&p101(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p102(X1))&p101(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p2(X1)&~p102(X1))&p101(X1)))))))|~((~p101(X2)&p100(X2)))))&(((![X1]:((~r1(X2,X1)|~p6(X1)|~p105(X1)))|p6(X2))&(![X1]:((~r1(X2,X1)|p6(X1)|~p105(X1)))|~p6(X2)))|~p105(X2)))&(((![X1]:((~r1(X2,X1)|~p5(X1)|~p104(X1)))|p5(X2))&(![X1]:((~r1(X2,X1)|p5(X1)|~p104(X1)))|~p5(X2)))|~p104(X2)))&(((![X1]:((~r1(X2,X1)|~p4(X1)|~p103(X1)))|p4(X2))&(![X1]:((~r1(X2,X1)|p4(X1)|~p103(X1)))|~p4(X2)))|~p103(X2)))&(((![X1]:((~r1(X2,X1)|~p3(X1)|~p102(X1)))|p3(X2))&(![X1]:((~r1(X2,X1)|p3(X1)|~p102(X1)))|~p3(X2)))|~p102(X2)))&(((![X1]:((~r1(X2,X1)|~p2(X1)|~p101(X1)))|p2(X2))&(![X1]:((~r1(X2,X1)|p2(X1)|~p101(X1)))|~p2(X2)))|~p101(X2)))&(((![X1]:((~r1(X2,X1)|~p1(X1)|~p100(X1)))|p1(X2))&(![X1]:((~r1(X2,X1)|p1(X1)|~p100(X1)))|~p1(X2)))|~p100(X2)))&(p105(X2)|~p106(X2)))&(p104(X2)|~p105(X2)))&(p103(X2)|~p104(X2)))&(p102(X2)|~p103(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2))))), introduced(definition)).
% 0.69/0.62 fof(c_0_4, plain, ![X2]:((epred1_1(X2)=>((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p106(X1))&p105(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p6(X1)&~p106(X1))&p105(X1)))))))|~((~p105(X2)&p104(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p105(X1))&p104(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p105(X1))&p104(X1)))))))|~((~p104(X2)&p103(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p104(X1))&p103(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p4(X1)&~p104(X1))&p103(X1)))))))|~((~p103(X2)&p102(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p103(X1))&p102(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p103(X1))&p102(X1)))))))|~((~p102(X2)&p101(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p102(X1))&p101(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p2(X1)&~p102(X1))&p101(X1)))))))|~((~p101(X2)&p100(X2)))))&(((![X1]:((~r1(X2,X1)|~p6(X1)|~p105(X1)))|p6(X2))&(![X1]:((~r1(X2,X1)|p6(X1)|~p105(X1)))|~p6(X2)))|~p105(X2)))&(((![X1]:((~r1(X2,X1)|~p5(X1)|~p104(X1)))|p5(X2))&(![X1]:((~r1(X2,X1)|p5(X1)|~p104(X1)))|~p5(X2)))|~p104(X2)))&(((![X1]:((~r1(X2,X1)|~p4(X1)|~p103(X1)))|p4(X2))&(![X1]:((~r1(X2,X1)|p4(X1)|~p103(X1)))|~p4(X2)))|~p103(X2)))&(((![X1]:((~r1(X2,X1)|~p3(X1)|~p102(X1)))|p3(X2))&(![X1]:((~r1(X2,X1)|p3(X1)|~p102(X1)))|~p3(X2)))|~p102(X2)))&(((![X1]:((~r1(X2,X1)|~p2(X1)|~p101(X1)))|p2(X2))&(![X1]:((~r1(X2,X1)|p2(X1)|~p101(X1)))|~p2(X2)))|~p101(X2)))&(((![X1]:((~r1(X2,X1)|~p1(X1)|~p100(X1)))|p1(X2))&(![X1]:((~r1(X2,X1)|p1(X1)|~p100(X1)))|~p1(X2)))|~p100(X2)))&(p105(X2)|~p106(X2)))&(p104(X2)|~p105(X2)))&(p103(X2)|~p104(X2)))&(p102(X2)|~p103(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2))))), inference(split_equiv,[status(thm)],[c_0_3])).
% 0.69/0.62 fof(c_0_5, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|p3(X2))))|~(((![X2]:((~r1(X1,X2)|epred1_1(X2)))&~p101(X1))&p100(X1)))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_3])).
% 0.69/0.62 fof(c_0_6, plain, ![X11, X22, X23, X24, X25, X26, X27, X28, X29, X30, X31, X32, X33]:((((((((((((((((((((r1(X11,esk2_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(((~p6(esk2_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(~p106(esk2_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))&(p105(esk2_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))))&((r1(X11,esk3_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(((p6(esk3_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(~p106(esk3_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))&(p105(esk3_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))))&(((r1(X11,esk4_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(((~p5(esk4_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(~p105(esk4_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11)))&(p104(esk4_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))))&((r1(X11,esk5_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(((p5(esk5_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(~p105(esk5_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11)))&(p104(esk5_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))))))&(((r1(X11,esk6_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(((~p4(esk6_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(~p104(esk6_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11)))&(p103(esk6_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))))&((r1(X11,esk7_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(((p4(esk7_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(~p104(esk7_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11)))&(p103(esk7_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))))))&(((r1(X11,esk8_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(((~p3(esk8_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(~p103(esk8_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11)))&(p102(esk8_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))))&((r1(X11,esk9_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(((p3(esk9_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(~p103(esk9_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11)))&(p102(esk9_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))))))&(((r1(X11,esk10_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(((~p2(esk10_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(~p102(esk10_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11)))&(p101(esk10_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))))&((r1(X11,esk11_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(((p2(esk11_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(~p102(esk11_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11)))&(p101(esk11_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))))))&((~r1(X11,X22)|~p6(X22)|~p105(X22)|p6(X11)|~p105(X11)|~epred1_1(X11))&(~r1(X11,X23)|p6(X23)|~p105(X23)|~p6(X11)|~p105(X11)|~epred1_1(X11))))&((~r1(X11,X24)|~p5(X24)|~p104(X24)|p5(X11)|~p104(X11)|~epred1_1(X11))&(~r1(X11,X25)|p5(X25)|~p104(X25)|~p5(X11)|~p104(X11)|~epred1_1(X11))))&((~r1(X11,X26)|~p4(X26)|~p103(X26)|p4(X11)|~p103(X11)|~epred1_1(X11))&(~r1(X11,X27)|p4(X27)|~p103(X27)|~p4(X11)|~p103(X11)|~epred1_1(X11))))&((~r1(X11,X28)|~p3(X28)|~p102(X28)|p3(X11)|~p102(X11)|~epred1_1(X11))&(~r1(X11,X29)|p3(X29)|~p102(X29)|~p3(X11)|~p102(X11)|~epred1_1(X11))))&((~r1(X11,X30)|~p2(X30)|~p101(X30)|p2(X11)|~p101(X11)|~epred1_1(X11))&(~r1(X11,X31)|p2(X31)|~p101(X31)|~p2(X11)|~p101(X11)|~epred1_1(X11))))&((~r1(X11,X32)|~p1(X32)|~p100(X32)|p1(X11)|~p100(X11)|~epred1_1(X11))&(~r1(X11,X33)|p1(X33)|~p100(X33)|~p1(X11)|~p100(X11)|~epred1_1(X11))))&(p105(X11)|~p106(X11)|~epred1_1(X11)))&(p104(X11)|~p105(X11)|~epred1_1(X11)))&(p103(X11)|~p104(X11)|~epred1_1(X11)))&(p102(X11)|~p103(X11)|~epred1_1(X11)))&(p101(X11)|~p102(X11)|~epred1_1(X11)))&(p100(X11)|~p101(X11)|~epred1_1(X11)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])])])).
% 0.69/0.62 fof(c_0_7, negated_conjecture, ![X5, X6]:(((~r1(esk1_0,X5)|p3(X5))&(((~r1(esk1_0,X6)|epred1_1(X6))&~p101(esk1_0))&p100(esk1_0)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])])).
% 0.69/0.62 cnf(c_0_8, plain, (r1(X1,esk11_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.69/0.62 cnf(c_0_9, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.69/0.62 fof(c_0_10, plain, ![X7]:(r1(X7,X7)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.69/0.62 fof(c_0_11, plain, ![X8, X9, X10]:((~r1(X8,X9)|~r1(X9,X10)|r1(X8,X10))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])])])).
% 0.69/0.62 cnf(c_0_12, negated_conjecture, (p101(X1)|r1(X1,esk11_1(X1))|~p100(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_8, c_0_9])).
% 0.69/0.62 cnf(c_0_13, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.69/0.62 cnf(c_0_14, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.69/0.62 cnf(c_0_15, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.69/0.62 cnf(c_0_16, plain, (p101(esk11_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.69/0.62 cnf(c_0_17, plain, (r1(X1,esk8_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.69/0.62 cnf(c_0_18, plain, (r1(X1,X3)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.69/0.62 cnf(c_0_19, negated_conjecture, (r1(esk1_0,esk11_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14])]), c_0_15])).
% 0.69/0.62 cnf(c_0_20, negated_conjecture, (p101(esk11_1(X1))|p101(X1)|~p100(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_16, c_0_9])).
% 0.69/0.62 cnf(c_0_21, negated_conjecture, (p102(X1)|r1(X1,esk8_1(X1))|~p101(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_17, c_0_9])).
% 0.69/0.62 cnf(c_0_22, negated_conjecture, (r1(X1,esk11_1(esk1_0))|~r1(X1,esk1_0)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 0.69/0.62 cnf(c_0_23, negated_conjecture, (p101(esk11_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_13]), c_0_14])]), c_0_15])).
% 0.69/0.62 cnf(c_0_24, plain, (p102(X1)|~p3(esk8_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.69/0.62 cnf(c_0_25, negated_conjecture, (p102(esk11_1(esk1_0))|r1(esk11_1(esk1_0),esk8_1(esk11_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_22]), c_0_23]), c_0_13])])).
% 0.69/0.62 cnf(c_0_26, negated_conjecture, (p102(X1)|~p101(X1)|~p3(esk8_1(X1))|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_24, c_0_9])).
% 0.69/0.62 cnf(c_0_27, negated_conjecture, (p3(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.69/0.62 cnf(c_0_28, negated_conjecture, (p102(esk11_1(esk1_0))|r1(X1,esk8_1(esk11_1(esk1_0)))|~r1(X1,esk11_1(esk1_0))), inference(spm,[status(thm)],[c_0_18, c_0_25])).
% 0.69/0.62 cnf(c_0_29, plain, (p101(X1)|~p102(esk11_1(X1))|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.69/0.62 cnf(c_0_30, negated_conjecture, (p102(X1)|~p101(X1)|~r1(esk1_0,esk8_1(X1))|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.69/0.62 cnf(c_0_31, negated_conjecture, (p102(esk11_1(esk1_0))|r1(esk1_0,esk8_1(esk11_1(esk1_0)))), inference(spm,[status(thm)],[c_0_28, c_0_19])).
% 0.69/0.62 cnf(c_0_32, negated_conjecture, (p101(X1)|~p100(X1)|~p102(esk11_1(X1))|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_29, c_0_9])).
% 0.69/0.62 cnf(c_0_33, negated_conjecture, (p102(esk11_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_23]), c_0_19])])).
% 0.69/0.62 cnf(c_0_34, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_14]), c_0_13])]), c_0_15]), ['proof']).
% 0.69/0.62 % SZS output end Proof
% 0.69/0.62 % User time : 0.027 s
% 0.69/0.62 % System time : 0.006 s
% 0.69/0.62 % Total time : 0.032 s
% 0.69/0.62 % User time : 0.028 s
% 0.69/0.62 % System time : 0.011 s
% 0.69/0.62 % Total time : 0.039 s
% 0.69/0.62
%------------------------------------------------------------------------------