%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n010.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:21 AM UTC 2026
% Result : Theorem 0.25s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL656+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.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 17:25:39 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.25/0.47 start to proof:theBenchmark.p
% 0.25/0.55 % Version : CSI_E---1.1
% 0.25/0.55 % Problem : theBenchmark.p
% 0.25/0.55 % Proof found!
% 0.25/0.55 % SZS status Theorem for theBenchmark.p
% 0.25/0.55 % SZS output start Proof
% 0.25/0.55 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2))))))))))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![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.25/0.55 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 0.25/0.55 fof(c_0_2, 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.25/0.55 fof(c_0_3, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2))))))))))))|~(((![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![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_2])).
% 0.25/0.55 fof(c_0_4, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X10, X11, X12, X13]:(((~r1(esk1_0,X4)|(~r1(X4,X5)|(~r1(X5,X6)|(~r1(X6,X7)|(~r1(X7,X8)|p3(X8))))))&(((~r1(esk1_0,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|epred1_1(X13))))))&~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_3])])])])])).
% 0.25/0.55 fof(c_0_5, plain, ![X14]:(r1(X14,X14)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.25/0.55 cnf(c_0_6, negated_conjecture, (epred1_1(X5)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 cnf(c_0_7, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.25/0.55 cnf(c_0_8, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 0.25/0.55 fof(c_0_9, 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_2])).
% 0.25/0.55 cnf(c_0_10, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_8, c_0_7])).
% 0.25/0.55 cnf(c_0_11, negated_conjecture, (p3(X5)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 fof(c_0_12, plain, ![X15, X26, X27, X28, X29, X30, X31, X32, X33, X34, X35, X36, X37]:((((((((((((((((((((r1(X15,esk2_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15))&(((~p6(esk2_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15))&(~p106(esk2_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15)))&(p105(esk2_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15))))&((r1(X15,esk3_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15))&(((p6(esk3_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15))&(~p106(esk3_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15)))&(p105(esk3_1(X15))|(p105(X15)|~p104(X15))|~epred1_1(X15)))))&(((r1(X15,esk4_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15))&(((~p5(esk4_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15))&(~p105(esk4_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15)))&(p104(esk4_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15))))&((r1(X15,esk5_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15))&(((p5(esk5_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15))&(~p105(esk5_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15)))&(p104(esk5_1(X15))|(p104(X15)|~p103(X15))|~epred1_1(X15))))))&(((r1(X15,esk6_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15))&(((~p4(esk6_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15))&(~p104(esk6_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15)))&(p103(esk6_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15))))&((r1(X15,esk7_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15))&(((p4(esk7_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15))&(~p104(esk7_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15)))&(p103(esk7_1(X15))|(p103(X15)|~p102(X15))|~epred1_1(X15))))))&(((r1(X15,esk8_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15))&(((~p3(esk8_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15))&(~p103(esk8_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15)))&(p102(esk8_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15))))&((r1(X15,esk9_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15))&(((p3(esk9_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15))&(~p103(esk9_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15)))&(p102(esk9_1(X15))|(p102(X15)|~p101(X15))|~epred1_1(X15))))))&(((r1(X15,esk10_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15))&(((~p2(esk10_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15))&(~p102(esk10_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15)))&(p101(esk10_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15))))&((r1(X15,esk11_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15))&(((p2(esk11_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15))&(~p102(esk11_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15)))&(p101(esk11_1(X15))|(p101(X15)|~p100(X15))|~epred1_1(X15))))))&((~r1(X15,X26)|~p6(X26)|~p105(X26)|p6(X15)|~p105(X15)|~epred1_1(X15))&(~r1(X15,X27)|p6(X27)|~p105(X27)|~p6(X15)|~p105(X15)|~epred1_1(X15))))&((~r1(X15,X28)|~p5(X28)|~p104(X28)|p5(X15)|~p104(X15)|~epred1_1(X15))&(~r1(X15,X29)|p5(X29)|~p104(X29)|~p5(X15)|~p104(X15)|~epred1_1(X15))))&((~r1(X15,X30)|~p4(X30)|~p103(X30)|p4(X15)|~p103(X15)|~epred1_1(X15))&(~r1(X15,X31)|p4(X31)|~p103(X31)|~p4(X15)|~p103(X15)|~epred1_1(X15))))&((~r1(X15,X32)|~p3(X32)|~p102(X32)|p3(X15)|~p102(X15)|~epred1_1(X15))&(~r1(X15,X33)|p3(X33)|~p102(X33)|~p3(X15)|~p102(X15)|~epred1_1(X15))))&((~r1(X15,X34)|~p2(X34)|~p101(X34)|p2(X15)|~p101(X15)|~epred1_1(X15))&(~r1(X15,X35)|p2(X35)|~p101(X35)|~p2(X15)|~p101(X15)|~epred1_1(X15))))&((~r1(X15,X36)|~p1(X36)|~p100(X36)|p1(X15)|~p100(X15)|~epred1_1(X15))&(~r1(X15,X37)|p1(X37)|~p100(X37)|~p1(X15)|~p100(X15)|~epred1_1(X15))))&(p105(X15)|~p106(X15)|~epred1_1(X15)))&(p104(X15)|~p105(X15)|~epred1_1(X15)))&(p103(X15)|~p104(X15)|~epred1_1(X15)))&(p102(X15)|~p103(X15)|~epred1_1(X15)))&(p101(X15)|~p102(X15)|~epred1_1(X15)))&(p100(X15)|~p101(X15)|~epred1_1(X15)))), 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_9])])])])])])).
% 0.25/0.56 cnf(c_0_13, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_7])).
% 0.25/0.56 cnf(c_0_14, negated_conjecture, (p3(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_11, c_0_7])).
% 0.25/0.56 cnf(c_0_15, plain, (r1(X1,esk11_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.25/0.56 cnf(c_0_16, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_13, c_0_7])).
% 0.25/0.56 cnf(c_0_17, plain, (p101(esk11_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.25/0.56 cnf(c_0_18, negated_conjecture, (p3(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_14, c_0_7])).
% 0.25/0.56 cnf(c_0_19, plain, (p101(X1)|r1(X1,esk11_1(X1))|~p100(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 0.25/0.56 cnf(c_0_20, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.56 cnf(c_0_21, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.56 cnf(c_0_22, plain, (r1(X1,esk8_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.25/0.56 cnf(c_0_23, plain, (p101(esk11_1(X1))|p101(X1)|~p100(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_17, c_0_16])).
% 0.25/0.56 cnf(c_0_24, negated_conjecture, (p3(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_18, c_0_7])).
% 0.25/0.56 cnf(c_0_25, plain, (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_19, c_0_7]), c_0_20])]), c_0_21])).
% 0.25/0.56 cnf(c_0_26, plain, (p102(X1)|r1(X1,esk8_1(X1))|~p101(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_22, c_0_16])).
% 0.25/0.56 cnf(c_0_27, plain, (p101(esk11_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_7]), c_0_20])]), c_0_21])).
% 0.25/0.56 cnf(c_0_28, plain, (p102(X1)|~p3(esk8_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.25/0.56 cnf(c_0_29, negated_conjecture, (p3(X1)|~r1(esk11_1(esk1_0),X1)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.25/0.56 cnf(c_0_30, plain, (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(spm,[status(thm)],[c_0_26, c_0_25]), c_0_27])])).
% 0.25/0.56 cnf(c_0_31, plain, (p101(X1)|~p102(esk11_1(X1))|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.25/0.56 cnf(c_0_32, plain, (p102(X1)|~p101(X1)|~p3(esk8_1(X1))|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_28, c_0_16])).
% 0.25/0.56 cnf(c_0_33, negated_conjecture, (p102(esk11_1(esk1_0))|p3(esk8_1(esk11_1(esk1_0)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 0.25/0.56 cnf(c_0_34, plain, (p101(X1)|~p100(X1)|~p102(esk11_1(X1))|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_31, c_0_16])).
% 0.25/0.56 cnf(c_0_35, plain, (p102(esk11_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_27]), c_0_25])])).
% 0.25/0.56 cnf(c_0_36, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_20]), c_0_7])]), c_0_21]), ['proof']).
% 0.25/0.56 % SZS output end Proof
% 0.25/0.56 % User time : 0.028 s
% 0.25/0.56 % System time : 0.001 s
% 0.25/0.56 % Total time : 0.029 s
% 0.25/0.56 % User time : 0.028 s
% 0.25/0.56 % System time : 0.006 s
% 0.25/0.56 % Total time : 0.034 s
% 0.25/0.56
%------------------------------------------------------------------------------