%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : GRP775+1 : TPTP v9.3.1. Released v4.1.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 07:24:38 AM UTC 2026 % Result : Theorem 39.24s 10.52s % Output : CNFRefutation 39.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : GRP775+1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.43 % Computer : n009.cluster.edu % 0.19/0.43 % Model : x86_64 x86_64 % 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.43 % Memory : 8046.5625MB % 0.19/0.43 % OS : Linux 6.8.0-71-generic % 0.19/0.43 % CPULimit : 300 % 0.19/0.43 % WCLimit : 300 % 0.19/0.43 % DateTime : Fri Sep 25 15:46:29 UTC 2026 % 0.19/0.43 % CPUTime : % 0.19/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.24/10.52 % SZS status Theorem for theBenchmark.p % 39.24/10.52 % SZS output start CNFRefutation for theBenchmark.p % 39.24/10.52 fof(sos01, axiom, ! [X0] : ! [X1] : ! [X2] : product(product(X2,X1),X0) = product(X2,product(X1,X0))). % 39.24/10.52 fof(sos02, axiom, ! [X0] : product(X0,X0) = X0). % 39.24/10.52 fof(sos03, axiom, ! [X0] : ! [X1] : ((l(X0,X1) <=> (product(X0,X1) = X0 & product(X1,X0) = X1)))). % 39.24/10.52 fof(sos04, axiom, ! [X0] : ! [X1] : ((r(X0,X1) <=> (product(X0,X1) = X1 & product(X1,X0) = X0)))). % 39.24/10.52 fof(sos05, axiom, ! [X0] : ! [X1] : ((d(X0,X1) <=> ? [X2] : ((r(X0,X2) & l(X2,X1)))))). % 39.24/10.52 fof(goals, conjecture, ! [X0] : ! [X1] : ((d(X0,X1) <=> (product(X0,product(X1,X0)) = X0 & product(X1,product(X0,X1)) = X1)))). % 39.24/10.52 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((d(X0,X1) <=> (product(X0,product(X1,X0)) = X0 & product(X1,product(X0,X1)) = X1))), inference(negate_conjecture, [status(cth)], [goals])). % 39.24/10.52 cnf(c0, plain, product(X0,product(X1,X2)) = product(product(X0,X1),X2), inference(clausification, [status(esa)], [sos01])). % 39.24/10.52 cnf(c1, plain, product(X0,X0) = X0, inference(clausification, [status(esa)], [sos02])). % 39.24/10.52 cnf(c2, plain, ~l(X0,X1) | product(X0,X1) = X0, inference(clausification, [status(esa)], [sos03])). % 39.24/10.52 cnf(c3, plain, ~l(X0,X1) | product(X1,X0) = X1, inference(clausification, [status(esa)], [sos03])). % 39.24/10.52 cnf(c4, plain, l(X0,X1) | product(X1,X0) != X1 | product(X0,X1) != X0, inference(clausification, [status(esa)], [sos03])). % 39.24/10.52 cnf(c5, plain, ~r(X0,X1) | product(X0,X1) = X1, inference(clausification, [status(esa)], [sos04])). % 39.24/10.52 cnf(c6, plain, ~r(X0,X1) | product(X1,X0) = X0, inference(clausification, [status(esa)], [sos04])). % 39.24/10.52 cnf(c7, plain, r(X0,X1) | product(X1,X0) != X0 | product(X0,X1) != X1, inference(clausification, [status(esa)], [sos04])). % 39.24/10.52 cnf(c8, plain, ~d(X0,X1) | r(X0,sK10(X0,X1)), inference(clausification, [status(esa)], [sos05])). % 39.24/10.52 cnf(c9, plain, ~d(X0,X1) | l(sK10(X0,X1),X1), inference(clausification, [status(esa)], [sos05])). % 39.24/10.52 cnf(c10, plain, d(X0,X1) | ~r(X0,X2) | ~l(X2,X1), inference(clausification, [status(esa)], [sos05])). % 39.24/10.52 cnf(c11, plain, d(sK13,sK14) | X0(sK13,sK14), inference(clausification, [status(esa)], [negated_conjecture])). % 39.24/10.52 cnf(c12, plain, product(sK13,product(sK14,sK13)) != sK13 | product(sK14,product(sK13,sK14)) != sK14 | X0(sK13,sK14), inference(clausification, [status(esa)], [negated_conjecture])). % 39.24/10.52 cnf(c13, plain, ~X0(X1,X2) | ~d(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 39.24/10.52 cnf(c14, plain, ~X0(X1,X2) | product(X2,product(X1,X2)) = X2, inference(clausification, [status(esa)], [negated_conjecture])). % 39.24/10.52 cnf(c15, plain, ~X0(X1,X2) | product(X1,product(X2,X1)) = X1, inference(clausification, [status(esa)], [negated_conjecture])). % 39.24/10.52 cnf(d0, plain, product(X0,product(X0,X1)) = product(X0,X1), inference(superposition, [status(thm)], [c1,c0])). % 39.24/10.52 cnf(d1, plain, product(X0,X1) != product(X0,X1) | product(product(X0,X1),X0) != X0 | r(X0,product(X0,X1)), inference(superposition, [status(thm)], [d0,c7])). % 39.24/10.52 cnf(d2, plain, product(X0,X1) != product(X0,X1) | product(X0,product(X1,X0)) != X0 | r(X0,product(X0,X1)), inference(demodulation, [status(thm)], [d1,c0])). % 39.24/10.52 cnf(d3, plain, product(sK13,product(sK14,sK13)) = sK13 | d(sK13,sK14), inference(resolution, [status(thm)], [c15,c11])). % 39.24/10.52 cnf(d4, plain, ~d(X0,X1) | product(sK10(X0,X1),X0) = X0, inference(resolution, [status(thm)], [c8,c6])). % 39.24/10.52 cnf(d5, plain, product(sK10(sK13,sK14),sK13) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(resolution, [status(thm)], [d4,d3])). % 39.24/10.52 cnf(d6, plain, ~d(X0,X1) | product(sK10(X0,X1),X1) = sK10(X0,X1), inference(resolution, [status(thm)], [c9,c2])). % 39.24/10.52 cnf(d7, plain, product(sK10(sK13,sK14),sK14) = sK10(sK13,sK14) | product(sK13,product(sK14,sK13)) = sK13, inference(resolution, [status(thm)], [d6,d3])). % 39.24/10.52 cnf(d8, plain, product(sK10(sK13,sK14),product(sK14,X0)) = product(sK10(sK13,sK14),X0) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d7,c0])). % 39.24/10.52 cnf(d9, plain, product(sK10(sK13,sK14),product(sK13,X0)) = product(sK13,X0) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d5,c0])). % 39.24/10.52 cnf(d10, plain, ~d(X0,X1) | product(X1,sK10(X0,X1)) = X1, inference(resolution, [status(thm)], [c9,c3])). % 39.24/10.52 cnf(d11, plain, product(sK14,sK10(sK13,sK14)) = sK14 | product(sK13,product(sK14,sK13)) = sK13, inference(resolution, [status(thm)], [d10,d3])). % 39.24/10.52 cnf(d12, plain, product(sK14,product(sK10(sK13,sK14),X0)) = product(sK14,X0) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d11,c0])). % 39.24/10.52 cnf(d13, plain, ~d(X0,X1) | product(X0,sK10(X0,X1)) = sK10(X0,X1), inference(resolution, [status(thm)], [c8,c5])). % 39.24/10.52 cnf(d14, plain, product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | product(sK13,product(sK14,sK13)) = sK13, inference(resolution, [status(thm)], [d13,d3])). % 39.24/10.52 cnf(d15, plain, product(sK13,product(sK10(sK13,sK14),X0)) = product(sK10(sK13,sK14),X0) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d14,c0])). % 39.24/10.52 cnf(d16, plain, product(sK13,sK10(sK13,sK14)) = product(sK10(sK13,sK14),sK14) | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d7,d15])). % 39.24/10.52 cnf(d17, plain, product(sK14,product(sK13,sK10(sK13,sK14))) = product(sK14,sK14) | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d16,d12])). % 39.24/10.52 cnf(d18, plain, product(sK13,product(sK14,sK13)) = sK13 | product(sK14,product(sK13,sK10(sK13,sK14))) = sK14, inference(demodulation, [status(thm)], [d17,c1])). % 39.24/10.52 cnf(d19, plain, product(sK14,sK14) = product(sK14,product(sK13,sK10(sK13,sK14))) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d18,d0])). % 39.24/10.52 cnf(d20, plain, product(sK13,product(sK14,sK13)) = sK13 | sK14 = product(sK14,product(sK13,sK10(sK13,sK14))), inference(demodulation, [status(thm)], [d19,c1])). % 39.24/10.52 cnf(d21, plain, product(X0,product(X1,product(product(X0,X1),X2))) = product(product(X0,X1),X2), inference(superposition, [status(thm)], [d0,c0])). % 39.24/10.52 cnf(d22, plain, product(X0,product(X1,product(X0,product(X1,X2)))) = product(product(X0,X1),X2), inference(demodulation, [status(thm)], [d21,c0])). % 39.24/10.52 cnf(d23, plain, product(X0,product(X1,product(X0,product(X1,X2)))) = product(X0,product(X1,X2)), inference(demodulation, [status(thm)], [d22,c0])). % 39.24/10.52 cnf(d24, plain, product(sK14,product(sK13,sK14)) = product(sK14,product(sK13,sK10(sK13,sK14))) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d18,d23])). % 39.24/10.52 cnf(d25, plain, sK14 = product(sK14,product(sK13,sK14)) | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d24,d20])). % 39.24/10.52 cnf(d26, plain, product(sK10(sK13,sK14),sK14) = product(sK10(sK13,sK14),product(sK13,sK14)) | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d25,d8])). % 39.24/10.52 cnf(d27, plain, product(sK10(sK13,sK14),sK14) = product(sK13,sK14) | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d26,d9])). % 39.24/10.52 cnf(d28, plain, product(sK10(sK13,sK14),product(sK14,X0)) = product(product(sK13,sK14),X0) | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d27,c0])). % 39.24/10.52 cnf(d29, plain, product(sK10(sK13,sK14),product(sK14,X0)) = product(sK13,product(sK14,X0)) | product(sK13,product(sK14,sK13)) = sK13, inference(demodulation, [status(thm)], [d28,c0])). % 39.24/10.52 cnf(d30, plain, product(sK13,product(sK14,X0)) = product(sK10(sK13,sK14),X0) | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d29,d8])). % 39.24/10.52 cnf(d31, plain, product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13 | product(sK13,product(sK14,sK13)) = sK13, inference(superposition, [status(thm)], [d30,d5])). % 39.24/10.52 cnf(d32, plain, sK13 != sK13 | product(sK13,sK14) != product(sK13,sK14) | r(sK13,product(sK13,sK14)), inference(superposition, [status(thm)], [d31,d2])). % 39.24/10.52 cnf(d33, plain, product(X0,product(X1,product(X0,X1))) = product(X0,X1), inference(superposition, [status(thm)], [c1,c0])). % 39.24/10.52 cnf(d34, plain, product(X0,product(product(X0,X1),product(X0,X1))) = product(X0,product(X0,X1)), inference(superposition, [status(thm)], [d0,d33])). % 39.24/10.52 cnf(d35, plain, product(X0,product(X0,product(X1,product(X0,X1)))) = product(X0,product(X0,X1)), inference(demodulation, [status(thm)], [d34,c0])). % 39.24/10.52 cnf(d36, plain, product(X0,product(X1,product(X0,X1))) = product(X0,product(X0,X1)), inference(demodulation, [status(thm)], [d35,d0])). % 39.24/10.52 cnf(d37, plain, product(X0,X1) = product(X0,product(X0,X1)), inference(demodulation, [status(thm)], [d36,d33])). % 39.24/10.52 cnf(d38, plain, product(sK13,product(sK14,sK13)) = product(sK13,sK13), inference(superposition, [status(thm)], [d31,d37])). % 39.24/10.52 cnf(d39, plain, sK13 = product(sK13,sK13), inference(demodulation, [status(thm)], [d38,d31])). % 39.24/10.52 cnf(d40, plain, sK13 = sK13, inference(demodulation, [status(thm)], [d39,c1])). % 39.24/10.52 cnf(d41, plain, product(sK13,sK14) != product(sK13,sK14) | r(sK13,product(sK13,sK14)), inference(resolution, [status(thm)], [d40,d32])). % 39.24/10.52 cnf(d42, plain, product(sK13,product(product(sK14,sK13),X0)) = product(sK13,X0), inference(superposition, [status(thm)], [d31,c0])). % 39.24/10.52 cnf(d43, plain, product(sK13,product(sK14,product(sK13,X0))) = product(sK13,X0), inference(demodulation, [status(thm)], [d42,c0])). % 39.24/10.52 cnf(d44, plain, product(sK13,product(sK14,product(sK13,X0))) = product(sK13,product(sK13,X0)), inference(superposition, [status(thm)], [d43,d37])). % 39.24/10.52 cnf(d45, plain, product(sK13,X0) = product(sK13,product(sK13,X0)), inference(demodulation, [status(thm)], [d44,d43])). % 39.24/10.52 cnf(d46, plain, product(sK13,X0) = product(sK13,X0), inference(demodulation, [status(thm)], [d45,d0])). % 39.24/10.52 cnf(d47, plain, r(sK13,product(sK13,sK14)), inference(resolution, [status(thm)], [d46,d41])). % 39.24/10.52 cnf(d48, plain, ~l(product(sK13,sK14),X0) | d(sK13,X0), inference(resolution, [status(thm)], [d47,c10])). % 39.24/10.52 cnf(d49, plain, product(sK14,product(sK13,sK14)) = sK14 | d(sK13,sK14), inference(resolution, [status(thm)], [c14,c11])). % 39.24/10.52 cnf(d50, plain, product(sK14,sK10(sK13,sK14)) = sK14 | product(sK14,product(sK13,sK14)) = sK14, inference(resolution, [status(thm)], [d10,d49])). % 39.24/10.52 cnf(d51, plain, product(sK14,product(sK10(sK13,sK14),X0)) = product(sK14,X0) | product(sK14,product(sK13,sK14)) = sK14, inference(superposition, [status(thm)], [d50,c0])). % 39.24/10.52 cnf(d52, plain, product(sK14,sK14) != sK14 | product(sK14,sK10(sK13,sK14)) != product(sK14,sK10(sK13,sK14)) | r(sK14,product(sK14,sK10(sK13,sK14))) | product(sK14,product(sK13,sK14)) = sK14, inference(superposition, [status(thm)], [d51,d2])). % 39.24/10.52 cnf(d53, plain, product(sK14,product(sK13,sK14)) = sK14 | product(sK14,sK10(sK13,sK14)) != product(sK14,sK10(sK13,sK14)) | sK14 != sK14 | r(sK14,product(sK14,sK10(sK13,sK14))), inference(demodulation, [status(thm)], [d52,c1])). % 39.24/10.52 cnf(d54, plain, product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | product(sK14,product(sK13,sK14)) = sK14, inference(resolution, [status(thm)], [d13,d49])). % 39.24/10.52 cnf(d55, plain, sK14 != sK14 | product(product(sK13,sK14),sK14) != product(sK13,sK14) | l(product(sK13,sK14),sK14) | product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14), inference(superposition, [status(thm)], [d54,c4])). % 39.24/10.52 cnf(d56, plain, product(sK13,product(sK14,sK14)) != product(sK13,sK14) | product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | sK14 != sK14 | l(product(sK13,sK14),sK14), inference(demodulation, [status(thm)], [d55,c0])). % 39.24/10.52 cnf(d57, plain, product(sK13,sK14) != product(sK13,sK14) | product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | sK14 != sK14 | l(product(sK13,sK14),sK14), inference(demodulation, [status(thm)], [d56,c1])). % 39.24/10.52 cnf(d58, plain, product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | sK14 != sK14 | l(product(sK13,sK14),sK14), inference(equality_resolution, [status(thm)], [d57])). % 39.24/10.52 cnf(d59, plain, product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | l(product(sK13,sK14),sK14), inference(equality_resolution, [status(thm)], [d58])). % 39.24/10.52 cnf(d60, plain, d(sK13,sK14) | product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14), inference(resolution, [status(thm)], [d48,d59])). % 39.24/10.52 cnf(d61, plain, product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14) | product(sK13,sK10(sK13,sK14)) = sK10(sK13,sK14), inference(resolution, [status(thm)], [d60,d13])). % 39.24/10.52 cnf(d62, plain, product(product(X0,X1),product(X2,X3)) = product(product(X0,product(X1,X2)),X3), inference(superposition, [status(thm)], [c0,c0])). % 39.24/10.52 cnf(d63, plain, product(X0,product(X1,product(X2,X3))) = product(product(X0,product(X1,X2)),X3), inference(demodulation, [status(thm)], [d62,c0])). % 39.24/10.52 cnf(d64, plain, product(X0,product(X1,product(X2,X3))) = product(X0,product(product(X1,X2),X3)), inference(demodulation, [status(thm)], [d63,c0])). % 39.24/10.52 cnf(d65, plain, product(X3,product(X0,product(X1,X2))) = product(X3,product(X0,product(X1,X2))), inference(demodulation, [status(thm)], [d64,c0])). % 39.24/10.52 cnf(d66, plain, product(X0,product(X1,X2)) = product(X0,product(X0,product(X1,X2))), inference(superposition, [status(thm)], [d0,d65])). % 39.24/10.52 cnf(d67, plain, product(X0,product(X1,X2)) = product(X0,product(X1,X2)), inference(demodulation, [status(thm)], [d66,d0])). % 39.24/10.52 cnf(d68, plain, product(X0,sK10(sK13,sK14)) = product(X0,product(sK13,sK10(sK13,sK14))), inference(superposition, [status(thm)], [d61,d67])). % 39.24/10.52 cnf(d69, plain, product(X0,sK10(sK13,sK14)) = product(X0,sK10(sK13,sK14)), inference(demodulation, [status(thm)], [d68,d61])). % 39.24/10.52 cnf(d70, plain, product(sK14,product(sK13,sK14)) = sK14 | sK14 != sK14 | r(sK14,product(sK14,sK10(sK13,sK14))), inference(resolution, [status(thm)], [d69,d53])). % 39.24/10.52 cnf(d71, plain, product(sK14,product(sK13,sK14)) = sK14 | r(sK14,product(sK14,sK10(sK13,sK14))), inference(equality_resolution, [status(thm)], [d70])). % 39.24/10.52 cnf(d72, plain, product(sK14,product(sK13,sK14)) = sK14 | product(product(sK14,sK10(sK13,sK14)),sK14) = sK14, inference(resolution, [status(thm)], [d71,c6])). % 39.24/10.52 cnf(d73, plain, product(sK14,product(sK10(sK13,sK14),sK14)) = sK14 | product(sK14,product(sK13,sK14)) = sK14, inference(demodulation, [status(thm)], [d72,c0])). % 39.24/10.52 cnf(d74, plain, product(sK13,X0) = product(sK13,product(sK14,product(sK13,X0))), inference(superposition, [status(thm)], [d43,d67])). % 39.24/10.52 cnf(d75, plain, product(sK13,sK10(sK13,sK14)) = product(sK13,product(sK14,sK10(sK13,sK14))), inference(superposition, [status(thm)], [d61,d74])). % 39.24/10.52 cnf(d76, plain, sK10(sK13,sK14) = product(sK13,product(sK14,sK10(sK13,sK14))), inference(demodulation, [status(thm)], [d75,d61])). % 39.24/10.52 cnf(d77, plain, product(sK13,product(product(sK14,sK10(sK13,sK14)),X0)) = product(sK10(sK13,sK14),X0), inference(superposition, [status(thm)], [d76,c0])). % 39.24/10.52 cnf(d78, plain, product(sK13,product(sK14,product(sK10(sK13,sK14),X0))) = product(sK10(sK13,sK14),X0), inference(demodulation, [status(thm)], [d77,c0])). % 39.24/10.52 cnf(d79, plain, product(sK13,sK14) = product(sK10(sK13,sK14),sK14) | product(sK14,product(sK13,sK14)) = sK14, inference(superposition, [status(thm)], [d73,d78])). % 39.24/10.52 cnf(d80, plain, product(sK14,product(sK13,sK14)) = sK14 | product(sK14,product(sK13,sK14)) = sK14 | product(sK14,product(sK13,sK14)) = sK14, inference(superposition, [status(thm)], [d79,d73])). % 39.24/10.52 cnf(d81, plain, sK14 != sK14 | product(product(sK13,sK14),sK14) != product(sK13,sK14) | l(product(sK13,sK14),sK14), inference(superposition, [status(thm)], [d80,c4])). % 39.24/10.52 cnf(d82, plain, product(sK13,product(sK14,sK14)) != product(sK13,sK14) | sK14 != sK14 | l(product(sK13,sK14),sK14), inference(demodulation, [status(thm)], [d81,c0])). % 39.24/10.52 cnf(d83, plain, product(sK13,sK14) != product(sK13,sK14) | sK14 != sK14 | l(product(sK13,sK14),sK14), inference(demodulation, [status(thm)], [d82,c1])). % 39.24/10.52 cnf(d84, plain, product(sK14,product(sK13,sK14)) = product(sK14,sK14), inference(superposition, [status(thm)], [d80,d37])). % 39.24/10.52 cnf(d85, plain, sK14 = product(sK14,sK14), inference(demodulation, [status(thm)], [d84,d80])). % 39.24/10.52 cnf(d86, plain, sK14 = sK14, inference(demodulation, [status(thm)], [d85,c1])). % 39.24/10.52 cnf(d87, plain, product(sK13,sK14) != product(sK13,sK14) | l(product(sK13,sK14),sK14), inference(resolution, [status(thm)], [d86,d83])). % 39.24/10.52 cnf(d88, plain, product(X1,product(X0,product(X1,X0))) = product(X1,product(X0,X0)), inference(superposition, [status(thm)], [c1,d23])). % 39.24/10.52 cnf(d89, plain, product(X0,X1) = product(X0,product(X1,X1)), inference(demodulation, [status(thm)], [d88,d33])). % 39.24/10.52 cnf(d90, plain, product(X1,X0) = product(X1,X0), inference(demodulation, [status(thm)], [d89,c1])). % 39.24/10.52 cnf(d91, plain, l(product(sK13,sK14),sK14), inference(resolution, [status(thm)], [d90,d87])). % 39.24/10.52 cnf(d92, plain, d(sK13,sK14), inference(resolution, [status(thm)], [d91,d48])). % 39.24/10.52 cnf(d93, plain, product(sK14,product(sK13,sK14)) != sK14 | 'Ts12'(sK13,sK14), inference(resolution, [status(thm)], [d31,c12])). % 39.24/10.52 cnf(d94, plain, 'Ts12'(sK13,sK14), inference(resolution, [status(thm)], [d80,d93])). % 39.24/10.52 cnf(d95, plain, ~d(sK13,sK14), inference(resolution, [status(thm)], [d94,c13])). % 39.24/10.52 cnf(d96, plain, $false, inference(resolution, [status(thm)], [d95,d92])). % 39.24/10.52 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------