%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n009.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 : Sun Sep 27 07:55:15 AM UTC 2026 % Result : Theorem 13.93s 2.79s % Output : CNFRefutation 13.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n009.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Fri Sep 25 23:23:28 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 13.93/2.79 % SZS status Theorem for theBenchmark.p % 13.93/2.79 % SZS output start CNFRefutation for theBenchmark.p % 13.93/2.79 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 13.93/2.79 fof(main, conjecture, ~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p45(X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0)))))) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~((! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | $false)) | ~! [X1] : ((~r1(X0,X1) | ~(((p44(X1) & ~p43(X1)) | (~p44(X1) & p43(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p43(X0) & ~p42(X0)) | (~p43(X0) & p42(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p42(X1) & ~p41(X1)) | (~p42(X1) & p41(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p41(X0) & ~p40(X0)) | (~p41(X0) & p40(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p40(X1) & ~p39(X1)) | (~p40(X1) & p39(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p39(X0) & ~p38(X0)) | (~p39(X0) & p38(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p38(X1) & ~p37(X1)) | (~p38(X1) & p37(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p37(X0) & ~p36(X0)) | (~p37(X0) & p36(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p36(X1) & ~p35(X1)) | (~p36(X1) & p35(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p35(X0) & ~p34(X0)) | (~p35(X0) & p34(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p34(X1) & ~p33(X1)) | (~p34(X1) & p33(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p33(X0) & ~p32(X0)) | (~p33(X0) & p32(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p32(X1) & ~p31(X1)) | (~p32(X1) & p31(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p31(X0) & ~p30(X0)) | (~p31(X0) & p30(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p30(X1) & ~p29(X1)) | (~p30(X1) & p29(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p29(X0) & ~p28(X0)) | (~p29(X0) & p28(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p28(X1) & ~p27(X1)) | (~p28(X1) & p27(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p27(X0) & ~p26(X0)) | (~p27(X0) & p26(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p26(X1) & ~p25(X1)) | (~p26(X1) & p25(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p25(X0) & ~p24(X0)) | (~p25(X0) & p24(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p24(X1) & ~p23(X1)) | (~p24(X1) & p23(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p23(X0) & ~p22(X0)) | (~p23(X0) & p22(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p22(X1) & ~p21(X1)) | (~p22(X1) & p21(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p21(X0) & ~p20(X0)) | (~p21(X0) & p20(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p20(X1) & ~p19(X1)) | (~p20(X1) & p19(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p19(X0) & ~p18(X0)) | (~p19(X0) & p18(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p18(X1) & ~p17(X1)) | (~p18(X1) & p17(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p17(X0) & ~p16(X0)) | (~p17(X0) & p16(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p16(X1) & ~p15(X1)) | (~p16(X1) & p15(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p15(X0) & ~p14(X0)) | (~p15(X0) & p14(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p14(X1) & ~p13(X1)) | (~p14(X1) & p13(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p13(X0) & ~p12(X0)) | (~p13(X0) & p12(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p12(X1) & ~p11(X1)) | (~p12(X1) & p11(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p11(X0) & ~p10(X0)) | (~p11(X0) & p10(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p10(X1) & ~p9(X1)) | (~p10(X1) & p9(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p9(X0) & ~p8(X0)) | (~p9(X0) & p8(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p8(X1) & ~p7(X1)) | (~p8(X1) & p7(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p7(X0) & ~p6(X0)) | (~p7(X0) & p6(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p6(X1) & ~p5(X1)) | (~p6(X1) & p5(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p5(X0) & ~p4(X0)) | (~p5(X0) & p4(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p4(X1) & ~p3(X1)) | (~p4(X1) & p3(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p3(X0) & ~p2(X0)) | (~p3(X0) & p2(X0))))))))) | (~! [X1] : ((~r1(X0,X1) | ~(((p2(X1) & ~p1(X1)) | (~p2(X1) & p1(X1)))))) | (! [X1] : ((~r1(X0,X1) | p45(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p43(X1) & ~p44(X1)) | ((p44(X1) & p43(X1)) | ((~p42(X1) & ~p43(X1)) | ((p43(X1) & p42(X1)) | ((~p41(X1) & ~p42(X1)) | ((p42(X1) & p41(X1)) | ((~p40(X1) & ~p41(X1)) | ((p41(X1) & p40(X1)) | ((~p39(X1) & ~p40(X1)) | ((p40(X1) & p39(X1)) | ((~p38(X1) & ~p39(X1)) | ((p39(X1) & p38(X1)) | ((~p37(X1) & ~p38(X1)) | ((p38(X1) & p37(X1)) | ((~p36(X1) & ~p37(X1)) | ((p37(X1) & p36(X1)) | ((~p35(X1) & ~p36(X1)) | ((p36(X1) & p35(X1)) | ((~p34(X1) & ~p35(X1)) | ((p35(X1) & p34(X1)) | ((~p33(X1) & ~p34(X1)) | ((p34(X1) & p33(X1)) | ((~p32(X1) & ~p33(X1)) | ((p33(X1) & p32(X1)) | ((~p31(X1) & ~p32(X1)) | ((p32(X1) & p31(X1)) | ((~p30(X1) & ~p31(X1)) | ((p31(X1) & p30(X1)) | ((~p29(X1) & ~p30(X1)) | ((p30(X1) & p29(X1)) | ((~p28(X1) & ~p29(X1)) | ((p29(X1) & p28(X1)) | ((~p27(X1) & ~p28(X1)) | ((p28(X1) & p27(X1)) | ((~p26(X1) & ~p27(X1)) | ((p27(X1) & p26(X1)) | ((~p25(X1) & ~p26(X1)) | ((p26(X1) & p25(X1)) | ((~p24(X1) & ~p25(X1)) | ((p25(X1) & p24(X1)) | ((~p23(X1) & ~p24(X1)) | ((p24(X1) & p23(X1)) | ((~p22(X1) & ~p23(X1)) | ((p23(X1) & p22(X1)) | ((~p21(X1) & ~p22(X1)) | ((p22(X1) & p21(X1)) | ((~p20(X1) & ~p21(X1)) | ((p21(X1) & p20(X1)) | ((~p19(X1) & ~p20(X1)) | ((p20(X1) & p19(X1)) | ((~p18(X1) & ~p19(X1)) | ((p19(X1) & p18(X1)) | ((~p17(X1) & ~p18(X1)) | ((p18(X1) & p17(X1)) | ((~p16(X1) & ~p17(X1)) | ((p17(X1) & p16(X1)) | ((~p15(X1) & ~p16(X1)) | ((p16(X1) & p15(X1)) | ((~p14(X1) & ~p15(X1)) | ((p15(X1) & p14(X1)) | ((~p13(X1) & ~p14(X1)) | ((p14(X1) & p13(X1)) | ((~p12(X1) & ~p13(X1)) | ((p13(X1) & p12(X1)) | ((~p11(X1) & ~p12(X1)) | ((p12(X1) & p11(X1)) | ((~p10(X1) & ~p11(X1)) | ((p11(X1) & p10(X1)) | ((~p9(X1) & ~p10(X1)) | ((p10(X1) & p9(X1)) | ((~p8(X1) & ~p9(X1)) | ((p9(X1) & p8(X1)) | ((~p7(X1) & ~p8(X1)) | ((p8(X1) & p7(X1)) | ((~p6(X1) & ~p7(X1)) | ((p7(X1) & p6(X1)) | ((~p5(X1) & ~p6(X1)) | ((p6(X1) & p5(X1)) | ((~p4(X1) & ~p5(X1)) | ((p5(X1) & p4(X1)) | ((~p3(X1) & ~p4(X1)) | ((p4(X1) & p3(X1)) | ((~p2(X1) & ~p3(X1)) | ((p3(X1) & p2(X1)) | ((~p1(X1) & ~p2(X1)) | (p2(X1) & p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 13.93/2.79 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p45(X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0)))))) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~((! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | $false)) | ~! [X1] : ((~r1(X0,X1) | ~(((p44(X1) & ~p43(X1)) | (~p44(X1) & p43(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p43(X0) & ~p42(X0)) | (~p43(X0) & p42(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p42(X1) & ~p41(X1)) | (~p42(X1) & p41(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p41(X0) & ~p40(X0)) | (~p41(X0) & p40(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p40(X1) & ~p39(X1)) | (~p40(X1) & p39(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p39(X0) & ~p38(X0)) | (~p39(X0) & p38(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p38(X1) & ~p37(X1)) | (~p38(X1) & p37(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p37(X0) & ~p36(X0)) | (~p37(X0) & p36(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p36(X1) & ~p35(X1)) | (~p36(X1) & p35(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p35(X0) & ~p34(X0)) | (~p35(X0) & p34(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p34(X1) & ~p33(X1)) | (~p34(X1) & p33(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p33(X0) & ~p32(X0)) | (~p33(X0) & p32(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p32(X1) & ~p31(X1)) | (~p32(X1) & p31(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p31(X0) & ~p30(X0)) | (~p31(X0) & p30(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p30(X1) & ~p29(X1)) | (~p30(X1) & p29(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p29(X0) & ~p28(X0)) | (~p29(X0) & p28(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p28(X1) & ~p27(X1)) | (~p28(X1) & p27(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p27(X0) & ~p26(X0)) | (~p27(X0) & p26(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p26(X1) & ~p25(X1)) | (~p26(X1) & p25(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p25(X0) & ~p24(X0)) | (~p25(X0) & p24(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p24(X1) & ~p23(X1)) | (~p24(X1) & p23(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p23(X0) & ~p22(X0)) | (~p23(X0) & p22(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p22(X1) & ~p21(X1)) | (~p22(X1) & p21(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p21(X0) & ~p20(X0)) | (~p21(X0) & p20(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p20(X1) & ~p19(X1)) | (~p20(X1) & p19(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p19(X0) & ~p18(X0)) | (~p19(X0) & p18(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p18(X1) & ~p17(X1)) | (~p18(X1) & p17(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p17(X0) & ~p16(X0)) | (~p17(X0) & p16(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p16(X1) & ~p15(X1)) | (~p16(X1) & p15(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p15(X0) & ~p14(X0)) | (~p15(X0) & p14(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p14(X1) & ~p13(X1)) | (~p14(X1) & p13(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p13(X0) & ~p12(X0)) | (~p13(X0) & p12(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p12(X1) & ~p11(X1)) | (~p12(X1) & p11(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p11(X0) & ~p10(X0)) | (~p11(X0) & p10(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p10(X1) & ~p9(X1)) | (~p10(X1) & p9(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p9(X0) & ~p8(X0)) | (~p9(X0) & p8(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p8(X1) & ~p7(X1)) | (~p8(X1) & p7(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p7(X0) & ~p6(X0)) | (~p7(X0) & p6(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p6(X1) & ~p5(X1)) | (~p6(X1) & p5(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p5(X0) & ~p4(X0)) | (~p5(X0) & p4(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p4(X1) & ~p3(X1)) | (~p4(X1) & p3(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p3(X0) & ~p2(X0)) | (~p3(X0) & p2(X0))))))))) | (~! [X1] : ((~r1(X0,X1) | ~(((p2(X1) & ~p1(X1)) | (~p2(X1) & p1(X1)))))) | (! [X1] : ((~r1(X0,X1) | p45(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p43(X1) & ~p44(X1)) | ((p44(X1) & p43(X1)) | ((~p42(X1) & ~p43(X1)) | ((p43(X1) & p42(X1)) | ((~p41(X1) & ~p42(X1)) | ((p42(X1) & p41(X1)) | ((~p40(X1) & ~p41(X1)) | ((p41(X1) & p40(X1)) | ((~p39(X1) & ~p40(X1)) | ((p40(X1) & p39(X1)) | ((~p38(X1) & ~p39(X1)) | ((p39(X1) & p38(X1)) | ((~p37(X1) & ~p38(X1)) | ((p38(X1) & p37(X1)) | ((~p36(X1) & ~p37(X1)) | ((p37(X1) & p36(X1)) | ((~p35(X1) & ~p36(X1)) | ((p36(X1) & p35(X1)) | ((~p34(X1) & ~p35(X1)) | ((p35(X1) & p34(X1)) | ((~p33(X1) & ~p34(X1)) | ((p34(X1) & p33(X1)) | ((~p32(X1) & ~p33(X1)) | ((p33(X1) & p32(X1)) | ((~p31(X1) & ~p32(X1)) | ((p32(X1) & p31(X1)) | ((~p30(X1) & ~p31(X1)) | ((p31(X1) & p30(X1)) | ((~p29(X1) & ~p30(X1)) | ((p30(X1) & p29(X1)) | ((~p28(X1) & ~p29(X1)) | ((p29(X1) & p28(X1)) | ((~p27(X1) & ~p28(X1)) | ((p28(X1) & p27(X1)) | ((~p26(X1) & ~p27(X1)) | ((p27(X1) & p26(X1)) | ((~p25(X1) & ~p26(X1)) | ((p26(X1) & p25(X1)) | ((~p24(X1) & ~p25(X1)) | ((p25(X1) & p24(X1)) | ((~p23(X1) & ~p24(X1)) | ((p24(X1) & p23(X1)) | ((~p22(X1) & ~p23(X1)) | ((p23(X1) & p22(X1)) | ((~p21(X1) & ~p22(X1)) | ((p22(X1) & p21(X1)) | ((~p20(X1) & ~p21(X1)) | ((p21(X1) & p20(X1)) | ((~p19(X1) & ~p20(X1)) | ((p20(X1) & p19(X1)) | ((~p18(X1) & ~p19(X1)) | ((p19(X1) & p18(X1)) | ((~p17(X1) & ~p18(X1)) | ((p18(X1) & p17(X1)) | ((~p16(X1) & ~p17(X1)) | ((p17(X1) & p16(X1)) | ((~p15(X1) & ~p16(X1)) | ((p16(X1) & p15(X1)) | ((~p14(X1) & ~p15(X1)) | ((p15(X1) & p14(X1)) | ((~p13(X1) & ~p14(X1)) | ((p14(X1) & p13(X1)) | ((~p12(X1) & ~p13(X1)) | ((p13(X1) & p12(X1)) | ((~p11(X1) & ~p12(X1)) | ((p12(X1) & p11(X1)) | ((~p10(X1) & ~p11(X1)) | ((p11(X1) & p10(X1)) | ((~p9(X1) & ~p10(X1)) | ((p10(X1) & p9(X1)) | ((~p8(X1) & ~p9(X1)) | ((p9(X1) & p8(X1)) | ((~p7(X1) & ~p8(X1)) | ((p8(X1) & p7(X1)) | ((~p6(X1) & ~p7(X1)) | ((p7(X1) & p6(X1)) | ((~p5(X1) & ~p6(X1)) | ((p6(X1) & p5(X1)) | ((~p4(X1) & ~p5(X1)) | ((p5(X1) & p4(X1)) | ((~p3(X1) & ~p4(X1)) | ((p4(X1) & p3(X1)) | ((~p2(X1) & ~p3(X1)) | ((p3(X1) & p2(X1)) | ((~p1(X1) & ~p2(X1)) | (p2(X1) & p1(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 13.93/2.79 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 13.93/2.79 cnf(c7, plain, ~r1(sK8,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 13.93/2.79 cnf(c135, plain, ~X0(X1) | ~r1(X1,X2) | ~p2(X2) | p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 13.93/2.79 cnf(c136, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2) | ~p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 13.93/2.79 cnf(c139, plain, ~X0(X1) | r1(X1,sK97(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.93/2.79 cnf(c224, plain, ~X0(X1) | p1(sK97(X1)) | p2(sK97(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.93/2.79 cnf(c225, plain, ~X0(X1) | ~p2(sK97(X1)) | ~p1(sK97(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.93/2.79 cnf(d0, plain, p1(X0) | ~'Ts4'(X0) | ~p2(X0), inference(resolution, [status(thm)], [c135,c0])). % 13.93/2.79 cnf(d1, plain, ~'Ts4'(sK8) | 'Ts4'(sK97(sK8)), inference(resolution, [status(thm)], [c139,c7])). % 13.93/2.79 cnf(d2, plain, 'Ts4'(sK8), inference(resolution, [status(thm)], [c7,c0])). % 13.93/2.79 cnf(d3, plain, 'Ts4'(sK97(sK8)), inference(resolution, [status(thm)], [d2,d1])). % 13.93/2.79 cnf(d4, plain, ~p1(X0) | ~'Ts4'(X0) | p2(X0), inference(resolution, [status(thm)], [c136,c0])). % 13.93/2.79 cnf(d5, plain, ~p1(sK97(sK8)) | p2(sK97(sK8)), inference(resolution, [status(thm)], [d4,d3])). % 13.93/2.79 cnf(d6, plain, ~'Ts4'(sK8) | p2(sK97(sK8)) | p2(sK97(sK8)), inference(resolution, [status(thm)], [c224,d5])). % 13.93/2.79 cnf(d7, plain, p2(sK97(sK8)), inference(resolution, [status(thm)], [d2,d6])). % 13.93/2.79 cnf(d8, plain, p1(sK97(sK8)) | ~'Ts4'(sK97(sK8)), inference(resolution, [status(thm)], [d7,d0])). % 13.93/2.79 cnf(d9, plain, p1(sK97(sK8)), inference(resolution, [status(thm)], [d3,d8])). % 13.93/2.79 cnf(d10, plain, ~p1(sK97(sK8)) | ~'Ts4'(sK8), inference(resolution, [status(thm)], [d7,c225])). % 13.93/2.79 cnf(d11, plain, ~p1(sK97(sK8)), inference(resolution, [status(thm)], [d2,d10])). % 13.93/2.79 cnf(d12, plain, $false, inference(resolution, [status(thm)], [d11,d9])). % 13.93/2.79 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------