%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG194+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n002.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:48:03 AM UTC 2026 % Result : Theorem 21.62s 3.31s % Output : CNFRefutation 21.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG194+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.36 % Computer : n002.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/0.36 % OS : Linux 6.8.0-71-generic % 0.08/0.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sat Sep 26 21:27:21 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 21.62/3.31 % SZS status Theorem for theBenchmark.p % 21.62/3.31 % SZS output start CNFRefutation for theBenchmark.p % 21.62/3.31 fof(co1, conjecture, ((op(e0,e0) != e0 & (op(e1,e1) != e1 & (op(e2,e2) != e2 & (op(e3,e3) != e3 & (op(e4,e4) != e4 & (op(e5,e5) != e5 & op(e6,e6) != e6)))))) | ((op(e0,e0) = e0 & (op(e1,e1) = e1 & (op(e2,e2) = e2 & (op(e3,e3) = e3 & (op(e4,e4) = e4 & (op(e5,e5) = e5 & op(e6,e6) = e6)))))) | ((op(e0,e0) = e0 | (op(e1,e1) = e1 | (op(e2,e2) = e2 | (op(e3,e3) = e3 | (op(e4,e4) = e4 | (op(e5,e5) = e5 | op(e6,e6) = e6)))))) & (op(e0,e0) != e0 | (op(e1,e1) != e1 | (op(e2,e2) != e2 | (op(e3,e3) != e3 | (op(e4,e4) != e4 | (op(e5,e5) != e5 | op(e6,e6) != e6)))))))))). % 21.62/3.31 fof(negated_conjecture, negated_conjecture, ~(((op(e0,e0) != e0 & (op(e1,e1) != e1 & (op(e2,e2) != e2 & (op(e3,e3) != e3 & (op(e4,e4) != e4 & (op(e5,e5) != e5 & op(e6,e6) != e6)))))) | ((op(e0,e0) = e0 & (op(e1,e1) = e1 & (op(e2,e2) = e2 & (op(e3,e3) = e3 & (op(e4,e4) = e4 & (op(e5,e5) = e5 & op(e6,e6) = e6)))))) | ((op(e0,e0) = e0 | (op(e1,e1) = e1 | (op(e2,e2) = e2 | (op(e3,e3) = e3 | (op(e4,e4) = e4 | (op(e5,e5) = e5 | op(e6,e6) = e6)))))) & (op(e0,e0) != e0 | (op(e1,e1) != e1 | (op(e2,e2) != e2 | (op(e3,e3) != e3 | (op(e4,e4) != e4 | (op(e5,e5) != e5 | op(e6,e6) != e6)))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 21.62/3.31 cnf(c511, plain, op(e4,e4) = e4 | op(e6,e6) = e6 | op(e1,e1) = e1 | op(e5,e5) = e5 | op(e2,e2) = e2 | op(e0,e0) = e0 | op(e3,e3) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c512, plain, op(e1,e1) != e1 | op(e6,e6) != e6 | op(e5,e5) != e5 | op(e3,e3) != e3 | op(e4,e4) != e4 | op(e0,e0) != e0 | op(e2,e2) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c513, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c514, plain, X0 | op(e0,e0) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c515, plain, X0 | op(e1,e1) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c516, plain, X0 | op(e2,e2) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c517, plain, X0 | op(e3,e3) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c518, plain, X0 | op(e4,e4) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c519, plain, X0 | op(e5,e5) != e5, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c520, plain, X0 | op(e6,e6) != e6, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c521, plain, X0 | op(e0,e0) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c522, plain, X0 | op(e1,e1) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c523, plain, X0 | op(e2,e2) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c524, plain, X0 | op(e3,e3) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c525, plain, X0 | op(e4,e4) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c526, plain, X0 | op(e5,e5) = e5, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(c527, plain, X0 | op(e6,e6) = e6, inference(clausification, [status(esa)], [negated_conjecture])). % 21.62/3.31 cnf(d0, plain, op(e1,e1) = e1 | ~'Ts0', inference(resolution, [status(thm)], [c522,c513])). % 21.62/3.31 cnf(d1, plain, op(e0,e0) = e0 | ~'Ts0', inference(resolution, [status(thm)], [c521,c513])). % 21.62/3.31 cnf(d2, plain, op(e5,e5) = e5 | ~'Ts0', inference(resolution, [status(thm)], [c526,c513])). % 21.62/3.31 cnf(d3, plain, op(e6,e6) = e6 | ~'Ts0', inference(resolution, [status(thm)], [c527,c513])). % 21.62/3.31 cnf(d4, plain, e1 != e1 | 'Ts0' | op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e2,e2) = e2 | op(e4,e4) = e4, inference(superposition, [status(thm)], [c511,c515])). % 21.62/3.31 cnf(d5, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e2,e2) = e2 | op(e4,e4) = e4 | 'Ts0', inference(equality_resolution, [status(thm)], [d4])). % 21.62/3.31 cnf(d6, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e2,e2) = e2 | op(e4,e4) = e4 | op(e6,e6) = e6, inference(resolution, [status(thm)], [d5,d3])). % 21.62/3.31 cnf(d7, plain, e4 != e4 | 'Ts0' | op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e2,e2) = e2, inference(superposition, [status(thm)], [d6,c518])). % 21.62/3.31 cnf(d8, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e2,e2) = e2 | 'Ts0', inference(equality_resolution, [status(thm)], [d7])). % 21.62/3.31 cnf(d9, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e2,e2) = e2 | op(e6,e6) = e6, inference(resolution, [status(thm)], [d8,d3])). % 21.62/3.31 cnf(d10, plain, e2 != e2 | 'Ts0' | op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3, inference(superposition, [status(thm)], [d9,c516])). % 21.62/3.31 cnf(d11, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | 'Ts0', inference(equality_resolution, [status(thm)], [d10])). % 21.62/3.31 cnf(d12, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e3,e3) = e3 | op(e6,e6) = e6, inference(resolution, [status(thm)], [d11,d3])). % 21.62/3.31 cnf(d13, plain, e3 != e3 | 'Ts0' | op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6, inference(superposition, [status(thm)], [d12,c517])). % 21.62/3.31 cnf(d14, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | 'Ts0', inference(equality_resolution, [status(thm)], [d13])). % 21.62/3.31 cnf(d15, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e6,e6) = e6 | op(e6,e6) = e6, inference(resolution, [status(thm)], [d14,d3])). % 21.62/3.31 cnf(d16, plain, e6 != e6 | 'Ts0' | op(e0,e0) = e0 | op(e5,e5) = e5, inference(superposition, [status(thm)], [d15,c520])). % 21.62/3.31 cnf(d17, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | 'Ts0', inference(equality_resolution, [status(thm)], [d16])). % 21.62/3.31 cnf(d18, plain, op(e0,e0) = e0 | op(e5,e5) = e5 | op(e5,e5) = e5, inference(resolution, [status(thm)], [d17,d2])). % 21.62/3.31 cnf(d19, plain, e5 != e5 | 'Ts0' | op(e0,e0) = e0, inference(superposition, [status(thm)], [d18,c519])). % 21.62/3.31 cnf(d20, plain, op(e0,e0) = e0 | 'Ts0', inference(equality_resolution, [status(thm)], [d19])). % 21.62/3.31 cnf(d21, plain, op(e0,e0) = e0 | op(e0,e0) = e0, inference(resolution, [status(thm)], [d20,d1])). % 21.62/3.31 cnf(d22, plain, 'Ts0', inference(resolution, [status(thm)], [d21,c514])). % 21.62/3.31 cnf(d23, plain, op(e1,e1) = e1, inference(resolution, [status(thm)], [d22,d0])). % 21.62/3.31 cnf(d24, plain, op(e4,e4) = e4 | ~'Ts0', inference(resolution, [status(thm)], [c525,c513])). % 21.62/3.31 cnf(d25, plain, op(e4,e4) = e4, inference(resolution, [status(thm)], [d22,d24])). % 21.62/3.31 cnf(d26, plain, op(e2,e2) = e2 | ~'Ts0', inference(resolution, [status(thm)], [c523,c513])). % 21.62/3.31 cnf(d27, plain, op(e2,e2) = e2, inference(resolution, [status(thm)], [d22,d26])). % 21.62/3.31 cnf(d28, plain, op(e3,e3) = e3 | ~'Ts0', inference(resolution, [status(thm)], [c524,c513])). % 21.62/3.31 cnf(d29, plain, op(e3,e3) = e3, inference(resolution, [status(thm)], [d22,d28])). % 21.62/3.31 cnf(d30, plain, op(e6,e6) = e6, inference(resolution, [status(thm)], [d22,d3])). % 21.62/3.31 cnf(d31, plain, op(e5,e5) = e5, inference(resolution, [status(thm)], [d22,d2])). % 21.62/3.31 cnf(d32, plain, e0 != e0 | op(e5,e5) != e5 | op(e6,e6) != e6 | op(e3,e3) != e3 | op(e2,e2) != e2 | op(e4,e4) != e4 | op(e1,e1) != e1, inference(demodulation, [status(thm)], [c512,d21])). % 21.62/3.31 cnf(d33, plain, e0 != e0 | e5 != e5 | op(e6,e6) != e6 | op(e3,e3) != e3 | op(e2,e2) != e2 | op(e4,e4) != e4 | op(e1,e1) != e1, inference(demodulation, [status(thm)], [d32,d31])). % 21.62/3.31 cnf(d34, plain, e0 != e0 | e5 != e5 | e6 != e6 | op(e3,e3) != e3 | op(e2,e2) != e2 | op(e4,e4) != e4 | op(e1,e1) != e1, inference(demodulation, [status(thm)], [d33,d30])). % 21.62/3.31 cnf(d35, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3 | op(e2,e2) != e2 | op(e4,e4) != e4 | op(e1,e1) != e1, inference(demodulation, [status(thm)], [d34,d29])). % 21.62/3.31 cnf(d36, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3 | e2 != e2 | op(e4,e4) != e4 | op(e1,e1) != e1, inference(demodulation, [status(thm)], [d35,d27])). % 21.62/3.31 cnf(d37, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3 | e2 != e2 | e4 != e4 | op(e1,e1) != e1, inference(demodulation, [status(thm)], [d36,d25])). % 21.62/3.31 cnf(d38, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3 | e2 != e2 | e4 != e4 | e1 != e1, inference(demodulation, [status(thm)], [d37,d23])). % 21.62/3.31 cnf(d39, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3 | e2 != e2 | e4 != e4, inference(equality_resolution, [status(thm)], [d38])). % 21.62/3.31 cnf(d40, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3 | e2 != e2, inference(equality_resolution, [status(thm)], [d39])). % 21.62/3.31 cnf(d41, plain, e0 != e0 | e5 != e5 | e6 != e6 | e3 != e3, inference(equality_resolution, [status(thm)], [d40])). % 21.62/3.31 cnf(d42, plain, e0 != e0 | e5 != e5 | e6 != e6, inference(equality_resolution, [status(thm)], [d41])). % 21.62/3.31 cnf(d43, plain, e0 != e0 | e5 != e5, inference(equality_resolution, [status(thm)], [d42])). % 21.62/3.31 cnf(d44, plain, e0 != e0, inference(equality_resolution, [status(thm)], [d43])). % 21.62/3.31 cnf(d45, plain, $false, inference(equality_resolution, [status(thm)], [d44])). % 21.62/3.31 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------