%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : COM140+1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n019.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 24.91s 3.59s % Output : CNFRefutation 24.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : COM140+1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.36 % Computer : n019.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 23:36:33 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 24.91/3.59 % SZS status Theorem for theBenchmark.p % 24.91/3.59 % SZS output start CNFRefutation for theBenchmark.p % 24.91/3.59 fof(T-Weak-abs-1-gen, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : (((X0 != X3 & (vlookup(X0,X2) = vnoType & vtcheck(X2,vabs(X3,X4,X5),X6))) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,X5),X6)))). % 24.91/3.59 fof(isFreeVar0, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((X0 = X3 & X1 = vvar(X2)) => ((X2 = X3 => visFreeVar(X0,X1)) & (visFreeVar(X0,X1) => X2 = X3))))). % 24.91/3.59 fof(isFreeVar2, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((X0 = X3 & X1 = vapp(X2,X4)) => (((visFreeVar(X3,X2) | visFreeVar(X3,X4)) => visFreeVar(X0,X1)) & (visFreeVar(X0,X1) => (visFreeVar(X3,X2) | visFreeVar(X3,X4))))))). % 24.91/3.59 fof(gensym-is-fresh, axiom, ! [X0] : ! [X1] : ((vgensym(X1) = X0 => ~visFreeVar(X0,X1)))). % 24.91/3.59 fof(alpha-equiv-sym, axiom, ! [X0] : ! [X1] : ((valphaEquivalent(X1,X0) => valphaEquivalent(X0,X1)))). % 24.91/3.59 fof(alpha-equiv-subst-abs, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((~visFreeVar(X2,X3) => valphaEquivalent(vabs(X1,X0,X3),vabs(X2,X0,vsubst(X1,vvar(X2),X3)))))). % 24.91/3.59 fof(alpha-equiv-typing, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((vtcheck(X1,X0,X3) & valphaEquivalent(X0,X2)) => vtcheck(X1,X2,X3)))). % 24.91/3.59 fof(T-Weak-abs-2, conjecture, ! [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)))). % 24.91/3.59 fof(negated_conjecture, negated_conjecture, ~! [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))), inference(negate_conjecture, [status(cth)], [T-Weak-abs-2])). % 24.91/3.59 cnf(c0, plain, X0 = X1 | vlookup(X0,X2) != vnoType | ~vtcheck(X2,vabs(X1,X3,X4),X5) | vtcheck(vbind(X0,X6,X2),vabs(X1,X3,X4),X5), inference(clausification, [status(esa)], [T-Weak-abs-1-gen])). % 24.91/3.59 cnf(c16, plain, X0 != X1 | X2 != vvar(X3) | X3 != X1 | visFreeVar(X0,X2), inference(clausification, [status(esa)], [isFreeVar0])). % 24.91/3.59 cnf(c21, plain, X0 != X1 | X2 != vapp(X3,X4) | ~visFreeVar(X1,X3) | visFreeVar(X0,X2), inference(clausification, [status(esa)], [isFreeVar2])). % 24.91/3.59 cnf(c22, plain, X0 != X1 | X2 != vapp(X3,X4) | ~visFreeVar(X1,X4) | visFreeVar(X0,X2), inference(clausification, [status(esa)], [isFreeVar2])). % 24.91/3.59 cnf(c53, plain, vgensym(X0) != X1 | ~visFreeVar(X1,X0), inference(clausification, [status(esa)], [gensym-is-fresh])). % 24.91/3.59 cnf(c149, plain, ~valphaEquivalent(X0,X1) | valphaEquivalent(X1,X0), inference(clausification, [status(esa)], [alpha-equiv-sym])). % 24.91/3.59 cnf(c151, plain, visFreeVar(X0,X1) | valphaEquivalent(vabs(X2,X3,X1),vabs(X0,X3,vsubst(X2,vvar(X0),X1))), inference(clausification, [status(esa)], [alpha-equiv-subst-abs])). % 24.91/3.59 cnf(c152, plain, ~vtcheck(X0,X1,X2) | ~valphaEquivalent(X1,X3) | vtcheck(X0,X3,X2), inference(clausification, [status(esa)], [alpha-equiv-typing])). % 24.91/3.59 cnf(c154, plain, sK345 = sK348, inference(clausification, [status(esa)], [negated_conjecture])). % 24.91/3.59 cnf(c155, plain, vlookup(sK345,sK347) = vnoType, inference(clausification, [status(esa)], [negated_conjecture])). % 24.91/3.59 cnf(c156, plain, vtcheck(sK347,vabs(sK348,sK349,veabs),sK350), inference(clausification, [status(esa)], [negated_conjecture])). % 24.91/3.59 cnf(c157, plain, ~vtcheck(vbind(sK345,sK346,sK347),vabs(sK348,sK349,veabs),sK350), inference(clausification, [status(esa)], [negated_conjecture])). % 24.91/3.59 cnf(d0, plain, X0 != X1 | X2 != X1 | visFreeVar(X2,vvar(X0)), inference(equality_resolution, [status(thm)], [c16])). % 24.91/3.59 cnf(d1, plain, X0 != X1 | visFreeVar(X0,vvar(X1)), inference(equality_resolution, [status(thm)], [d0])). % 24.91/3.59 cnf(d2, plain, visFreeVar(X0,vvar(X0)), inference(equality_resolution, [status(thm)], [d1])). % 24.91/3.59 cnf(d3, plain, ~visFreeVar(vgensym(X0),X0), inference(equality_resolution, [status(thm)], [c53])). % 24.91/3.59 cnf(d4, plain, X0 != X1 | visFreeVar(X0,vapp(X2,X3)) | ~visFreeVar(X1,X3), inference(equality_resolution, [status(thm)], [c22])). % 24.91/3.59 cnf(d5, plain, ~visFreeVar(X0,X1) | visFreeVar(X0,vapp(X2,X1)), inference(equality_resolution, [status(thm)], [d4])). % 24.91/3.59 cnf(d6, plain, ~visFreeVar(vgensym(vapp(X0,X1)),X1), inference(resolution, [status(thm)], [d5,d3])). % 24.91/3.59 cnf(d7, plain, ~vtcheck(vbind(sK345,sK346,sK347),vabs(sK345,sK349,veabs),sK350), inference(demodulation, [status(thm)], [c157,c154])). % 24.91/3.59 cnf(d8, plain, vtcheck(sK347,vabs(sK345,sK349,veabs),sK350), inference(demodulation, [status(thm)], [c156,c154])). % 24.91/3.59 cnf(d9, plain, vtcheck(sK347,X0,sK350) | ~valphaEquivalent(vabs(sK345,sK349,veabs),X0), inference(resolution, [status(thm)], [c152,d8])). % 24.91/3.59 cnf(d10, plain, vtcheck(sK347,vabs(X0,sK349,vsubst(sK345,vvar(X0),veabs)),sK350) | visFreeVar(X0,veabs), inference(resolution, [status(thm)], [d9,c151])). % 24.91/3.59 cnf(d11, plain, vnoType != vnoType | sK345 = X0 | ~vtcheck(sK347,vabs(X0,X1,X2),X3) | vtcheck(vbind(sK345,X4,sK347),vabs(X0,X1,X2),X3), inference(superposition, [status(thm)], [c155,c0])). % 24.91/3.59 cnf(d12, plain, sK345 = X0 | vtcheck(vbind(sK345,X1,sK347),vabs(X0,X2,X3),X4) | ~vtcheck(sK347,vabs(X0,X2,X3),X4), inference(equality_resolution, [status(thm)], [d11])). % 24.91/3.59 cnf(d13, plain, vtcheck(vbind(sK345,X0,sK347),X1,X2) | ~valphaEquivalent(vabs(X3,X4,X5),X1) | sK345 = X3 | ~vtcheck(sK347,vabs(X3,X4,X5),X2), inference(resolution, [status(thm)], [c152,d12])). % 24.91/3.59 cnf(d14, plain, sK345 = X0 | vtcheck(vbind(sK345,X1,sK347),X2,sK350) | ~valphaEquivalent(vabs(X0,sK349,vsubst(sK345,vvar(X0),veabs)),X2) | visFreeVar(X0,veabs), inference(resolution, [status(thm)], [d13,d10])). % 24.91/3.59 cnf(d15, plain, visFreeVar(X0,X1) | valphaEquivalent(vabs(X0,X2,vsubst(X3,vvar(X0),X1)),vabs(X3,X2,X1)), inference(resolution, [status(thm)], [c151,c149])). % 24.91/3.59 cnf(d16, plain, visFreeVar(X0,veabs) | sK345 = X0 | vtcheck(vbind(sK345,X1,sK347),vabs(sK345,sK349,veabs),sK350) | visFreeVar(X0,veabs), inference(resolution, [status(thm)], [d15,d14])). % 24.91/3.59 cnf(d17, plain, sK345 = X0 | visFreeVar(X0,veabs), inference(resolution, [status(thm)], [d16,d7])). % 24.91/3.59 cnf(d18, plain, X0 != X1 | visFreeVar(X0,vapp(X2,X3)) | ~visFreeVar(X1,X2), inference(equality_resolution, [status(thm)], [c21])). % 24.91/3.59 cnf(d19, plain, ~visFreeVar(X0,X1) | visFreeVar(X0,vapp(X1,X2)), inference(equality_resolution, [status(thm)], [d18])). % 24.91/3.59 cnf(d20, plain, ~visFreeVar(vgensym(vapp(X0,X1)),X0), inference(resolution, [status(thm)], [d19,d3])). % 24.91/3.59 cnf(d21, plain, sK345 = vgensym(vapp(veabs,X0)), inference(resolution, [status(thm)], [d20,d17])). % 24.91/3.59 cnf(d22, plain, ~visFreeVar(sK345,X0), inference(superposition, [status(thm)], [d21,d6])). % 24.91/3.59 cnf(d23, plain, $false, inference(resolution, [status(thm)], [d22,d2])). % 24.91/3.59 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------