%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : COM003+3 : TPTP v9.3.1. Released v2.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 06:58:30 AM UTC 2026 % Result : Theorem 10.08s 1.91s % Output : CNFRefutation 10.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.35 % Computer : n020.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 26 23:20:04 UTC 2026 % 0.09/0.35 % CPUTime : % 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 10.08/1.91 % SZS status Theorem for theBenchmark.p % 10.08/1.91 % SZS output start CNFRefutation for theBenchmark.p % 10.08/1.91 fof(p1, axiom, (? [X0] : ((algorithm(X0) & ! [X1] : ((program(X1) => ! [X2] : decides(X0,X1,X2))))) => ? [X3] : ((program(X3) & ! [X1] : ((program(X1) => ! [X2] : decides(X3,X1,X2))))))). % 10.08/1.91 fof(p2, axiom, ! [X0] : (((program(X0) & ! [X1] : ((program(X1) => ! [X2] : decides(X0,X1,X2)))) => ! [X1] : ! [X2] : ((((program(X1) & halts2(X1,X2)) => (halts3(X0,X1,X2) & outputs(X0,good))) & ((program(X1) & ~halts2(X1,X2)) => (halts3(X0,X1,X2) & outputs(X0,bad)))))))). % 10.08/1.91 fof(p3, axiom, ! [X0] : (((program(X0) & ! [X1] : ! [X2] : ((((program(X1) & halts2(X1,X2)) => (halts3(X0,X1,X2) & outputs(X0,good))) & ((program(X1) & ~halts2(X1,X2)) => (halts3(X0,X1,X2) & outputs(X0,bad)))))) => ? [X3] : ((program(X3) & ! [X1] : ((((program(X1) & (halts3(X0,X1,X1) & outputs(X0,good))) => ~halts2(X3,X1)) & ((program(X1) & (halts3(X0,X1,X1) & outputs(X0,bad))) => (halts2(X3,X1) & outputs(X3,bad)))))))))). % 10.08/1.91 fof(prove_this, conjecture, ~? [X0] : ((algorithm(X0) & ! [X1] : ((program(X1) => ! [X2] : decides(X0,X1,X2)))))). % 10.08/1.91 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ((algorithm(X0) & ! [X1] : ((program(X1) => ! [X2] : decides(X0,X1,X2))))), inference(negate_conjecture, [status(cth)], [prove_this])). % 10.08/1.91 cnf(c0, plain, ~algorithm(X0) | program(sK1(X0)) | program(sK3), inference(clausification, [status(esa)], [p1])). % 10.08/1.91 cnf(c1, plain, ~algorithm(X0) | program(sK1(X0)) | ~program(X1) | decides(sK3,X1,X2), inference(clausification, [status(esa)], [p1])). % 10.08/1.91 cnf(c2, plain, ~algorithm(X0) | ~decides(X0,sK1(X0),sK2(X0)) | program(sK3), inference(clausification, [status(esa)], [p1])). % 10.08/1.91 cnf(c3, plain, ~algorithm(X0) | ~decides(X0,sK1(X0),sK2(X0)) | ~program(X1) | decides(sK3,X1,X2), inference(clausification, [status(esa)], [p1])). % 10.08/1.91 cnf(c4, plain, ~program(X0) | program(sK8(X0)) | X1(X0), inference(clausification, [status(esa)], [p2])). % 10.08/1.91 cnf(c5, plain, ~program(X0) | ~decides(X0,sK8(X0),sK9(X0)) | X1(X0), inference(clausification, [status(esa)], [p2])). % 10.08/1.91 cnf(c6, plain, ~X0(X1) | ~program(X2) | ~halts2(X2,X3) | halts3(X1,X2,X3), inference(clausification, [status(esa)], [p2])). % 10.08/1.91 cnf(c7, plain, ~X0(X1) | ~program(X2) | ~halts2(X2,X3) | outputs(X1,good), inference(clausification, [status(esa)], [p2])). % 10.08/1.91 cnf(c8, plain, ~X0(X1) | ~program(X2) | halts2(X2,X3) | halts3(X1,X2,X3), inference(clausification, [status(esa)], [p2])). % 10.08/1.91 cnf(c9, plain, ~X0(X1) | ~program(X2) | halts2(X2,X3) | outputs(X1,bad), inference(clausification, [status(esa)], [p2])). % 10.08/1.91 cnf(c10, plain, ~program(X0) | ~X1(X0,sK15(X0),sK16(X0)) | program(sK15(X0)) | X2(X0), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c11, plain, ~program(X0) | ~X1(X0,sK15(X0),sK16(X0)) | ~halts2(sK15(X0),sK16(X0)) | X2(X0), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c12, plain, X0(X1) | ~X2(X1,sK15(X1),sK16(X1)) | ~halts3(X1,sK15(X1),sK16(X1)) | ~outputs(X1,bad) | ~program(X1), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c13, plain, X0(X1,X2,X3) | program(X2), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c14, plain, X0(X1,X2,X3) | halts2(X2,X3), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c15, plain, X0(X1,X2,X3) | ~halts3(X1,X2,X3) | ~outputs(X1,good), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c16, plain, ~X0(X1) | program(sK17(X1)), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c17, plain, ~halts3(X0,X1,X1) | ~halts2(sK17(X0),X1) | ~program(X1) | ~outputs(X0,good) | ~X2(X0), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c18, plain, ~halts3(X0,X1,X1) | ~program(X1) | ~outputs(X0,bad) | halts2(sK17(X0),X1) | ~X2(X0), inference(clausification, [status(esa)], [p3])). % 10.08/1.91 cnf(c20, plain, algorithm(sK19), inference(clausification, [status(esa)], [negated_conjecture])). % 10.08/1.91 cnf(c21, plain, ~program(X0) | decides(sK19,X0,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 10.08/1.91 cnf(d0, plain, ~algorithm(sK19) | program(sK3) | ~program(sK1(sK19)), inference(resolution, [status(thm)], [c2,c21])). % 10.08/1.91 cnf(d1, plain, ~program(sK1(sK19)) | program(sK3), inference(resolution, [status(thm)], [c20,d0])). % 10.08/1.91 cnf(d2, plain, program(sK3) | ~algorithm(sK19) | program(sK3), inference(resolution, [status(thm)], [d1,c0])). % 10.08/1.91 cnf(d3, plain, program(sK3), inference(resolution, [status(thm)], [c20,d2])). % 10.08/1.91 cnf(d4, plain, ~program(X0) | ~halts2(sK17(X1),X0) | ~outputs(X1,good) | ~'Ts13'(X1) | ~program(X0) | ~'Ts6'(X1) | halts2(X0,X0), inference(resolution, [status(thm)], [c17,c8])). % 10.08/1.91 cnf(d5, plain, ~program(X0) | halts2(sK17(X1),X0) | ~outputs(X1,bad) | ~'Ts13'(X1) | ~program(X0) | ~'Ts6'(X1) | halts2(X0,X0), inference(resolution, [status(thm)], [c18,c8])). % 10.08/1.91 cnf(d6, plain, ~program(X0) | ~'Ts6'(X1) | halts2(X0,X0) | halts2(sK17(X1),X0) | ~'Ts13'(X1) | ~program(X2) | ~'Ts6'(X1) | halts2(X2,X3), inference(resolution, [status(thm)], [d5,c9])). % 10.08/1.91 cnf(d7, plain, ~program(X0) | ~program(X0) | ~'Ts6'(X1) | halts2(X0,X0) | halts2(sK17(X1),X0) | ~'Ts13'(X1), inference(factoring, [status(thm)], [d6])). % 10.08/1.91 cnf(d8, plain, ~program(X0) | halts2(sK17(X1),X0) | ~outputs(X1,bad) | ~'Ts13'(X1) | ~program(X0) | ~'Ts6'(X1) | ~halts2(X0,X0), inference(resolution, [status(thm)], [c18,c6])). % 10.08/1.91 cnf(d9, plain, ~algorithm(sK19) | ~program(X0) | decides(sK3,X0,X1) | ~program(sK1(sK19)), inference(resolution, [status(thm)], [c3,c21])). % 10.08/1.91 cnf(d10, plain, ~program(X0) | ~program(sK1(sK19)) | decides(sK3,X0,X1), inference(resolution, [status(thm)], [c20,d9])). % 10.08/1.91 cnf(d11, plain, ~program(sK8(sK3)) | ~program(sK1(sK19)) | ~program(sK3) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d10,c5])). % 10.08/1.91 cnf(d12, plain, ~program(sK1(sK19)) | ~program(sK8(sK3)) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d3,d11])). % 10.08/1.91 cnf(d13, plain, ~program(sK1(sK19)) | 'Ts6'(sK3) | ~program(sK3) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d12,c4])). % 10.08/1.91 cnf(d14, plain, ~program(sK1(sK19)) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d3,d13])). % 10.08/1.91 cnf(d15, plain, 'Ts6'(sK3) | ~algorithm(sK19) | ~program(X0) | decides(sK3,X0,X1), inference(resolution, [status(thm)], [d14,c1])). % 10.08/1.91 cnf(d16, plain, ~program(X0) | decides(sK3,X0,X1) | 'Ts6'(sK3), inference(resolution, [status(thm)], [c20,d15])). % 10.08/1.91 cnf(d17, plain, ~program(sK8(sK3)) | 'Ts6'(sK3) | ~program(sK3) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d16,c5])). % 10.08/1.91 cnf(d18, plain, ~program(sK8(sK3)) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d3,d17])). % 10.08/1.91 cnf(d19, plain, 'Ts6'(sK3) | ~program(sK3) | 'Ts6'(sK3), inference(resolution, [status(thm)], [d18,c4])). % 10.08/1.91 cnf(d20, plain, 'Ts6'(sK3), inference(resolution, [status(thm)], [d3,d19])). % 10.08/1.91 cnf(d21, plain, ~program(X0) | ~'Ts6'(X1) | outputs(X1,bad) | ~program(X0) | ~'Ts6'(X2) | outputs(X2,good), inference(resolution, [status(thm)], [c9,c7])). % 10.08/1.91 cnf(d22, plain, ~program(X0) | ~'Ts6'(X1) | outputs(X1,good) | outputs(sK3,bad), inference(resolution, [status(thm)], [d21,d20])). % 10.08/1.91 cnf(d23, plain, ~program(X0) | outputs(sK3,good) | outputs(sK3,bad), inference(resolution, [status(thm)], [d22,d20])). % 10.08/1.91 cnf(d24, plain, outputs(sK3,good) | outputs(sK3,bad), inference(resolution, [status(thm)], [d23,d3])). % 10.08/1.91 cnf(d25, plain, ~program(X0) | ~halts2(sK17(X1),X0) | ~outputs(X1,good) | ~'Ts13'(X1) | ~program(X0) | ~'Ts6'(X1) | ~halts2(X0,X0), inference(resolution, [status(thm)], [c17,c6])). % 10.08/1.91 cnf(d26, plain, ~program(X0) | ~'Ts6'(X1) | ~halts2(X0,X0) | ~outputs(X1,good) | ~'Ts13'(X1) | ~program(sK17(X1)) | ~'Ts6'(X2) | outputs(X2,bad), inference(resolution, [status(thm)], [d25,c9])). % 10.08/1.91 cnf(d27, plain, ~program(X0) | ~program(sK17(sK3)) | ~'Ts6'(X1) | ~'Ts6'(sK3) | ~halts2(X0,X0) | outputs(X1,bad) | ~'Ts13'(sK3) | outputs(sK3,bad), inference(resolution, [status(thm)], [d26,d24])). % 10.08/1.91 cnf(d28, plain, ~program(X0) | ~program(sK17(sK3)) | ~'Ts6'(X1) | ~halts2(X0,X0) | outputs(X1,bad) | outputs(sK3,bad) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d27])). % 10.08/1.91 cnf(d29, plain, ~program(X0) | ~program(sK17(sK3)) | ~'Ts6'(X1) | outputs(X1,bad) | outputs(sK3,bad) | ~'Ts13'(sK3) | ~program(X0) | ~'Ts6'(X2) | outputs(X2,bad), inference(resolution, [status(thm)], [d28,c9])). % 10.08/1.91 cnf(d30, plain, ~program(X0) | ~'Ts6'(X1) | ~'Ts6'(X2) | outputs(X1,bad) | outputs(X2,bad) | outputs(sK3,bad) | ~'Ts13'(sK3) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d29,c16])). % 10.08/1.91 cnf(d31, plain, program(sK15(X0)) | ~program(X0) | program(sK15(X0)) | 'Ts13'(X0), inference(resolution, [status(thm)], [c13,c10])). % 10.08/1.91 cnf(d32, plain, halts2(sK15(X0),sK16(X0)) | ~program(X0) | ~halts3(X0,sK15(X0),sK16(X0)) | ~outputs(X0,bad) | 'Ts13'(X0), inference(resolution, [status(thm)], [c14,c12])). % 10.08/1.91 cnf(d33, plain, ~program(X0) | halts2(sK15(X0),sK16(X0)) | ~outputs(X0,bad) | 'Ts13'(X0) | ~program(sK15(X0)) | ~'Ts6'(X0) | halts2(sK15(X0),sK16(X0)), inference(resolution, [status(thm)], [d32,c8])). % 10.08/1.91 cnf(d34, plain, ~outputs(X0,good) | 'Ts12'(X0,X1,X2) | ~program(X1) | ~'Ts6'(X0) | ~halts2(X1,X2), inference(resolution, [status(thm)], [c15,c6])). % 10.08/1.91 cnf(d35, plain, ~program(sK15(X0)) | ~'Ts6'(X0) | ~halts2(sK15(X0),sK16(X0)) | ~outputs(X0,good) | ~program(X0) | ~halts2(sK15(X0),sK16(X0)) | 'Ts13'(X0), inference(resolution, [status(thm)], [d34,c11])). % 10.08/1.91 cnf(d36, plain, ~program(X0) | ~program(sK15(X0)) | ~'Ts6'(X0) | ~outputs(X0,good) | 'Ts13'(X0) | ~program(X0) | ~program(sK15(X0)) | ~'Ts6'(X0) | ~outputs(X0,bad) | 'Ts13'(X0), inference(resolution, [status(thm)], [d35,d33])). % 10.08/1.91 cnf(d37, plain, ~program(X0) | ~program(sK15(X0)) | ~'Ts6'(X0) | ~outputs(X0,good) | 'Ts13'(X0) | ~program(sK15(X0)) | ~'Ts6'(X1) | outputs(X1,bad), inference(resolution, [status(thm)], [d35,c9])). % 10.08/1.91 cnf(d38, plain, ~program(sK3) | ~program(sK15(sK3)) | ~'Ts6'(X0) | ~'Ts6'(sK3) | outputs(X0,bad) | 'Ts13'(sK3) | outputs(sK3,bad), inference(resolution, [status(thm)], [d37,d24])). % 10.08/1.91 cnf(d39, plain, ~program(sK15(sK3)) | ~'Ts6'(X0) | ~'Ts6'(sK3) | outputs(X0,bad) | outputs(sK3,bad) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d3,d38])). % 10.08/1.91 cnf(d40, plain, ~program(sK15(sK3)) | ~'Ts6'(X0) | outputs(X0,bad) | outputs(sK3,bad) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d39])). % 10.08/1.91 cnf(d41, plain, ~'Ts6'(X0) | outputs(X0,bad) | outputs(sK3,bad) | 'Ts13'(sK3) | ~program(sK3) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d40,d31])). % 10.08/1.91 cnf(d42, plain, ~'Ts6'(X0) | outputs(X0,bad) | outputs(sK3,bad) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d3,d41])). % 10.08/1.91 cnf(d43, plain, ~'Ts6'(sK3) | outputs(sK3,bad) | 'Ts13'(sK3), inference(factoring, [status(thm)], [d42])). % 10.08/1.91 cnf(d44, plain, outputs(sK3,bad) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d43])). % 10.08/1.91 cnf(d45, plain, 'Ts13'(sK3) | ~program(sK3) | ~program(sK15(sK3)) | ~'Ts6'(sK3) | ~outputs(sK3,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d44,d36])). % 10.08/1.91 cnf(d46, plain, ~program(sK15(sK3)) | ~'Ts6'(sK3) | ~outputs(sK3,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d3,d45])). % 10.08/1.91 cnf(d47, plain, ~program(sK15(sK3)) | ~outputs(sK3,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d46])). % 10.08/1.91 cnf(d48, plain, ~program(X0) | ~program(sK15(X0)) | ~'Ts6'(X0) | ~outputs(X0,bad) | 'Ts13'(X0) | ~program(sK15(X0)) | ~'Ts6'(X1) | outputs(X1,good), inference(resolution, [status(thm)], [d33,c7])). % 10.08/1.91 cnf(d49, plain, 'Ts13'(sK3) | ~program(sK3) | ~program(sK15(sK3)) | ~'Ts6'(X0) | ~'Ts6'(sK3) | outputs(X0,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d44,d48])). % 10.08/1.91 cnf(d50, plain, ~program(sK15(sK3)) | ~'Ts6'(X0) | ~'Ts6'(sK3) | outputs(X0,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d3,d49])). % 10.08/1.91 cnf(d51, plain, ~program(sK15(sK3)) | ~'Ts6'(X0) | outputs(X0,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d50])). % 10.08/1.91 cnf(d52, plain, ~'Ts6'(X0) | outputs(X0,good) | 'Ts13'(sK3) | ~program(sK3) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d51,d31])). % 10.08/1.91 cnf(d53, plain, ~'Ts6'(X0) | outputs(X0,good) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d3,d52])). % 10.08/1.91 cnf(d54, plain, ~'Ts6'(sK3) | 'Ts13'(sK3) | ~program(sK15(sK3)) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d53,d47])). % 10.08/1.91 cnf(d55, plain, ~program(sK15(sK3)) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d54])). % 10.08/1.91 cnf(d56, plain, 'Ts13'(sK3) | ~program(sK3) | 'Ts13'(sK3), inference(resolution, [status(thm)], [d55,d31])). % 10.08/1.91 cnf(d57, plain, 'Ts13'(sK3), inference(resolution, [status(thm)], [d3,d56])). % 10.08/1.91 cnf(d58, plain, ~program(X0) | ~'Ts6'(X1) | ~'Ts6'(X2) | outputs(X1,bad) | outputs(X2,bad) | outputs(sK3,bad), inference(resolution, [status(thm)], [d57,d30])). % 10.08/1.91 cnf(d59, plain, ~program(X0) | ~'Ts6'(X1) | outputs(X1,bad) | outputs(sK3,bad) | outputs(sK3,bad), inference(resolution, [status(thm)], [d58,d20])). % 10.08/1.91 cnf(d60, plain, ~program(X0) | outputs(sK3,bad) | outputs(sK3,bad), inference(resolution, [status(thm)], [d59,d20])). % 10.08/1.91 cnf(d61, plain, outputs(sK3,bad), inference(resolution, [status(thm)], [d60,d3])). % 10.08/1.91 cnf(d62, plain, ~program(X0) | ~'Ts6'(sK3) | ~halts2(X0,X0) | halts2(sK17(sK3),X0) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d61,d8])). % 10.08/1.91 cnf(d63, plain, ~program(X0) | ~halts2(X0,X0) | halts2(sK17(sK3),X0) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d62])). % 10.08/1.91 cnf(d64, plain, ~program(X0) | ~halts2(X0,X0) | halts2(sK17(sK3),X0), inference(resolution, [status(thm)], [d57,d63])). % 10.08/1.91 cnf(d65, plain, ~program(X0) | halts2(sK17(sK3),X0) | ~program(X0) | ~'Ts6'(X1) | halts2(sK17(X1),X0) | ~'Ts13'(X1), inference(resolution, [status(thm)], [d64,d7])). % 10.08/1.91 cnf(d66, plain, ~program(X0) | ~'Ts6'(sK3) | halts2(sK17(sK3),X0) | ~'Ts13'(sK3), inference(factoring, [status(thm)], [d65])). % 10.08/1.91 cnf(d67, plain, ~program(X0) | halts2(sK17(sK3),X0) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d66])). % 10.08/1.91 cnf(d68, plain, ~program(X0) | halts2(sK17(sK3),X0), inference(resolution, [status(thm)], [d57,d67])). % 10.08/1.91 cnf(d69, plain, ~program(X0) | ~program(X0) | ~'Ts6'(sK3) | halts2(X0,X0) | ~outputs(sK3,good) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d68,d4])). % 10.08/1.91 cnf(d70, plain, ~program(X0) | halts2(X0,X0) | ~outputs(sK3,good) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d69])). % 10.08/1.91 cnf(d71, plain, ~program(X0) | halts2(X0,X0) | ~outputs(sK3,good), inference(resolution, [status(thm)], [d57,d70])). % 10.08/1.91 cnf(d72, plain, ~program(X0) | ~program(sK17(sK3)) | ~'Ts6'(X1) | outputs(X1,good), inference(resolution, [status(thm)], [d68,c7])). % 10.08/1.91 cnf(d73, plain, ~program(X0) | ~'Ts6'(X1) | outputs(X1,good) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d72,c16])). % 10.08/1.91 cnf(d74, plain, ~program(X0) | ~'Ts6'(X1) | outputs(X1,good), inference(resolution, [status(thm)], [d57,d73])). % 10.08/1.91 cnf(d75, plain, ~program(X0) | outputs(sK3,good), inference(resolution, [status(thm)], [d74,d20])). % 10.08/1.91 cnf(d76, plain, outputs(sK3,good), inference(resolution, [status(thm)], [d75,d3])). % 10.08/1.91 cnf(d77, plain, ~program(X0) | halts2(X0,X0), inference(resolution, [status(thm)], [d76,d71])). % 10.08/1.91 cnf(d78, plain, ~program(X0) | ~program(X0) | ~'Ts6'(sK3) | ~halts2(X0,X0) | ~outputs(sK3,good) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d68,d25])). % 10.08/1.91 cnf(d79, plain, ~program(X0) | ~halts2(X0,X0) | ~outputs(sK3,good) | ~'Ts13'(sK3), inference(resolution, [status(thm)], [d20,d78])). % 10.08/1.91 cnf(d80, plain, ~program(X0) | ~halts2(X0,X0) | ~outputs(sK3,good), inference(resolution, [status(thm)], [d57,d79])). % 10.08/1.91 cnf(d81, plain, ~program(X0) | ~halts2(X0,X0), inference(resolution, [status(thm)], [d76,d80])). % 10.08/1.91 cnf(d82, plain, ~program(X0) | ~program(X0), inference(resolution, [status(thm)], [d81,d77])). % 10.08/1.91 cnf(d83, plain, $false, inference(resolution, [status(thm)], [d82,d3])). % 10.08/1.91 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------