%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : COM141+1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n020.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:58:53 AM UTC 2026 % Result : Theorem 15.42s 2.69s % Output : CNFRefutation 15.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : COM141+1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.37 % Computer : n020.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 23:37:05 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.42/2.69 % SZS status Theorem for theBenchmark.p % 15.42/2.69 % SZS output start CNFRefutation for theBenchmark.p % 15.42/2.69 fof(T-Weak-abs-1, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((X0 != X3 & (vlookup(X0,X2) = vnoType & vtcheck(X2,vabs(X3,X4,veabs),X5))) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)))). % 15.42/2.69 fof(T-Weak-abs-2, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((X0 = X3 & (vlookup(X0,X2) = vnoType & vtcheck(X2,vabs(X3,X4,veabs),X5))) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)))). % 15.42/2.69 fof(T-Weak-abs, conjecture, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((vlookup(X0,X2) = vnoType & vtcheck(X2,vabs(X3,X4,veabs),X5)) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)))). % 15.42/2.69 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((vlookup(X0,X2) = vnoType & vtcheck(X2,vabs(X3,X4,veabs),X5)) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5))), inference(negate_conjecture, [status(cth)], [T-Weak-abs])). % 15.42/2.69 cnf(c1, plain, X0 = X1 | vlookup(X0,X2) != vnoType | ~vtcheck(X2,vabs(X1,X3,veabs),X4) | vtcheck(vbind(X0,X5,X2),vabs(X1,X3,veabs),X4), inference(clausification, [status(esa)], [T-Weak-abs-1])). % 15.42/2.69 cnf(c2, plain, X0 != X1 | vlookup(X0,X2) != vnoType | ~vtcheck(X2,vabs(X1,X3,veabs),X4) | vtcheck(vbind(X0,X5,X2),vabs(X1,X3,veabs),X4), inference(clausification, [status(esa)], [T-Weak-abs-2])). % 15.42/2.69 cnf(c150, plain, vlookup(sK337,sK339) = vnoType, inference(clausification, [status(esa)], [negated_conjecture])). % 15.42/2.69 cnf(c151, plain, vtcheck(sK339,vabs(sK340,sK341,veabs),sK342), inference(clausification, [status(esa)], [negated_conjecture])). % 15.42/2.69 cnf(c152, plain, ~vtcheck(vbind(sK337,sK338,sK339),vabs(sK340,sK341,veabs),sK342), inference(clausification, [status(esa)], [negated_conjecture])). % 15.42/2.69 cnf(d0, plain, vnoType != vnoType | sK337 = X0 | ~vtcheck(sK339,vabs(X0,X1,veabs),X2) | vtcheck(vbind(sK337,X3,sK339),vabs(X0,X1,veabs),X2), inference(superposition, [status(thm)], [c150,c1])). % 15.42/2.69 cnf(d1, plain, sK337 = X0 | vtcheck(vbind(sK337,X1,sK339),vabs(X0,X2,veabs),X3) | ~vtcheck(sK339,vabs(X0,X2,veabs),X3), inference(equality_resolution, [status(thm)], [d0])). % 15.42/2.69 cnf(d2, plain, sK337 = sK340 | ~vtcheck(sK339,vabs(sK340,sK341,veabs),sK342), inference(resolution, [status(thm)], [d1,c152])). % 15.42/2.69 cnf(d3, plain, sK337 = sK340, inference(resolution, [status(thm)], [c151,d2])). % 15.42/2.69 cnf(d4, plain, ~vtcheck(vbind(sK337,sK338,sK339),vabs(sK337,sK341,veabs),sK342), inference(demodulation, [status(thm)], [c152,d3])). % 15.42/2.69 cnf(d5, plain, vnoType != vnoType | sK337 != X0 | ~vtcheck(sK339,vabs(X0,X1,veabs),X2) | vtcheck(vbind(sK337,X3,sK339),vabs(X0,X1,veabs),X2), inference(superposition, [status(thm)], [c150,c2])). % 15.42/2.69 cnf(d6, plain, vnoType != vnoType | vtcheck(vbind(sK337,X0,sK339),vabs(sK337,X1,veabs),X2) | ~vtcheck(sK339,vabs(sK337,X1,veabs),X2), inference(equality_resolution, [status(thm)], [d5])). % 15.42/2.69 cnf(d7, plain, vtcheck(vbind(sK337,X0,sK339),vabs(sK337,X1,veabs),X2) | ~vtcheck(sK339,vabs(sK337,X1,veabs),X2), inference(equality_resolution, [status(thm)], [d6])). % 15.42/2.69 cnf(d8, plain, ~vtcheck(sK339,vabs(sK337,sK341,veabs),sK342), inference(resolution, [status(thm)], [d7,d4])). % 15.42/2.69 cnf(d9, plain, vtcheck(sK339,vabs(sK337,sK341,veabs),sK342), inference(demodulation, [status(thm)], [c151,d3])). % 15.42/2.69 cnf(d10, plain, $false, inference(resolution, [status(thm)], [d9,d8])). % 15.42/2.69 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------