%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM837+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 : n014.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:55 AM UTC 2026 % Result : Theorem 10.29s 11.82s % Output : CNFRefutation 10.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM837+2 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/10.38 % Computer : n014.cluster.edu % 0.09/10.38 % Model : x86_64 x86_64 % 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/10.38 % Memory : 8046.5625MB % 0.09/10.38 % OS : Linux 6.8.0-71-generic % 0.09/10.38 % CPULimit : 300 % 0.09/10.38 % WCLimit : 300 % 0.09/10.38 % DateTime : Sat Sep 26 04:11:27 UTC 2026 % 0.09/10.38 % CPUTime : % 0.09/10.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.29/11.82 % SZS status Theorem for theBenchmark.p % 10.29/11.82 % SZS output start CNFRefutation for theBenchmark.p % 10.29/11.82 fof(holds(conjunct1(170), 270, 0), axiom, less(vd268,vd269)). % 10.29/11.82 fof(ass(cond(147, 0), 0), axiom, ! [X0] : ! [X1] : ((less(X0,X1) => greater(X1,X0)))). % 10.29/11.82 fof(ass(cond(goal(130), 0), 1), axiom, ! [X0] : ! [X1] : ((X0 != X1 | ~less(X0,X1)))). % 10.29/11.82 fof(ass(cond(goal(130), 0), 2), axiom, ! [X0] : ! [X1] : ((~greater(X0,X1) | ~less(X0,X1)))). % 10.29/11.82 fof(def(cond(conseq(axiom(3)), 12), 1), axiom, ! [X0] : ! [X1] : ((less(X1,X0) <=> ? [X2] : X0 = vplus(X1,X2)))). % 10.29/11.82 fof(ass(cond(goal(88), 0), 0), axiom, ! [X0] : ! [X1] : ((X0 = X1 | (? [X2] : X0 = vplus(X1,X2) | ? [X3] : X1 = vplus(X0,X3))))). % 10.29/11.82 fof(qe(171), conjecture, ? [X0] : vd269 = vplus(vd268,X0)). % 10.29/11.82 fof(negated_conjecture, negated_conjecture, ~? [X0] : vd269 = vplus(vd268,X0), inference(negate_conjecture, [status(cth)], [qe(171)])). % 10.29/11.82 cnf(c1, plain, less(vd268,vd269), inference(clausification, [status(esa)], [holds(conjunct1(170), 270, 0)])). % 10.29/11.82 cnf(c10, plain, ~less(X0,X1) | greater(X1,X0), inference(clausification, [status(esa)], [ass(cond(147, 0), 0)])). % 10.29/11.82 cnf(c13, plain, X0 != X1 | ~less(X0,X1), inference(clausification, [status(esa)], [ass(cond(goal(130), 0), 1)])). % 10.29/11.82 cnf(c14, plain, ~greater(X0,X1) | ~less(X0,X1), inference(clausification, [status(esa)], [ass(cond(goal(130), 0), 2)])). % 10.29/11.82 cnf(c17, plain, less(X0,X1) | X1 != vplus(X0,X2), inference(clausification, [status(esa)], [def(cond(conseq(axiom(3)), 12), 1)])). % 10.29/11.82 cnf(c20, plain, X0 = X1 | X0 = vplus(X1,sK30(X0,X1)) | X1 = vplus(X0,sK31(X0,X1)), inference(clausification, [status(esa)], [ass(cond(goal(88), 0), 0)])). % 10.29/11.82 cnf(c28, plain, vd269 != vplus(vd268,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 10.29/11.82 cnf(d0, plain, vd269 != X0 | vd268 = X0 | vd268 = vplus(X0,sK30(vd268,X0)), inference(superposition, [status(thm)], [c20,c28])). % 10.29/11.82 cnf(d1, plain, vd268 = vd269 | vd268 = vplus(vd269,sK30(vd268,vd269)), inference(equality_resolution, [status(thm)], [d0])). % 10.29/11.82 cnf(d2, plain, X0 != vd268 | less(vd269,X0) | vd268 = vd269, inference(superposition, [status(thm)], [d1,c17])). % 10.29/11.82 cnf(d3, plain, vd268 = vd269 | less(vd269,vd268), inference(equality_resolution, [status(thm)], [d2])). % 10.29/11.82 cnf(d4, plain, vd268 = vd269 | greater(vd268,vd269), inference(resolution, [status(thm)], [d3,c10])). % 10.29/11.82 cnf(d5, plain, vd268 = vd269 | ~less(vd268,vd269), inference(resolution, [status(thm)], [d4,c14])). % 10.29/11.82 cnf(d6, plain, vd268 = vd269, inference(resolution, [status(thm)], [c1,d5])). % 10.29/11.82 cnf(d7, plain, less(vd269,vd269), inference(demodulation, [status(thm)], [c1,d6])). % 10.29/11.82 cnf(d8, plain, ~less(X0,X0), inference(equality_resolution, [status(thm)], [c13])). % 10.29/11.82 cnf(d9, plain, $false, inference(resolution, [status(thm)], [d8,d7])). % 10.29/11.82 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------