%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL686+1.020 : 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 : n020.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 21.62s 8.32s % Output : CNFRefutation 21.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL686+1.020 : 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.10/5.37 % Computer : n020.cluster.edu % 0.10/5.37 % Model : x86_64 x86_64 % 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/5.37 % Memory : 8046.5625MB % 0.10/5.37 % OS : Linux 6.8.0-71-generic % 0.10/5.37 % CPULimit : 300 % 0.10/5.37 % WCLimit : 300 % 0.10/5.37 % DateTime : Fri Sep 25 23:24:55 UTC 2026 % 0.10/5.37 % CPUTime : % 0.10/5.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 21.62/8.32 % SZS status Theorem for theBenchmark.p % 21.62/8.32 % SZS output start CNFRefutation for theBenchmark.p % 21.62/8.32 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 21.62/8.32 fof(main, conjecture, ~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p60(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) | (! [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) | $false)) | ~! [X0] : ((~r1(X1,X0) | ~(((p59(X0) & ~p58(X0)) | (~p59(X0) & p58(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p58(X1) & ~p57(X1)) | (~p58(X1) & p57(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p57(X0) & ~p56(X0)) | (~p57(X0) & p56(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p56(X1) & ~p55(X1)) | (~p56(X1) & p55(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p55(X0) & ~p54(X0)) | (~p55(X0) & p54(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p54(X1) & ~p53(X1)) | (~p54(X1) & p53(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p53(X0) & ~p52(X0)) | (~p53(X0) & p52(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p52(X1) & ~p51(X1)) | (~p52(X1) & p51(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p51(X0) & ~p50(X0)) | (~p51(X0) & p50(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p50(X1) & ~p49(X1)) | (~p50(X1) & p49(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p49(X0) & ~p48(X0)) | (~p49(X0) & p48(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p48(X1) & ~p47(X1)) | (~p48(X1) & p47(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p47(X0) & ~p46(X0)) | (~p47(X0) & p46(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p46(X1) & ~p45(X1)) | (~p46(X1) & p45(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p45(X0) & ~p44(X0)) | (~p45(X0) & p44(X0))))))))) | ~! [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) | p60(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p58(X1) & ~p59(X1)) | ((p59(X1) & p58(X1)) | ((~p57(X1) & ~p58(X1)) | ((p58(X1) & p57(X1)) | ((~p56(X1) & ~p57(X1)) | ((p57(X1) & p56(X1)) | ((~p55(X1) & ~p56(X1)) | ((p56(X1) & p55(X1)) | ((~p54(X1) & ~p55(X1)) | ((p55(X1) & p54(X1)) | ((~p53(X1) & ~p54(X1)) | ((p54(X1) & p53(X1)) | ((~p52(X1) & ~p53(X1)) | ((p53(X1) & p52(X1)) | ((~p51(X1) & ~p52(X1)) | ((p52(X1) & p51(X1)) | ((~p50(X1) & ~p51(X1)) | ((p51(X1) & p50(X1)) | ((~p49(X1) & ~p50(X1)) | ((p50(X1) & p49(X1)) | ((~p48(X1) & ~p49(X1)) | ((p49(X1) & p48(X1)) | ((~p47(X1) & ~p48(X1)) | ((p48(X1) & p47(X1)) | ((~p46(X1) & ~p47(X1)) | ((p47(X1) & p46(X1)) | ((~p45(X1) & ~p46(X1)) | ((p46(X1) & p45(X1)) | ((~p44(X1) & ~p45(X1)) | ((p45(X1) & p44(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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 21.62/8.32 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p60(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) | (! [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) | $false)) | ~! [X0] : ((~r1(X1,X0) | ~(((p59(X0) & ~p58(X0)) | (~p59(X0) & p58(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p58(X1) & ~p57(X1)) | (~p58(X1) & p57(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p57(X0) & ~p56(X0)) | (~p57(X0) & p56(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p56(X1) & ~p55(X1)) | (~p56(X1) & p55(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p55(X0) & ~p54(X0)) | (~p55(X0) & p54(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p54(X1) & ~p53(X1)) | (~p54(X1) & p53(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p53(X0) & ~p52(X0)) | (~p53(X0) & p52(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p52(X1) & ~p51(X1)) | (~p52(X1) & p51(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p51(X0) & ~p50(X0)) | (~p51(X0) & p50(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p50(X1) & ~p49(X1)) | (~p50(X1) & p49(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p49(X0) & ~p48(X0)) | (~p49(X0) & p48(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p48(X1) & ~p47(X1)) | (~p48(X1) & p47(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p47(X0) & ~p46(X0)) | (~p47(X0) & p46(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p46(X1) & ~p45(X1)) | (~p46(X1) & p45(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p45(X0) & ~p44(X0)) | (~p45(X0) & p44(X0))))))))) | ~! [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) | p60(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p58(X1) & ~p59(X1)) | ((p59(X1) & p58(X1)) | ((~p57(X1) & ~p58(X1)) | ((p58(X1) & p57(X1)) | ((~p56(X1) & ~p57(X1)) | ((p57(X1) & p56(X1)) | ((~p55(X1) & ~p56(X1)) | ((p56(X1) & p55(X1)) | ((~p54(X1) & ~p55(X1)) | ((p55(X1) & p54(X1)) | ((~p53(X1) & ~p54(X1)) | ((p54(X1) & p53(X1)) | ((~p52(X1) & ~p53(X1)) | ((p53(X1) & p52(X1)) | ((~p51(X1) & ~p52(X1)) | ((p52(X1) & p51(X1)) | ((~p50(X1) & ~p51(X1)) | ((p51(X1) & p50(X1)) | ((~p49(X1) & ~p50(X1)) | ((p50(X1) & p49(X1)) | ((~p48(X1) & ~p49(X1)) | ((p49(X1) & p48(X1)) | ((~p47(X1) & ~p48(X1)) | ((p48(X1) & p47(X1)) | ((~p46(X1) & ~p47(X1)) | ((p47(X1) & p46(X1)) | ((~p45(X1) & ~p46(X1)) | ((p46(X1) & p45(X1)) | ((~p44(X1) & ~p45(X1)) | ((p45(X1) & p44(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])). % 21.62/8.32 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 21.62/8.32 cnf(c7, plain, ~r1(sK8,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/8.32 cnf(c180, plain, ~X0(X1) | ~r1(X1,X2) | ~p2(X2) | p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/8.32 cnf(c181, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2) | ~p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/8.32 cnf(c184, plain, ~X0(X1) | r1(X1,sK127(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/8.32 cnf(c299, plain, ~X0(X1) | p1(sK127(X1)) | p2(sK127(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/8.32 cnf(c300, plain, ~X0(X1) | ~p2(sK127(X1)) | ~p1(sK127(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/8.32 cnf(d0, plain, p1(X0) | ~'Ts4'(X0) | ~p2(X0), inference(resolution, [status(thm)], [c180,c0])). % 21.62/8.32 cnf(d1, plain, ~'Ts4'(sK8) | 'Ts4'(sK127(sK8)), inference(resolution, [status(thm)], [c184,c7])). % 21.62/8.32 cnf(d2, plain, 'Ts4'(sK8), inference(resolution, [status(thm)], [c7,c0])). % 21.62/8.32 cnf(d3, plain, 'Ts4'(sK127(sK8)), inference(resolution, [status(thm)], [d2,d1])). % 21.62/8.32 cnf(d4, plain, ~p1(X0) | ~'Ts4'(X0) | p2(X0), inference(resolution, [status(thm)], [c181,c0])). % 21.62/8.32 cnf(d5, plain, ~p1(sK127(sK8)) | p2(sK127(sK8)), inference(resolution, [status(thm)], [d4,d3])). % 21.62/8.32 cnf(d6, plain, ~'Ts4'(sK8) | p2(sK127(sK8)) | p2(sK127(sK8)), inference(resolution, [status(thm)], [c299,d5])). % 21.62/8.32 cnf(d7, plain, p2(sK127(sK8)), inference(resolution, [status(thm)], [d2,d6])). % 21.62/8.32 cnf(d8, plain, p1(sK127(sK8)) | ~'Ts4'(sK127(sK8)), inference(resolution, [status(thm)], [d7,d0])). % 21.62/8.32 cnf(d9, plain, p1(sK127(sK8)), inference(resolution, [status(thm)], [d3,d8])). % 21.62/8.32 cnf(d10, plain, ~p1(sK127(sK8)) | ~'Ts4'(sK8), inference(resolution, [status(thm)], [d7,c300])). % 21.62/8.32 cnf(d11, plain, ~p1(sK127(sK8)), inference(resolution, [status(thm)], [d2,d10])). % 21.62/8.32 cnf(d12, plain, $false, inference(resolution, [status(thm)], [d11,d9])). % 21.62/8.32 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------