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