%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SYN551+3 : 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 : n001.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 12.85s 2.03s % Output : CNFRefutation 12.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN551+3 : 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.11/0.36 % Computer : n001.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 26 18:19:00 UTC 2026 % 0.14/0.36 % CPUTime : % 0.14/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 12.85/2.03 % SZS status Theorem for theBenchmark.p % 12.85/2.03 % SZS output start CNFRefutation for theBenchmark.p % 12.85/2.03 fof(prove_this_cute_thing, conjecture, (? [X0] : ((X0 = f(g(X0)) & ! [X1] : ((X1 = f(g(X1)) => X1 = X0)))) <=> ? [X0] : ((X0 = g(f(X0)) & ! [X1] : ((X1 = g(f(X1)) => X1 = X0)))))). % 12.85/2.03 fof(negated_conjecture, negated_conjecture, ~((? [X0] : ((X0 = f(g(X0)) & ! [X1] : ((X1 = f(g(X1)) => X1 = X0)))) <=> ? [X0] : ((X0 = g(f(X0)) & ! [X1] : ((X1 = g(f(X1)) => X1 = X0)))))), inference(negate_conjecture, [status(cth)], [prove_this_cute_thing])). % 12.85/2.03 cnf(c1, plain, X0 | sK3 = g(f(sK3)), inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c2, plain, X0 | X1 != g(f(X1)) | X1 = sK3, inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c3, plain, X0 != g(f(X0)) | sK2(X0) = g(f(sK2(X0))) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c4, plain, X0 != g(f(X0)) | sK2(X0) = g(f(sK2(X0))) | sK3 = g(f(sK3)), inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c6, plain, X0 != g(f(X0)) | sK2(X0) != X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c7, plain, X0 != g(f(X0)) | sK2(X0) != X0 | sK3 = g(f(sK3)), inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c9, plain, ~X0 | sK5 = f(g(sK5)), inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c10, plain, ~X0 | X1 != f(g(X1)) | X1 = sK5, inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c11, plain, X0 | X1 != f(g(X1)) | sK8(X1) = f(g(sK8(X1))), inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(c12, plain, X0 | X1 != f(g(X1)) | sK8(X1) != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 12.85/2.03 cnf(d0, plain, sK5 = f(g(sK5)) | sK3 = g(f(sK3)), inference(resolution, [status(thm)], [c9,c1])). % 12.85/2.03 cnf(d1, plain, g(sK5) != g(sK5) | sK3 = g(f(sK3)) | sK2(g(sK5)) != g(sK5) | sK3 = g(f(sK3)), inference(superposition, [status(thm)], [d0,c7])). % 12.85/2.03 cnf(d2, plain, g(sK5) != g(sK5) | sK3 = g(f(sK3)) | sK2(g(sK5)) = g(f(sK2(g(sK5)))) | sK3 = g(f(sK3)), inference(superposition, [status(thm)], [d0,c4])). % 12.85/2.03 cnf(d3, plain, sK3 = g(f(sK3)) | sK2(g(sK5)) = g(f(sK2(g(sK5)))), inference(equality_resolution, [status(thm)], [d2])). % 12.85/2.03 cnf(d4, plain, f(sK2(g(sK5))) != f(sK2(g(sK5))) | f(sK2(g(sK5))) = sK5 | ~'Ts0' | sK3 = g(f(sK3)), inference(superposition, [status(thm)], [d3,c10])). % 12.85/2.03 cnf(d5, plain, sK3 = g(f(sK3)) | f(sK2(g(sK5))) = sK5 | ~'Ts0', inference(equality_resolution, [status(thm)], [d4])). % 12.85/2.03 cnf(d6, plain, sK3 = g(f(sK3)) | f(sK2(g(sK5))) = sK5 | sK3 = g(f(sK3)), inference(resolution, [status(thm)], [d5,c1])). % 12.85/2.03 cnf(d7, plain, sK2(g(sK5)) = g(sK5) | sK3 = g(f(sK3)) | sK3 = g(f(sK3)), inference(superposition, [status(thm)], [d6,d3])). % 12.85/2.03 cnf(d8, plain, g(sK5) != g(sK5) | sK3 = g(f(sK3)) | g(sK5) != g(sK5) | sK3 = g(f(sK3)), inference(superposition, [status(thm)], [d7,d1])). % 12.85/2.03 cnf(d9, plain, sK3 = g(f(sK3)), inference(equality_resolution, [status(thm)], [d8])). % 12.85/2.03 cnf(d10, plain, f(sK3) != f(sK3) | f(sK3) = sK5 | ~'Ts0', inference(superposition, [status(thm)], [d9,c10])). % 12.85/2.03 cnf(d11, plain, f(sK3) = sK5 | ~'Ts0', inference(equality_resolution, [status(thm)], [d10])). % 12.85/2.03 cnf(d12, plain, f(sK3) != f(sK3) | sK8(f(sK3)) != f(sK3) | 'Ts0', inference(superposition, [status(thm)], [d9,c12])). % 12.85/2.03 cnf(d13, plain, f(sK3) != f(sK3) | sK8(f(sK3)) = f(g(sK8(f(sK3)))) | 'Ts0', inference(superposition, [status(thm)], [d9,c11])). % 12.85/2.03 cnf(d14, plain, sK8(f(sK3)) = f(g(sK8(f(sK3)))) | 'Ts0', inference(equality_resolution, [status(thm)], [d13])). % 12.85/2.03 cnf(d15, plain, sK8(f(sK3)) = f(g(sK8(f(sK3)))) | f(sK3) = sK5, inference(resolution, [status(thm)], [d14,d11])). % 12.85/2.03 cnf(d16, plain, g(sK8(f(sK3))) != g(sK8(f(sK3))) | g(sK8(f(sK3))) = sK3 | 'Ts0' | f(sK3) = sK5, inference(superposition, [status(thm)], [d15,c2])). % 12.85/2.03 cnf(d17, plain, g(sK8(f(sK3))) = sK3 | f(sK3) = sK5 | 'Ts0', inference(equality_resolution, [status(thm)], [d16])). % 12.85/2.03 cnf(d18, plain, g(sK8(f(sK3))) = sK3 | f(sK3) = sK5 | f(sK3) = sK5, inference(resolution, [status(thm)], [d17,d11])). % 12.85/2.03 cnf(d19, plain, sK8(f(sK3)) = f(sK3) | f(sK3) = sK5 | f(sK3) = sK5, inference(superposition, [status(thm)], [d18,d15])). % 12.85/2.03 cnf(d20, plain, f(sK3) != f(sK3) | f(sK3) != f(sK3) | 'Ts0' | f(sK3) = sK5, inference(superposition, [status(thm)], [d19,d12])). % 12.85/2.03 cnf(d21, plain, f(sK3) = sK5 | 'Ts0', inference(equality_resolution, [status(thm)], [d20])). % 12.85/2.03 cnf(d22, plain, f(sK3) = sK5 | f(sK3) = sK5, inference(resolution, [status(thm)], [d21,d11])). % 12.85/2.03 cnf(d23, plain, sK5 != f(sK3) | sK8(f(sK3)) != f(sK3) | 'Ts0', inference(demodulation, [status(thm)], [d12,d22])). % 12.85/2.03 cnf(d24, plain, sK5 != sK5 | sK8(f(sK3)) != f(sK3) | 'Ts0', inference(demodulation, [status(thm)], [d23,d22])). % 12.85/2.03 cnf(d25, plain, sK5 != sK5 | sK8(sK5) != f(sK3) | 'Ts0', inference(demodulation, [status(thm)], [d24,d22])). % 12.85/2.03 cnf(d26, plain, sK5 != sK5 | sK8(sK5) != sK5 | 'Ts0', inference(demodulation, [status(thm)], [d25,d22])). % 12.85/2.03 cnf(d27, plain, sK3 != sK3 | sK2(sK3) != sK3 | ~'Ts0', inference(superposition, [status(thm)], [d9,c6])). % 12.85/2.03 cnf(d28, plain, sK3 = g(sK5), inference(demodulation, [status(thm)], [d9,d22])). % 12.85/2.03 cnf(d29, plain, sK3 != sK3 | sK2(sK3) = g(f(sK2(sK3))) | ~'Ts0', inference(superposition, [status(thm)], [d9,c3])). % 12.85/2.03 cnf(d30, plain, sK2(sK3) = g(f(sK2(sK3))) | ~'Ts0', inference(equality_resolution, [status(thm)], [d29])). % 12.85/2.03 cnf(d31, plain, sK8(f(sK3)) = f(g(sK8(f(sK3)))) | sK2(sK3) = g(f(sK2(sK3))), inference(resolution, [status(thm)], [d14,d30])). % 12.85/2.03 cnf(d32, plain, sK2(sK3) = g(f(sK2(sK3))) | sK8(sK5) = f(g(sK8(f(sK3)))), inference(demodulation, [status(thm)], [d31,d22])). % 12.85/2.03 cnf(d33, plain, sK2(sK3) = g(f(sK2(sK3))) | sK8(sK5) = f(g(sK8(sK5))), inference(demodulation, [status(thm)], [d32,d22])). % 12.85/2.03 cnf(d34, plain, g(sK8(f(sK3))) != g(sK8(f(sK3))) | g(sK8(f(sK3))) = sK3 | 'Ts0' | sK2(sK3) = g(f(sK2(sK3))), inference(superposition, [status(thm)], [d31,c2])). % 12.85/2.03 cnf(d35, plain, g(sK8(sK5)) = sK3 | g(sK8(f(sK3))) != g(sK8(f(sK3))) | sK2(sK3) = g(f(sK2(sK3))) | 'Ts0', inference(demodulation, [status(thm)], [d34,d22])). % 12.85/2.03 cnf(d36, plain, g(sK8(sK5)) = sK3 | g(sK8(sK5)) != g(sK8(f(sK3))) | sK2(sK3) = g(f(sK2(sK3))) | 'Ts0', inference(demodulation, [status(thm)], [d35,d22])). % 12.85/2.03 cnf(d37, plain, g(sK8(sK5)) = sK3 | g(sK8(sK5)) != g(sK8(sK5)) | sK2(sK3) = g(f(sK2(sK3))) | 'Ts0', inference(demodulation, [status(thm)], [d36,d22])). % 12.85/2.03 cnf(d38, plain, g(sK8(sK5)) = sK3 | sK2(sK3) = g(f(sK2(sK3))) | 'Ts0', inference(equality_resolution, [status(thm)], [d37])). % 12.85/2.03 cnf(d39, plain, g(sK8(sK5)) = sK3 | sK2(sK3) = g(f(sK2(sK3))) | sK2(sK3) = g(f(sK2(sK3))), inference(resolution, [status(thm)], [d38,d30])). % 12.85/2.03 cnf(d40, plain, sK2(sK3) != sK2(sK3) | sK2(sK3) = sK3 | 'Ts0' | g(sK8(sK5)) = sK3, inference(superposition, [status(thm)], [d39,c2])). % 12.85/2.03 cnf(d41, plain, g(sK8(sK5)) = sK3 | sK2(sK3) = sK3 | 'Ts0', inference(equality_resolution, [status(thm)], [d40])). % 12.85/2.03 cnf(d42, plain, f(sK2(sK3)) != f(sK2(sK3)) | f(sK2(sK3)) = sK5 | ~'Ts0' | g(sK8(sK5)) = sK3, inference(superposition, [status(thm)], [d39,c10])). % 12.85/2.03 cnf(d43, plain, g(sK8(sK5)) = sK3 | f(sK2(sK3)) = sK5 | ~'Ts0', inference(equality_resolution, [status(thm)], [d42])). % 12.85/2.03 cnf(d44, plain, g(sK8(sK5)) = sK3 | f(sK2(sK3)) = sK5 | g(sK8(sK5)) = sK3 | sK2(sK3) = sK3, inference(resolution, [status(thm)], [d43,d41])). % 12.85/2.03 cnf(d45, plain, sK2(sK3) = g(sK5) | g(sK8(sK5)) = sK3 | g(sK8(sK5)) = sK3 | sK2(sK3) = sK3, inference(superposition, [status(thm)], [d44,d39])). % 12.85/2.03 cnf(d46, plain, g(sK8(sK5)) = sK3 | sK2(sK3) = sK3 | sK2(sK3) = sK3, inference(demodulation, [status(thm)], [d45,d28])). % 12.85/2.03 cnf(d47, plain, sK8(sK5) = f(sK3) | sK2(sK3) = g(f(sK2(sK3))) | sK2(sK3) = sK3 | sK2(sK3) = sK3, inference(superposition, [status(thm)], [d46,d33])). % 12.85/2.03 cnf(d48, plain, sK2(sK3) = sK3 | sK2(sK3) = g(f(sK2(sK3))) | sK8(sK5) = sK5, inference(demodulation, [status(thm)], [d47,d22])). % 12.85/2.03 cnf(d49, plain, sK2(sK3) != sK2(sK3) | sK2(sK3) = sK3 | 'Ts0' | sK2(sK3) = sK3 | sK8(sK5) = sK5, inference(superposition, [status(thm)], [d48,c2])). % 12.85/2.03 cnf(d50, plain, sK2(sK3) = sK3 | sK8(sK5) = sK5 | 'Ts0', inference(equality_resolution, [status(thm)], [d49])). % 12.85/2.03 cnf(d51, plain, f(sK2(sK3)) != f(sK2(sK3)) | f(sK2(sK3)) = sK5 | ~'Ts0' | sK2(sK3) = sK3 | sK8(sK5) = sK5, inference(superposition, [status(thm)], [d48,c10])). % 12.85/2.03 cnf(d52, plain, f(sK2(sK3)) = sK5 | sK2(sK3) = sK3 | sK8(sK5) = sK5 | ~'Ts0', inference(equality_resolution, [status(thm)], [d51])). % 12.85/2.03 cnf(d53, plain, f(sK2(sK3)) = sK5 | sK2(sK3) = sK3 | sK8(sK5) = sK5 | sK2(sK3) = sK3 | sK8(sK5) = sK5, inference(resolution, [status(thm)], [d52,d50])). % 12.85/2.03 cnf(d54, plain, sK2(sK3) = g(sK5) | sK2(sK3) = sK3 | sK8(sK5) = sK5 | sK2(sK3) = sK3 | sK8(sK5) = sK5, inference(superposition, [status(thm)], [d53,d48])). % 12.85/2.03 cnf(d55, plain, sK2(sK3) = sK3 | sK2(sK3) = sK3 | sK8(sK5) = sK5, inference(demodulation, [status(thm)], [d54,d28])). % 12.85/2.03 cnf(d56, plain, sK5 != sK5 | sK5 != sK5 | 'Ts0' | sK2(sK3) = sK3 | sK2(sK3) = sK3, inference(superposition, [status(thm)], [d55,d26])). % 12.85/2.03 cnf(d57, plain, sK2(sK3) = sK3 | 'Ts0', inference(equality_resolution, [status(thm)], [d56])). % 12.85/2.03 cnf(d58, plain, sK2(sK3) = sK3 | sK2(sK3) = g(f(sK2(sK3))), inference(resolution, [status(thm)], [d57,d30])). % 12.85/2.03 cnf(d59, plain, f(sK2(sK3)) != f(sK2(sK3)) | f(sK2(sK3)) = sK5 | ~'Ts0' | sK2(sK3) = sK3, inference(superposition, [status(thm)], [d58,c10])). % 12.85/2.03 cnf(d60, plain, f(sK2(sK3)) = sK5 | sK2(sK3) = sK3 | ~'Ts0', inference(equality_resolution, [status(thm)], [d59])). % 12.85/2.03 cnf(d61, plain, f(sK2(sK3)) = sK5 | sK2(sK3) = sK3 | sK2(sK3) = sK3, inference(resolution, [status(thm)], [d60,d57])). % 12.85/2.03 cnf(d62, plain, sK2(sK3) = g(sK5) | sK2(sK3) = sK3 | sK2(sK3) = sK3, inference(superposition, [status(thm)], [d61,d58])). % 12.85/2.03 cnf(d63, plain, sK2(sK3) = sK3 | sK2(sK3) = sK3, inference(demodulation, [status(thm)], [d62,d28])). % 12.85/2.03 cnf(d64, plain, sK3 != sK3 | sK2(sK3) = sK3, inference(equality_factoring, [status(thm)], [d63])). % 12.85/2.03 cnf(d65, plain, sK2(sK3) = sK3, inference(equality_resolution, [status(thm)], [d64])). % 12.85/2.03 cnf(d66, plain, sK3 != sK3 | ~'Ts0', inference(resolution, [status(thm)], [d65,d27])). % 12.85/2.03 cnf(d67, plain, ~'Ts0', inference(equality_resolution, [status(thm)], [d66])). % 12.85/2.03 cnf(d68, plain, sK5 != sK5 | sK8(sK5) != sK5, inference(resolution, [status(thm)], [d67,d26])). % 12.85/2.03 cnf(d69, plain, X0 = sK3 | X0 != g(f(X0)), inference(resolution, [status(thm)], [d67,c2])). % 12.85/2.03 cnf(d70, plain, sK8(sK5) = f(g(sK8(f(sK3)))) | 'Ts0', inference(demodulation, [status(thm)], [d14,d22])). % 12.85/2.03 cnf(d71, plain, sK8(sK5) = f(g(sK8(sK5))) | 'Ts0', inference(demodulation, [status(thm)], [d70,d22])). % 12.85/2.03 cnf(d72, plain, sK8(sK5) = f(g(sK8(sK5))), inference(resolution, [status(thm)], [d67,d71])). % 12.85/2.03 cnf(d73, plain, g(sK8(sK5)) != g(sK8(sK5)) | g(sK8(sK5)) = sK3, inference(superposition, [status(thm)], [d72,d69])). % 12.85/2.03 cnf(d74, plain, g(sK8(sK5)) = sK3, inference(equality_resolution, [status(thm)], [d73])). % 12.85/2.03 cnf(d75, plain, sK8(sK5) = f(sK3), inference(demodulation, [status(thm)], [d72,d74])). % 12.85/2.03 cnf(d76, plain, sK8(sK5) = sK5, inference(demodulation, [status(thm)], [d75,d22])). % 12.85/2.03 cnf(d77, plain, sK5 != sK5, inference(resolution, [status(thm)], [d76,d68])). % 12.85/2.03 cnf(d78, plain, $false, inference(equality_resolution, [status(thm)], [d77])). % 12.85/2.03 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------