%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : KLE017+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n016.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:43:25 AM UTC 2026 % Result : Theorem 94.54s 28.69s % Output : CNFRefutation 94.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : KLE017+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/5.59 % Computer : n016.cluster.edu % 0.13/5.59 % Model : x86_64 x86_64 % 0.13/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/5.59 % Memory : 8046.5625MB % 0.13/5.59 % OS : Linux 6.8.0-71-generic % 0.13/5.59 % CPULimit : 300 % 0.13/5.59 % WCLimit : 300 % 0.13/5.59 % DateTime : Fri Sep 25 19:18:50 UTC 2026 % 0.13/5.59 % CPUTime : % 0.13/5.59 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 94.54/28.69 % SZS status Theorem for theBenchmark.p % 94.54/28.69 % SZS output start CNFRefutation for theBenchmark.p % 94.54/28.69 fof(additive_commutativity, axiom, ! [X0] : ! [X1] : addition(X0,X1) = addition(X1,X0)). % 94.54/28.69 fof(additive_associativity, axiom, ! [X0] : ! [X1] : ! [X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0)). % 94.54/28.69 fof(additive_identity, axiom, ! [X0] : addition(X0,zero) = X0). % 94.54/28.69 fof(additive_idempotence, axiom, ! [X0] : addition(X0,X0) = X0). % 94.54/28.69 fof(multiplicative_associativity, axiom, ! [X0] : ! [X1] : ! [X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2)). % 94.54/28.69 fof(multiplicative_right_identity, axiom, ! [X0] : multiplication(X0,one) = X0). % 94.54/28.69 fof(multiplicative_left_identity, axiom, ! [X0] : multiplication(one,X0) = X0). % 94.54/28.69 fof(right_distributivity, axiom, ! [X0] : ! [X1] : ! [X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))). % 94.54/28.69 fof(left_distributivity, axiom, ! [X0] : ! [X1] : ! [X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))). % 94.54/28.69 fof(order, axiom, ! [X0] : ! [X1] : ((leq(X0,X1) <=> addition(X0,X1) = X1))). % 94.54/28.69 fof(test_1, axiom, ! [X0] : ((test(X0) <=> ? [X1] : complement(X1,X0)))). % 94.54/28.69 fof(test_2, axiom, ! [X0] : ! [X1] : ((complement(X1,X0) <=> (multiplication(X0,X1) = zero & (multiplication(X1,X0) = zero & addition(X0,X1) = one))))). % 94.54/28.69 fof(goals, conjecture, ! [X0] : ! [X1] : ! [X2] : (((test(X0) & (test(X1) & test(X2))) => (leq(X2,multiplication(X0,X1)) <=> (leq(X2,X0) & leq(X2,X1)))))). % 94.54/28.69 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : (((test(X0) & (test(X1) & test(X2))) => (leq(X2,multiplication(X0,X1)) <=> (leq(X2,X0) & leq(X2,X1))))), inference(negate_conjecture, [status(cth)], [goals])). % 94.54/28.69 cnf(c0, plain, addition(X0,X1) = addition(X1,X0), inference(clausification, [status(esa)], [additive_commutativity])). % 94.54/28.69 cnf(c1, plain, addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)), inference(clausification, [status(esa)], [additive_associativity])). % 94.54/28.69 cnf(c2, plain, addition(X0,zero) = X0, inference(clausification, [status(esa)], [additive_identity])). % 94.54/28.69 cnf(c3, plain, addition(X0,X0) = X0, inference(clausification, [status(esa)], [additive_idempotence])). % 94.54/28.69 cnf(c4, plain, multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)), inference(clausification, [status(esa)], [multiplicative_associativity])). % 94.54/28.69 cnf(c5, plain, multiplication(X0,one) = X0, inference(clausification, [status(esa)], [multiplicative_right_identity])). % 94.54/28.69 cnf(c6, plain, multiplication(one,X0) = X0, inference(clausification, [status(esa)], [multiplicative_left_identity])). % 94.54/28.69 cnf(c7, plain, addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)), inference(clausification, [status(esa)], [right_distributivity])). % 94.54/28.69 cnf(c8, plain, addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1), inference(clausification, [status(esa)], [left_distributivity])). % 94.54/28.69 cnf(c11, plain, ~leq(X0,X1) | addition(X0,X1) = X1, inference(clausification, [status(esa)], [order])). % 94.54/28.69 cnf(c12, plain, leq(X0,X1) | addition(X0,X1) != X1, inference(clausification, [status(esa)], [order])). % 94.54/28.69 cnf(c13, plain, ~test(X0) | complement(sK23(X0),X0), inference(clausification, [status(esa)], [test_1])). % 94.54/28.69 cnf(c15, plain, ~complement(X0,X1) | multiplication(X1,X0) = zero, inference(clausification, [status(esa)], [test_2])). % 94.54/28.69 cnf(c16, plain, ~complement(X0,X1) | addition(X1,X0) = one, inference(clausification, [status(esa)], [test_2])). % 94.54/28.69 cnf(c22, plain, test(sK32), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c23, plain, test(sK33), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c24, plain, test(sK31), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c25, plain, leq(sK33,multiplication(sK31,sK32)) | X0(sK31,sK32,sK33), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c26, plain, ~leq(sK33,sK31) | ~leq(sK33,sK32) | X0(sK31,sK32,sK33), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c27, plain, ~X0(X1,X2,X3) | ~leq(X3,multiplication(X1,X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c28, plain, ~X0(X1,X2,X3) | leq(X3,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(c29, plain, ~X0(X1,X2,X3) | leq(X3,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 94.54/28.69 cnf(d0, plain, multiplication(addition(X0,X2),X1) != multiplication(X2,X1) | leq(multiplication(X0,X1),multiplication(X2,X1)), inference(superposition, [status(thm)], [c8,c12])). % 94.54/28.69 cnf(d1, plain, addition(X0,X1) = addition(X0,addition(X0,X1)), inference(superposition, [status(thm)], [c3,c1])). % 94.54/28.69 cnf(d2, plain, multiplication(addition(X0,X1),X2) != multiplication(addition(X0,X1),X2) | leq(multiplication(X0,X2),multiplication(addition(X0,X1),X2)), inference(superposition, [status(thm)], [d1,d0])). % 94.54/28.69 cnf(d3, plain, multiplication(X0,multiplication(X1,one)) = multiplication(X0,X1), inference(superposition, [status(thm)], [c4,c5])). % 94.54/28.69 cnf(d4, plain, multiplication(X1,X0) = multiplication(X1,X0), inference(demodulation, [status(thm)], [d3,c5])). % 94.54/28.69 cnf(d5, plain, leq(multiplication(X0,X1),multiplication(addition(X0,X2),X1)), inference(resolution, [status(thm)], [d4,d2])). % 94.54/28.69 cnf(d6, plain, addition(sK33,multiplication(sK31,sK32)) = multiplication(sK31,sK32) | 'Ts30'(sK31,sK32,sK33), inference(resolution, [status(thm)], [c11,c25])). % 94.54/28.69 cnf(d7, plain, addition(sK33,multiplication(sK31,sK32)) = multiplication(sK31,sK32) | leq(sK33,sK31), inference(resolution, [status(thm)], [d6,c29])). % 94.54/28.69 cnf(d8, plain, addition(sK33,multiplication(sK31,sK32)) = multiplication(sK31,sK32) | addition(sK33,sK31) = sK31, inference(resolution, [status(thm)], [d7,c11])). % 94.54/28.69 cnf(d9, plain, addition(multiplication(sK31,sK32),X0) = addition(sK33,addition(multiplication(sK31,sK32),X0)) | addition(sK33,sK31) = sK31, inference(superposition, [status(thm)], [d8,c1])). % 94.54/28.69 cnf(d10, plain, addition(multiplication(sK31,sK32),X0) = addition(sK33,addition(X0,multiplication(sK31,sK32))) | addition(sK33,sK31) = sK31, inference(superposition, [status(thm)], [c0,d9])). % 94.54/28.69 cnf(d11, plain, addition(multiplication(sK31,sK32),X0) != addition(X0,multiplication(sK31,sK32)) | leq(sK33,addition(X0,multiplication(sK31,sK32))) | addition(sK33,sK31) = sK31, inference(superposition, [status(thm)], [d10,c12])). % 94.54/28.69 cnf(d12, plain, addition(sK33,sK31) = sK31 | leq(sK33,addition(X0,multiplication(sK31,sK32))), inference(resolution, [status(thm)], [c0,d11])). % 94.54/28.69 cnf(d13, plain, addition(X0,multiplication(X0,X1)) = multiplication(X0,addition(one,X1)), inference(superposition, [status(thm)], [c5,c7])). % 94.54/28.69 cnf(d14, plain, addition(X0,sK23(X0)) = one | ~test(X0), inference(resolution, [status(thm)], [c16,c13])). % 94.54/28.69 cnf(d15, plain, addition(sK32,sK23(sK32)) = one, inference(resolution, [status(thm)], [d14,c22])). % 94.54/28.69 cnf(d16, plain, addition(sK32,sK23(sK32)) = addition(sK32,one), inference(superposition, [status(thm)], [d15,d1])). % 94.54/28.69 cnf(d17, plain, one = addition(sK32,one), inference(demodulation, [status(thm)], [d16,d15])). % 94.54/28.69 cnf(d18, plain, one = addition(one,sK32), inference(demodulation, [status(thm)], [d17,c0])). % 94.54/28.69 cnf(d19, plain, addition(X0,multiplication(X0,sK32)) = multiplication(X0,one), inference(superposition, [status(thm)], [d18,d13])). % 94.54/28.69 cnf(d20, plain, addition(X0,multiplication(X0,sK32)) = X0, inference(demodulation, [status(thm)], [d19,c5])). % 94.54/28.69 cnf(d21, plain, leq(sK33,sK31) | addition(sK33,sK31) = sK31, inference(superposition, [status(thm)], [d20,d12])). % 94.54/28.69 cnf(d22, plain, addition(sK33,sK31) = sK31 | addition(sK33,sK31) = sK31, inference(resolution, [status(thm)], [d21,c11])). % 94.54/28.69 cnf(d23, plain, leq(multiplication(sK33,X0),multiplication(sK31,X0)), inference(superposition, [status(thm)], [d22,d5])). % 94.54/28.69 cnf(d24, plain, ~'Ts30'(sK31,X0,multiplication(sK33,X0)), inference(resolution, [status(thm)], [d23,c27])). % 94.54/28.69 cnf(d25, plain, multiplication(X0,sK23(X0)) = zero | ~test(X0), inference(resolution, [status(thm)], [c15,c13])). % 94.54/28.69 cnf(d26, plain, multiplication(sK33,sK23(sK33)) = zero, inference(resolution, [status(thm)], [d25,c23])). % 94.54/28.69 cnf(d27, plain, addition(multiplication(sK33,X0),zero) = multiplication(sK33,addition(X0,sK23(sK33))), inference(superposition, [status(thm)], [d26,c7])). % 94.54/28.69 cnf(d28, plain, multiplication(sK33,X0) = multiplication(sK33,addition(X0,sK23(sK33))), inference(demodulation, [status(thm)], [d27,c2])). % 94.54/28.69 cnf(d29, plain, addition(X2,addition(X0,X1)) = addition(X0,addition(X1,X2)), inference(superposition, [status(thm)], [c1,c0])). % 94.54/28.69 cnf(d30, plain, addition(addition(X1,X2),X0) = addition(X2,addition(X0,X1)), inference(superposition, [status(thm)], [d29,c0])). % 94.54/28.69 cnf(d31, plain, addition(sK33,multiplication(sK31,sK32)) = multiplication(sK31,sK32) | leq(sK33,sK32), inference(resolution, [status(thm)], [d6,c28])). % 94.54/28.69 cnf(d32, plain, addition(sK33,multiplication(sK31,sK32)) = multiplication(sK31,sK32) | addition(sK33,sK32) = sK32, inference(resolution, [status(thm)], [d31,c11])). % 94.54/28.69 cnf(d33, plain, addition(sK33,multiplication(sK31,sK32)) = multiplication(sK31,sK32) | addition(sK32,sK33) = sK32, inference(demodulation, [status(thm)], [d32,c0])). % 94.54/28.69 cnf(d34, plain, addition(multiplication(sK31,sK32),X0) = addition(sK33,addition(multiplication(sK31,sK32),X0)) | addition(sK32,sK33) = sK32, inference(superposition, [status(thm)], [d33,c1])). % 94.54/28.69 cnf(d35, plain, addition(multiplication(sK31,sK32),X0) = addition(sK33,addition(X0,multiplication(sK31,sK32))) | addition(sK32,sK33) = sK32, inference(superposition, [status(thm)], [c0,d34])). % 94.54/28.69 cnf(d36, plain, addition(multiplication(sK31,sK32),X0) != addition(X0,multiplication(sK31,sK32)) | leq(sK33,addition(X0,multiplication(sK31,sK32))) | addition(sK32,sK33) = sK32, inference(superposition, [status(thm)], [d35,c12])). % 94.54/28.69 cnf(d37, plain, addition(sK32,sK33) = sK32 | leq(sK33,addition(X0,multiplication(sK31,sK32))), inference(resolution, [status(thm)], [c0,d36])). % 94.54/28.69 cnf(d38, plain, addition(X0,multiplication(X1,X0)) = multiplication(addition(one,X1),X0), inference(superposition, [status(thm)], [c6,c8])). % 94.54/28.69 cnf(d39, plain, addition(sK31,sK23(sK31)) = one, inference(resolution, [status(thm)], [d14,c24])). % 94.54/28.69 cnf(d40, plain, addition(sK31,sK23(sK31)) = addition(sK31,one), inference(superposition, [status(thm)], [d39,d1])). % 94.54/28.69 cnf(d41, plain, one = addition(sK31,one), inference(demodulation, [status(thm)], [d40,d39])). % 94.54/28.69 cnf(d42, plain, one = addition(one,sK31), inference(demodulation, [status(thm)], [d41,c0])). % 94.54/28.69 cnf(d43, plain, addition(X0,multiplication(sK31,X0)) = multiplication(one,X0), inference(superposition, [status(thm)], [d42,d38])). % 94.54/28.69 cnf(d44, plain, addition(X0,multiplication(sK31,X0)) = X0, inference(demodulation, [status(thm)], [d43,c6])). % 94.54/28.69 cnf(d45, plain, leq(sK33,sK32) | addition(sK32,sK33) = sK32, inference(superposition, [status(thm)], [d44,d37])). % 94.54/28.69 cnf(d46, plain, multiplication(sK31,sK32) != multiplication(sK31,sK32) | leq(sK33,multiplication(sK31,sK32)) | addition(sK32,sK33) = sK32, inference(superposition, [status(thm)], [d33,c12])). % 94.54/28.69 cnf(d47, plain, addition(sK32,sK33) = sK32 | leq(sK33,multiplication(sK31,sK32)), inference(equality_resolution, [status(thm)], [d46])). % 94.54/28.69 cnf(d48, plain, addition(sK32,sK33) = sK32 | ~'Ts30'(sK31,sK32,sK33), inference(resolution, [status(thm)], [d47,c27])). % 94.54/28.69 cnf(d49, plain, addition(sK32,sK33) = sK32 | ~leq(sK33,sK32) | ~leq(sK33,sK31), inference(resolution, [status(thm)], [d48,c26])). % 94.54/28.69 cnf(d50, plain, sK31 != sK31 | leq(sK33,sK31), inference(superposition, [status(thm)], [d22,c12])). % 94.54/28.69 cnf(d51, plain, leq(sK33,sK31), inference(equality_resolution, [status(thm)], [d50])). % 94.54/28.69 cnf(d52, plain, addition(sK32,sK33) = sK32 | ~leq(sK33,sK32), inference(resolution, [status(thm)], [d51,d49])). % 94.54/28.69 cnf(d53, plain, addition(sK32,sK33) = sK32 | addition(sK32,sK33) = sK32, inference(resolution, [status(thm)], [d52,d45])). % 94.54/28.69 cnf(d54, plain, addition(sK32,X0) = addition(sK33,addition(X0,sK32)), inference(superposition, [status(thm)], [d53,d30])). % 94.54/28.69 cnf(d55, plain, addition(sK32,X0) = addition(sK32,addition(sK33,X0)), inference(demodulation, [status(thm)], [d54,d29])). % 94.54/28.69 cnf(d56, plain, addition(sK33,sK23(sK33)) = one, inference(resolution, [status(thm)], [d14,c23])). % 94.54/28.69 cnf(d57, plain, addition(sK32,sK23(sK33)) = addition(sK32,one), inference(superposition, [status(thm)], [d56,d55])). % 94.54/28.69 cnf(d58, plain, addition(sK32,sK23(sK33)) = addition(one,sK32), inference(demodulation, [status(thm)], [d57,c0])). % 94.54/28.69 cnf(d59, plain, addition(sK32,sK23(sK33)) = one, inference(demodulation, [status(thm)], [d58,d18])). % 94.54/28.69 cnf(d60, plain, multiplication(sK33,sK32) = multiplication(sK33,one), inference(superposition, [status(thm)], [d59,d28])). % 94.54/28.69 cnf(d61, plain, multiplication(sK33,sK32) = sK33, inference(demodulation, [status(thm)], [d60,c5])). % 94.54/28.69 cnf(d62, plain, ~'Ts30'(sK31,sK32,sK33), inference(superposition, [status(thm)], [d61,d24])). % 94.54/28.69 cnf(d63, plain, ~leq(sK33,sK32) | 'Ts30'(sK31,sK32,sK33), inference(resolution, [status(thm)], [d51,c26])). % 94.54/28.69 cnf(d64, plain, addition(X1,X0) != X1 | leq(X0,X1), inference(superposition, [status(thm)], [c0,c12])). % 94.54/28.69 cnf(d65, plain, sK32 != sK32 | leq(sK33,sK32), inference(superposition, [status(thm)], [d53,d64])). % 94.54/28.69 cnf(d66, plain, leq(sK33,sK32), inference(equality_resolution, [status(thm)], [d65])). % 94.54/28.69 cnf(d67, plain, 'Ts30'(sK31,sK32,sK33), inference(resolution, [status(thm)], [d66,d63])). % 94.54/28.69 cnf(d68, plain, $false, inference(resolution, [status(thm)], [d67,d62])). % 94.54/28.69 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------