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