%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n013.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.57s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n013.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 : Fri Sep 4 19:16:19 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 0.57/0.57 % Version : CSI_E---1.1
% 0.57/0.57 % Problem : theBenchmark.p
% 0.57/0.57 % Proof found!
% 0.57/0.57 % SZS status Theorem for theBenchmark.p
% 0.57/0.57 % SZS output start Proof
% 0.57/0.57 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 0.57/0.57 fof(main, conjecture, ~(?[X1]:(~((![X2]:((~(r1(X1,X2))|~(p45(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))|![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))|~$true))|~(![X2]:((~(r1(X1,X2))|~(((p44(X2)&~(p43(X2)))|(~(p44(X2))&p43(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p43(X1)&~(p42(X1)))|(~(p43(X1))&p42(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p42(X2)&~(p41(X2)))|(~(p42(X2))&p41(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p41(X1)&~(p40(X1)))|(~(p41(X1))&p40(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p40(X2)&~(p39(X2)))|(~(p40(X2))&p39(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p39(X1)&~(p38(X1)))|(~(p39(X1))&p38(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p38(X2)&~(p37(X2)))|(~(p38(X2))&p37(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p37(X1)&~(p36(X1)))|(~(p37(X1))&p36(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p36(X2)&~(p35(X2)))|(~(p36(X2))&p35(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p35(X1)&~(p34(X1)))|(~(p35(X1))&p34(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p34(X2)&~(p33(X2)))|(~(p34(X2))&p33(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p33(X1)&~(p32(X1)))|(~(p33(X1))&p32(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p32(X2)&~(p31(X2)))|(~(p32(X2))&p31(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p31(X1)&~(p30(X1)))|(~(p31(X1))&p30(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p30(X2)&~(p29(X2)))|(~(p30(X2))&p29(X2)))))))))|~(![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))|p45(X2)))|![X2]:((~(r1(X1,X2))|(~(p43(X2))&~(p44(X2)))|(p44(X2)&p43(X2))|(~(p42(X2))&~(p43(X2)))|(p43(X2)&p42(X2))|(~(p41(X2))&~(p42(X2)))|(p42(X2)&p41(X2))|(~(p40(X2))&~(p41(X2)))|(p41(X2)&p40(X2))|(~(p39(X2))&~(p40(X2)))|(p40(X2)&p39(X2))|(~(p38(X2))&~(p39(X2)))|(p39(X2)&p38(X2))|(~(p37(X2))&~(p38(X2)))|(p38(X2)&p37(X2))|(~(p36(X2))&~(p37(X2)))|(p37(X2)&p36(X2))|(~(p35(X2))&~(p36(X2)))|(p36(X2)&p35(X2))|(~(p34(X2))&~(p35(X2)))|(p35(X2)&p34(X2))|(~(p33(X2))&~(p34(X2)))|(p34(X2)&p33(X2))|(~(p32(X2))&~(p33(X2)))|(p33(X2)&p32(X2))|(~(p31(X2))&~(p32(X2)))|(p32(X2)&p31(X2))|(~(p30(X2))&~(p31(X2)))|(p31(X2)&p30(X2))|(~(p29(X2))&~(p30(X2)))|(p30(X2)&p29(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.57/0.57 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)|![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)|~($true)))|~(![X2]:((~r1(X1,X2)|~(((p44(X2)&~p43(X2))|(~p44(X2)&p43(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p43(X1)&~p42(X1))|(~p43(X1)&p42(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p42(X2)&~p41(X2))|(~p42(X2)&p41(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p41(X1)&~p40(X1))|(~p41(X1)&p40(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p40(X2)&~p39(X2))|(~p40(X2)&p39(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p39(X1)&~p38(X1))|(~p39(X1)&p38(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p38(X2)&~p37(X2))|(~p38(X2)&p37(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p37(X1)&~p36(X1))|(~p37(X1)&p36(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p36(X2)&~p35(X2))|(~p36(X2)&p35(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p35(X1)&~p34(X1))|(~p35(X1)&p34(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p34(X2)&~p33(X2))|(~p34(X2)&p33(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p33(X1)&~p32(X1))|(~p33(X1)&p32(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p32(X2)&~p31(X2))|(~p32(X2)&p31(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p31(X1)&~p30(X1))|(~p31(X1)&p30(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p30(X2)&~p29(X2))|(~p30(X2)&p29(X2)))))))))|~(![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)|p45(X2)))|![X2]:((~r1(X1,X2)|(~p43(X2)&~p44(X2))|(p44(X2)&p43(X2))|(~p42(X2)&~p43(X2))|(p43(X2)&p42(X2))|(~p41(X2)&~p42(X2))|(p42(X2)&p41(X2))|(~p40(X2)&~p41(X2))|(p41(X2)&p40(X2))|(~p39(X2)&~p40(X2))|(p40(X2)&p39(X2))|(~p38(X2)&~p39(X2))|(p39(X2)&p38(X2))|(~p37(X2)&~p38(X2))|(p38(X2)&p37(X2))|(~p36(X2)&~p37(X2))|(p37(X2)&p36(X2))|(~p35(X2)&~p36(X2))|(p36(X2)&p35(X2))|(~p34(X2)&~p35(X2))|(p35(X2)&p34(X2))|(~p33(X2)&~p34(X2))|(p34(X2)&p33(X2))|(~p32(X2)&~p33(X2))|(p33(X2)&p32(X2))|(~p31(X2)&~p32(X2))|(p32(X2)&p31(X2))|(~p30(X2)&~p31(X2))|(p31(X2)&p30(X2))|(~p29(X2)&~p30(X2))|(p30(X2)&p29(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.57/0.57 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)|![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)|~($true)))|~(![X2]:((~r1(X1,X2)|~(((p44(X2)&~p43(X2))|(~p44(X2)&p43(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p43(X1)&~p42(X1))|(~p43(X1)&p42(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p42(X2)&~p41(X2))|(~p42(X2)&p41(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p41(X1)&~p40(X1))|(~p41(X1)&p40(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p40(X2)&~p39(X2))|(~p40(X2)&p39(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p39(X1)&~p38(X1))|(~p39(X1)&p38(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p38(X2)&~p37(X2))|(~p38(X2)&p37(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p37(X1)&~p36(X1))|(~p37(X1)&p36(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p36(X2)&~p35(X2))|(~p36(X2)&p35(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p35(X1)&~p34(X1))|(~p35(X1)&p34(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p34(X2)&~p33(X2))|(~p34(X2)&p33(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p33(X1)&~p32(X1))|(~p33(X1)&p32(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p32(X2)&~p31(X2))|(~p32(X2)&p31(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p31(X1)&~p30(X1))|(~p31(X1)&p30(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p30(X2)&~p29(X2))|(~p30(X2)&p29(X2)))))))))|~(![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)|p45(X2)))|![X2]:((~r1(X1,X2)|(~p43(X2)&~p44(X2))|(p44(X2)&p43(X2))|(~p42(X2)&~p43(X2))|(p43(X2)&p42(X2))|(~p41(X2)&~p42(X2))|(p42(X2)&p41(X2))|(~p40(X2)&~p41(X2))|(p41(X2)&p40(X2))|(~p39(X2)&~p40(X2))|(p40(X2)&p39(X2))|(~p38(X2)&~p39(X2))|(p39(X2)&p38(X2))|(~p37(X2)&~p38(X2))|(p38(X2)&p37(X2))|(~p36(X2)&~p37(X2))|(p37(X2)&p36(X2))|(~p35(X2)&~p36(X2))|(p36(X2)&p35(X2))|(~p34(X2)&~p35(X2))|(p35(X2)&p34(X2))|(~p33(X2)&~p34(X2))|(p34(X2)&p33(X2))|(~p32(X2)&~p33(X2))|(p33(X2)&p32(X2))|(~p31(X2)&~p32(X2))|(p32(X2)&p31(X2))|(~p30(X2)&~p31(X2))|(p31(X2)&p30(X2))|(~p29(X2)&~p30(X2))|(p30(X2)&p29(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.57/0.57 fof(c_0_4, plain, ![X13, X57, X58, X59, X60, X61, X62, X63, X64, X65, X66, X67, X68, X69, X70, X71, X72, X73, X74, X75, X76, X77, X78, X79, X80, X81, X82, X83, X84, X85, X86, X87, X88, X89, X90, X91, X92, X93, X94, X95, X96, X97, X98, X99]:(((((((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))&(((r1(esk32_1(X13),esk33_1(X13))|~epred1_1(X13))&(((r1(esk33_1(X13),esk34_1(X13))|~epred1_1(X13))&(((r1(esk34_1(X13),esk35_1(X13))|~epred1_1(X13))&(((r1(esk35_1(X13),esk36_1(X13))|~epred1_1(X13))&(((r1(esk36_1(X13),esk37_1(X13))|~epred1_1(X13))&(((r1(esk37_1(X13),esk38_1(X13))|~epred1_1(X13))&(((r1(esk38_1(X13),esk39_1(X13))|~epred1_1(X13))&(((r1(esk39_1(X13),esk40_1(X13))|~epred1_1(X13))&(((r1(esk40_1(X13),esk41_1(X13))|~epred1_1(X13))&(((r1(esk41_1(X13),esk42_1(X13))|~epred1_1(X13))&(((r1(esk42_1(X13),esk43_1(X13))|~epred1_1(X13))&(((r1(esk43_1(X13),esk44_1(X13))|~epred1_1(X13))&(((r1(esk44_1(X13),esk45_1(X13))|~epred1_1(X13))&(((r1(esk45_1(X13),esk46_1(X13))|~epred1_1(X13))&((r1(esk46_1(X13),esk47_1(X13))|~epred1_1(X13))&($true|~epred1_1(X13))))&((~p44(X57)|p43(X57)|~r1(esk46_1(X13),X57)|~epred1_1(X13))&(p44(X57)|~p43(X57)|~r1(esk46_1(X13),X57)|~epred1_1(X13)))))&((~p43(X58)|p42(X58)|~r1(esk45_1(X13),X58)|~epred1_1(X13))&(p43(X58)|~p42(X58)|~r1(esk45_1(X13),X58)|~epred1_1(X13)))))&((~p42(X59)|p41(X59)|~r1(esk44_1(X13),X59)|~epred1_1(X13))&(p42(X59)|~p41(X59)|~r1(esk44_1(X13),X59)|~epred1_1(X13)))))&((~p41(X60)|p40(X60)|~r1(esk43_1(X13),X60)|~epred1_1(X13))&(p41(X60)|~p40(X60)|~r1(esk43_1(X13),X60)|~epred1_1(X13)))))&((~p40(X61)|p39(X61)|~r1(esk42_1(X13),X61)|~epred1_1(X13))&(p40(X61)|~p39(X61)|~r1(esk42_1(X13),X61)|~epred1_1(X13)))))&((~p39(X62)|p38(X62)|~r1(esk41_1(X13),X62)|~epred1_1(X13))&(p39(X62)|~p38(X62)|~r1(esk41_1(X13),X62)|~epred1_1(X13)))))&((~p38(X63)|p37(X63)|~r1(esk40_1(X13),X63)|~epred1_1(X13))&(p38(X63)|~p37(X63)|~r1(esk40_1(X13),X63)|~epred1_1(X13)))))&((~p37(X64)|p36(X64)|~r1(esk39_1(X13),X64)|~epred1_1(X13))&(p37(X64)|~p36(X64)|~r1(esk39_1(X13),X64)|~epred1_1(X13)))))&((~p36(X65)|p35(X65)|~r1(esk38_1(X13),X65)|~epred1_1(X13))&(p36(X65)|~p35(X65)|~r1(esk38_1(X13),X65)|~epred1_1(X13)))))&((~p35(X66)|p34(X66)|~r1(esk37_1(X13),X66)|~epred1_1(X13))&(p35(X66)|~p34(X66)|~r1(esk37_1(X13),X66)|~epred1_1(X13)))))&((~p34(X67)|p33(X67)|~r1(esk36_1(X13),X67)|~epred1_1(X13))&(p34(X67)|~p33(X67)|~r1(esk36_1(X13),X67)|~epred1_1(X13)))))&((~p33(X68)|p32(X68)|~r1(esk35_1(X13),X68)|~epred1_1(X13))&(p33(X68)|~p32(X68)|~r1(esk35_1(X13),X68)|~epred1_1(X13)))))&((~p32(X69)|p31(X69)|~r1(esk34_1(X13),X69)|~epred1_1(X13))&(p32(X69)|~p31(X69)|~r1(esk34_1(X13),X69)|~epred1_1(X13)))))&((~p31(X70)|p30(X70)|~r1(esk33_1(X13),X70)|~epred1_1(X13))&(p31(X70)|~p30(X70)|~r1(esk33_1(X13),X70)|~epred1_1(X13)))))&((~p30(X71)|p29(X71)|~r1(esk32_1(X13),X71)|~epred1_1(X13))&(p30(X71)|~p29(X71)|~r1(esk32_1(X13),X71)|~epred1_1(X13)))))&((~p29(X72)|p28(X72)|~r1(esk31_1(X13),X72)|~epred1_1(X13))&(p29(X72)|~p28(X72)|~r1(esk31_1(X13),X72)|~epred1_1(X13)))))&((~p28(X73)|p27(X73)|~r1(esk30_1(X13),X73)|~epred1_1(X13))&(p28(X73)|~p27(X73)|~r1(esk30_1(X13),X73)|~epred1_1(X13)))))&((~p27(X74)|p26(X74)|~r1(esk29_1(X13),X74)|~epred1_1(X13))&(p27(X74)|~p26(X74)|~r1(esk29_1(X13),X74)|~epred1_1(X13)))))&((~p26(X75)|p25(X75)|~r1(esk28_1(X13),X75)|~epred1_1(X13))&(p26(X75)|~p25(X75)|~r1(esk28_1(X13),X75)|~epred1_1(X13)))))&((~p25(X76)|p24(X76)|~r1(esk27_1(X13),X76)|~epred1_1(X13))&(p25(X76)|~p24(X76)|~r1(esk27_1(X13),X76)|~epred1_1(X13)))))&((~p24(X77)|p23(X77)|~r1(esk26_1(X13),X77)|~epred1_1(X13))&(p24(X77)|~p23(X77)|~r1(esk26_1(X13),X77)|~epred1_1(X13)))))&((~p23(X78)|p22(X78)|~r1(esk25_1(X13),X78)|~epred1_1(X13))&(p23(X78)|~p22(X78)|~r1(esk25_1(X13),X78)|~epred1_1(X13)))))&((~p22(X79)|p21(X79)|~r1(esk24_1(X13),X79)|~epred1_1(X13))&(p22(X79)|~p21(X79)|~r1(esk24_1(X13),X79)|~epred1_1(X13)))))&((~p21(X80)|p20(X80)|~r1(esk23_1(X13),X80)|~epred1_1(X13))&(p21(X80)|~p20(X80)|~r1(esk23_1(X13),X80)|~epred1_1(X13)))))&((~p20(X81)|p19(X81)|~r1(esk22_1(X13),X81)|~epred1_1(X13))&(p20(X81)|~p19(X81)|~r1(esk22_1(X13),X81)|~epred1_1(X13)))))&((~p19(X82)|p18(X82)|~r1(esk21_1(X13),X82)|~epred1_1(X13))&(p19(X82)|~p18(X82)|~r1(esk21_1(X13),X82)|~epred1_1(X13)))))&((~p18(X83)|p17(X83)|~r1(esk20_1(X13),X83)|~epred1_1(X13))&(p18(X83)|~p17(X83)|~r1(esk20_1(X13),X83)|~epred1_1(X13)))))&((~p17(X84)|p16(X84)|~r1(esk19_1(X13),X84)|~epred1_1(X13))&(p17(X84)|~p16(X84)|~r1(esk19_1(X13),X84)|~epred1_1(X13)))))&((~p16(X85)|p15(X85)|~r1(esk18_1(X13),X85)|~epred1_1(X13))&(p16(X85)|~p15(X85)|~r1(esk18_1(X13),X85)|~epred1_1(X13)))))&((~p15(X86)|p14(X86)|~r1(esk17_1(X13),X86)|~epred1_1(X13))&(p15(X86)|~p14(X86)|~r1(esk17_1(X13),X86)|~epred1_1(X13)))))&((~p14(X87)|p13(X87)|~r1(esk16_1(X13),X87)|~epred1_1(X13))&(p14(X87)|~p13(X87)|~r1(esk16_1(X13),X87)|~epred1_1(X13)))))&((~p13(X88)|p12(X88)|~r1(esk15_1(X13),X88)|~epred1_1(X13))&(p13(X88)|~p12(X88)|~r1(esk15_1(X13),X88)|~epred1_1(X13)))))&((~p12(X89)|p11(X89)|~r1(esk14_1(X13),X89)|~epred1_1(X13))&(p12(X89)|~p11(X89)|~r1(esk14_1(X13),X89)|~epred1_1(X13)))))&((~p11(X90)|p10(X90)|~r1(esk13_1(X13),X90)|~epred1_1(X13))&(p11(X90)|~p10(X90)|~r1(esk13_1(X13),X90)|~epred1_1(X13)))))&((~p10(X91)|p9(X91)|~r1(esk12_1(X13),X91)|~epred1_1(X13))&(p10(X91)|~p9(X91)|~r1(esk12_1(X13),X91)|~epred1_1(X13)))))&((~p9(X92)|p8(X92)|~r1(esk11_1(X13),X92)|~epred1_1(X13))&(p9(X92)|~p8(X92)|~r1(esk11_1(X13),X92)|~epred1_1(X13)))))&((~p8(X93)|p7(X93)|~r1(esk10_1(X13),X93)|~epred1_1(X13))&(p8(X93)|~p7(X93)|~r1(esk10_1(X13),X93)|~epred1_1(X13)))))&((~p7(X94)|p6(X94)|~r1(esk9_1(X13),X94)|~epred1_1(X13))&(p7(X94)|~p6(X94)|~r1(esk9_1(X13),X94)|~epred1_1(X13)))))&((~p6(X95)|p5(X95)|~r1(esk8_1(X13),X95)|~epred1_1(X13))&(p6(X95)|~p5(X95)|~r1(esk8_1(X13),X95)|~epred1_1(X13)))))&((~p5(X96)|p4(X96)|~r1(esk7_1(X13),X96)|~epred1_1(X13))&(p5(X96)|~p4(X96)|~r1(esk7_1(X13),X96)|~epred1_1(X13)))))&((~p4(X97)|p3(X97)|~r1(esk6_1(X13),X97)|~epred1_1(X13))&(p4(X97)|~p3(X97)|~r1(esk6_1(X13),X97)|~epred1_1(X13)))))&((~p3(X98)|p2(X98)|~r1(esk5_1(X13),X98)|~epred1_1(X13))&(p3(X98)|~p2(X98)|~r1(esk5_1(X13),X98)|~epred1_1(X13))))&((~p2(X99)|p1(X99)|~r1(X13,X99)|~epred1_1(X13))&(p2(X99)|~p1(X99)|~r1(X13,X99)|~epred1_1(X13))))&((r1(X13,esk48_1(X13))|~epred1_1(X13))&(~p45(esk48_1(X13))|~epred1_1(X13))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X13,esk49_1(X13))|~epred1_1(X13))&(p43(esk49_1(X13))|p44(esk49_1(X13))|~epred1_1(X13)))&(~p44(esk49_1(X13))|~p43(esk49_1(X13))|~epred1_1(X13)))&(p42(esk49_1(X13))|p43(esk49_1(X13))|~epred1_1(X13)))&(~p43(esk49_1(X13))|~p42(esk49_1(X13))|~epred1_1(X13)))&(p41(esk49_1(X13))|p42(esk49_1(X13))|~epred1_1(X13)))&(~p42(esk49_1(X13))|~p41(esk49_1(X13))|~epred1_1(X13)))&(p40(esk49_1(X13))|p41(esk49_1(X13))|~epred1_1(X13)))&(~p41(esk49_1(X13))|~p40(esk49_1(X13))|~epred1_1(X13)))&(p39(esk49_1(X13))|p40(esk49_1(X13))|~epred1_1(X13)))&(~p40(esk49_1(X13))|~p39(esk49_1(X13))|~epred1_1(X13)))&(p38(esk49_1(X13))|p39(esk49_1(X13))|~epred1_1(X13)))&(~p39(esk49_1(X13))|~p38(esk49_1(X13))|~epred1_1(X13)))&(p37(esk49_1(X13))|p38(esk49_1(X13))|~epred1_1(X13)))&(~p38(esk49_1(X13))|~p37(esk49_1(X13))|~epred1_1(X13)))&(p36(esk49_1(X13))|p37(esk49_1(X13))|~epred1_1(X13)))&(~p37(esk49_1(X13))|~p36(esk49_1(X13))|~epred1_1(X13)))&(p35(esk49_1(X13))|p36(esk49_1(X13))|~epred1_1(X13)))&(~p36(esk49_1(X13))|~p35(esk49_1(X13))|~epred1_1(X13)))&(p34(esk49_1(X13))|p35(esk49_1(X13))|~epred1_1(X13)))&(~p35(esk49_1(X13))|~p34(esk49_1(X13))|~epred1_1(X13)))&(p33(esk49_1(X13))|p34(esk49_1(X13))|~epred1_1(X13)))&(~p34(esk49_1(X13))|~p33(esk49_1(X13))|~epred1_1(X13)))&(p32(esk49_1(X13))|p33(esk49_1(X13))|~epred1_1(X13)))&(~p33(esk49_1(X13))|~p32(esk49_1(X13))|~epred1_1(X13)))&(p31(esk49_1(X13))|p32(esk49_1(X13))|~epred1_1(X13)))&(~p32(esk49_1(X13))|~p31(esk49_1(X13))|~epred1_1(X13)))&(p30(esk49_1(X13))|p31(esk49_1(X13))|~epred1_1(X13)))&(~p31(esk49_1(X13))|~p30(esk49_1(X13))|~epred1_1(X13)))&(p29(esk49_1(X13))|p30(esk49_1(X13))|~epred1_1(X13)))&(~p30(esk49_1(X13))|~p29(esk49_1(X13))|~epred1_1(X13)))&(p28(esk49_1(X13))|p29(esk49_1(X13))|~epred1_1(X13)))&(~p29(esk49_1(X13))|~p28(esk49_1(X13))|~epred1_1(X13)))&(p27(esk49_1(X13))|p28(esk49_1(X13))|~epred1_1(X13)))&(~p28(esk49_1(X13))|~p27(esk49_1(X13))|~epred1_1(X13)))&(p26(esk49_1(X13))|p27(esk49_1(X13))|~epred1_1(X13)))&(~p27(esk49_1(X13))|~p26(esk49_1(X13))|~epred1_1(X13)))&(p25(esk49_1(X13))|p26(esk49_1(X13))|~epred1_1(X13)))&(~p26(esk49_1(X13))|~p25(esk49_1(X13))|~epred1_1(X13)))&(p24(esk49_1(X13))|p25(esk49_1(X13))|~epred1_1(X13)))&(~p25(esk49_1(X13))|~p24(esk49_1(X13))|~epred1_1(X13)))&(p23(esk49_1(X13))|p24(esk49_1(X13))|~epred1_1(X13)))&(~p24(esk49_1(X13))|~p23(esk49_1(X13))|~epred1_1(X13)))&(p22(esk49_1(X13))|p23(esk49_1(X13))|~epred1_1(X13)))&(~p23(esk49_1(X13))|~p22(esk49_1(X13))|~epred1_1(X13)))&(p21(esk49_1(X13))|p22(esk49_1(X13))|~epred1_1(X13)))&(~p22(esk49_1(X13))|~p21(esk49_1(X13))|~epred1_1(X13)))&(p20(esk49_1(X13))|p21(esk49_1(X13))|~epred1_1(X13)))&(~p21(esk49_1(X13))|~p20(esk49_1(X13))|~epred1_1(X13)))&(p19(esk49_1(X13))|p20(esk49_1(X13))|~epred1_1(X13)))&(~p20(esk49_1(X13))|~p19(esk49_1(X13))|~epred1_1(X13)))&(p18(esk49_1(X13))|p19(esk49_1(X13))|~epred1_1(X13)))&(~p19(esk49_1(X13))|~p18(esk49_1(X13))|~epred1_1(X13)))&(p17(esk49_1(X13))|p18(esk49_1(X13))|~epred1_1(X13)))&(~p18(esk49_1(X13))|~p17(esk49_1(X13))|~epred1_1(X13)))&(p16(esk49_1(X13))|p17(esk49_1(X13))|~epred1_1(X13)))&(~p17(esk49_1(X13))|~p16(esk49_1(X13))|~epred1_1(X13)))&(p15(esk49_1(X13))|p16(esk49_1(X13))|~epred1_1(X13)))&(~p16(esk49_1(X13))|~p15(esk49_1(X13))|~epred1_1(X13)))&(p14(esk49_1(X13))|p15(esk49_1(X13))|~epred1_1(X13)))&(~p15(esk49_1(X13))|~p14(esk49_1(X13))|~epred1_1(X13)))&(p13(esk49_1(X13))|p14(esk49_1(X13))|~epred1_1(X13)))&(~p14(esk49_1(X13))|~p13(esk49_1(X13))|~epred1_1(X13)))&(p12(esk49_1(X13))|p13(esk49_1(X13))|~epred1_1(X13)))&(~p13(esk49_1(X13))|~p12(esk49_1(X13))|~epred1_1(X13)))&(p11(esk49_1(X13))|p12(esk49_1(X13))|~epred1_1(X13)))&(~p12(esk49_1(X13))|~p11(esk49_1(X13))|~epred1_1(X13)))&(p10(esk49_1(X13))|p11(esk49_1(X13))|~epred1_1(X13)))&(~p11(esk49_1(X13))|~p10(esk49_1(X13))|~epred1_1(X13)))&(p9(esk49_1(X13))|p10(esk49_1(X13))|~epred1_1(X13)))&(~p10(esk49_1(X13))|~p9(esk49_1(X13))|~epred1_1(X13)))&(p8(esk49_1(X13))|p9(esk49_1(X13))|~epred1_1(X13)))&(~p9(esk49_1(X13))|~p8(esk49_1(X13))|~epred1_1(X13)))&(p7(esk49_1(X13))|p8(esk49_1(X13))|~epred1_1(X13)))&(~p8(esk49_1(X13))|~p7(esk49_1(X13))|~epred1_1(X13)))&(p6(esk49_1(X13))|p7(esk49_1(X13))|~epred1_1(X13)))&(~p7(esk49_1(X13))|~p6(esk49_1(X13))|~epred1_1(X13)))&(p5(esk49_1(X13))|p6(esk49_1(X13))|~epred1_1(X13)))&(~p6(esk49_1(X13))|~p5(esk49_1(X13))|~epred1_1(X13)))&(p4(esk49_1(X13))|p5(esk49_1(X13))|~epred1_1(X13)))&(~p5(esk49_1(X13))|~p4(esk49_1(X13))|~epred1_1(X13)))&(p3(esk49_1(X13))|p4(esk49_1(X13))|~epred1_1(X13)))&(~p4(esk49_1(X13))|~p3(esk49_1(X13))|~epred1_1(X13)))&(p2(esk49_1(X13))|p3(esk49_1(X13))|~epred1_1(X13)))&(~p3(esk49_1(X13))|~p2(esk49_1(X13))|~epred1_1(X13)))&(p1(esk49_1(X13))|p2(esk49_1(X13))|~epred1_1(X13)))&(~p2(esk49_1(X13))|~p1(esk49_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.57/0.57 fof(c_0_5, plain, ![X9]:(r1(X9,X9)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.57/0.57 fof(c_0_6, negated_conjecture, ~(~(?[X1]:(~((![X2]:((~r1(X1,X2)|~p45(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.57/0.57 cnf(c_0_7, plain, (p1(X1)|~p2(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.57/0.57 cnf(c_0_8, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.57/0.57 fof(c_0_9, negated_conjecture, ![X8]:((((r1(esk1_0,esk2_0)&p45(esk2_0))&(r1(esk2_0,esk3_0)&p1(esk3_0)))&(r1(esk1_0,esk4_0)&(~r1(esk4_0,X8)|epred1_1(X8))))), 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_6])])])])])).
% 0.57/0.57 cnf(c_0_10, plain, (~p2(esk49_1(X1))|~p1(esk49_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.57/0.57 cnf(c_0_11, plain, (p1(X1)|~epred1_1(X1)|~p2(X1)), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 0.57/0.57 cnf(c_0_12, plain, (p2(X1)|~p1(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.57/0.57 cnf(c_0_13, plain, (r1(X1,esk49_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.57/0.57 cnf(c_0_14, plain, (p1(esk49_1(X1))|p2(esk49_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.57/0.57 cnf(c_0_15, negated_conjecture, (epred1_1(X1)|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.57/0.57 cnf(c_0_16, plain, (~epred1_1(esk49_1(X1))|~epred1_1(X1)|~p2(esk49_1(X1))), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 0.57/0.57 cnf(c_0_17, plain, (p2(esk49_1(X1))|~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14])).
% 0.57/0.57 cnf(c_0_18, negated_conjecture, (epred1_1(esk4_0)), inference(spm,[status(thm)],[c_0_15, c_0_8])).
% 0.57/0.57 cnf(c_0_19, plain, (~epred1_1(esk49_1(X1))|~epred1_1(X1)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 0.57/0.57 cnf(c_0_20, negated_conjecture, (epred1_1(esk49_1(esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_13]), c_0_18])])).
% 0.57/0.57 cnf(c_0_21, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_18])]), ['proof']).
% 0.57/0.57 % SZS output end Proof
% 0.57/0.57 % User time : 0.022 s
% 0.57/0.57 % System time : 0.006 s
% 0.57/0.57 % Total time : 0.028 s
% 0.57/0.57 % User time : 0.024 s
% 0.57/0.57 % System time : 0.009 s
% 0.57/0.57 % Total time : 0.033 s
% 0.57/0.57
%------------------------------------------------------------------------------