%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n008.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:31 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 : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n008.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 5 16:25:38 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.14/0.46 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))|~(p30(X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~$true))|~(![X1]:((~(r1(X2,X1))|~(((p29(X1)&~(p28(X1)))|(~(p29(X1))&p28(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p28(X2)&~(p27(X2)))|(~(p28(X2))&p27(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p27(X1)&~(p26(X1)))|(~(p27(X1))&p26(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p26(X2)&~(p25(X2)))|(~(p26(X2))&p25(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p25(X1)&~(p24(X1)))|(~(p25(X1))&p24(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p24(X2)&~(p23(X2)))|(~(p24(X2))&p23(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p23(X1)&~(p22(X1)))|(~(p23(X1))&p22(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p22(X2)&~(p21(X2)))|(~(p22(X2))&p21(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p21(X1)&~(p20(X1)))|(~(p21(X1))&p20(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p20(X2)&~(p19(X2)))|(~(p20(X2))&p19(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p19(X1)&~(p18(X1)))|(~(p19(X1))&p18(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p18(X2)&~(p17(X2)))|(~(p18(X2))&p17(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p17(X1)&~(p16(X1)))|(~(p17(X1))&p16(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p16(X2)&~(p15(X2)))|(~(p16(X2))&p15(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p15(X1)&~(p14(X1)))|(~(p15(X1))&p14(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p14(X2)&~(p13(X2)))|(~(p14(X2))&p13(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p13(X1)&~(p12(X1)))|(~(p13(X1))&p12(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p12(X2)&~(p11(X2)))|(~(p12(X2))&p11(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p11(X1)&~(p10(X1)))|(~(p11(X1))&p10(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p10(X2)&~(p9(X2)))|(~(p10(X2))&p9(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p9(X1)&~(p8(X1)))|(~(p9(X1))&p8(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p8(X2)&~(p7(X2)))|(~(p8(X2))&p7(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p7(X1)&~(p6(X1)))|(~(p7(X1))&p6(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p6(X2)&~(p5(X2)))|(~(p6(X2))&p5(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p4(X1)))|(~(p5(X1))&p4(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p4(X2)&~(p3(X2)))|(~(p4(X2))&p3(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p2(X1)))|(~(p3(X1))&p2(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:((~(r1(X1,X2))|p30(X2)))|![X2]:((~(r1(X1,X2))|(~(p28(X2))&~(p29(X2)))|(p29(X2)&p28(X2))|(~(p27(X2))&~(p28(X2)))|(p28(X2)&p27(X2))|(~(p26(X2))&~(p27(X2)))|(p27(X2)&p26(X2))|(~(p25(X2))&~(p26(X2)))|(p26(X2)&p25(X2))|(~(p24(X2))&~(p25(X2)))|(p25(X2)&p24(X2))|(~(p23(X2))&~(p24(X2)))|(p24(X2)&p23(X2))|(~(p22(X2))&~(p23(X2)))|(p23(X2)&p22(X2))|(~(p21(X2))&~(p22(X2)))|(p22(X2)&p21(X2))|(~(p20(X2))&~(p21(X2)))|(p21(X2)&p20(X2))|(~(p19(X2))&~(p20(X2)))|(p20(X2)&p19(X2))|(~(p18(X2))&~(p19(X2)))|(p19(X2)&p18(X2))|(~(p17(X2))&~(p18(X2)))|(p18(X2)&p17(X2))|(~(p16(X2))&~(p17(X2)))|(p17(X2)&p16(X2))|(~(p15(X2))&~(p16(X2)))|(p16(X2)&p15(X2))|(~(p14(X2))&~(p15(X2)))|(p15(X2)&p14(X2))|(~(p13(X2))&~(p14(X2)))|(p14(X2)&p13(X2))|(~(p12(X2))&~(p13(X2)))|(p13(X2)&p12(X2))|(~(p11(X2))&~(p12(X2)))|(p12(X2)&p11(X2))|(~(p10(X2))&~(p11(X2)))|(p11(X2)&p10(X2))|(~(p9(X2))&~(p10(X2)))|(p10(X2)&p9(X2))|(~(p8(X2))&~(p9(X2)))|(p9(X2)&p8(X2))|(~(p7(X2))&~(p8(X2)))|(p8(X2)&p7(X2))|(~(p6(X2))&~(p7(X2)))|(p7(X2)&p6(X2))|(~(p5(X2))&~(p6(X2)))|(p6(X2)&p5(X2))|(~(p4(X2))&~(p5(X2)))|(p5(X2)&p4(X2))|(~(p3(X2))&~(p4(X2)))|(p4(X2)&p3(X2))|(~(p2(X2))&~(p3(X2)))|(p3(X2)&p2(X2))|(~(p1(X2))&~(p2(X2)))|(p2(X2)&p1(X2))))))))))))))), 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, ![X1]:((epred1_1(X1)<=>~((![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~($true)))|~(![X1]:((~r1(X2,X1)|~(((p29(X1)&~p28(X1))|(~p29(X1)&p28(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p28(X2)&~p27(X2))|(~p28(X2)&p27(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p27(X1)&~p26(X1))|(~p27(X1)&p26(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p26(X2)&~p25(X2))|(~p26(X2)&p25(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p25(X1)&~p24(X1))|(~p25(X1)&p24(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p24(X2)&~p23(X2))|(~p24(X2)&p23(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p23(X1)&~p22(X1))|(~p23(X1)&p22(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p22(X2)&~p21(X2))|(~p22(X2)&p21(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p21(X1)&~p20(X1))|(~p21(X1)&p20(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p20(X2)&~p19(X2))|(~p20(X2)&p19(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p19(X1)&~p18(X1))|(~p19(X1)&p18(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p18(X2)&~p17(X2))|(~p18(X2)&p17(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p17(X1)&~p16(X1))|(~p17(X1)&p16(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p16(X2)&~p15(X2))|(~p16(X2)&p15(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p15(X1)&~p14(X1))|(~p15(X1)&p14(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p14(X2)&~p13(X2))|(~p14(X2)&p13(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p13(X1)&~p12(X1))|(~p13(X1)&p12(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p12(X2)&~p11(X2))|(~p12(X2)&p11(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p10(X1))|(~p11(X1)&p10(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p10(X2)&~p9(X2))|(~p10(X2)&p9(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p8(X1))|(~p9(X1)&p8(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p8(X2)&~p7(X2))|(~p8(X2)&p7(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p6(X1))|(~p7(X1)&p6(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p5(X2))|(~p6(X2)&p5(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p4(X1))|(~p5(X1)&p4(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p3(X2))|(~p4(X2)&p3(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p2(X1))|(~p3(X1)&p2(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p1(X2))|(~p2(X2)&p1(X2)))))))|![X2]:((~r1(X1,X2)|p30(X2)))|![X2]:((~r1(X1,X2)|(~p28(X2)&~p29(X2))|(p29(X2)&p28(X2))|(~p27(X2)&~p28(X2))|(p28(X2)&p27(X2))|(~p26(X2)&~p27(X2))|(p27(X2)&p26(X2))|(~p25(X2)&~p26(X2))|(p26(X2)&p25(X2))|(~p24(X2)&~p25(X2))|(p25(X2)&p24(X2))|(~p23(X2)&~p24(X2))|(p24(X2)&p23(X2))|(~p22(X2)&~p23(X2))|(p23(X2)&p22(X2))|(~p21(X2)&~p22(X2))|(p22(X2)&p21(X2))|(~p20(X2)&~p21(X2))|(p21(X2)&p20(X2))|(~p19(X2)&~p20(X2))|(p20(X2)&p19(X2))|(~p18(X2)&~p19(X2))|(p19(X2)&p18(X2))|(~p17(X2)&~p18(X2))|(p18(X2)&p17(X2))|(~p16(X2)&~p17(X2))|(p17(X2)&p16(X2))|(~p15(X2)&~p16(X2))|(p16(X2)&p15(X2))|(~p14(X2)&~p15(X2))|(p15(X2)&p14(X2))|(~p13(X2)&~p14(X2))|(p14(X2)&p13(X2))|(~p12(X2)&~p13(X2))|(p13(X2)&p12(X2))|(~p11(X2)&~p12(X2))|(p12(X2)&p11(X2))|(~p10(X2)&~p11(X2))|(p11(X2)&p10(X2))|(~p9(X2)&~p10(X2))|(p10(X2)&p9(X2))|(~p8(X2)&~p9(X2))|(p9(X2)&p8(X2))|(~p7(X2)&~p8(X2))|(p8(X2)&p7(X2))|(~p6(X2)&~p7(X2))|(p7(X2)&p6(X2))|(~p5(X2)&~p6(X2))|(p6(X2)&p5(X2))|(~p4(X2)&~p5(X2))|(p5(X2)&p4(X2))|(~p3(X2)&~p4(X2))|(p4(X2)&p3(X2))|(~p2(X2)&~p3(X2))|(p3(X2)&p2(X2))|(~p1(X2)&~p2(X2))|(p2(X2)&p1(X2)))))))), introduced(definition)).
% 0.25/0.55 fof(c_0_3, plain, ![X1]:((epred1_1(X1)=>~((![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~($true)))|~(![X1]:((~r1(X2,X1)|~(((p29(X1)&~p28(X1))|(~p29(X1)&p28(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p28(X2)&~p27(X2))|(~p28(X2)&p27(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p27(X1)&~p26(X1))|(~p27(X1)&p26(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p26(X2)&~p25(X2))|(~p26(X2)&p25(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p25(X1)&~p24(X1))|(~p25(X1)&p24(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p24(X2)&~p23(X2))|(~p24(X2)&p23(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p23(X1)&~p22(X1))|(~p23(X1)&p22(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p22(X2)&~p21(X2))|(~p22(X2)&p21(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p21(X1)&~p20(X1))|(~p21(X1)&p20(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p20(X2)&~p19(X2))|(~p20(X2)&p19(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p19(X1)&~p18(X1))|(~p19(X1)&p18(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p18(X2)&~p17(X2))|(~p18(X2)&p17(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p17(X1)&~p16(X1))|(~p17(X1)&p16(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p16(X2)&~p15(X2))|(~p16(X2)&p15(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p15(X1)&~p14(X1))|(~p15(X1)&p14(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p14(X2)&~p13(X2))|(~p14(X2)&p13(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p13(X1)&~p12(X1))|(~p13(X1)&p12(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p12(X2)&~p11(X2))|(~p12(X2)&p11(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p10(X1))|(~p11(X1)&p10(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p10(X2)&~p9(X2))|(~p10(X2)&p9(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p8(X1))|(~p9(X1)&p8(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p8(X2)&~p7(X2))|(~p8(X2)&p7(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p6(X1))|(~p7(X1)&p6(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p5(X2))|(~p6(X2)&p5(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p4(X1))|(~p5(X1)&p4(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p3(X2))|(~p4(X2)&p3(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p2(X1))|(~p3(X1)&p2(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p1(X2))|(~p2(X2)&p1(X2)))))))|![X2]:((~r1(X1,X2)|p30(X2)))|![X2]:((~r1(X1,X2)|(~p28(X2)&~p29(X2))|(p29(X2)&p28(X2))|(~p27(X2)&~p28(X2))|(p28(X2)&p27(X2))|(~p26(X2)&~p27(X2))|(p27(X2)&p26(X2))|(~p25(X2)&~p26(X2))|(p26(X2)&p25(X2))|(~p24(X2)&~p25(X2))|(p25(X2)&p24(X2))|(~p23(X2)&~p24(X2))|(p24(X2)&p23(X2))|(~p22(X2)&~p23(X2))|(p23(X2)&p22(X2))|(~p21(X2)&~p22(X2))|(p22(X2)&p21(X2))|(~p20(X2)&~p21(X2))|(p21(X2)&p20(X2))|(~p19(X2)&~p20(X2))|(p20(X2)&p19(X2))|(~p18(X2)&~p19(X2))|(p19(X2)&p18(X2))|(~p17(X2)&~p18(X2))|(p18(X2)&p17(X2))|(~p16(X2)&~p17(X2))|(p17(X2)&p16(X2))|(~p15(X2)&~p16(X2))|(p16(X2)&p15(X2))|(~p14(X2)&~p15(X2))|(p15(X2)&p14(X2))|(~p13(X2)&~p14(X2))|(p14(X2)&p13(X2))|(~p12(X2)&~p13(X2))|(p13(X2)&p12(X2))|(~p11(X2)&~p12(X2))|(p12(X2)&p11(X2))|(~p10(X2)&~p11(X2))|(p11(X2)&p10(X2))|(~p9(X2)&~p10(X2))|(p10(X2)&p9(X2))|(~p8(X2)&~p9(X2))|(p9(X2)&p8(X2))|(~p7(X2)&~p8(X2))|(p8(X2)&p7(X2))|(~p6(X2)&~p7(X2))|(p7(X2)&p6(X2))|(~p5(X2)&~p6(X2))|(p6(X2)&p5(X2))|(~p4(X2)&~p5(X2))|(p5(X2)&p4(X2))|(~p3(X2)&~p4(X2))|(p4(X2)&p3(X2))|(~p2(X2)&~p3(X2))|(p3(X2)&p2(X2))|(~p1(X2)&~p2(X2))|(p2(X2)&p1(X2)))))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 0.25/0.55 fof(c_0_4, plain, ![X13, X42, X43, X44, X45, X46, X47, X48, X49, X50, X51, X52, X53, X54, X55, X56, X57, X58, X59, X60, X61, X62, X63, X64, X65, X66, X67, X68, X69]:(((((((r1(X13,esk5_1(X13))|~epred1_1(X13))&(((r1(esk5_1(X13),esk6_1(X13))|~epred1_1(X13))&(((r1(esk6_1(X13),esk7_1(X13))|~epred1_1(X13))&(((r1(esk7_1(X13),esk8_1(X13))|~epred1_1(X13))&(((r1(esk8_1(X13),esk9_1(X13))|~epred1_1(X13))&(((r1(esk9_1(X13),esk10_1(X13))|~epred1_1(X13))&(((r1(esk10_1(X13),esk11_1(X13))|~epred1_1(X13))&(((r1(esk11_1(X13),esk12_1(X13))|~epred1_1(X13))&(((r1(esk12_1(X13),esk13_1(X13))|~epred1_1(X13))&(((r1(esk13_1(X13),esk14_1(X13))|~epred1_1(X13))&(((r1(esk14_1(X13),esk15_1(X13))|~epred1_1(X13))&(((r1(esk15_1(X13),esk16_1(X13))|~epred1_1(X13))&(((r1(esk16_1(X13),esk17_1(X13))|~epred1_1(X13))&(((r1(esk17_1(X13),esk18_1(X13))|~epred1_1(X13))&(((r1(esk18_1(X13),esk19_1(X13))|~epred1_1(X13))&(((r1(esk19_1(X13),esk20_1(X13))|~epred1_1(X13))&(((r1(esk20_1(X13),esk21_1(X13))|~epred1_1(X13))&(((r1(esk21_1(X13),esk22_1(X13))|~epred1_1(X13))&(((r1(esk22_1(X13),esk23_1(X13))|~epred1_1(X13))&(((r1(esk23_1(X13),esk24_1(X13))|~epred1_1(X13))&(((r1(esk24_1(X13),esk25_1(X13))|~epred1_1(X13))&(((r1(esk25_1(X13),esk26_1(X13))|~epred1_1(X13))&(((r1(esk26_1(X13),esk27_1(X13))|~epred1_1(X13))&(((r1(esk27_1(X13),esk28_1(X13))|~epred1_1(X13))&(((r1(esk28_1(X13),esk29_1(X13))|~epred1_1(X13))&(((r1(esk29_1(X13),esk30_1(X13))|~epred1_1(X13))&(((r1(esk30_1(X13),esk31_1(X13))|~epred1_1(X13))&((r1(esk31_1(X13),esk32_1(X13))|~epred1_1(X13))&($true|~epred1_1(X13))))&((~p29(X42)|p28(X42)|~r1(esk31_1(X13),X42)|~epred1_1(X13))&(p29(X42)|~p28(X42)|~r1(esk31_1(X13),X42)|~epred1_1(X13)))))&((~p28(X43)|p27(X43)|~r1(esk30_1(X13),X43)|~epred1_1(X13))&(p28(X43)|~p27(X43)|~r1(esk30_1(X13),X43)|~epred1_1(X13)))))&((~p27(X44)|p26(X44)|~r1(esk29_1(X13),X44)|~epred1_1(X13))&(p27(X44)|~p26(X44)|~r1(esk29_1(X13),X44)|~epred1_1(X13)))))&((~p26(X45)|p25(X45)|~r1(esk28_1(X13),X45)|~epred1_1(X13))&(p26(X45)|~p25(X45)|~r1(esk28_1(X13),X45)|~epred1_1(X13)))))&((~p25(X46)|p24(X46)|~r1(esk27_1(X13),X46)|~epred1_1(X13))&(p25(X46)|~p24(X46)|~r1(esk27_1(X13),X46)|~epred1_1(X13)))))&((~p24(X47)|p23(X47)|~r1(esk26_1(X13),X47)|~epred1_1(X13))&(p24(X47)|~p23(X47)|~r1(esk26_1(X13),X47)|~epred1_1(X13)))))&((~p23(X48)|p22(X48)|~r1(esk25_1(X13),X48)|~epred1_1(X13))&(p23(X48)|~p22(X48)|~r1(esk25_1(X13),X48)|~epred1_1(X13)))))&((~p22(X49)|p21(X49)|~r1(esk24_1(X13),X49)|~epred1_1(X13))&(p22(X49)|~p21(X49)|~r1(esk24_1(X13),X49)|~epred1_1(X13)))))&((~p21(X50)|p20(X50)|~r1(esk23_1(X13),X50)|~epred1_1(X13))&(p21(X50)|~p20(X50)|~r1(esk23_1(X13),X50)|~epred1_1(X13)))))&((~p20(X51)|p19(X51)|~r1(esk22_1(X13),X51)|~epred1_1(X13))&(p20(X51)|~p19(X51)|~r1(esk22_1(X13),X51)|~epred1_1(X13)))))&((~p19(X52)|p18(X52)|~r1(esk21_1(X13),X52)|~epred1_1(X13))&(p19(X52)|~p18(X52)|~r1(esk21_1(X13),X52)|~epred1_1(X13)))))&((~p18(X53)|p17(X53)|~r1(esk20_1(X13),X53)|~epred1_1(X13))&(p18(X53)|~p17(X53)|~r1(esk20_1(X13),X53)|~epred1_1(X13)))))&((~p17(X54)|p16(X54)|~r1(esk19_1(X13),X54)|~epred1_1(X13))&(p17(X54)|~p16(X54)|~r1(esk19_1(X13),X54)|~epred1_1(X13)))))&((~p16(X55)|p15(X55)|~r1(esk18_1(X13),X55)|~epred1_1(X13))&(p16(X55)|~p15(X55)|~r1(esk18_1(X13),X55)|~epred1_1(X13)))))&((~p15(X56)|p14(X56)|~r1(esk17_1(X13),X56)|~epred1_1(X13))&(p15(X56)|~p14(X56)|~r1(esk17_1(X13),X56)|~epred1_1(X13)))))&((~p14(X57)|p13(X57)|~r1(esk16_1(X13),X57)|~epred1_1(X13))&(p14(X57)|~p13(X57)|~r1(esk16_1(X13),X57)|~epred1_1(X13)))))&((~p13(X58)|p12(X58)|~r1(esk15_1(X13),X58)|~epred1_1(X13))&(p13(X58)|~p12(X58)|~r1(esk15_1(X13),X58)|~epred1_1(X13)))))&((~p12(X59)|p11(X59)|~r1(esk14_1(X13),X59)|~epred1_1(X13))&(p12(X59)|~p11(X59)|~r1(esk14_1(X13),X59)|~epred1_1(X13)))))&((~p11(X60)|p10(X60)|~r1(esk13_1(X13),X60)|~epred1_1(X13))&(p11(X60)|~p10(X60)|~r1(esk13_1(X13),X60)|~epred1_1(X13)))))&((~p10(X61)|p9(X61)|~r1(esk12_1(X13),X61)|~epred1_1(X13))&(p10(X61)|~p9(X61)|~r1(esk12_1(X13),X61)|~epred1_1(X13)))))&((~p9(X62)|p8(X62)|~r1(esk11_1(X13),X62)|~epred1_1(X13))&(p9(X62)|~p8(X62)|~r1(esk11_1(X13),X62)|~epred1_1(X13)))))&((~p8(X63)|p7(X63)|~r1(esk10_1(X13),X63)|~epred1_1(X13))&(p8(X63)|~p7(X63)|~r1(esk10_1(X13),X63)|~epred1_1(X13)))))&((~p7(X64)|p6(X64)|~r1(esk9_1(X13),X64)|~epred1_1(X13))&(p7(X64)|~p6(X64)|~r1(esk9_1(X13),X64)|~epred1_1(X13)))))&((~p6(X65)|p5(X65)|~r1(esk8_1(X13),X65)|~epred1_1(X13))&(p6(X65)|~p5(X65)|~r1(esk8_1(X13),X65)|~epred1_1(X13)))))&((~p5(X66)|p4(X66)|~r1(esk7_1(X13),X66)|~epred1_1(X13))&(p5(X66)|~p4(X66)|~r1(esk7_1(X13),X66)|~epred1_1(X13)))))&((~p4(X67)|p3(X67)|~r1(esk6_1(X13),X67)|~epred1_1(X13))&(p4(X67)|~p3(X67)|~r1(esk6_1(X13),X67)|~epred1_1(X13)))))&((~p3(X68)|p2(X68)|~r1(esk5_1(X13),X68)|~epred1_1(X13))&(p3(X68)|~p2(X68)|~r1(esk5_1(X13),X68)|~epred1_1(X13))))&((~p2(X69)|p1(X69)|~r1(X13,X69)|~epred1_1(X13))&(p2(X69)|~p1(X69)|~r1(X13,X69)|~epred1_1(X13))))&((r1(X13,esk33_1(X13))|~epred1_1(X13))&(~p30(esk33_1(X13))|~epred1_1(X13))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X13,esk34_1(X13))|~epred1_1(X13))&(p28(esk34_1(X13))|p29(esk34_1(X13))|~epred1_1(X13)))&(~p29(esk34_1(X13))|~p28(esk34_1(X13))|~epred1_1(X13)))&(p27(esk34_1(X13))|p28(esk34_1(X13))|~epred1_1(X13)))&(~p28(esk34_1(X13))|~p27(esk34_1(X13))|~epred1_1(X13)))&(p26(esk34_1(X13))|p27(esk34_1(X13))|~epred1_1(X13)))&(~p27(esk34_1(X13))|~p26(esk34_1(X13))|~epred1_1(X13)))&(p25(esk34_1(X13))|p26(esk34_1(X13))|~epred1_1(X13)))&(~p26(esk34_1(X13))|~p25(esk34_1(X13))|~epred1_1(X13)))&(p24(esk34_1(X13))|p25(esk34_1(X13))|~epred1_1(X13)))&(~p25(esk34_1(X13))|~p24(esk34_1(X13))|~epred1_1(X13)))&(p23(esk34_1(X13))|p24(esk34_1(X13))|~epred1_1(X13)))&(~p24(esk34_1(X13))|~p23(esk34_1(X13))|~epred1_1(X13)))&(p22(esk34_1(X13))|p23(esk34_1(X13))|~epred1_1(X13)))&(~p23(esk34_1(X13))|~p22(esk34_1(X13))|~epred1_1(X13)))&(p21(esk34_1(X13))|p22(esk34_1(X13))|~epred1_1(X13)))&(~p22(esk34_1(X13))|~p21(esk34_1(X13))|~epred1_1(X13)))&(p20(esk34_1(X13))|p21(esk34_1(X13))|~epred1_1(X13)))&(~p21(esk34_1(X13))|~p20(esk34_1(X13))|~epred1_1(X13)))&(p19(esk34_1(X13))|p20(esk34_1(X13))|~epred1_1(X13)))&(~p20(esk34_1(X13))|~p19(esk34_1(X13))|~epred1_1(X13)))&(p18(esk34_1(X13))|p19(esk34_1(X13))|~epred1_1(X13)))&(~p19(esk34_1(X13))|~p18(esk34_1(X13))|~epred1_1(X13)))&(p17(esk34_1(X13))|p18(esk34_1(X13))|~epred1_1(X13)))&(~p18(esk34_1(X13))|~p17(esk34_1(X13))|~epred1_1(X13)))&(p16(esk34_1(X13))|p17(esk34_1(X13))|~epred1_1(X13)))&(~p17(esk34_1(X13))|~p16(esk34_1(X13))|~epred1_1(X13)))&(p15(esk34_1(X13))|p16(esk34_1(X13))|~epred1_1(X13)))&(~p16(esk34_1(X13))|~p15(esk34_1(X13))|~epred1_1(X13)))&(p14(esk34_1(X13))|p15(esk34_1(X13))|~epred1_1(X13)))&(~p15(esk34_1(X13))|~p14(esk34_1(X13))|~epred1_1(X13)))&(p13(esk34_1(X13))|p14(esk34_1(X13))|~epred1_1(X13)))&(~p14(esk34_1(X13))|~p13(esk34_1(X13))|~epred1_1(X13)))&(p12(esk34_1(X13))|p13(esk34_1(X13))|~epred1_1(X13)))&(~p13(esk34_1(X13))|~p12(esk34_1(X13))|~epred1_1(X13)))&(p11(esk34_1(X13))|p12(esk34_1(X13))|~epred1_1(X13)))&(~p12(esk34_1(X13))|~p11(esk34_1(X13))|~epred1_1(X13)))&(p10(esk34_1(X13))|p11(esk34_1(X13))|~epred1_1(X13)))&(~p11(esk34_1(X13))|~p10(esk34_1(X13))|~epred1_1(X13)))&(p9(esk34_1(X13))|p10(esk34_1(X13))|~epred1_1(X13)))&(~p10(esk34_1(X13))|~p9(esk34_1(X13))|~epred1_1(X13)))&(p8(esk34_1(X13))|p9(esk34_1(X13))|~epred1_1(X13)))&(~p9(esk34_1(X13))|~p8(esk34_1(X13))|~epred1_1(X13)))&(p7(esk34_1(X13))|p8(esk34_1(X13))|~epred1_1(X13)))&(~p8(esk34_1(X13))|~p7(esk34_1(X13))|~epred1_1(X13)))&(p6(esk34_1(X13))|p7(esk34_1(X13))|~epred1_1(X13)))&(~p7(esk34_1(X13))|~p6(esk34_1(X13))|~epred1_1(X13)))&(p5(esk34_1(X13))|p6(esk34_1(X13))|~epred1_1(X13)))&(~p6(esk34_1(X13))|~p5(esk34_1(X13))|~epred1_1(X13)))&(p4(esk34_1(X13))|p5(esk34_1(X13))|~epred1_1(X13)))&(~p5(esk34_1(X13))|~p4(esk34_1(X13))|~epred1_1(X13)))&(p3(esk34_1(X13))|p4(esk34_1(X13))|~epred1_1(X13)))&(~p4(esk34_1(X13))|~p3(esk34_1(X13))|~epred1_1(X13)))&(p2(esk34_1(X13))|p3(esk34_1(X13))|~epred1_1(X13)))&(~p3(esk34_1(X13))|~p2(esk34_1(X13))|~epred1_1(X13)))&(p1(esk34_1(X13))|p2(esk34_1(X13))|~epred1_1(X13)))&(~p2(esk34_1(X13))|~p1(esk34_1(X13))|~epred1_1(X13))))), 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_3])])])])])])).
% 0.25/0.55 fof(c_0_5, negated_conjecture, ~(~(?[X1]:(~((![X2]:((~r1(X1,X2)|~p30(X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|epred1_1(X1))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_2])).
% 0.25/0.55 cnf(c_0_6, plain, (p1(X1)|~p2(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 cnf(c_0_7, plain, (r1(X1,esk34_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 cnf(c_0_8, plain, (p1(esk34_1(X1))|p2(esk34_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 fof(c_0_9, negated_conjecture, ![X12]:((((r1(esk1_0,esk2_0)&p30(esk2_0))&(r1(esk2_0,esk3_0)&p1(esk3_0)))&(r1(esk1_0,esk4_0)&(~r1(esk4_0,X12)|epred1_1(X12))))), 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.25/0.55 fof(c_0_10, plain, ![X4]:(r1(X4,X4)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.25/0.55 cnf(c_0_11, plain, (p2(X1)|~p1(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 cnf(c_0_12, plain, (p1(esk34_1(X1))|~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_6, c_0_7]), c_0_8])).
% 0.25/0.55 cnf(c_0_13, negated_conjecture, (epred1_1(X1)|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_14, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.25/0.55 cnf(c_0_15, plain, (~p2(esk34_1(X1))|~p1(esk34_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.55 cnf(c_0_16, plain, (p2(esk34_1(X1))|~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_11, c_0_7]), c_0_12])).
% 0.25/0.55 cnf(c_0_17, negated_conjecture, (epred1_1(esk4_0)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.25/0.55 cnf(c_0_18, plain, (~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_16]), c_0_12])).
% 0.25/0.55 cnf(c_0_19, negated_conjecture, ($false), inference(sr,[status(thm)],[c_0_17, c_0_18]), ['proof']).
% 0.25/0.55 % SZS output end Proof
% 0.25/0.55 % User time : 0.021 s
% 0.25/0.55 % System time : 0.005 s
% 0.25/0.55 % Total time : 0.026 s
% 0.25/0.55 % User time : 0.067 s
% 0.25/0.55 % System time : 0.013 s
% 0.25/0.55 % Total time : 0.079 s
% 0.25/0.55
%------------------------------------------------------------------------------