%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SYN551+2 : TPTP v9.3.1. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n017.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 09:29:04 AM UTC 2026 % Result : Theorem 46.25s 7.30s % Output : CNFRefutation 46.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN551+2 : TPTP v9.3.1. Bugfixed v3.1.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.36 % Computer : n017.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 26 18:08:50 UTC 2026 % 0.10/0.36 % CPUTime : % 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.25/7.30 % SZS status Theorem for theBenchmark.p % 46.25/7.30 % SZS output start CNFRefutation for theBenchmark.p % 46.25/7.30 fof(prove_this_cute_thing, conjecture, (? [X0] : ! [X1] : ((X1 = f(g(X1)) <=> X0 = X1)) <=> ? [X0] : ! [X1] : ((X1 = g(f(X1)) <=> X0 = X1)))). % 46.25/7.30 fof(negated_conjecture, negated_conjecture, ~((? [X0] : ! [X1] : ((X1 = f(g(X1)) <=> X0 = X1)) <=> ? [X0] : ! [X1] : ((X1 = g(f(X1)) <=> X0 = X1)))), inference(negate_conjecture, [status(cth)], [prove_this_cute_thing])). % 46.25/7.30 cnf(c0, plain, X0 | X1, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c1, plain, ~X0 | f(g(X1)) != X1 | X1 = sK2, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c2, plain, ~X0 | f(g(X1)) = X1 | X1 != sK2, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c4, plain, ~X0 | g(f(sK5(X1))) = sK5(X1) | sK5(X1) = X1, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c5, plain, ~X0 | sK5(X1) != X1 | g(f(sK5(X1))) != sK5(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c8, plain, ~X0 | f(g(sK7(X1))) = sK7(X1) | sK7(X1) = X1, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c9, plain, ~X0 | sK7(X1) != X1 | f(g(sK7(X1))) != sK7(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c11, plain, ~X0 | g(f(X1)) != X1 | X1 = sK8, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(c12, plain, ~X0 | g(f(X1)) = X1 | X1 != sK8, inference(clausification, [status(esa)], [negated_conjecture])). % 46.25/7.30 cnf(d0, plain, f(g(sK2)) = sK2 | ~'Ts0', inference(equality_resolution, [status(thm)], [c2])). % 46.25/7.30 cnf(d1, plain, f(g(sK7(X0))) = sK7(X0) | sK7(X0) = X0 | 'Ts0', inference(resolution, [status(thm)], [c8,c0])). % 46.25/7.30 cnf(d2, plain, f(g(sK7(X0))) = sK7(X0) | sK7(X0) = X0 | f(g(sK2)) = sK2, inference(resolution, [status(thm)], [d1,d0])). % 46.25/7.30 cnf(d3, plain, g(sK7(X0)) != g(sK7(X0)) | g(sK7(X0)) = sK8 | ~'Ts1' | f(g(sK2)) = sK2 | sK7(X0) = X0, inference(superposition, [status(thm)], [d2,c11])). % 46.25/7.30 cnf(d4, plain, f(g(sK2)) = sK2 | g(sK7(X0)) = sK8 | sK7(X0) = X0 | ~'Ts1', inference(equality_resolution, [status(thm)], [d3])). % 46.25/7.30 cnf(d5, plain, f(g(sK2)) = sK2 | g(sK7(X0)) = sK8 | sK7(X0) = X0 | 'Ts0', inference(resolution, [status(thm)], [d4,c0])). % 46.25/7.30 cnf(d6, plain, f(g(sK2)) = sK2 | f(g(sK2)) = sK2 | g(sK7(X0)) = sK8 | sK7(X0) = X0, inference(resolution, [status(thm)], [d0,d5])). % 46.25/7.30 cnf(d7, plain, f(sK8) = sK7(X0) | f(g(sK2)) = sK2 | sK7(X0) = X0 | f(g(sK2)) = sK2 | sK7(X0) = X0, inference(superposition, [status(thm)], [d6,d2])). % 46.25/7.30 cnf(d8, plain, f(sK8) != X0 | f(g(sK2)) = sK2 | sK7(X0) = X0, inference(equality_factoring, [status(thm)], [d7])). % 46.25/7.30 cnf(d9, plain, f(g(sK2)) = sK2 | sK7(f(sK8)) = f(sK8), inference(equality_resolution, [status(thm)], [d8])). % 46.25/7.30 cnf(d10, plain, f(g(f(sK8))) != sK7(f(sK8)) | sK7(f(sK8)) != f(sK8) | ~'Ts1' | f(g(sK2)) = sK2, inference(superposition, [status(thm)], [d9,c9])). % 46.25/7.30 cnf(d11, plain, f(g(f(sK8))) = sK7(X0) | f(g(sK2)) = sK2 | sK7(X0) = X0 | f(g(sK2)) = sK2 | sK7(X0) = X0, inference(superposition, [status(thm)], [d7,d2])). % 46.25/7.30 cnf(d12, plain, f(g(f(sK8))) != X0 | f(g(sK2)) = sK2 | sK7(X0) = X0, inference(equality_factoring, [status(thm)], [d11])). % 46.25/7.30 cnf(d13, plain, f(g(sK2)) = sK2 | sK7(f(g(f(sK8)))) = f(g(f(sK8))), inference(equality_resolution, [status(thm)], [d12])). % 46.25/7.30 cnf(d14, plain, g(f(sK8)) = sK8 | ~'Ts1', inference(equality_resolution, [status(thm)], [c12])). % 46.25/7.30 cnf(d15, plain, g(f(sK8)) = sK8 | 'Ts0', inference(resolution, [status(thm)], [d14,c0])). % 46.25/7.30 cnf(d16, plain, g(f(sK8)) = sK8 | f(g(sK2)) = sK2, inference(resolution, [status(thm)], [d15,d0])). % 46.25/7.30 cnf(d17, plain, sK7(f(sK8)) = f(g(f(sK8))) | f(g(sK2)) = sK2 | f(g(sK2)) = sK2, inference(superposition, [status(thm)], [d16,d13])). % 46.25/7.30 cnf(d18, plain, sK7(f(sK8)) != X0 | f(g(sK2)) = sK2 | sK7(X0) = X0 | f(g(sK2)) = sK2, inference(superposition, [status(thm)], [d17,d12])). % 46.25/7.30 cnf(d19, plain, f(g(sK2)) = sK2 | sK7(f(sK8)) != f(sK8) | f(g(f(sK8))) != sK7(f(sK8)) | f(g(sK2)) = sK2 | ~'Ts1', inference(resolution, [status(thm)], [d18,d10])). % 46.25/7.30 cnf(d20, plain, f(g(sK2)) = sK2 | f(g(f(sK8))) != sK7(f(sK8)) | f(g(sK2)) = sK2 | ~'Ts1', inference(resolution, [status(thm)], [d9,d19])). % 46.25/7.30 cnf(d21, plain, f(g(sK2)) = sK2 | sK7(sK7(f(sK8))) = sK7(f(sK8)), inference(equality_resolution, [status(thm)], [d18])). % 46.25/7.30 cnf(d22, plain, sK7(sK7(f(sK8))) = f(g(f(sK8))) | f(g(sK2)) = sK2 | f(g(sK2)) = sK2, inference(superposition, [status(thm)], [d17,d13])). % 46.25/7.30 cnf(d23, plain, f(g(f(sK8))) = sK7(f(sK8)) | f(g(sK2)) = sK2 | f(g(sK2)) = sK2, inference(superposition, [status(thm)], [d22,d21])). % 46.25/7.30 cnf(d24, plain, f(g(sK2)) = sK2 | f(g(sK2)) = sK2 | ~'Ts1', inference(resolution, [status(thm)], [d23,d20])). % 46.25/7.30 cnf(d25, plain, f(g(sK2)) = sK2 | 'Ts0', inference(resolution, [status(thm)], [d24,c0])). % 46.25/7.30 cnf(d26, plain, f(g(sK2)) = sK2 | f(g(sK2)) = sK2, inference(resolution, [status(thm)], [d0,d25])). % 46.25/7.30 cnf(d27, plain, g(sK2) != g(sK2) | g(sK2) = sK8 | ~'Ts1', inference(superposition, [status(thm)], [d26,c11])). % 46.25/7.30 cnf(d28, plain, g(sK2) = sK8 | ~'Ts1', inference(equality_resolution, [status(thm)], [d27])). % 46.25/7.30 cnf(d29, plain, g(sK2) = sK8 | 'Ts0', inference(resolution, [status(thm)], [d28,c0])). % 46.25/7.30 cnf(d30, plain, g(f(sK8)) = sK8 | g(f(sK5(X0))) = sK5(X0) | sK5(X0) = X0, inference(resolution, [status(thm)], [d15,c4])). % 46.25/7.30 cnf(d31, plain, f(sK5(X0)) != f(sK5(X0)) | f(sK5(X0)) = sK2 | ~'Ts0' | g(f(sK8)) = sK8 | sK5(X0) = X0, inference(superposition, [status(thm)], [d30,c1])). % 46.25/7.30 cnf(d32, plain, g(f(sK8)) = sK8 | f(sK5(X0)) != f(sK5(X0)) | f(sK5(X0)) = sK2 | g(f(sK8)) = sK8 | sK5(X0) = X0, inference(resolution, [status(thm)], [d15,d31])). % 46.25/7.30 cnf(d33, plain, f(sK5(X0)) = sK2 | g(f(sK8)) = sK8 | sK5(X0) = X0, inference(equality_resolution, [status(thm)], [d32])). % 46.25/7.30 cnf(d34, plain, g(sK2) = sK5(X0) | g(f(sK8)) = sK8 | sK5(X0) = X0 | g(f(sK8)) = sK8 | sK5(X0) = X0, inference(superposition, [status(thm)], [d33,d30])). % 46.25/7.30 cnf(d35, plain, g(sK2) != X0 | g(f(sK8)) = sK8 | sK5(X0) = X0, inference(equality_factoring, [status(thm)], [d34])). % 46.25/7.30 cnf(d36, plain, g(f(sK8)) = sK8 | sK5(g(sK2)) = g(sK2), inference(equality_resolution, [status(thm)], [d35])). % 46.25/7.30 cnf(d37, plain, g(f(g(sK2))) != sK5(g(sK2)) | sK5(g(sK2)) != g(sK2) | ~'Ts0' | g(f(sK8)) = sK8, inference(superposition, [status(thm)], [d36,c5])). % 46.25/7.30 cnf(d38, plain, g(sK2) != sK5(g(sK2)) | g(f(sK8)) = sK8 | sK5(g(sK2)) != g(sK2) | ~'Ts0', inference(demodulation, [status(thm)], [d37,d26])). % 46.25/7.30 cnf(d39, plain, g(f(sK8)) = sK8 | g(sK2) != sK5(g(sK2)) | g(f(sK8)) = sK8 | sK5(g(sK2)) != g(sK2), inference(resolution, [status(thm)], [d15,d38])). % 46.25/7.30 cnf(d40, plain, X0 != g(sK2) | g(f(sK8)) = sK8 | g(sK2) = sK5(X0), inference(equality_factoring, [status(thm)], [d34])). % 46.25/7.30 cnf(d41, plain, g(f(sK8)) = sK8 | g(sK2) = sK5(g(sK2)), inference(equality_resolution, [status(thm)], [d40])). % 46.25/7.30 cnf(d42, plain, g(f(sK8)) = sK8 | g(f(sK8)) = sK8 | sK5(g(sK2)) != g(sK2), inference(resolution, [status(thm)], [d41,d39])). % 46.25/7.30 cnf(d43, plain, g(f(sK8)) = sK8 | g(f(sK8)) = sK8, inference(resolution, [status(thm)], [d36,d42])). % 46.25/7.30 cnf(d44, plain, f(sK8) != f(sK8) | f(sK8) = sK2 | ~'Ts0', inference(superposition, [status(thm)], [d43,c1])). % 46.25/7.30 cnf(d45, plain, f(sK8) = sK2 | ~'Ts0', inference(equality_resolution, [status(thm)], [d44])). % 46.25/7.30 cnf(d46, plain, f(sK8) = sK2 | g(sK2) = sK8, inference(resolution, [status(thm)], [d45,d29])). % 46.25/7.30 cnf(d47, plain, f(sK8) = sK2 | f(sK8) = sK2, inference(superposition, [status(thm)], [d46,d26])). % 46.25/7.30 cnf(d48, plain, g(sK2) = sK8, inference(demodulation, [status(thm)], [d43,d47])). % 46.25/7.30 cnf(d49, plain, sK7(f(sK8)) = f(g(f(sK8))) | f(g(sK2)) = sK2 | f(g(sK2)) = sK2 | sK7(f(sK8)) = f(sK8), inference(superposition, [status(thm)], [d7,d22])). % 46.25/7.30 cnf(d50, plain, f(sK8) = sK2 | sK7(f(sK8)) = f(g(f(sK8))) | sK7(f(sK8)) = f(sK8), inference(demodulation, [status(thm)], [d49,d48])). % 46.25/7.30 cnf(d51, plain, sK2 = sK2 | sK7(f(sK8)) = f(g(f(sK8))) | sK7(f(sK8)) = f(sK8), inference(demodulation, [status(thm)], [d50,d47])). % 46.25/7.30 cnf(d52, plain, sK2 = sK2 | sK7(sK2) = f(g(f(sK8))) | sK7(f(sK8)) = f(sK8), inference(demodulation, [status(thm)], [d51,d47])). % 46.25/7.30 cnf(d53, plain, sK2 = sK2 | sK7(sK2) = f(g(sK2)) | sK7(f(sK8)) = f(sK8), inference(demodulation, [status(thm)], [d52,d47])). % 46.25/7.30 cnf(d54, plain, sK2 = sK2 | sK7(sK2) = f(sK8) | sK7(f(sK8)) = f(sK8), inference(demodulation, [status(thm)], [d53,d48])). % 46.25/7.30 cnf(d55, plain, sK2 = sK2 | sK7(sK2) = sK2 | sK7(f(sK8)) = f(sK8), inference(demodulation, [status(thm)], [d54,d47])). % 46.25/7.30 cnf(d56, plain, sK2 = sK2 | sK7(sK2) = sK2 | sK7(sK2) = f(sK8), inference(demodulation, [status(thm)], [d55,d47])). % 46.25/7.30 cnf(d57, plain, sK2 = sK2 | sK7(sK2) = sK2 | sK7(sK2) = sK2, inference(demodulation, [status(thm)], [d56,d47])). % 46.25/7.30 cnf(d58, plain, f(g(sK7(X0))) = sK7(X0) | sK7(X0) = X0 | g(f(sK5(X1))) = sK5(X1) | sK5(X1) = X1, inference(resolution, [status(thm)], [d1,c4])). % 46.25/7.30 cnf(d59, plain, f(sK5(X0)) != f(sK5(X0)) | f(sK5(X0)) = sK2 | ~'Ts0' | f(g(sK7(X1))) = sK7(X1) | sK5(X0) = X0 | sK7(X1) = X1, inference(superposition, [status(thm)], [d58,c1])). % 46.25/7.30 cnf(d60, plain, f(g(sK7(X0))) = sK7(X0) | f(sK5(X1)) = sK2 | sK5(X1) = X1 | sK7(X0) = X0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d59])). % 46.25/7.30 cnf(d61, plain, f(g(sK7(X0))) = sK7(X0) | f(sK5(X1)) = sK2 | sK5(X1) = X1 | sK7(X0) = X0 | f(g(sK7(X2))) = sK7(X2) | sK7(X2) = X2, inference(resolution, [status(thm)], [d60,d1])). % 46.25/7.30 cnf(d62, plain, f(g(sK7(X0))) = sK7(X0) | f(sK5(X1)) = sK2 | sK5(X1) = X1 | sK7(X0) = X0 | sK7(X0) = X0, inference(factoring, [status(thm)], [d61])). % 46.25/7.30 cnf(d63, plain, g(sK2) = sK5(X0) | f(g(sK7(X1))) = sK7(X1) | sK5(X0) = X0 | sK7(X1) = X1 | f(g(sK7(X2))) = sK7(X2) | sK5(X0) = X0 | sK7(X2) = X2, inference(superposition, [status(thm)], [d62,d58])). % 46.25/7.30 cnf(d64, plain, f(g(sK7(X0))) = sK7(X0) | f(g(sK7(X1))) = sK7(X1) | sK8 = sK5(X2) | sK5(X2) = X2 | sK7(X0) = X0 | sK7(X1) = X1, inference(demodulation, [status(thm)], [d63,d48])). % 46.25/7.30 cnf(d65, plain, sK8 != X0 | f(g(sK7(X1))) = sK7(X1) | f(g(sK7(X2))) = sK7(X2) | sK5(X0) = X0 | sK7(X1) = X1 | sK7(X2) = X2, inference(equality_factoring, [status(thm)], [d64])). % 46.25/7.30 cnf(d66, plain, f(g(sK7(X0))) = sK7(X0) | sK5(X1) = X1 | sK7(X0) = X0 | sK7(X0) = X0 | sK8 != X1, inference(factoring, [status(thm)], [d65])). % 46.25/7.30 cnf(d67, plain, f(g(sK7(X0))) = sK7(X0) | sK5(sK8) = sK8 | sK7(X0) = X0, inference(equality_resolution, [status(thm)], [d66])). % 46.25/7.30 cnf(d68, plain, sK7(X0) != sK7(X0) | sK7(X0) = sK2 | ~'Ts0' | sK5(sK8) = sK8 | sK7(X0) = X0, inference(superposition, [status(thm)], [d67,c1])). % 46.25/7.30 cnf(d69, plain, sK5(sK8) = sK8 | sK7(X0) = X0 | sK7(X0) = sK2 | ~'Ts0', inference(equality_resolution, [status(thm)], [d68])). % 46.25/7.30 cnf(d70, plain, g(sK7(X0)) != g(sK7(X0)) | g(sK7(X0)) = sK8 | ~'Ts1' | g(f(sK5(X1))) = sK5(X1) | sK5(X1) = X1 | sK7(X0) = X0, inference(superposition, [status(thm)], [d58,c11])). % 46.25/7.30 cnf(d71, plain, g(f(sK5(X0))) = sK5(X0) | g(sK7(X1)) = sK8 | sK5(X0) = X0 | sK7(X1) = X1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d70])). % 46.25/7.30 cnf(d72, plain, g(f(sK5(X0))) = sK5(X0) | g(sK7(X1)) = sK8 | sK5(X0) = X0 | sK7(X1) = X1 | 'Ts0', inference(resolution, [status(thm)], [d71,c0])). % 46.25/7.30 cnf(d73, plain, g(f(sK5(X0))) = sK5(X0) | g(sK7(X1)) = sK8 | sK5(X0) = X0 | sK7(X1) = X1 | g(f(sK5(X2))) = sK5(X2) | sK5(X2) = X2, inference(resolution, [status(thm)], [d72,c4])). % 46.25/7.30 cnf(d74, plain, g(f(sK5(X0))) = sK5(X0) | g(sK7(X1)) = sK8 | sK5(X0) = X0 | sK5(X0) = X0 | sK7(X1) = X1, inference(factoring, [status(thm)], [d73])). % 46.25/7.30 cnf(d75, plain, f(sK8) = sK7(X0) | g(f(sK5(X1))) = sK5(X1) | sK5(X1) = X1 | sK7(X0) = X0 | g(f(sK5(X2))) = sK5(X2) | sK5(X2) = X2 | sK7(X0) = X0, inference(superposition, [status(thm)], [d74,d58])). % 46.25/7.30 cnf(d76, plain, sK2 = sK7(X0) | g(f(sK5(X1))) = sK5(X1) | g(f(sK5(X2))) = sK5(X2) | sK5(X1) = X1 | sK5(X2) = X2 | sK7(X0) = X0, inference(demodulation, [status(thm)], [d75,d47])). % 46.25/7.30 cnf(d77, plain, sK2 != X0 | g(f(sK5(X1))) = sK5(X1) | g(f(sK5(X2))) = sK5(X2) | sK5(X1) = X1 | sK5(X2) = X2 | sK7(X0) = X0, inference(equality_factoring, [status(thm)], [d76])). % 46.25/7.30 cnf(d78, plain, g(f(sK5(X0))) = sK5(X0) | sK2 != X1 | sK5(X0) = X0 | sK5(X0) = X0 | sK7(X1) = X1, inference(factoring, [status(thm)], [d77])). % 46.25/7.30 cnf(d79, plain, g(f(sK5(X0))) = sK5(X0) | sK5(X0) = X0 | sK7(sK2) = sK2, inference(equality_resolution, [status(thm)], [d78])). % 46.25/7.30 cnf(d80, plain, sK5(X0) != sK5(X0) | sK5(X0) = sK8 | ~'Ts1' | sK5(X0) = X0 | sK7(sK2) = sK2, inference(superposition, [status(thm)], [d79,c11])). % 46.25/7.30 cnf(d81, plain, sK5(X0) = X0 | sK5(X0) = sK8 | sK7(sK2) = sK2 | ~'Ts1', inference(equality_resolution, [status(thm)], [d80])). % 46.25/7.30 cnf(d82, plain, sK5(X0) = X0 | sK5(X0) = sK8 | sK7(sK2) = sK2 | 'Ts0', inference(resolution, [status(thm)], [d81,c0])). % 46.25/7.30 cnf(d83, plain, sK5(X0) = X0 | sK5(X0) = sK8 | sK7(sK2) = sK2 | sK5(sK8) = sK8 | sK7(X1) = X1 | sK7(X1) = sK2, inference(resolution, [status(thm)], [d82,d69])). % 46.25/7.30 cnf(d84, plain, sK5(sK8) = sK8 | sK5(sK8) = sK8 | sK7(X0) = X0 | sK7(X0) = sK2 | sK7(sK2) = sK2, inference(factoring, [status(thm)], [d83])). % 46.25/7.30 cnf(d85, plain, sK5(sK8) = sK8 | sK7(sK2) = sK2 | sK7(sK2) = sK2, inference(factoring, [status(thm)], [d84])). % 46.25/7.30 cnf(d86, plain, f(g(sK2)) != sK7(sK2) | sK7(sK2) != sK2 | ~'Ts1' | sK5(sK8) = sK8, inference(superposition, [status(thm)], [d85,c9])). % 46.25/7.30 cnf(d87, plain, f(sK8) != sK7(sK2) | sK5(sK8) = sK8 | sK7(sK2) != sK2 | ~'Ts1', inference(demodulation, [status(thm)], [d86,d48])). % 46.25/7.30 cnf(d88, plain, sK2 != sK7(sK2) | sK5(sK8) = sK8 | sK7(sK2) != sK2 | ~'Ts1', inference(demodulation, [status(thm)], [d87,d47])). % 46.25/7.30 cnf(d89, plain, sK5(sK8) = sK8 | sK2 != sK7(sK2) | sK5(sK8) = sK8 | ~'Ts1', inference(resolution, [status(thm)], [d85,d88])). % 46.25/7.30 cnf(d90, plain, sK2 != sK2 | sK5(sK8) = sK8 | ~'Ts1' | sK5(sK8) = sK8, inference(superposition, [status(thm)], [d85,d89])). % 46.25/7.30 cnf(d91, plain, sK5(sK8) = sK8 | ~'Ts1', inference(equality_resolution, [status(thm)], [d90])). % 46.25/7.30 cnf(d92, plain, sK5(sK8) = sK8 | 'Ts0', inference(resolution, [status(thm)], [d91,c0])). % 46.25/7.30 cnf(d93, plain, sK5(sK8) = sK8 | g(f(sK5(X0))) = sK5(X0) | sK5(X0) = X0, inference(resolution, [status(thm)], [d92,c4])). % 46.25/7.30 cnf(d94, plain, f(sK5(X0)) != f(sK5(X0)) | f(sK5(X0)) = sK2 | ~'Ts0' | sK5(X0) = X0 | sK5(sK8) = sK8, inference(superposition, [status(thm)], [d93,c1])). % 46.25/7.30 cnf(d95, plain, sK5(sK8) = sK8 | f(sK5(X0)) != f(sK5(X0)) | f(sK5(X0)) = sK2 | sK5(X0) = X0 | sK5(sK8) = sK8, inference(resolution, [status(thm)], [d92,d94])). % 46.25/7.30 cnf(d96, plain, f(sK5(X0)) = sK2 | sK5(X0) = X0 | sK5(sK8) = sK8, inference(equality_resolution, [status(thm)], [d95])). % 46.25/7.30 cnf(d97, plain, g(sK2) = sK5(X0) | sK5(X0) = X0 | sK5(sK8) = sK8 | sK5(X0) = X0 | sK5(sK8) = sK8, inference(superposition, [status(thm)], [d96,d93])). % 46.25/7.30 cnf(d98, plain, sK8 = sK5(X0) | sK5(X0) = X0 | sK5(sK8) = sK8, inference(demodulation, [status(thm)], [d97,d48])). % 46.25/7.30 cnf(d99, plain, sK8 != sK8 | sK5(sK8) = sK8 | sK5(sK8) = sK8, inference(equality_factoring, [status(thm)], [d98])). % 46.25/7.30 cnf(d100, plain, sK5(sK8) = sK8, inference(equality_resolution, [status(thm)], [d99])). % 46.25/7.30 cnf(d101, plain, g(f(sK8)) != sK5(sK8) | sK5(sK8) != sK8 | ~'Ts0', inference(superposition, [status(thm)], [d100,c5])). % 46.25/7.30 cnf(d102, plain, g(sK2) != sK5(sK8) | sK5(sK8) != sK8 | ~'Ts0', inference(demodulation, [status(thm)], [d101,d47])). % 46.25/7.30 cnf(d103, plain, sK8 != sK5(sK8) | sK5(sK8) != sK8 | ~'Ts0', inference(demodulation, [status(thm)], [d102,d48])). % 46.25/7.30 cnf(d104, plain, sK8 != sK8 | sK5(sK8) != sK8 | ~'Ts0', inference(demodulation, [status(thm)], [d103,d100])). % 46.25/7.30 cnf(d105, plain, sK8 != sK8 | sK8 != sK8 | ~'Ts0', inference(demodulation, [status(thm)], [d104,d100])). % 46.25/7.30 cnf(d106, plain, sK8 != sK8 | ~'Ts0', inference(equality_resolution, [status(thm)], [d105])). % 46.25/7.30 cnf(d107, plain, ~'Ts0', inference(equality_resolution, [status(thm)], [d106])). % 46.25/7.30 cnf(d108, plain, f(g(sK7(X0))) = sK7(X0) | sK7(X0) = X0, inference(resolution, [status(thm)], [d107,d1])). % 46.25/7.30 cnf(d109, plain, 'Ts1', inference(resolution, [status(thm)], [d107,c0])). % 46.25/7.30 cnf(d110, plain, X0 = sK8 | g(f(X0)) != X0, inference(resolution, [status(thm)], [d109,c11])). % 46.25/7.30 cnf(d111, plain, g(sK7(X0)) != g(sK7(X0)) | g(sK7(X0)) = sK8 | sK7(X0) = X0, inference(superposition, [status(thm)], [d108,d110])). % 46.25/7.30 cnf(d112, plain, g(sK7(X0)) = sK8 | sK7(X0) = X0, inference(equality_resolution, [status(thm)], [d111])). % 46.25/7.30 cnf(d113, plain, f(sK8) = sK7(X0) | sK7(X0) = X0 | sK7(X0) = X0, inference(superposition, [status(thm)], [d112,d108])). % 46.25/7.30 cnf(d114, plain, sK2 = sK7(X0) | sK7(X0) = X0, inference(demodulation, [status(thm)], [d113,d47])). % 46.25/7.30 cnf(d115, plain, sK2 != X0 | sK7(X0) = X0, inference(equality_factoring, [status(thm)], [d114])). % 46.25/7.30 cnf(d116, plain, sK7(sK2) = sK2 | sK7(sK2) = sK2 | sK7(sK2) = sK2, inference(resolution, [status(thm)], [d115,d57])). % 46.25/7.30 cnf(d117, plain, f(g(sK7(X0))) != sK7(X0) | sK7(X0) != X0, inference(resolution, [status(thm)], [d109,c9])). % 46.25/7.30 cnf(d118, plain, f(g(sK2)) != sK7(sK2) | sK7(sK2) != sK2, inference(superposition, [status(thm)], [d116,d117])). % 46.25/7.30 cnf(d119, plain, f(sK8) != sK7(sK2) | sK7(sK2) != sK2, inference(demodulation, [status(thm)], [d118,d48])). % 46.25/7.30 cnf(d120, plain, sK2 != sK7(sK2) | sK7(sK2) != sK2, inference(demodulation, [status(thm)], [d119,d47])). % 46.25/7.30 cnf(d121, plain, sK2 != sK2 | sK7(sK2) != sK2, inference(demodulation, [status(thm)], [d120,d116])). % 46.25/7.30 cnf(d122, plain, sK2 != sK2 | sK2 != sK2, inference(demodulation, [status(thm)], [d121,d116])). % 46.25/7.30 cnf(d123, plain, sK2 != sK2, inference(equality_resolution, [status(thm)], [d122])). % 46.25/7.30 cnf(d124, plain, $false, inference(equality_resolution, [status(thm)], [d123])). % 46.25/7.30 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------