%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n029.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.81s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n029.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 21:14:25 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 0.81/0.59 % Version : CSI_E---1.1
% 0.81/0.59 % Problem : theBenchmark.p
% 0.81/0.59 % Proof found!
% 0.81/0.59 % SZS status Theorem for theBenchmark.p
% 0.81/0.59 % SZS output start Proof
% 0.81/0.59 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|p5(X2))))|~(((![X2]:((~(r1(X1,X2))|(((((((((((((((((((((((((((((((((~(![X1]:((~(r1(X2,X1))|~(((~(p11(X1))&~(p111(X1)))&p110(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p11(X1)&~(p111(X1)))&p110(X1)))))))|~((~(p110(X2))&p109(X2))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p10(X1))&~(p110(X1)))&p109(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p10(X1)&~(p110(X1)))&p109(X1)))))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p9(X1))&~(p109(X1)))&p108(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p9(X1)&~(p109(X1)))&p108(X1)))))))|~((~(p108(X2))&p107(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1)))))))|~((~(p107(X2))&p106(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p7(X1))&~(p107(X1)))&p106(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p7(X1)&~(p107(X1)))&p106(X1)))))))|~((~(p106(X2))&p105(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))|~(p11(X1))|~(p110(X1))))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1)|~(p110(X1))))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1))|~(p109(X1))))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1)|~(p109(X1))))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1))|~(p108(X1))))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1)|~(p108(X1))))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1))|~(p107(X1))))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1)|~(p107(X1))))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1))|~(p106(X1))))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1)|~(p106(X1))))|~(p7(X2))))|~(p106(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))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(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.81/0.59 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 0.81/0.59 fof(transitivity, axiom, ![X1, X2, X3]:(((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', transitivity)).
% 0.81/0.59 fof(c_0_3, plain, ![X2]:((epred1_1(X2)<=>(((((((((((((((((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p111(X1))&p110(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p111(X1))&p110(X1)))))))|~((~p110(X2)&p109(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p110(X1))&p109(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p10(X1)&~p110(X1))&p109(X1)))))))|~((~p109(X2)&p108(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p109(X1))&p108(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p109(X1))&p108(X1)))))))|~((~p108(X2)&p107(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p8(X1)&~p108(X1))&p107(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p8(X1)&~p108(X1))&p107(X1)))))))|~((~p107(X2)&p106(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p107(X1))&p106(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p107(X1))&p106(X1)))))))|~((~p106(X2)&p105(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)|~p11(X1)|~p110(X1)))|p11(X2))&(![X1]:((~r1(X2,X1)|p11(X1)|~p110(X1)))|~p11(X2)))|~p110(X2)))&(((![X1]:((~r1(X2,X1)|~p10(X1)|~p109(X1)))|p10(X2))&(![X1]:((~r1(X2,X1)|p10(X1)|~p109(X1)))|~p10(X2)))|~p109(X2)))&(((![X1]:((~r1(X2,X1)|~p9(X1)|~p108(X1)))|p9(X2))&(![X1]:((~r1(X2,X1)|p9(X1)|~p108(X1)))|~p9(X2)))|~p108(X2)))&(((![X1]:((~r1(X2,X1)|~p8(X1)|~p107(X1)))|p8(X2))&(![X1]:((~r1(X2,X1)|p8(X1)|~p107(X1)))|~p8(X2)))|~p107(X2)))&(((![X1]:((~r1(X2,X1)|~p7(X1)|~p106(X1)))|p7(X2))&(![X1]:((~r1(X2,X1)|p7(X1)|~p106(X1)))|~p7(X2)))|~p106(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)))&(p110(X2)|~p111(X2)))&(p109(X2)|~p110(X2)))&(p108(X2)|~p109(X2)))&(p107(X2)|~p108(X2)))&(p106(X2)|~p107(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.81/0.59 fof(c_0_4, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|p5(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.81/0.59 fof(c_0_5, plain, ![X2]:((epred1_1(X2)=>(((((((((((((((((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p111(X1))&p110(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p111(X1))&p110(X1)))))))|~((~p110(X2)&p109(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p110(X1))&p109(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p10(X1)&~p110(X1))&p109(X1)))))))|~((~p109(X2)&p108(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p109(X1))&p108(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p109(X1))&p108(X1)))))))|~((~p108(X2)&p107(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p8(X1)&~p108(X1))&p107(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p8(X1)&~p108(X1))&p107(X1)))))))|~((~p107(X2)&p106(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p107(X1))&p106(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p107(X1))&p106(X1)))))))|~((~p106(X2)&p105(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)|~p11(X1)|~p110(X1)))|p11(X2))&(![X1]:((~r1(X2,X1)|p11(X1)|~p110(X1)))|~p11(X2)))|~p110(X2)))&(((![X1]:((~r1(X2,X1)|~p10(X1)|~p109(X1)))|p10(X2))&(![X1]:((~r1(X2,X1)|p10(X1)|~p109(X1)))|~p10(X2)))|~p109(X2)))&(((![X1]:((~r1(X2,X1)|~p9(X1)|~p108(X1)))|p9(X2))&(![X1]:((~r1(X2,X1)|p9(X1)|~p108(X1)))|~p9(X2)))|~p108(X2)))&(((![X1]:((~r1(X2,X1)|~p8(X1)|~p107(X1)))|p8(X2))&(![X1]:((~r1(X2,X1)|p8(X1)|~p107(X1)))|~p8(X2)))|~p107(X2)))&(((![X1]:((~r1(X2,X1)|~p7(X1)|~p106(X1)))|p7(X2))&(![X1]:((~r1(X2,X1)|p7(X1)|~p106(X1)))|~p7(X2)))|~p106(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)))&(p110(X2)|~p111(X2)))&(p109(X2)|~p110(X2)))&(p108(X2)|~p109(X2)))&(p107(X2)|~p108(X2)))&(p106(X2)|~p107(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.81/0.59 fof(c_0_6, negated_conjecture, ![X5, X6]:(((~r1(esk1_0,X5)|p5(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_4])])])])])).
% 0.81/0.59 fof(c_0_7, plain, ![X7]:(r1(X7,X7)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.81/0.59 fof(c_0_8, plain, ![X11, X32, X33, X34, X35, X36, X37, X38, X39, X40, X41, X42, X43, X44, X45, X46, X47, X48, X49, X50, X51, X52, X53]:(((((((((((((((((((((((((((((((((((r1(X11,esk2_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(((~p11(esk2_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(~p111(esk2_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11)))&(p110(esk2_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))))&((r1(X11,esk3_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(((p11(esk3_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(~p111(esk3_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11)))&(p110(esk3_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11)))))&(((r1(X11,esk4_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(((~p10(esk4_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(~p110(esk4_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11)))&(p109(esk4_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))))&((r1(X11,esk5_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(((p10(esk5_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(~p110(esk5_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11)))&(p109(esk5_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))))))&(((r1(X11,esk6_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(((~p9(esk6_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(~p109(esk6_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11)))&(p108(esk6_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))))&((r1(X11,esk7_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(((p9(esk7_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(~p109(esk7_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11)))&(p108(esk7_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))))))&(((r1(X11,esk8_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(((~p8(esk8_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(~p108(esk8_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11)))&(p107(esk8_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))))&((r1(X11,esk9_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(((p8(esk9_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(~p108(esk9_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11)))&(p107(esk9_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))))))&(((r1(X11,esk10_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(((~p7(esk10_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(~p107(esk10_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11)))&(p106(esk10_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))))&((r1(X11,esk11_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(((p7(esk11_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(~p107(esk11_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11)))&(p106(esk11_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))))))&(((r1(X11,esk12_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(((~p6(esk12_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(~p106(esk12_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))&(p105(esk12_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))))&((r1(X11,esk13_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(((p6(esk13_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(~p106(esk13_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))&(p105(esk13_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))))))&(((r1(X11,esk14_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(((~p5(esk14_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(~p105(esk14_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11)))&(p104(esk14_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))))&((r1(X11,esk15_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(((p5(esk15_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(~p105(esk15_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11)))&(p104(esk15_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))))))&(((r1(X11,esk16_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(((~p4(esk16_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(~p104(esk16_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11)))&(p103(esk16_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))))&((r1(X11,esk17_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(((p4(esk17_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(~p104(esk17_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11)))&(p103(esk17_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))))))&(((r1(X11,esk18_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(((~p3(esk18_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(~p103(esk18_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11)))&(p102(esk18_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))))&((r1(X11,esk19_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(((p3(esk19_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(~p103(esk19_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11)))&(p102(esk19_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))))))&(((r1(X11,esk20_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(((~p2(esk20_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(~p102(esk20_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11)))&(p101(esk20_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))))&((r1(X11,esk21_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(((p2(esk21_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(~p102(esk21_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11)))&(p101(esk21_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))))))&((~r1(X11,X32)|~p11(X32)|~p110(X32)|p11(X11)|~p110(X11)|~epred1_1(X11))&(~r1(X11,X33)|p11(X33)|~p110(X33)|~p11(X11)|~p110(X11)|~epred1_1(X11))))&((~r1(X11,X34)|~p10(X34)|~p109(X34)|p10(X11)|~p109(X11)|~epred1_1(X11))&(~r1(X11,X35)|p10(X35)|~p109(X35)|~p10(X11)|~p109(X11)|~epred1_1(X11))))&((~r1(X11,X36)|~p9(X36)|~p108(X36)|p9(X11)|~p108(X11)|~epred1_1(X11))&(~r1(X11,X37)|p9(X37)|~p108(X37)|~p9(X11)|~p108(X11)|~epred1_1(X11))))&((~r1(X11,X38)|~p8(X38)|~p107(X38)|p8(X11)|~p107(X11)|~epred1_1(X11))&(~r1(X11,X39)|p8(X39)|~p107(X39)|~p8(X11)|~p107(X11)|~epred1_1(X11))))&((~r1(X11,X40)|~p7(X40)|~p106(X40)|p7(X11)|~p106(X11)|~epred1_1(X11))&(~r1(X11,X41)|p7(X41)|~p106(X41)|~p7(X11)|~p106(X11)|~epred1_1(X11))))&((~r1(X11,X42)|~p6(X42)|~p105(X42)|p6(X11)|~p105(X11)|~epred1_1(X11))&(~r1(X11,X43)|p6(X43)|~p105(X43)|~p6(X11)|~p105(X11)|~epred1_1(X11))))&((~r1(X11,X44)|~p5(X44)|~p104(X44)|p5(X11)|~p104(X11)|~epred1_1(X11))&(~r1(X11,X45)|p5(X45)|~p104(X45)|~p5(X11)|~p104(X11)|~epred1_1(X11))))&((~r1(X11,X46)|~p4(X46)|~p103(X46)|p4(X11)|~p103(X11)|~epred1_1(X11))&(~r1(X11,X47)|p4(X47)|~p103(X47)|~p4(X11)|~p103(X11)|~epred1_1(X11))))&((~r1(X11,X48)|~p3(X48)|~p102(X48)|p3(X11)|~p102(X11)|~epred1_1(X11))&(~r1(X11,X49)|p3(X49)|~p102(X49)|~p3(X11)|~p102(X11)|~epred1_1(X11))))&((~r1(X11,X50)|~p2(X50)|~p101(X50)|p2(X11)|~p101(X11)|~epred1_1(X11))&(~r1(X11,X51)|p2(X51)|~p101(X51)|~p2(X11)|~p101(X11)|~epred1_1(X11))))&((~r1(X11,X52)|~p1(X52)|~p100(X52)|p1(X11)|~p100(X11)|~epred1_1(X11))&(~r1(X11,X53)|p1(X53)|~p100(X53)|~p1(X11)|~p100(X11)|~epred1_1(X11))))&(p110(X11)|~p111(X11)|~epred1_1(X11)))&(p109(X11)|~p110(X11)|~epred1_1(X11)))&(p108(X11)|~p109(X11)|~epred1_1(X11)))&(p107(X11)|~p108(X11)|~epred1_1(X11)))&(p106(X11)|~p107(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_5])])])])])])).
% 0.81/0.59 cnf(c_0_9, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.81/0.59 cnf(c_0_10, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.81/0.59 cnf(c_0_11, plain, (r1(X1,esk21_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_12, negated_conjecture, (epred1_1(esk1_0)), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 0.81/0.59 cnf(c_0_13, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.81/0.59 cnf(c_0_14, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.81/0.59 cnf(c_0_15, negated_conjecture, (r1(esk1_0,esk21_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_11, c_0_12]), c_0_13])]), c_0_14])).
% 0.81/0.59 cnf(c_0_16, plain, (p101(esk21_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_17, plain, (p101(X1)|~p102(esk21_1(X1))|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 fof(c_0_18, 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.81/0.59 cnf(c_0_19, plain, (r1(X1,esk19_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_20, negated_conjecture, (epred1_1(esk21_1(esk1_0))), inference(spm,[status(thm)],[c_0_9, c_0_15])).
% 0.81/0.59 cnf(c_0_21, negated_conjecture, (p101(esk21_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_12]), c_0_13])]), c_0_14])).
% 0.81/0.59 cnf(c_0_22, negated_conjecture, (~p102(esk21_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_13]), c_0_12])]), c_0_14])).
% 0.81/0.59 cnf(c_0_23, plain, (r1(X1,X3)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.81/0.59 cnf(c_0_24, negated_conjecture, (r1(esk21_1(esk1_0),esk19_1(esk21_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_21])]), c_0_22])).
% 0.81/0.59 cnf(c_0_25, plain, (p102(X1)|~p103(esk19_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_26, negated_conjecture, (r1(X1,esk19_1(esk21_1(esk1_0)))|~r1(X1,esk21_1(esk1_0))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.81/0.59 cnf(c_0_27, plain, (p102(esk19_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_28, negated_conjecture, (~epred1_1(esk21_1(esk1_0))|~p103(esk19_1(esk21_1(esk1_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_21]), c_0_22])).
% 0.81/0.59 cnf(c_0_29, plain, (r1(X1,esk16_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_30, negated_conjecture, (epred1_1(esk19_1(esk21_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_9, c_0_26]), c_0_15])])).
% 0.81/0.59 cnf(c_0_31, plain, (p102(esk19_1(esk21_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_20]), c_0_21])]), c_0_22])).
% 0.81/0.59 cnf(c_0_32, negated_conjecture, (~p103(esk19_1(esk21_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_20])])).
% 0.81/0.59 cnf(c_0_33, negated_conjecture, (r1(esk19_1(esk21_1(esk1_0)),esk16_1(esk19_1(esk21_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_31])]), c_0_32])).
% 0.81/0.59 cnf(c_0_34, plain, (p103(X1)|~p104(esk16_1(X1))|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_35, negated_conjecture, (r1(X1,esk16_1(esk19_1(esk21_1(esk1_0))))|~r1(X1,esk19_1(esk21_1(esk1_0)))), inference(spm,[status(thm)],[c_0_23, c_0_33])).
% 0.81/0.59 cnf(c_0_36, plain, (p104(X1)|~p5(esk14_1(X1))|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_37, negated_conjecture, (p5(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.81/0.59 cnf(c_0_38, plain, (p103(esk16_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_39, plain, (~epred1_1(esk19_1(esk21_1(esk1_0)))|~p104(esk16_1(esk19_1(esk21_1(esk1_0))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_31]), c_0_32])).
% 0.81/0.59 cnf(c_0_40, negated_conjecture, (epred1_1(esk16_1(esk19_1(esk21_1(esk1_0))))|~r1(esk1_0,esk19_1(esk21_1(esk1_0)))), inference(spm,[status(thm)],[c_0_9, c_0_35])).
% 0.81/0.59 cnf(c_0_41, negated_conjecture, (p104(X1)|~epred1_1(X1)|~p103(X1)|~r1(esk1_0,esk14_1(X1))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.81/0.59 cnf(c_0_42, negated_conjecture, (p103(esk16_1(esk19_1(esk21_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_30]), c_0_31])]), c_0_32])).
% 0.81/0.59 cnf(c_0_43, plain, (~p104(esk16_1(esk19_1(esk21_1(esk1_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_30])])).
% 0.81/0.59 cnf(c_0_44, plain, (r1(X1,esk14_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.81/0.59 cnf(c_0_45, negated_conjecture, (epred1_1(esk16_1(esk19_1(esk21_1(esk1_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_26]), c_0_15])])).
% 0.81/0.59 cnf(c_0_46, negated_conjecture, (~epred1_1(esk16_1(esk19_1(esk21_1(esk1_0))))|~r1(esk1_0,esk14_1(esk16_1(esk19_1(esk21_1(esk1_0)))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43])).
% 0.81/0.59 cnf(c_0_47, plain, (r1(esk16_1(esk19_1(esk21_1(esk1_0))),esk14_1(esk16_1(esk19_1(esk21_1(esk1_0)))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_42])]), c_0_43])).
% 0.81/0.59 cnf(c_0_48, negated_conjecture, (~r1(esk1_0,esk14_1(esk16_1(esk19_1(esk21_1(esk1_0)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_45])])).
% 0.81/0.59 cnf(c_0_49, plain, (r1(X1,esk14_1(esk16_1(esk19_1(esk21_1(esk1_0)))))|~r1(X1,esk16_1(esk19_1(esk21_1(esk1_0))))), inference(spm,[status(thm)],[c_0_23, c_0_47])).
% 0.81/0.59 cnf(c_0_50, negated_conjecture, (r1(X1,esk16_1(esk19_1(esk21_1(esk1_0))))|~r1(X2,esk19_1(esk21_1(esk1_0)))|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_23, c_0_35])).
% 0.81/0.59 cnf(c_0_51, negated_conjecture, (~r1(esk1_0,esk16_1(esk19_1(esk21_1(esk1_0))))), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 0.81/0.59 cnf(c_0_52, negated_conjecture, (r1(X1,esk16_1(esk19_1(esk21_1(esk1_0))))|~r1(X1,esk21_1(esk1_0))), inference(spm,[status(thm)],[c_0_50, c_0_24])).
% 0.81/0.59 cnf(c_0_53, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_15])]), ['proof']).
% 0.81/0.59 % SZS output end Proof
% 0.81/0.59 % User time : 0.066 s
% 0.81/0.59 % System time : 0.010 s
% 0.81/0.59 % Total time : 0.076 s
% 0.81/0.59 % User time : 0.067 s
% 0.81/0.59 % System time : 0.012 s
% 0.81/0.59 % Total time : 0.079 s
% 0.81/0.59
%------------------------------------------------------------------------------