%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM845+2 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n011.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 08:13:57 AM UTC 2026 % Result : Theorem 9.17s 2.44s % Output : CNFRefutation 9.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM845+2 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/0.36 % Computer : n011.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 04:12:44 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.17/2.44 % SZS status Theorem for theBenchmark.p % 9.17/2.44 % SZS output start CNFRefutation for theBenchmark.p % 9.17/2.44 fof(ass(cond(conseq(263), 1), 1), axiom, ! [X0] : ((vmul(vsucc(vd411),X0) = vplus(vmul(vd411,X0),X0) => vplus(vmul(vd411,X0),vplus(vd411,vsucc(X0))) = vplus(vplus(vmul(vd411,X0),vd411),vsucc(X0))))). % 9.17/2.44 fof(qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0))), axiom, ! [X0] : ! [X1] : ((vmul(X0,vsucc(X1)) = vplus(vmul(X0,X1),X0) & vmul(X0,v1) = X0))). % 9.17/2.44 fof(ass(cond(61, 0), 0), axiom, ! [X0] : ! [X1] : vplus(X1,X0) = vplus(X0,X1)). % 9.17/2.44 fof(ass(cond(43, 0), 0), axiom, ! [X0] : vplus(v1,X0) = vsucc(X0)). % 9.17/2.44 fof(ass(cond(33, 0), 0), axiom, ! [X0] : ! [X1] : ! [X2] : vplus(vplus(X0,X1),X2) = vplus(X0,vplus(X1,X2))). % 9.17/2.44 fof(qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0))), axiom, ! [X0] : ! [X1] : ((vplus(X0,vsucc(X1)) = vsucc(vplus(X0,X1)) & vplus(X0,v1) = vsucc(X0)))). % 9.17/2.44 fof(qu(ind(267), imp(267)), conjecture, ! [X0] : ((vmul(vsucc(vd411),X0) = vplus(vmul(vd411,X0),X0) => vmul(vsucc(vd411),vsucc(X0)) = vplus(vmul(vd411,vsucc(X0)),vsucc(X0))))). % 9.17/2.44 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((vmul(vsucc(vd411),X0) = vplus(vmul(vd411,X0),X0) => vmul(vsucc(vd411),vsucc(X0)) = vplus(vmul(vd411,vsucc(X0)),vsucc(X0)))), inference(negate_conjecture, [status(cth)], [qu(ind(267), imp(267))])). % 9.17/2.44 cnf(c1, plain, vmul(vsucc(vd411),X0) != vplus(vmul(vd411,X0),X0) | vplus(vmul(vd411,X0),vplus(vd411,vsucc(X0))) = vplus(vplus(vmul(vd411,X0),vd411),vsucc(X0)), inference(clausification, [status(esa)], [ass(cond(conseq(263), 1), 1)])). % 9.17/2.44 cnf(c9, plain, vmul(X0,vsucc(X1)) = vplus(vmul(X0,X1),X0), inference(clausification, [status(esa)], [qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))])). % 9.17/2.44 cnf(c11, plain, vplus(X0,X1) = vplus(X1,X0), inference(clausification, [status(esa)], [ass(cond(61, 0), 0)])). % 9.17/2.44 cnf(c12, plain, vplus(v1,X0) = vsucc(X0), inference(clausification, [status(esa)], [ass(cond(43, 0), 0)])). % 9.17/2.44 cnf(c13, plain, vplus(vplus(X0,X1),X2) = vplus(X0,vplus(X1,X2)), inference(clausification, [status(esa)], [ass(cond(33, 0), 0)])). % 9.17/2.44 cnf(c14, plain, vplus(X0,vsucc(X1)) = vsucc(vplus(X0,X1)), inference(clausification, [status(esa)], [qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))])). % 9.17/2.44 cnf(c16, plain, vmul(vsucc(vd411),sK18) = vplus(vmul(vd411,sK18),sK18), inference(clausification, [status(esa)], [negated_conjecture])). % 9.17/2.44 cnf(c17, plain, vmul(vsucc(vd411),vsucc(sK18)) != vplus(vmul(vd411,vsucc(sK18)),vsucc(sK18)), inference(clausification, [status(esa)], [negated_conjecture])). % 9.17/2.44 cnf(d0, plain, vplus(vsucc(X0),X1) = vplus(v1,vplus(X0,X1)), inference(superposition, [status(thm)], [c12,c13])). % 9.17/2.44 cnf(d1, plain, vplus(vsucc(X0),X1) = vsucc(vplus(X0,X1)), inference(demodulation, [status(thm)], [d0,c12])). % 9.17/2.44 cnf(d2, plain, vplus(vsucc(X0),X1) = vplus(X0,vsucc(X1)), inference(demodulation, [status(thm)], [d1,c14])). % 9.17/2.44 cnf(d3, plain, vmul(vsucc(vd411),sK18) = vplus(sK18,vmul(vd411,sK18)), inference(demodulation, [status(thm)], [c16,c11])). % 9.17/2.44 cnf(d4, plain, vplus(X0,vplus(X1,X2)) = vplus(X2,vplus(X0,X1)), inference(superposition, [status(thm)], [c13,c11])). % 9.17/2.44 cnf(d5, plain, vplus(X0,vmul(vsucc(vd411),sK18)) = vplus(vmul(vd411,sK18),vplus(X0,sK18)), inference(superposition, [status(thm)], [d3,d4])). % 9.17/2.44 cnf(d6, plain, vplus(X0,vmul(vsucc(vd411),sK18)) = vplus(sK18,vplus(vmul(vd411,sK18),X0)), inference(demodulation, [status(thm)], [d5,d4])). % 9.17/2.44 cnf(d7, plain, vplus(X0,vmul(vsucc(vd411),sK18)) = vplus(X0,vplus(sK18,vmul(vd411,sK18))), inference(superposition, [status(thm)], [d6,d4])). % 9.17/2.44 cnf(d8, plain, vplus(X0,vmul(vsucc(vd411),sK18)) = vplus(X0,vmul(vsucc(vd411),sK18)), inference(demodulation, [status(thm)], [d7,d3])). % 9.17/2.44 cnf(d9, plain, vmul(X0,vsucc(X1)) = vplus(X0,vmul(X0,X1)), inference(demodulation, [status(thm)], [c9,c11])). % 9.17/2.44 cnf(d10, plain, vmul(vsucc(vd411),vsucc(sK18)) = vplus(vsucc(vd411),vmul(vsucc(vd411),sK18)), inference(superposition, [status(thm)], [d9,d8])). % 9.17/2.44 cnf(d11, plain, vmul(vsucc(vd411),vsucc(sK18)) = vplus(vd411,vsucc(vmul(vsucc(vd411),sK18))), inference(demodulation, [status(thm)], [d10,d2])). % 9.17/2.44 cnf(d12, plain, vplus(vmul(vsucc(vd411),sK18),X0) = vplus(sK18,vplus(vmul(vd411,sK18),X0)), inference(superposition, [status(thm)], [d3,c13])). % 9.17/2.44 cnf(d13, plain, vplus(vmul(vsucc(vd411),sK18),X0) = vplus(sK18,vplus(X0,vmul(vd411,sK18))), inference(superposition, [status(thm)], [c11,d12])). % 9.17/2.44 cnf(d14, plain, vplus(sK18,vsucc(vplus(X0,vmul(vd411,sK18)))) = vsucc(vplus(vmul(vsucc(vd411),sK18),X0)), inference(superposition, [status(thm)], [d13,c14])). % 9.17/2.44 cnf(d15, plain, vplus(sK18,vplus(X0,vsucc(vmul(vd411,sK18)))) = vsucc(vplus(vmul(vsucc(vd411),sK18),X0)), inference(demodulation, [status(thm)], [d14,c14])). % 9.17/2.44 cnf(d16, plain, vplus(sK18,vplus(X0,vsucc(vmul(vd411,sK18)))) = vplus(vmul(vsucc(vd411),sK18),vsucc(X0)), inference(demodulation, [status(thm)], [d15,c14])). % 9.17/2.44 cnf(d17, plain, vplus(sK18,vsucc(vmul(vd411,sK18))) = vsucc(vmul(vsucc(vd411),sK18)), inference(superposition, [status(thm)], [d3,c14])). % 9.17/2.44 cnf(d18, plain, vplus(vsucc(vmul(vsucc(vd411),sK18)),X0) = vplus(sK18,vplus(vsucc(vmul(vd411,sK18)),X0)), inference(superposition, [status(thm)], [d17,c13])). % 9.17/2.44 cnf(d19, plain, vplus(vsucc(vmul(vsucc(vd411),sK18)),X0) = vplus(sK18,vplus(X0,vsucc(vmul(vd411,sK18)))), inference(superposition, [status(thm)], [c11,d18])). % 9.17/2.44 cnf(d20, plain, vplus(vsucc(vmul(vsucc(vd411),sK18)),X0) = vplus(vmul(vsucc(vd411),sK18),vsucc(X0)), inference(demodulation, [status(thm)], [d19,d16])). % 9.17/2.44 cnf(d21, plain, vplus(vmul(vsucc(vd411),sK18),vsucc(X0)) = vplus(X0,vsucc(vmul(vsucc(vd411),sK18))), inference(superposition, [status(thm)], [d20,c11])). % 9.17/2.44 cnf(d22, plain, vmul(vsucc(vd411),X0) != vplus(vmul(vd411,X0),X0) | vplus(vmul(vd411,X0),vplus(vd411,vsucc(X0))) = vplus(vmul(vd411,vsucc(X0)),vsucc(X0)), inference(demodulation, [status(thm)], [c1,c9])). % 9.17/2.44 cnf(d23, plain, vmul(vsucc(vd411),X0) != vplus(X0,vmul(vd411,X0)) | vplus(vmul(vd411,X0),vplus(vd411,vsucc(X0))) = vplus(vmul(vd411,vsucc(X0)),vsucc(X0)), inference(demodulation, [status(thm)], [d22,c11])). % 9.17/2.44 cnf(d24, plain, vmul(vsucc(vd411),X0) != vplus(X0,vmul(vd411,X0)) | vplus(vmul(vd411,X0),vplus(vd411,vsucc(X0))) = vplus(vsucc(X0),vmul(vd411,vsucc(X0))), inference(demodulation, [status(thm)], [d23,c11])). % 9.17/2.44 cnf(d25, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vplus(vmul(vd411,sK18),vplus(vd411,vsucc(sK18))) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(superposition, [status(thm)], [d3,d24])). % 9.17/2.44 cnf(d26, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vplus(vsucc(sK18),vplus(vmul(vd411,sK18),vd411)) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [d25,d4])). % 9.17/2.44 cnf(d27, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vplus(sK18,vsucc(vplus(vmul(vd411,sK18),vd411))) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [d26,d2])). % 9.17/2.44 cnf(d28, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vplus(sK18,vplus(vmul(vd411,sK18),vsucc(vd411))) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [d27,c14])). % 9.17/2.44 cnf(d29, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vplus(vmul(vsucc(vd411),sK18),vsucc(vd411)) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [d28,d12])). % 9.17/2.44 cnf(d30, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vplus(vd411,vsucc(vmul(vsucc(vd411),sK18))) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [d29,d21])). % 9.17/2.44 cnf(d31, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vmul(vsucc(vd411),vsucc(sK18)) = vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [d30,d11])). % 9.17/2.44 cnf(d32, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18) | vmul(vsucc(vd411),vsucc(sK18)) = vplus(sK18,vsucc(vmul(vd411,vsucc(sK18)))), inference(demodulation, [status(thm)], [d31,d2])). % 9.17/2.44 cnf(d33, plain, vmul(vsucc(vd411),vsucc(sK18)) != vplus(vsucc(sK18),vmul(vd411,vsucc(sK18))), inference(demodulation, [status(thm)], [c17,c11])). % 9.17/2.44 cnf(d34, plain, vmul(vsucc(vd411),vsucc(sK18)) != vplus(sK18,vsucc(vmul(vd411,vsucc(sK18)))), inference(demodulation, [status(thm)], [d33,d2])). % 9.17/2.44 cnf(d35, plain, vmul(vsucc(vd411),sK18) != vmul(vsucc(vd411),sK18), inference(resolution, [status(thm)], [d34,d32])). % 9.17/2.44 cnf(d36, plain, $false, inference(equality_resolution, [status(thm)], [d35])). % 9.17/2.44 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------