%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL660+1.001 : 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:04 AM UTC 2026 % Result : Theorem 97.56s 54.26s % Output : CNFRefutation 97.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : LCL660+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/10.45 % Computer : n020.cluster.edu % 0.18/10.45 % Model : x86_64 x86_64 % 0.18/10.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/10.45 % Memory : 8046.5625MB % 0.18/10.45 % OS : Linux 6.8.0-71-generic % 0.18/10.45 % CPULimit : 300 % 0.18/10.45 % WCLimit : 300 % 0.18/10.45 % DateTime : Fri Sep 25 23:05:16 UTC 2026 % 0.18/10.45 % CPUTime : % 0.18/10.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 97.56/54.26 % SZS status Theorem for theBenchmark.p % 97.56/54.26 % SZS output start CNFRefutation for theBenchmark.p % 97.56/54.26 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 97.56/54.26 fof(main, conjecture, ~? [X0] : ~(((~! [X1] : ((~r1(X0,X1) | ~p3(X1))) & (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | (! [X1] : ((~r1(X0,X1) | p4(X1))) | (~! [X1] : ((~r1(X0,X1) | (p4(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p4(X1))) | ~p4(X0))))))) | ((~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~p3(X0))))) & (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | (~! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~p1(X0))))))) | ~(((((! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1))))))))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))))) & (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))) | ~! [X1] : ((~r1(X0,X1) | (((! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | ~! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))) & (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ((! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | ~! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))) & (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))))) | ~(((! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1))))))))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))))) & (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))))))))) & ! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))))))))))))))). % 97.56/54.26 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~(((~! [X1] : ((~r1(X0,X1) | ~p3(X1))) & (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | (! [X1] : ((~r1(X0,X1) | p4(X1))) | (~! [X1] : ((~r1(X0,X1) | (p4(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p4(X1))) | ~p4(X0))))))) | ((~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~p3(X0))))) & (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | (~! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~p1(X0))))))) | ~(((((! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1))))))))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))))) & (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))) | ~! [X1] : ((~r1(X0,X1) | (((! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | ~! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))) & (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ((! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0))))))))) | ~! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))) & (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))))) | ~(((! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1))))))))) | ~! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p2(X1))) | ~p2(X0)))))))) & (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1)))))))))))))) & ! [X1] : ((~r1(X0,X1) | (p2(X1) | ~! [X0] : ((~r1(X1,X0) | (p2(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p2(X0))) | ~p2(X1))))))))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 97.56/54.26 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 97.56/54.26 cnf(c1, plain, ~r1(sK10,X0) | ~p3(X0) | ~X1(sK10), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c8, plain, ~r1(sK10,X0) | r1(X0,sK17(X0)) | ~X1(sK10), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c9, plain, ~r1(sK10,X0) | p3(sK17(X0)) | ~X1(sK10), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c16, plain, X0(sK10) | X1(sK10), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c17, plain, ~r1(sK10,X0) | p2(X0) | r1(X0,sK23(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c18, plain, ~r1(sK10,X0) | p2(X0) | ~p2(sK23(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c19, plain, p2(X0) | ~p2(X1) | ~r1(X1,X0) | p2(X2) | ~r1(sK23(X2),X1) | ~r1(sK10,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c20, plain, X0(X1) | r1(X1,sK26(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c21, plain, X0(X1) | ~p2(sK26(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c22, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(X2,sK28(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c23, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(sK28(X2),sK29(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c24, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | ~p2(sK29(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c25, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | p2(sK28(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c26, plain, X0(X1) | r1(X1,sK30(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c27, plain, X0(X1) | ~p2(sK30(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c28, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(X2,sK32(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c29, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(sK32(X2),sK33(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c30, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | ~p2(sK33(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c31, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | p2(sK32(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c32, plain, p2(X0) | ~X1(X2) | ~r1(X3,X0) | r1(X0,sK36(X0)) | ~r1(X2,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c33, plain, p2(X0) | r1(sK36(X0),sK37(X0)) | ~X1(X2) | ~r1(X3,X0) | ~r1(X2,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c34, plain, p2(X0) | ~X1(X2) | ~p2(sK37(X0)) | ~r1(X3,X0) | ~r1(X2,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c35, plain, p2(X0) | ~X1(X2) | ~r1(X3,X0) | p2(sK36(X0)) | ~r1(X2,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c36, plain, X0(X1) | r1(X1,sK38(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c37, plain, X0(X1) | r1(sK38(X1),sK39(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c38, plain, X0(X1) | ~p2(sK39(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c39, plain, p2(X0) | X1(X2) | ~r1(sK39(X2),X3) | ~p2(X3) | ~r1(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c40, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(X2,sK43(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c41, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(sK43(X2),sK44(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c42, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | ~p2(sK44(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c43, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | p2(sK43(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c51, plain, ~X0(X1) | p2(X1) | r1(X1,sK52(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c52, plain, ~X0(X1) | p2(X1) | r1(sK52(X1),sK53(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c53, plain, ~X0(X1) | p2(X1) | ~p2(sK53(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c54, plain, ~X0(X1) | p2(X1) | p2(sK52(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c59, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(X2,sK59(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c60, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | r1(sK59(X2),sK60(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c61, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | ~p2(sK60(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c62, plain, X0(X1) | ~r1(X1,X2) | p2(X2) | p2(sK59(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c63, plain, ~X0(X1) | X2(X1) | r1(X1,sK61(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c64, plain, ~X0(X1) | X2(X1) | ~p2(sK61(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c65, plain, ~X0(X1) | X2(X1) | p2(X3) | ~p2(X4) | ~r1(X4,X3) | ~r1(sK61(X1),X4), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c70, plain, ~X0(X1) | r1(X1,sK66(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c71, plain, ~X0(X1) | ~X2(sK66(X1)) | ~p2(sK66(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c72, plain, ~r1(sK66(X0),X1) | ~X2(sK66(X0)) | ~p2(X1) | p2(X3) | ~r1(X1,X3) | ~X4(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c73, plain, ~p2(X0) | ~r1(X0,X1) | ~X2(X3) | X4(X1) | ~r1(sK66(X3),X0) | ~X5(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(c74, plain, p2(X0) | ~r1(X1,X0) | ~r1(X2,X3) | ~r1(X2,X1) | ~p2(X1) | ~X4(X5) | X6(X3) | ~r1(sK66(X5),X2) | ~X7(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 97.56/54.26 cnf(d0, plain, ~'Ts8'(X0) | 'Ts3'(X0) | 'Ts1'(X0) | p2(sK61(X0)) | p2(sK28(sK61(X0))), inference(resolution, [status(thm)], [c63,c25])). % 97.56/54.26 cnf(d1, plain, ~'Ts8'(X0) | 'Ts3'(X0) | r1(sK28(sK61(X0)),sK29(sK61(X0))) | 'Ts1'(X0) | p2(sK61(X0)), inference(resolution, [status(thm)], [c63,c23])). % 97.56/54.26 cnf(d2, plain, ~'Ts8'(X0) | 'Ts3'(X0) | r1(sK61(X0),sK28(sK61(X0))) | 'Ts1'(X0) | p2(sK61(X0)), inference(resolution, [status(thm)], [c63,c22])). % 97.56/54.26 cnf(d3, plain, 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0) | ~r1(sK28(sK61(X0)),X1) | ~'Ts8'(X0) | p2(X1) | ~p2(sK28(sK61(X0))) | 'Ts3'(X0), inference(resolution, [status(thm)], [d2,c65])). % 97.56/54.26 cnf(d4, plain, 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK29(sK61(X0))) | ~p2(sK28(sK61(X0))) | p2(sK61(X0)) | 'Ts3'(X0) | 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0), inference(resolution, [status(thm)], [d3,d1])). % 97.56/54.26 cnf(d5, plain, 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK29(sK61(X0))) | p2(sK61(X0)) | 'Ts3'(X0) | 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0), inference(resolution, [status(thm)], [d4,d0])). % 97.56/54.26 cnf(d6, plain, 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0) | ~r1(X1,sK61(X0)) | 'Ts1'(X1) | p2(sK61(X0)), inference(resolution, [status(thm)], [d5,c24])). % 97.56/54.26 cnf(d7, plain, 'Ts1'(X0) | 'Ts1'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0) | ~'Ts8'(X0) | 'Ts3'(X0), inference(resolution, [status(thm)], [d6,c63])). % 97.56/54.26 cnf(d8, plain, 'Ts1'(X0) | ~'Ts8'(X0) | 'Ts3'(X0) | ~'Ts8'(X0) | 'Ts3'(X0), inference(resolution, [status(thm)], [d7,c64])). % 97.56/54.26 cnf(d9, plain, ~'Ts9'(X0) | 'Ts1'(X0) | p2(sK66(X0)) | p2(sK28(sK66(X0))), inference(resolution, [status(thm)], [c70,c25])). % 97.56/54.26 cnf(d10, plain, ~'Ts9'(X0) | r1(sK28(sK66(X0)),sK29(sK66(X0))) | 'Ts1'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [c70,c23])). % 97.56/54.26 cnf(d11, plain, ~'Ts9'(X0) | r1(sK66(X0),sK28(sK66(X0))) | 'Ts1'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [c70,c22])). % 97.56/54.26 cnf(d12, plain, 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK66(X0)) | ~r1(sK28(sK66(X0)),X1) | ~'Ts9'(X0) | p2(X1) | ~p2(sK28(sK66(X0))) | ~'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d11,c72])). % 97.56/54.26 cnf(d13, plain, 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK29(sK66(X0))) | ~p2(sK28(sK66(X0))) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [d12,d10])). % 97.56/54.26 cnf(d14, plain, 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK29(sK66(X0))) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [d13,d9])). % 97.56/54.26 cnf(d15, plain, 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | ~r1(X1,sK66(X0)) | 'Ts1'(X1) | p2(sK66(X0)), inference(resolution, [status(thm)], [d14,c24])). % 97.56/54.26 cnf(d16, plain, 'Ts1'(X0) | 'Ts1'(X0) | ~'Ts9'(X0) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | ~'Ts9'(X0), inference(resolution, [status(thm)], [d15,c70])). % 97.56/54.26 cnf(d17, plain, p2(sK23(X0)) | p2(sK43(sK23(X0))) | 'Ts4'(X0) | ~r1(sK10,X0) | p2(X0), inference(resolution, [status(thm)], [c43,c17])). % 97.56/54.26 cnf(d18, plain, r1(sK43(sK23(X0)),sK44(sK23(X0))) | p2(sK23(X0)) | 'Ts4'(X0) | ~r1(sK10,X0) | p2(X0), inference(resolution, [status(thm)], [c41,c17])). % 97.56/54.26 cnf(d19, plain, r1(sK23(X0),sK43(sK23(X0))) | p2(sK23(X0)) | 'Ts4'(X0) | ~r1(sK10,X0) | p2(X0), inference(resolution, [status(thm)], [c40,c17])). % 97.56/54.26 cnf(d20, plain, ~r1(sK10,X0) | p2(X0) | p2(sK23(X0)) | 'Ts4'(X0) | ~r1(sK43(sK23(X0)),X1) | ~r1(sK10,X0) | p2(X1) | ~p2(sK43(sK23(X0))) | p2(X0), inference(resolution, [status(thm)], [d19,c19])). % 97.56/54.26 cnf(d21, plain, ~r1(sK10,X0) | p2(sK44(sK23(X0))) | p2(X0) | p2(sK23(X0)) | ~p2(sK43(sK23(X0))) | 'Ts4'(X0) | ~r1(sK10,X0) | p2(X0) | p2(sK23(X0)) | 'Ts4'(X0), inference(resolution, [status(thm)], [d20,d18])). % 97.56/54.26 cnf(d22, plain, ~r1(sK10,X0) | p2(X0) | p2(sK23(X0)) | p2(sK44(sK23(X0))) | 'Ts4'(X0) | ~r1(sK10,X0) | p2(X0) | p2(sK23(X0)) | 'Ts4'(X0), inference(resolution, [status(thm)], [d21,d17])). % 97.56/54.26 cnf(d23, plain, ~r1(sK10,X0) | p2(X0) | p2(sK23(X0)) | 'Ts4'(X0) | ~r1(X1,sK23(X0)) | p2(sK23(X0)) | 'Ts4'(X1), inference(resolution, [status(thm)], [d22,c42])). % 97.56/54.26 cnf(d24, plain, ~r1(sK10,X0) | p2(X0) | p2(sK23(X0)) | 'Ts4'(X0) | 'Ts4'(X0) | ~r1(sK10,X0) | p2(X0), inference(resolution, [status(thm)], [d23,c17])). % 97.56/54.26 cnf(d25, plain, p2(sK66(sK10)) | p2(sK23(sK66(sK10))) | 'Ts4'(sK66(sK10)) | ~'Ts9'(sK10), inference(resolution, [status(thm)], [d24,c70])). % 97.56/54.26 cnf(d26, plain, ~'Ts9'(sK10) | p2(sK66(sK10)) | 'Ts4'(sK66(sK10)) | ~r1(sK10,sK66(sK10)) | p2(sK66(sK10)), inference(resolution, [status(thm)], [d25,c18])). % 97.56/54.26 cnf(d27, plain, ~'Ts9'(sK10) | p2(sK66(sK10)) | 'Ts4'(sK66(sK10)) | ~'Ts9'(sK10), inference(resolution, [status(thm)], [d26,c70])). % 97.56/54.26 cnf(d28, plain, ~'Ts9'(sK10) | p2(sK66(sK10)) | 'Ts1'(sK10) | ~'Ts9'(sK10) | p2(sK66(sK10)), inference(resolution, [status(thm)], [d27,d16])). % 97.56/54.26 cnf(d29, plain, p2(sK39(X0)) | ~'Ts6'(sK39(X0)) | ~r1(sK52(sK39(X0)),X1) | p2(X1) | ~p2(sK52(sK39(X0))) | 'Ts4'(X0), inference(resolution, [status(thm)], [c51,c39])). % 97.56/54.26 cnf(d30, plain, p2(sK53(sK39(X0))) | p2(sK39(X0)) | ~p2(sK52(sK39(X0))) | 'Ts4'(X0) | ~'Ts6'(sK39(X0)) | p2(sK39(X0)) | ~'Ts6'(sK39(X0)), inference(resolution, [status(thm)], [d29,c52])). % 97.56/54.26 cnf(d31, plain, p2(sK39(X0)) | p2(sK53(sK39(X0))) | 'Ts4'(X0) | ~'Ts6'(sK39(X0)) | p2(sK39(X0)) | ~'Ts6'(sK39(X0)), inference(resolution, [status(thm)], [d30,c54])). % 97.56/54.26 cnf(d32, plain, p2(sK39(X0)) | 'Ts4'(X0) | ~'Ts6'(sK39(X0)) | p2(sK39(X0)) | ~'Ts6'(sK39(X0)), inference(resolution, [status(thm)], [d31,c53])). % 97.56/54.26 cnf(d33, plain, ~r1(sK38(sK66(X0)),X1) | ~'Ts9'(X0) | ~p2(sK38(sK66(X0))) | 'Ts6'(X1) | ~'Ts7'(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [c73,c36])). % 97.56/54.26 cnf(d34, plain, ~'Ts9'(X0) | ~p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | ~'Ts7'(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d33,c37])). % 97.56/54.26 cnf(d35, plain, p2(sK39(X0)) | p2(sK59(sK39(X0))) | 'Ts7'(sK38(X0)) | 'Ts4'(X0), inference(resolution, [status(thm)], [c62,c37])). % 97.56/54.26 cnf(d36, plain, r1(sK59(sK39(X0)),sK60(sK39(X0))) | p2(sK39(X0)) | 'Ts7'(sK38(X0)) | 'Ts4'(X0), inference(resolution, [status(thm)], [c60,c37])). % 97.56/54.26 cnf(d37, plain, r1(sK39(X0),sK59(sK39(X0))) | p2(sK39(X0)) | 'Ts7'(sK38(X0)) | 'Ts4'(X0), inference(resolution, [status(thm)], [c59,c37])). % 97.56/54.26 cnf(d38, plain, p2(sK39(X0)) | 'Ts4'(X0) | 'Ts7'(sK38(X0)) | ~r1(sK59(sK39(X0)),X1) | p2(X1) | ~p2(sK59(sK39(X0))) | 'Ts4'(X0), inference(resolution, [status(thm)], [d37,c39])). % 97.56/54.26 cnf(d39, plain, p2(sK60(sK39(X0))) | p2(sK39(X0)) | ~p2(sK59(sK39(X0))) | 'Ts4'(X0) | 'Ts7'(sK38(X0)) | p2(sK39(X0)) | 'Ts4'(X0) | 'Ts7'(sK38(X0)), inference(resolution, [status(thm)], [d38,d36])). % 97.56/54.26 cnf(d40, plain, p2(sK39(X0)) | p2(sK60(sK39(X0))) | 'Ts4'(X0) | 'Ts7'(sK38(X0)) | p2(sK39(X0)) | 'Ts4'(X0) | 'Ts7'(sK38(X0)), inference(resolution, [status(thm)], [d39,d35])). % 97.56/54.26 cnf(d41, plain, p2(sK39(X0)) | 'Ts4'(X0) | 'Ts7'(sK38(X0)) | ~r1(X1,sK39(X0)) | p2(sK39(X0)) | 'Ts7'(X1), inference(resolution, [status(thm)], [d40,c61])). % 97.56/54.26 cnf(d42, plain, p2(sK39(X0)) | 'Ts4'(X0) | 'Ts7'(sK38(X0)) | 'Ts7'(sK38(X0)) | 'Ts4'(X0), inference(resolution, [status(thm)], [d41,c37])). % 97.56/54.26 cnf(d43, plain, p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)) | ~'Ts9'(X0) | ~p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))), inference(resolution, [status(thm)], [d42,d34])). % 97.56/54.26 cnf(d44, plain, p2(sK38(X0)) | p2(sK43(sK38(X0))) | 'Ts4'(X0) | 'Ts4'(X0), inference(resolution, [status(thm)], [c43,c36])). % 97.56/54.26 cnf(d45, plain, r1(sK43(sK38(X0)),sK44(sK38(X0))) | p2(sK38(X0)) | 'Ts4'(X0) | 'Ts4'(X0), inference(resolution, [status(thm)], [c41,c36])). % 97.56/54.26 cnf(d46, plain, r1(sK38(X0),sK43(sK38(X0))) | p2(sK38(X0)) | 'Ts4'(X0) | 'Ts4'(X0), inference(resolution, [status(thm)], [c40,c36])). % 97.56/54.26 cnf(d47, plain, ~r1(sK38(sK66(X0)),X1) | ~r1(sK38(sK66(X0)),X2) | ~r1(X2,X3) | ~'Ts9'(X0) | p2(X3) | ~p2(X2) | 'Ts6'(X1) | ~'Ts7'(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [c74,c36])). % 97.56/54.26 cnf(d48, plain, ~r1(X0,X1) | ~r1(sK38(sK66(X2)),X0) | ~'Ts9'(X2) | p2(X1) | ~p2(X0) | 'Ts4'(sK66(X2)) | 'Ts6'(sK39(sK66(X2))) | ~'Ts7'(sK38(sK66(X2))) | 'Ts4'(sK66(X2)), inference(resolution, [status(thm)], [d47,c37])). % 97.56/54.26 cnf(d49, plain, ~r1(sK43(sK38(sK66(X0))),X1) | ~'Ts9'(X0) | p2(X1) | ~p2(sK43(sK38(sK66(X0)))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | ~'Ts7'(sK38(sK66(X0))) | p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d48,d46])). % 97.56/54.26 cnf(d50, plain, ~'Ts9'(X0) | p2(sK44(sK38(sK66(X0)))) | p2(sK38(sK66(X0))) | ~p2(sK43(sK38(sK66(X0)))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | ~'Ts7'(sK38(sK66(X0))) | p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d49,d45])). % 97.56/54.26 cnf(d51, plain, ~'Ts9'(X0) | p2(sK38(sK66(X0))) | p2(sK44(sK38(sK66(X0)))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | ~'Ts7'(sK38(sK66(X0))) | p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d50,d44])). % 97.56/54.26 cnf(d52, plain, ~'Ts9'(X0) | p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | ~'Ts7'(sK38(sK66(X0))) | ~r1(X1,sK38(sK66(X0))) | p2(sK38(sK66(X0))) | 'Ts4'(X1), inference(resolution, [status(thm)], [d51,c42])). % 97.56/54.26 cnf(d53, plain, ~'Ts9'(X0) | p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | ~'Ts7'(sK38(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d52,c36])). % 97.56/54.26 cnf(d54, plain, ~'Ts9'(X0) | p2(sK38(sK66(X0))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d53,d42])). % 97.56/54.26 cnf(d55, plain, ~'Ts9'(X0) | p2(sK38(sK66(X0))) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d54,d32])). % 97.56/54.26 cnf(d56, plain, ~'Ts9'(X0) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)) | ~'Ts9'(X0) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)) | 'Ts6'(sK39(sK66(X0))), inference(resolution, [status(thm)], [d55,d43])). % 97.56/54.26 cnf(d57, plain, ~'Ts9'(X0) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)) | p2(sK39(sK66(X0))) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d56,d32])). % 97.56/54.26 cnf(d58, plain, ~'Ts9'(X0) | 'Ts4'(sK66(X0)) | 'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d57,c38])). % 97.56/54.26 cnf(d59, plain, ~'Ts9'(X0) | ~'Ts9'(X0) | ~p2(sK66(X0)), inference(resolution, [status(thm)], [d58,c71])). % 97.56/54.26 cnf(d60, plain, ~'Ts9'(sK10) | 'Ts1'(sK10) | ~'Ts9'(sK10), inference(resolution, [status(thm)], [d59,d28])). % 97.56/54.26 cnf(d61, plain, 'Ts1'(sK10) | 'Ts8'(sK10), inference(resolution, [status(thm)], [d60,c16])). % 97.56/54.26 cnf(d62, plain, p3(sK17(sK10)) | ~'Ts2'(sK10), inference(resolution, [status(thm)], [c9,c0])). % 97.56/54.26 cnf(d63, plain, ~r1(sK10,sK10) | ~'Ts2'(sK10) | ~'Ts1'(sK10) | ~p3(sK17(sK10)), inference(resolution, [status(thm)], [c8,c1])). % 97.56/54.26 cnf(d64, plain, ~'Ts1'(sK10) | ~p3(sK17(sK10)) | ~'Ts2'(sK10), inference(resolution, [status(thm)], [c0,d63])). % 97.56/54.26 cnf(d65, plain, ~'Ts1'(sK10) | ~'Ts2'(sK10) | ~'Ts2'(sK10), inference(resolution, [status(thm)], [d64,d62])). % 97.56/54.26 cnf(d66, plain, ~r1(sK30(X0),X1) | p2(X1) | p2(sK36(X1)) | ~'Ts3'(X0) | 'Ts2'(X0), inference(resolution, [status(thm)], [c35,c26])). % 97.56/54.26 cnf(d67, plain, 'Ts2'(X0) | p2(sK23(sK30(X0))) | p2(sK36(sK23(sK30(X0)))) | ~'Ts3'(X0) | ~r1(sK10,sK30(X0)) | p2(sK30(X0)), inference(resolution, [status(thm)], [d66,c17])). % 97.56/54.26 cnf(d68, plain, ~r1(sK30(X0),X1) | r1(sK36(X1),sK37(X1)) | p2(X1) | ~'Ts3'(X0) | 'Ts2'(X0), inference(resolution, [status(thm)], [c33,c26])). % 97.56/54.26 cnf(d69, plain, r1(sK36(sK23(sK30(X0))),sK37(sK23(sK30(X0)))) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | ~'Ts3'(X0) | ~r1(sK10,sK30(X0)) | p2(sK30(X0)), inference(resolution, [status(thm)], [d68,c17])). % 97.56/54.26 cnf(d70, plain, r1(X0,sK36(X0)) | ~r1(sK30(X1),X0) | p2(X0) | ~'Ts3'(X1) | 'Ts2'(X1), inference(resolution, [status(thm)], [c32,c26])). % 97.56/54.26 cnf(d71, plain, r1(sK23(sK30(X0)),sK36(sK23(sK30(X0)))) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | ~'Ts3'(X0) | ~r1(sK10,sK30(X0)) | p2(sK30(X0)), inference(resolution, [status(thm)], [d70,c17])). % 97.56/54.26 cnf(d72, plain, ~r1(sK10,sK30(X0)) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | p2(sK30(X0)) | ~'Ts3'(X0) | ~r1(sK36(sK23(sK30(X0))),X1) | ~r1(sK10,sK30(X0)) | p2(X1) | ~p2(sK36(sK23(sK30(X0)))) | p2(sK30(X0)), inference(resolution, [status(thm)], [d71,c19])). % 97.56/54.26 cnf(d73, plain, ~r1(sK10,sK30(X0)) | 'Ts2'(X0) | p2(sK37(sK23(sK30(X0)))) | p2(sK23(sK30(X0))) | p2(sK30(X0)) | ~p2(sK36(sK23(sK30(X0)))) | ~'Ts3'(X0) | ~r1(sK10,sK30(X0)) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | p2(sK30(X0)) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d72,d69])). % 97.56/54.26 cnf(d74, plain, ~r1(sK10,sK30(X0)) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | p2(sK30(X0)) | p2(sK37(sK23(sK30(X0)))) | ~'Ts3'(X0) | ~r1(sK10,sK30(X0)) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | p2(sK30(X0)) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d73,d67])). % 97.56/54.26 cnf(d75, plain, ~r1(sK10,sK30(X0)) | 'Ts2'(X0) | p2(sK23(sK30(X0))) | p2(sK30(X0)) | ~'Ts3'(X0) | ~r1(X1,sK23(sK30(X0))) | ~r1(X2,X1) | p2(sK23(sK30(X0))) | ~'Ts3'(X2), inference(resolution, [status(thm)], [d74,c34])). % 97.56/54.26 cnf(d76, plain, ~r1(X0,sK30(X1)) | ~r1(sK10,sK30(X1)) | 'Ts2'(X1) | p2(sK23(sK30(X1))) | p2(sK30(X1)) | ~'Ts3'(X0) | ~'Ts3'(X1) | ~r1(sK10,sK30(X1)) | p2(sK30(X1)), inference(resolution, [status(thm)], [d75,c17])). % 97.56/54.26 cnf(d77, plain, ~r1(X0,sK30(sK10)) | 'Ts2'(sK10) | p2(sK23(sK30(sK10))) | p2(sK30(sK10)) | ~'Ts3'(sK10) | ~'Ts3'(X0) | 'Ts2'(sK10), inference(resolution, [status(thm)], [d76,c26])). % 97.56/54.26 cnf(d78, plain, 'Ts2'(sK10) | p2(sK23(sK30(sK10))) | p2(sK30(sK10)) | ~'Ts3'(sK10) | ~'Ts3'(sK10) | 'Ts2'(sK10), inference(resolution, [status(thm)], [d77,c26])). % 97.56/54.26 cnf(d79, plain, 'Ts2'(sK10) | p2(sK30(sK10)) | ~'Ts3'(sK10) | ~r1(sK10,sK30(sK10)) | p2(sK30(sK10)), inference(resolution, [status(thm)], [d78,c18])). % 97.56/54.26 cnf(d80, plain, 'Ts2'(sK10) | p2(sK30(sK10)) | ~'Ts3'(sK10) | 'Ts2'(sK10), inference(resolution, [status(thm)], [d79,c26])). % 97.56/54.26 cnf(d81, plain, 'Ts2'(sK10) | ~'Ts3'(sK10) | 'Ts2'(sK10), inference(resolution, [status(thm)], [d80,c27])). % 97.56/54.26 cnf(d82, plain, ~'Ts8'(X0) | 'Ts3'(X0) | 'Ts2'(X0) | p2(sK61(X0)) | p2(sK32(sK61(X0))), inference(resolution, [status(thm)], [c63,c31])). % 97.56/54.26 cnf(d83, plain, ~'Ts8'(X0) | 'Ts3'(X0) | r1(sK32(sK61(X0)),sK33(sK61(X0))) | 'Ts2'(X0) | p2(sK61(X0)), inference(resolution, [status(thm)], [c63,c29])). % 97.56/54.26 cnf(d84, plain, ~'Ts8'(X0) | 'Ts3'(X0) | r1(sK61(X0),sK32(sK61(X0))) | 'Ts2'(X0) | p2(sK61(X0)), inference(resolution, [status(thm)], [c63,c28])). % 97.56/54.26 cnf(d85, plain, 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0) | ~r1(sK32(sK61(X0)),X1) | ~'Ts8'(X0) | p2(X1) | ~p2(sK32(sK61(X0))) | 'Ts3'(X0), inference(resolution, [status(thm)], [d84,c65])). % 97.56/54.26 cnf(d86, plain, 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK33(sK61(X0))) | ~p2(sK32(sK61(X0))) | p2(sK61(X0)) | 'Ts3'(X0) | 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0), inference(resolution, [status(thm)], [d85,d83])). % 97.56/54.26 cnf(d87, plain, 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK33(sK61(X0))) | p2(sK61(X0)) | 'Ts3'(X0) | 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0), inference(resolution, [status(thm)], [d86,d82])). % 97.56/54.26 cnf(d88, plain, 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0) | ~r1(X1,sK61(X0)) | 'Ts2'(X1) | p2(sK61(X0)), inference(resolution, [status(thm)], [d87,c30])). % 97.56/54.26 cnf(d89, plain, 'Ts2'(X0) | 'Ts2'(X0) | ~'Ts8'(X0) | p2(sK61(X0)) | 'Ts3'(X0) | ~'Ts8'(X0) | 'Ts3'(X0), inference(resolution, [status(thm)], [d88,c63])). % 97.56/54.26 cnf(d90, plain, 'Ts2'(X0) | ~'Ts8'(X0) | 'Ts3'(X0) | ~'Ts8'(X0) | 'Ts3'(X0), inference(resolution, [status(thm)], [d89,c64])). % 97.56/54.26 cnf(d91, plain, 'Ts2'(X0) | p2(sK66(X0)) | p2(sK32(sK66(X0))) | ~'Ts9'(X0), inference(resolution, [status(thm)], [c31,c70])). % 97.56/54.26 cnf(d92, plain, ~'Ts9'(X0) | r1(sK32(sK66(X0)),sK33(sK66(X0))) | 'Ts2'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [c70,c29])). % 97.56/54.26 cnf(d93, plain, ~'Ts9'(X0) | r1(sK66(X0),sK32(sK66(X0))) | 'Ts2'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [c70,c28])). % 97.56/54.26 cnf(d94, plain, 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK66(X0)) | ~r1(sK32(sK66(X0)),X1) | ~'Ts9'(X0) | p2(X1) | ~p2(sK32(sK66(X0))) | ~'Ts4'(sK66(X0)), inference(resolution, [status(thm)], [d93,c72])). % 97.56/54.26 cnf(d95, plain, 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK33(sK66(X0))) | ~p2(sK32(sK66(X0))) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [d94,d92])). % 97.56/54.26 cnf(d96, plain, 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK33(sK66(X0))) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK66(X0)), inference(resolution, [status(thm)], [d95,d91])). % 97.56/54.26 cnf(d97, plain, 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | ~r1(X1,sK66(X0)) | 'Ts2'(X1) | p2(sK66(X0)), inference(resolution, [status(thm)], [d96,c30])). % 97.56/54.26 cnf(d98, plain, 'Ts2'(X0) | 'Ts2'(X0) | ~'Ts9'(X0) | p2(sK66(X0)) | ~'Ts4'(sK66(X0)) | ~'Ts9'(X0), inference(resolution, [status(thm)], [d97,c70])). % 97.56/54.26 cnf(d99, plain, ~'Ts9'(sK10) | p2(sK66(sK10)) | 'Ts2'(sK10) | ~'Ts9'(sK10) | p2(sK66(sK10)), inference(resolution, [status(thm)], [d27,d98])). % 97.56/54.26 cnf(d100, plain, ~'Ts9'(sK10) | 'Ts2'(sK10) | ~'Ts9'(sK10), inference(resolution, [status(thm)], [d59,d99])). % 97.56/54.26 cnf(d101, plain, 'Ts2'(sK10) | 'Ts8'(sK10), inference(resolution, [status(thm)], [d100,c16])). % 97.56/54.26 cnf(d102, plain, 'Ts2'(sK10) | 'Ts2'(sK10) | 'Ts3'(sK10), inference(resolution, [status(thm)], [d101,d90])). % 97.56/54.26 cnf(d103, plain, 'Ts2'(sK10) | 'Ts2'(sK10), inference(resolution, [status(thm)], [d102,d81])). % 97.56/54.26 cnf(d104, plain, ~'Ts1'(sK10), inference(resolution, [status(thm)], [d103,d65])). % 97.56/54.26 cnf(d105, plain, 'Ts8'(sK10), inference(resolution, [status(thm)], [d104,d61])). % 97.56/54.26 cnf(d106, plain, 'Ts1'(sK10) | 'Ts3'(sK10), inference(resolution, [status(thm)], [d105,d8])). % 97.56/54.26 cnf(d107, plain, 'Ts3'(sK10), inference(resolution, [status(thm)], [d104,d106])). % 97.56/54.26 cnf(d108, plain, ~r1(sK26(X0),X1) | p2(X1) | p2(sK36(X1)) | ~'Ts3'(X0) | 'Ts1'(X0), inference(resolution, [status(thm)], [c35,c20])). % 97.56/54.26 cnf(d109, plain, 'Ts1'(X0) | p2(sK23(sK26(X0))) | p2(sK36(sK23(sK26(X0)))) | ~'Ts3'(X0) | ~r1(sK10,sK26(X0)) | p2(sK26(X0)), inference(resolution, [status(thm)], [d108,c17])). % 97.56/54.26 cnf(d110, plain, ~r1(sK26(X0),X1) | r1(sK36(X1),sK37(X1)) | p2(X1) | ~'Ts3'(X0) | 'Ts1'(X0), inference(resolution, [status(thm)], [c33,c20])). % 97.56/54.26 cnf(d111, plain, r1(sK36(sK23(sK26(X0))),sK37(sK23(sK26(X0)))) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | ~'Ts3'(X0) | ~r1(sK10,sK26(X0)) | p2(sK26(X0)), inference(resolution, [status(thm)], [d110,c17])). % 97.56/54.26 cnf(d112, plain, r1(X0,sK36(X0)) | ~r1(sK26(X1),X0) | p2(X0) | ~'Ts3'(X1) | 'Ts1'(X1), inference(resolution, [status(thm)], [c32,c20])). % 97.56/54.26 cnf(d113, plain, r1(sK23(sK26(X0)),sK36(sK23(sK26(X0)))) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | ~'Ts3'(X0) | ~r1(sK10,sK26(X0)) | p2(sK26(X0)), inference(resolution, [status(thm)], [d112,c17])). % 97.56/54.26 cnf(d114, plain, ~r1(sK10,sK26(X0)) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | p2(sK26(X0)) | ~'Ts3'(X0) | ~r1(sK36(sK23(sK26(X0))),X1) | ~r1(sK10,sK26(X0)) | p2(X1) | ~p2(sK36(sK23(sK26(X0)))) | p2(sK26(X0)), inference(resolution, [status(thm)], [d113,c19])). % 97.56/54.26 cnf(d115, plain, ~r1(sK10,sK26(X0)) | 'Ts1'(X0) | p2(sK37(sK23(sK26(X0)))) | p2(sK23(sK26(X0))) | p2(sK26(X0)) | ~p2(sK36(sK23(sK26(X0)))) | ~'Ts3'(X0) | ~r1(sK10,sK26(X0)) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | p2(sK26(X0)) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d114,d111])). % 97.56/54.26 cnf(d116, plain, ~r1(sK10,sK26(X0)) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | p2(sK26(X0)) | p2(sK37(sK23(sK26(X0)))) | ~'Ts3'(X0) | ~r1(sK10,sK26(X0)) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | p2(sK26(X0)) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d115,d109])). % 97.56/54.26 cnf(d117, plain, ~r1(sK10,sK26(X0)) | 'Ts1'(X0) | p2(sK23(sK26(X0))) | p2(sK26(X0)) | ~'Ts3'(X0) | ~r1(X1,sK23(sK26(X0))) | ~r1(X2,X1) | p2(sK23(sK26(X0))) | ~'Ts3'(X2), inference(resolution, [status(thm)], [d116,c34])). % 97.56/54.26 cnf(d118, plain, ~r1(X0,sK26(X1)) | ~r1(sK10,sK26(X1)) | 'Ts1'(X1) | p2(sK23(sK26(X1))) | p2(sK26(X1)) | ~'Ts3'(X0) | ~'Ts3'(X1) | ~r1(sK10,sK26(X1)) | p2(sK26(X1)), inference(resolution, [status(thm)], [d117,c17])). % 97.56/54.26 cnf(d119, plain, ~r1(X0,sK26(sK10)) | 'Ts1'(sK10) | p2(sK23(sK26(sK10))) | p2(sK26(sK10)) | ~'Ts3'(sK10) | ~'Ts3'(X0) | 'Ts1'(sK10), inference(resolution, [status(thm)], [d118,c20])). % 97.56/54.26 cnf(d120, plain, 'Ts1'(sK10) | p2(sK23(sK26(sK10))) | p2(sK26(sK10)) | ~'Ts3'(sK10) | ~'Ts3'(sK10) | 'Ts1'(sK10), inference(resolution, [status(thm)], [d119,c20])). % 97.56/54.26 cnf(d121, plain, 'Ts1'(sK10) | p2(sK26(sK10)) | ~'Ts3'(sK10) | ~r1(sK10,sK26(sK10)) | p2(sK26(sK10)), inference(resolution, [status(thm)], [d120,c18])). % 97.56/54.26 cnf(d122, plain, 'Ts1'(sK10) | p2(sK26(sK10)) | ~'Ts3'(sK10) | 'Ts1'(sK10), inference(resolution, [status(thm)], [d121,c20])). % 97.56/54.26 cnf(d123, plain, 'Ts1'(sK10) | ~'Ts3'(sK10) | 'Ts1'(sK10), inference(resolution, [status(thm)], [d122,c21])). % 97.56/54.26 cnf(d124, plain, ~'Ts3'(sK10), inference(resolution, [status(thm)], [d104,d123])). % 97.56/54.26 cnf(d125, plain, $false, inference(resolution, [status(thm)], [d124,d107])). % 97.56/54.26 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------