%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n007.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.74s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n007.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 6 00:30:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.47 start to proof:theBenchmark.p
% 0.74/0.58 % Version : CSI_E---1.1
% 0.74/0.58 % Problem : theBenchmark.p
% 0.74/0.58 % Proof found!
% 0.74/0.58 % SZS status Theorem for theBenchmark.p
% 0.74/0.58 % SZS output start Proof
% 0.74/0.58 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 0.74/0.58 fof(main, conjecture, ~(?[X1]:(~((![X2]:((~(r1(X1,X2))|~(p60(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))|![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))|~(((p59(X1)&~(p58(X1)))|(~(p59(X1))&p58(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p58(X2)&~(p57(X2)))|(~(p58(X2))&p57(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p57(X1)&~(p56(X1)))|(~(p57(X1))&p56(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p56(X2)&~(p55(X2)))|(~(p56(X2))&p55(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p55(X1)&~(p54(X1)))|(~(p55(X1))&p54(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p54(X2)&~(p53(X2)))|(~(p54(X2))&p53(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p53(X1)&~(p52(X1)))|(~(p53(X1))&p52(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p52(X2)&~(p51(X2)))|(~(p52(X2))&p51(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p51(X1)&~(p50(X1)))|(~(p51(X1))&p50(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p50(X2)&~(p49(X2)))|(~(p50(X2))&p49(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p49(X1)&~(p48(X1)))|(~(p49(X1))&p48(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p48(X2)&~(p47(X2)))|(~(p48(X2))&p47(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p47(X1)&~(p46(X1)))|(~(p47(X1))&p46(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p46(X2)&~(p45(X2)))|(~(p46(X2))&p45(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p45(X1)&~(p44(X1)))|(~(p45(X1))&p44(X1)))))))))|~(![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))|p60(X2)))|![X2]:((~(r1(X1,X2))|(~(p58(X2))&~(p59(X2)))|(p59(X2)&p58(X2))|(~(p57(X2))&~(p58(X2)))|(p58(X2)&p57(X2))|(~(p56(X2))&~(p57(X2)))|(p57(X2)&p56(X2))|(~(p55(X2))&~(p56(X2)))|(p56(X2)&p55(X2))|(~(p54(X2))&~(p55(X2)))|(p55(X2)&p54(X2))|(~(p53(X2))&~(p54(X2)))|(p54(X2)&p53(X2))|(~(p52(X2))&~(p53(X2)))|(p53(X2)&p52(X2))|(~(p51(X2))&~(p52(X2)))|(p52(X2)&p51(X2))|(~(p50(X2))&~(p51(X2)))|(p51(X2)&p50(X2))|(~(p49(X2))&~(p50(X2)))|(p50(X2)&p49(X2))|(~(p48(X2))&~(p49(X2)))|(p49(X2)&p48(X2))|(~(p47(X2))&~(p48(X2)))|(p48(X2)&p47(X2))|(~(p46(X2))&~(p47(X2)))|(p47(X2)&p46(X2))|(~(p45(X2))&~(p46(X2)))|(p46(X2)&p45(X2))|(~(p44(X2))&~(p45(X2)))|(p45(X2)&p44(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/sandbox2/benchmark/theBenchmark.p', main)).
% 0.74/0.58 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)|![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)|~(((p59(X1)&~p58(X1))|(~p59(X1)&p58(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p58(X2)&~p57(X2))|(~p58(X2)&p57(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p57(X1)&~p56(X1))|(~p57(X1)&p56(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p56(X2)&~p55(X2))|(~p56(X2)&p55(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p55(X1)&~p54(X1))|(~p55(X1)&p54(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p54(X2)&~p53(X2))|(~p54(X2)&p53(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p53(X1)&~p52(X1))|(~p53(X1)&p52(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p52(X2)&~p51(X2))|(~p52(X2)&p51(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p51(X1)&~p50(X1))|(~p51(X1)&p50(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p50(X2)&~p49(X2))|(~p50(X2)&p49(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p49(X1)&~p48(X1))|(~p49(X1)&p48(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p48(X2)&~p47(X2))|(~p48(X2)&p47(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p47(X1)&~p46(X1))|(~p47(X1)&p46(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p46(X2)&~p45(X2))|(~p46(X2)&p45(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p45(X1)&~p44(X1))|(~p45(X1)&p44(X1)))))))))|~(![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)|p60(X2)))|![X2]:((~r1(X1,X2)|(~p58(X2)&~p59(X2))|(p59(X2)&p58(X2))|(~p57(X2)&~p58(X2))|(p58(X2)&p57(X2))|(~p56(X2)&~p57(X2))|(p57(X2)&p56(X2))|(~p55(X2)&~p56(X2))|(p56(X2)&p55(X2))|(~p54(X2)&~p55(X2))|(p55(X2)&p54(X2))|(~p53(X2)&~p54(X2))|(p54(X2)&p53(X2))|(~p52(X2)&~p53(X2))|(p53(X2)&p52(X2))|(~p51(X2)&~p52(X2))|(p52(X2)&p51(X2))|(~p50(X2)&~p51(X2))|(p51(X2)&p50(X2))|(~p49(X2)&~p50(X2))|(p50(X2)&p49(X2))|(~p48(X2)&~p49(X2))|(p49(X2)&p48(X2))|(~p47(X2)&~p48(X2))|(p48(X2)&p47(X2))|(~p46(X2)&~p47(X2))|(p47(X2)&p46(X2))|(~p45(X2)&~p46(X2))|(p46(X2)&p45(X2))|(~p44(X2)&~p45(X2))|(p45(X2)&p44(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.74/0.58 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)|![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)|~(((p59(X1)&~p58(X1))|(~p59(X1)&p58(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p58(X2)&~p57(X2))|(~p58(X2)&p57(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p57(X1)&~p56(X1))|(~p57(X1)&p56(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p56(X2)&~p55(X2))|(~p56(X2)&p55(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p55(X1)&~p54(X1))|(~p55(X1)&p54(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p54(X2)&~p53(X2))|(~p54(X2)&p53(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p53(X1)&~p52(X1))|(~p53(X1)&p52(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p52(X2)&~p51(X2))|(~p52(X2)&p51(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p51(X1)&~p50(X1))|(~p51(X1)&p50(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p50(X2)&~p49(X2))|(~p50(X2)&p49(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p49(X1)&~p48(X1))|(~p49(X1)&p48(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p48(X2)&~p47(X2))|(~p48(X2)&p47(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p47(X1)&~p46(X1))|(~p47(X1)&p46(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p46(X2)&~p45(X2))|(~p46(X2)&p45(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p45(X1)&~p44(X1))|(~p45(X1)&p44(X1)))))))))|~(![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)|p60(X2)))|![X2]:((~r1(X1,X2)|(~p58(X2)&~p59(X2))|(p59(X2)&p58(X2))|(~p57(X2)&~p58(X2))|(p58(X2)&p57(X2))|(~p56(X2)&~p57(X2))|(p57(X2)&p56(X2))|(~p55(X2)&~p56(X2))|(p56(X2)&p55(X2))|(~p54(X2)&~p55(X2))|(p55(X2)&p54(X2))|(~p53(X2)&~p54(X2))|(p54(X2)&p53(X2))|(~p52(X2)&~p53(X2))|(p53(X2)&p52(X2))|(~p51(X2)&~p52(X2))|(p52(X2)&p51(X2))|(~p50(X2)&~p51(X2))|(p51(X2)&p50(X2))|(~p49(X2)&~p50(X2))|(p50(X2)&p49(X2))|(~p48(X2)&~p49(X2))|(p49(X2)&p48(X2))|(~p47(X2)&~p48(X2))|(p48(X2)&p47(X2))|(~p46(X2)&~p47(X2))|(p47(X2)&p46(X2))|(~p45(X2)&~p46(X2))|(p46(X2)&p45(X2))|(~p44(X2)&~p45(X2))|(p45(X2)&p44(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.74/0.58 fof(c_0_4, plain, ![X13, 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, X100, X101, X102, X103, X104, X105, X106, X107, X108, X109, X110, X111, X112, X113, X114, X115, X116, X117, X118, X119, X120, X121, X122, X123, X124, X125, X126, X127, X128, X129]:(((((((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))&(((r1(esk47_1(X13),esk48_1(X13))|~epred1_1(X13))&(((r1(esk48_1(X13),esk49_1(X13))|~epred1_1(X13))&(((r1(esk49_1(X13),esk50_1(X13))|~epred1_1(X13))&(((r1(esk50_1(X13),esk51_1(X13))|~epred1_1(X13))&(((r1(esk51_1(X13),esk52_1(X13))|~epred1_1(X13))&(((r1(esk52_1(X13),esk53_1(X13))|~epred1_1(X13))&(((r1(esk53_1(X13),esk54_1(X13))|~epred1_1(X13))&(((r1(esk54_1(X13),esk55_1(X13))|~epred1_1(X13))&(((r1(esk55_1(X13),esk56_1(X13))|~epred1_1(X13))&(((r1(esk56_1(X13),esk57_1(X13))|~epred1_1(X13))&(((r1(esk57_1(X13),esk58_1(X13))|~epred1_1(X13))&(((r1(esk58_1(X13),esk59_1(X13))|~epred1_1(X13))&(((r1(esk59_1(X13),esk60_1(X13))|~epred1_1(X13))&(((r1(esk60_1(X13),esk61_1(X13))|~epred1_1(X13))&((r1(esk61_1(X13),esk62_1(X13))|~epred1_1(X13))&($true|~epred1_1(X13))))&((~p59(X72)|p58(X72)|~r1(esk61_1(X13),X72)|~epred1_1(X13))&(p59(X72)|~p58(X72)|~r1(esk61_1(X13),X72)|~epred1_1(X13)))))&((~p58(X73)|p57(X73)|~r1(esk60_1(X13),X73)|~epred1_1(X13))&(p58(X73)|~p57(X73)|~r1(esk60_1(X13),X73)|~epred1_1(X13)))))&((~p57(X74)|p56(X74)|~r1(esk59_1(X13),X74)|~epred1_1(X13))&(p57(X74)|~p56(X74)|~r1(esk59_1(X13),X74)|~epred1_1(X13)))))&((~p56(X75)|p55(X75)|~r1(esk58_1(X13),X75)|~epred1_1(X13))&(p56(X75)|~p55(X75)|~r1(esk58_1(X13),X75)|~epred1_1(X13)))))&((~p55(X76)|p54(X76)|~r1(esk57_1(X13),X76)|~epred1_1(X13))&(p55(X76)|~p54(X76)|~r1(esk57_1(X13),X76)|~epred1_1(X13)))))&((~p54(X77)|p53(X77)|~r1(esk56_1(X13),X77)|~epred1_1(X13))&(p54(X77)|~p53(X77)|~r1(esk56_1(X13),X77)|~epred1_1(X13)))))&((~p53(X78)|p52(X78)|~r1(esk55_1(X13),X78)|~epred1_1(X13))&(p53(X78)|~p52(X78)|~r1(esk55_1(X13),X78)|~epred1_1(X13)))))&((~p52(X79)|p51(X79)|~r1(esk54_1(X13),X79)|~epred1_1(X13))&(p52(X79)|~p51(X79)|~r1(esk54_1(X13),X79)|~epred1_1(X13)))))&((~p51(X80)|p50(X80)|~r1(esk53_1(X13),X80)|~epred1_1(X13))&(p51(X80)|~p50(X80)|~r1(esk53_1(X13),X80)|~epred1_1(X13)))))&((~p50(X81)|p49(X81)|~r1(esk52_1(X13),X81)|~epred1_1(X13))&(p50(X81)|~p49(X81)|~r1(esk52_1(X13),X81)|~epred1_1(X13)))))&((~p49(X82)|p48(X82)|~r1(esk51_1(X13),X82)|~epred1_1(X13))&(p49(X82)|~p48(X82)|~r1(esk51_1(X13),X82)|~epred1_1(X13)))))&((~p48(X83)|p47(X83)|~r1(esk50_1(X13),X83)|~epred1_1(X13))&(p48(X83)|~p47(X83)|~r1(esk50_1(X13),X83)|~epred1_1(X13)))))&((~p47(X84)|p46(X84)|~r1(esk49_1(X13),X84)|~epred1_1(X13))&(p47(X84)|~p46(X84)|~r1(esk49_1(X13),X84)|~epred1_1(X13)))))&((~p46(X85)|p45(X85)|~r1(esk48_1(X13),X85)|~epred1_1(X13))&(p46(X85)|~p45(X85)|~r1(esk48_1(X13),X85)|~epred1_1(X13)))))&((~p45(X86)|p44(X86)|~r1(esk47_1(X13),X86)|~epred1_1(X13))&(p45(X86)|~p44(X86)|~r1(esk47_1(X13),X86)|~epred1_1(X13)))))&((~p44(X87)|p43(X87)|~r1(esk46_1(X13),X87)|~epred1_1(X13))&(p44(X87)|~p43(X87)|~r1(esk46_1(X13),X87)|~epred1_1(X13)))))&((~p43(X88)|p42(X88)|~r1(esk45_1(X13),X88)|~epred1_1(X13))&(p43(X88)|~p42(X88)|~r1(esk45_1(X13),X88)|~epred1_1(X13)))))&((~p42(X89)|p41(X89)|~r1(esk44_1(X13),X89)|~epred1_1(X13))&(p42(X89)|~p41(X89)|~r1(esk44_1(X13),X89)|~epred1_1(X13)))))&((~p41(X90)|p40(X90)|~r1(esk43_1(X13),X90)|~epred1_1(X13))&(p41(X90)|~p40(X90)|~r1(esk43_1(X13),X90)|~epred1_1(X13)))))&((~p40(X91)|p39(X91)|~r1(esk42_1(X13),X91)|~epred1_1(X13))&(p40(X91)|~p39(X91)|~r1(esk42_1(X13),X91)|~epred1_1(X13)))))&((~p39(X92)|p38(X92)|~r1(esk41_1(X13),X92)|~epred1_1(X13))&(p39(X92)|~p38(X92)|~r1(esk41_1(X13),X92)|~epred1_1(X13)))))&((~p38(X93)|p37(X93)|~r1(esk40_1(X13),X93)|~epred1_1(X13))&(p38(X93)|~p37(X93)|~r1(esk40_1(X13),X93)|~epred1_1(X13)))))&((~p37(X94)|p36(X94)|~r1(esk39_1(X13),X94)|~epred1_1(X13))&(p37(X94)|~p36(X94)|~r1(esk39_1(X13),X94)|~epred1_1(X13)))))&((~p36(X95)|p35(X95)|~r1(esk38_1(X13),X95)|~epred1_1(X13))&(p36(X95)|~p35(X95)|~r1(esk38_1(X13),X95)|~epred1_1(X13)))))&((~p35(X96)|p34(X96)|~r1(esk37_1(X13),X96)|~epred1_1(X13))&(p35(X96)|~p34(X96)|~r1(esk37_1(X13),X96)|~epred1_1(X13)))))&((~p34(X97)|p33(X97)|~r1(esk36_1(X13),X97)|~epred1_1(X13))&(p34(X97)|~p33(X97)|~r1(esk36_1(X13),X97)|~epred1_1(X13)))))&((~p33(X98)|p32(X98)|~r1(esk35_1(X13),X98)|~epred1_1(X13))&(p33(X98)|~p32(X98)|~r1(esk35_1(X13),X98)|~epred1_1(X13)))))&((~p32(X99)|p31(X99)|~r1(esk34_1(X13),X99)|~epred1_1(X13))&(p32(X99)|~p31(X99)|~r1(esk34_1(X13),X99)|~epred1_1(X13)))))&((~p31(X100)|p30(X100)|~r1(esk33_1(X13),X100)|~epred1_1(X13))&(p31(X100)|~p30(X100)|~r1(esk33_1(X13),X100)|~epred1_1(X13)))))&((~p30(X101)|p29(X101)|~r1(esk32_1(X13),X101)|~epred1_1(X13))&(p30(X101)|~p29(X101)|~r1(esk32_1(X13),X101)|~epred1_1(X13)))))&((~p29(X102)|p28(X102)|~r1(esk31_1(X13),X102)|~epred1_1(X13))&(p29(X102)|~p28(X102)|~r1(esk31_1(X13),X102)|~epred1_1(X13)))))&((~p28(X103)|p27(X103)|~r1(esk30_1(X13),X103)|~epred1_1(X13))&(p28(X103)|~p27(X103)|~r1(esk30_1(X13),X103)|~epred1_1(X13)))))&((~p27(X104)|p26(X104)|~r1(esk29_1(X13),X104)|~epred1_1(X13))&(p27(X104)|~p26(X104)|~r1(esk29_1(X13),X104)|~epred1_1(X13)))))&((~p26(X105)|p25(X105)|~r1(esk28_1(X13),X105)|~epred1_1(X13))&(p26(X105)|~p25(X105)|~r1(esk28_1(X13),X105)|~epred1_1(X13)))))&((~p25(X106)|p24(X106)|~r1(esk27_1(X13),X106)|~epred1_1(X13))&(p25(X106)|~p24(X106)|~r1(esk27_1(X13),X106)|~epred1_1(X13)))))&((~p24(X107)|p23(X107)|~r1(esk26_1(X13),X107)|~epred1_1(X13))&(p24(X107)|~p23(X107)|~r1(esk26_1(X13),X107)|~epred1_1(X13)))))&((~p23(X108)|p22(X108)|~r1(esk25_1(X13),X108)|~epred1_1(X13))&(p23(X108)|~p22(X108)|~r1(esk25_1(X13),X108)|~epred1_1(X13)))))&((~p22(X109)|p21(X109)|~r1(esk24_1(X13),X109)|~epred1_1(X13))&(p22(X109)|~p21(X109)|~r1(esk24_1(X13),X109)|~epred1_1(X13)))))&((~p21(X110)|p20(X110)|~r1(esk23_1(X13),X110)|~epred1_1(X13))&(p21(X110)|~p20(X110)|~r1(esk23_1(X13),X110)|~epred1_1(X13)))))&((~p20(X111)|p19(X111)|~r1(esk22_1(X13),X111)|~epred1_1(X13))&(p20(X111)|~p19(X111)|~r1(esk22_1(X13),X111)|~epred1_1(X13)))))&((~p19(X112)|p18(X112)|~r1(esk21_1(X13),X112)|~epred1_1(X13))&(p19(X112)|~p18(X112)|~r1(esk21_1(X13),X112)|~epred1_1(X13)))))&((~p18(X113)|p17(X113)|~r1(esk20_1(X13),X113)|~epred1_1(X13))&(p18(X113)|~p17(X113)|~r1(esk20_1(X13),X113)|~epred1_1(X13)))))&((~p17(X114)|p16(X114)|~r1(esk19_1(X13),X114)|~epred1_1(X13))&(p17(X114)|~p16(X114)|~r1(esk19_1(X13),X114)|~epred1_1(X13)))))&((~p16(X115)|p15(X115)|~r1(esk18_1(X13),X115)|~epred1_1(X13))&(p16(X115)|~p15(X115)|~r1(esk18_1(X13),X115)|~epred1_1(X13)))))&((~p15(X116)|p14(X116)|~r1(esk17_1(X13),X116)|~epred1_1(X13))&(p15(X116)|~p14(X116)|~r1(esk17_1(X13),X116)|~epred1_1(X13)))))&((~p14(X117)|p13(X117)|~r1(esk16_1(X13),X117)|~epred1_1(X13))&(p14(X117)|~p13(X117)|~r1(esk16_1(X13),X117)|~epred1_1(X13)))))&((~p13(X118)|p12(X118)|~r1(esk15_1(X13),X118)|~epred1_1(X13))&(p13(X118)|~p12(X118)|~r1(esk15_1(X13),X118)|~epred1_1(X13)))))&((~p12(X119)|p11(X119)|~r1(esk14_1(X13),X119)|~epred1_1(X13))&(p12(X119)|~p11(X119)|~r1(esk14_1(X13),X119)|~epred1_1(X13)))))&((~p11(X120)|p10(X120)|~r1(esk13_1(X13),X120)|~epred1_1(X13))&(p11(X120)|~p10(X120)|~r1(esk13_1(X13),X120)|~epred1_1(X13)))))&((~p10(X121)|p9(X121)|~r1(esk12_1(X13),X121)|~epred1_1(X13))&(p10(X121)|~p9(X121)|~r1(esk12_1(X13),X121)|~epred1_1(X13)))))&((~p9(X122)|p8(X122)|~r1(esk11_1(X13),X122)|~epred1_1(X13))&(p9(X122)|~p8(X122)|~r1(esk11_1(X13),X122)|~epred1_1(X13)))))&((~p8(X123)|p7(X123)|~r1(esk10_1(X13),X123)|~epred1_1(X13))&(p8(X123)|~p7(X123)|~r1(esk10_1(X13),X123)|~epred1_1(X13)))))&((~p7(X124)|p6(X124)|~r1(esk9_1(X13),X124)|~epred1_1(X13))&(p7(X124)|~p6(X124)|~r1(esk9_1(X13),X124)|~epred1_1(X13)))))&((~p6(X125)|p5(X125)|~r1(esk8_1(X13),X125)|~epred1_1(X13))&(p6(X125)|~p5(X125)|~r1(esk8_1(X13),X125)|~epred1_1(X13)))))&((~p5(X126)|p4(X126)|~r1(esk7_1(X13),X126)|~epred1_1(X13))&(p5(X126)|~p4(X126)|~r1(esk7_1(X13),X126)|~epred1_1(X13)))))&((~p4(X127)|p3(X127)|~r1(esk6_1(X13),X127)|~epred1_1(X13))&(p4(X127)|~p3(X127)|~r1(esk6_1(X13),X127)|~epred1_1(X13)))))&((~p3(X128)|p2(X128)|~r1(esk5_1(X13),X128)|~epred1_1(X13))&(p3(X128)|~p2(X128)|~r1(esk5_1(X13),X128)|~epred1_1(X13))))&((~p2(X129)|p1(X129)|~r1(X13,X129)|~epred1_1(X13))&(p2(X129)|~p1(X129)|~r1(X13,X129)|~epred1_1(X13))))&((r1(X13,esk63_1(X13))|~epred1_1(X13))&(~p60(esk63_1(X13))|~epred1_1(X13))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X13,esk64_1(X13))|~epred1_1(X13))&(p58(esk64_1(X13))|p59(esk64_1(X13))|~epred1_1(X13)))&(~p59(esk64_1(X13))|~p58(esk64_1(X13))|~epred1_1(X13)))&(p57(esk64_1(X13))|p58(esk64_1(X13))|~epred1_1(X13)))&(~p58(esk64_1(X13))|~p57(esk64_1(X13))|~epred1_1(X13)))&(p56(esk64_1(X13))|p57(esk64_1(X13))|~epred1_1(X13)))&(~p57(esk64_1(X13))|~p56(esk64_1(X13))|~epred1_1(X13)))&(p55(esk64_1(X13))|p56(esk64_1(X13))|~epred1_1(X13)))&(~p56(esk64_1(X13))|~p55(esk64_1(X13))|~epred1_1(X13)))&(p54(esk64_1(X13))|p55(esk64_1(X13))|~epred1_1(X13)))&(~p55(esk64_1(X13))|~p54(esk64_1(X13))|~epred1_1(X13)))&(p53(esk64_1(X13))|p54(esk64_1(X13))|~epred1_1(X13)))&(~p54(esk64_1(X13))|~p53(esk64_1(X13))|~epred1_1(X13)))&(p52(esk64_1(X13))|p53(esk64_1(X13))|~epred1_1(X13)))&(~p53(esk64_1(X13))|~p52(esk64_1(X13))|~epred1_1(X13)))&(p51(esk64_1(X13))|p52(esk64_1(X13))|~epred1_1(X13)))&(~p52(esk64_1(X13))|~p51(esk64_1(X13))|~epred1_1(X13)))&(p50(esk64_1(X13))|p51(esk64_1(X13))|~epred1_1(X13)))&(~p51(esk64_1(X13))|~p50(esk64_1(X13))|~epred1_1(X13)))&(p49(esk64_1(X13))|p50(esk64_1(X13))|~epred1_1(X13)))&(~p50(esk64_1(X13))|~p49(esk64_1(X13))|~epred1_1(X13)))&(p48(esk64_1(X13))|p49(esk64_1(X13))|~epred1_1(X13)))&(~p49(esk64_1(X13))|~p48(esk64_1(X13))|~epred1_1(X13)))&(p47(esk64_1(X13))|p48(esk64_1(X13))|~epred1_1(X13)))&(~p48(esk64_1(X13))|~p47(esk64_1(X13))|~epred1_1(X13)))&(p46(esk64_1(X13))|p47(esk64_1(X13))|~epred1_1(X13)))&(~p47(esk64_1(X13))|~p46(esk64_1(X13))|~epred1_1(X13)))&(p45(esk64_1(X13))|p46(esk64_1(X13))|~epred1_1(X13)))&(~p46(esk64_1(X13))|~p45(esk64_1(X13))|~epred1_1(X13)))&(p44(esk64_1(X13))|p45(esk64_1(X13))|~epred1_1(X13)))&(~p45(esk64_1(X13))|~p44(esk64_1(X13))|~epred1_1(X13)))&(p43(esk64_1(X13))|p44(esk64_1(X13))|~epred1_1(X13)))&(~p44(esk64_1(X13))|~p43(esk64_1(X13))|~epred1_1(X13)))&(p42(esk64_1(X13))|p43(esk64_1(X13))|~epred1_1(X13)))&(~p43(esk64_1(X13))|~p42(esk64_1(X13))|~epred1_1(X13)))&(p41(esk64_1(X13))|p42(esk64_1(X13))|~epred1_1(X13)))&(~p42(esk64_1(X13))|~p41(esk64_1(X13))|~epred1_1(X13)))&(p40(esk64_1(X13))|p41(esk64_1(X13))|~epred1_1(X13)))&(~p41(esk64_1(X13))|~p40(esk64_1(X13))|~epred1_1(X13)))&(p39(esk64_1(X13))|p40(esk64_1(X13))|~epred1_1(X13)))&(~p40(esk64_1(X13))|~p39(esk64_1(X13))|~epred1_1(X13)))&(p38(esk64_1(X13))|p39(esk64_1(X13))|~epred1_1(X13)))&(~p39(esk64_1(X13))|~p38(esk64_1(X13))|~epred1_1(X13)))&(p37(esk64_1(X13))|p38(esk64_1(X13))|~epred1_1(X13)))&(~p38(esk64_1(X13))|~p37(esk64_1(X13))|~epred1_1(X13)))&(p36(esk64_1(X13))|p37(esk64_1(X13))|~epred1_1(X13)))&(~p37(esk64_1(X13))|~p36(esk64_1(X13))|~epred1_1(X13)))&(p35(esk64_1(X13))|p36(esk64_1(X13))|~epred1_1(X13)))&(~p36(esk64_1(X13))|~p35(esk64_1(X13))|~epred1_1(X13)))&(p34(esk64_1(X13))|p35(esk64_1(X13))|~epred1_1(X13)))&(~p35(esk64_1(X13))|~p34(esk64_1(X13))|~epred1_1(X13)))&(p33(esk64_1(X13))|p34(esk64_1(X13))|~epred1_1(X13)))&(~p34(esk64_1(X13))|~p33(esk64_1(X13))|~epred1_1(X13)))&(p32(esk64_1(X13))|p33(esk64_1(X13))|~epred1_1(X13)))&(~p33(esk64_1(X13))|~p32(esk64_1(X13))|~epred1_1(X13)))&(p31(esk64_1(X13))|p32(esk64_1(X13))|~epred1_1(X13)))&(~p32(esk64_1(X13))|~p31(esk64_1(X13))|~epred1_1(X13)))&(p30(esk64_1(X13))|p31(esk64_1(X13))|~epred1_1(X13)))&(~p31(esk64_1(X13))|~p30(esk64_1(X13))|~epred1_1(X13)))&(p29(esk64_1(X13))|p30(esk64_1(X13))|~epred1_1(X13)))&(~p30(esk64_1(X13))|~p29(esk64_1(X13))|~epred1_1(X13)))&(p28(esk64_1(X13))|p29(esk64_1(X13))|~epred1_1(X13)))&(~p29(esk64_1(X13))|~p28(esk64_1(X13))|~epred1_1(X13)))&(p27(esk64_1(X13))|p28(esk64_1(X13))|~epred1_1(X13)))&(~p28(esk64_1(X13))|~p27(esk64_1(X13))|~epred1_1(X13)))&(p26(esk64_1(X13))|p27(esk64_1(X13))|~epred1_1(X13)))&(~p27(esk64_1(X13))|~p26(esk64_1(X13))|~epred1_1(X13)))&(p25(esk64_1(X13))|p26(esk64_1(X13))|~epred1_1(X13)))&(~p26(esk64_1(X13))|~p25(esk64_1(X13))|~epred1_1(X13)))&(p24(esk64_1(X13))|p25(esk64_1(X13))|~epred1_1(X13)))&(~p25(esk64_1(X13))|~p24(esk64_1(X13))|~epred1_1(X13)))&(p23(esk64_1(X13))|p24(esk64_1(X13))|~epred1_1(X13)))&(~p24(esk64_1(X13))|~p23(esk64_1(X13))|~epred1_1(X13)))&(p22(esk64_1(X13))|p23(esk64_1(X13))|~epred1_1(X13)))&(~p23(esk64_1(X13))|~p22(esk64_1(X13))|~epred1_1(X13)))&(p21(esk64_1(X13))|p22(esk64_1(X13))|~epred1_1(X13)))&(~p22(esk64_1(X13))|~p21(esk64_1(X13))|~epred1_1(X13)))&(p20(esk64_1(X13))|p21(esk64_1(X13))|~epred1_1(X13)))&(~p21(esk64_1(X13))|~p20(esk64_1(X13))|~epred1_1(X13)))&(p19(esk64_1(X13))|p20(esk64_1(X13))|~epred1_1(X13)))&(~p20(esk64_1(X13))|~p19(esk64_1(X13))|~epred1_1(X13)))&(p18(esk64_1(X13))|p19(esk64_1(X13))|~epred1_1(X13)))&(~p19(esk64_1(X13))|~p18(esk64_1(X13))|~epred1_1(X13)))&(p17(esk64_1(X13))|p18(esk64_1(X13))|~epred1_1(X13)))&(~p18(esk64_1(X13))|~p17(esk64_1(X13))|~epred1_1(X13)))&(p16(esk64_1(X13))|p17(esk64_1(X13))|~epred1_1(X13)))&(~p17(esk64_1(X13))|~p16(esk64_1(X13))|~epred1_1(X13)))&(p15(esk64_1(X13))|p16(esk64_1(X13))|~epred1_1(X13)))&(~p16(esk64_1(X13))|~p15(esk64_1(X13))|~epred1_1(X13)))&(p14(esk64_1(X13))|p15(esk64_1(X13))|~epred1_1(X13)))&(~p15(esk64_1(X13))|~p14(esk64_1(X13))|~epred1_1(X13)))&(p13(esk64_1(X13))|p14(esk64_1(X13))|~epred1_1(X13)))&(~p14(esk64_1(X13))|~p13(esk64_1(X13))|~epred1_1(X13)))&(p12(esk64_1(X13))|p13(esk64_1(X13))|~epred1_1(X13)))&(~p13(esk64_1(X13))|~p12(esk64_1(X13))|~epred1_1(X13)))&(p11(esk64_1(X13))|p12(esk64_1(X13))|~epred1_1(X13)))&(~p12(esk64_1(X13))|~p11(esk64_1(X13))|~epred1_1(X13)))&(p10(esk64_1(X13))|p11(esk64_1(X13))|~epred1_1(X13)))&(~p11(esk64_1(X13))|~p10(esk64_1(X13))|~epred1_1(X13)))&(p9(esk64_1(X13))|p10(esk64_1(X13))|~epred1_1(X13)))&(~p10(esk64_1(X13))|~p9(esk64_1(X13))|~epred1_1(X13)))&(p8(esk64_1(X13))|p9(esk64_1(X13))|~epred1_1(X13)))&(~p9(esk64_1(X13))|~p8(esk64_1(X13))|~epred1_1(X13)))&(p7(esk64_1(X13))|p8(esk64_1(X13))|~epred1_1(X13)))&(~p8(esk64_1(X13))|~p7(esk64_1(X13))|~epred1_1(X13)))&(p6(esk64_1(X13))|p7(esk64_1(X13))|~epred1_1(X13)))&(~p7(esk64_1(X13))|~p6(esk64_1(X13))|~epred1_1(X13)))&(p5(esk64_1(X13))|p6(esk64_1(X13))|~epred1_1(X13)))&(~p6(esk64_1(X13))|~p5(esk64_1(X13))|~epred1_1(X13)))&(p4(esk64_1(X13))|p5(esk64_1(X13))|~epred1_1(X13)))&(~p5(esk64_1(X13))|~p4(esk64_1(X13))|~epred1_1(X13)))&(p3(esk64_1(X13))|p4(esk64_1(X13))|~epred1_1(X13)))&(~p4(esk64_1(X13))|~p3(esk64_1(X13))|~epred1_1(X13)))&(p2(esk64_1(X13))|p3(esk64_1(X13))|~epred1_1(X13)))&(~p3(esk64_1(X13))|~p2(esk64_1(X13))|~epred1_1(X13)))&(p1(esk64_1(X13))|p2(esk64_1(X13))|~epred1_1(X13)))&(~p2(esk64_1(X13))|~p1(esk64_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.74/0.58 fof(c_0_5, plain, ![X9]:(r1(X9,X9)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.74/0.58 fof(c_0_6, negated_conjecture, ~(~(?[X1]:(~((![X2]:((~r1(X1,X2)|~p60(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.74/0.58 cnf(c_0_7, plain, (p1(X1)|~p2(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.74/0.58 cnf(c_0_8, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.74/0.58 fof(c_0_9, negated_conjecture, ![X8]:((((r1(esk1_0,esk2_0)&p60(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.74/0.58 cnf(c_0_10, plain, (~p2(esk64_1(X1))|~p1(esk64_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.74/0.58 cnf(c_0_11, plain, (p1(X1)|~epred1_1(X1)|~p2(X1)), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 0.74/0.58 cnf(c_0_12, plain, (p2(X1)|~p1(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.74/0.58 cnf(c_0_13, plain, (r1(X1,esk64_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.74/0.58 cnf(c_0_14, plain, (p1(esk64_1(X1))|p2(esk64_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.74/0.58 cnf(c_0_15, negated_conjecture, (epred1_1(X1)|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.74/0.58 cnf(c_0_16, plain, (~epred1_1(esk64_1(X1))|~epred1_1(X1)|~p2(esk64_1(X1))), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 0.74/0.58 cnf(c_0_17, plain, (p2(esk64_1(X1))|~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14])).
% 0.74/0.58 cnf(c_0_18, negated_conjecture, (epred1_1(esk4_0)), inference(spm,[status(thm)],[c_0_15, c_0_8])).
% 0.74/0.58 cnf(c_0_19, plain, (~epred1_1(esk64_1(X1))|~epred1_1(X1)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 0.74/0.58 cnf(c_0_20, negated_conjecture, (epred1_1(esk64_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.74/0.58 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.74/0.58 % SZS output end Proof
% 0.74/0.58 % User time : 0.033 s
% 0.74/0.58 % System time : 0.010 s
% 0.74/0.58 % Total time : 0.043 s
% 0.74/0.58 % User time : 0.038 s
% 0.74/0.58 % System time : 0.014 s
% 0.74/0.58 % Total time : 0.053 s
% 0.74/0.58
%------------------------------------------------------------------------------