%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : COM124+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 : n017.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:51 AM UTC 2026 % Result : Theorem 20.06s 3.32s % Output : CNFRefutation 20.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : COM124+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.10/0.37 % Computer : n017.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:26:18 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 20.06/3.32 % SZS status Theorem for theBenchmark.p % 20.06/3.32 % SZS output start CNFRefutation for theBenchmark.p % 20.06/3.32 fof(T-Weak-FreeVar-abs-1-gen, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : (((X0 != X3 & (~visFreeVar(X0,vabs(X3,X4,X5)) & vtcheck(X2,vabs(X3,X4,X5),X6))) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,X5),X6)))). % 20.06/3.32 fof(isFreeVar0, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((X0 = X3 & X1 = vvar(X2)) => ((X2 = X3 => visFreeVar(X0,X1)) & (visFreeVar(X0,X1) => X2 = X3))))). % 20.06/3.32 fof(isFreeVar1, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((X1 = X4 & X2 = vabs(X3,X0,X5)) => (((X3 != X4 & visFreeVar(X4,X5)) => visFreeVar(X1,X2)) & (visFreeVar(X1,X2) => (X3 != X4 & visFreeVar(X4,X5))))))). % 20.06/3.32 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))))))). % 20.06/3.32 fof(gensym-is-fresh, axiom, ! [X0] : ! [X1] : ((vgensym(X1) = X0 => ~visFreeVar(X0,X1)))). % 20.06/3.32 fof(alpha-equiv-sym, axiom, ! [X0] : ! [X1] : ((valphaEquivalent(X1,X0) => valphaEquivalent(X0,X1)))). % 20.06/3.32 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)))))). % 20.06/3.32 fof(alpha-equiv-typing, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((vtcheck(X1,X0,X3) & valphaEquivalent(X0,X2)) => vtcheck(X1,X2,X3)))). % 20.06/3.32 fof(alpha-equiv-FreeVar, axiom, ! [X0] : ! [X1] : ! [X2] : (((~visFreeVar(X1,X0) & valphaEquivalent(X0,X2)) => ~visFreeVar(X1,X2)))). % 20.06/3.32 fof(T-Weak-FreeVar-abs-2, conjecture, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((X0 = X3 & (~visFreeVar(X0,vabs(X3,X4,veabs)) & vtcheck(X2,vabs(X3,X4,veabs),X5))) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)))). % 20.06/3.32 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((X0 = X3 & (~visFreeVar(X0,vabs(X3,X4,veabs)) & vtcheck(X2,vabs(X3,X4,veabs),X5))) => vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5))), inference(negate_conjecture, [status(cth)], [T-Weak-FreeVar-abs-2])). % 20.06/3.32 cnf(c2, plain, X0 = X1 | visFreeVar(X0,vabs(X1,X2,X3)) | ~vtcheck(X4,vabs(X1,X2,X3),X5) | vtcheck(vbind(X0,X6,X4),vabs(X1,X2,X3),X5), inference(clausification, [status(esa)], [T-Weak-FreeVar-abs-1-gen])). % 20.06/3.32 cnf(c18, plain, X0 != X1 | X2 != vvar(X3) | X3 != X1 | visFreeVar(X0,X2), inference(clausification, [status(esa)], [isFreeVar0])). % 20.06/3.32 cnf(c21, plain, X0 != X1 | X2 != vabs(X3,X4,X5) | ~visFreeVar(X0,X2) | X3 != X1, inference(clausification, [status(esa)], [isFreeVar1])). % 20.06/3.32 cnf(c23, plain, X0 != X1 | X2 != vapp(X3,X4) | ~visFreeVar(X1,X3) | visFreeVar(X0,X2), inference(clausification, [status(esa)], [isFreeVar2])). % 20.06/3.32 cnf(c24, plain, X0 != X1 | X2 != vapp(X3,X4) | ~visFreeVar(X1,X4) | visFreeVar(X0,X2), inference(clausification, [status(esa)], [isFreeVar2])). % 20.06/3.32 cnf(c55, plain, vgensym(X0) != X1 | ~visFreeVar(X1,X0), inference(clausification, [status(esa)], [gensym-is-fresh])). % 20.06/3.32 cnf(c151, plain, ~valphaEquivalent(X0,X1) | valphaEquivalent(X1,X0), inference(clausification, [status(esa)], [alpha-equiv-sym])). % 20.06/3.32 cnf(c153, 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])). % 20.06/3.32 cnf(c154, plain, ~vtcheck(X0,X1,X2) | ~valphaEquivalent(X1,X3) | vtcheck(X0,X3,X2), inference(clausification, [status(esa)], [alpha-equiv-typing])). % 20.06/3.32 cnf(c155, plain, visFreeVar(X0,X1) | ~valphaEquivalent(X1,X2) | ~visFreeVar(X0,X2), inference(clausification, [status(esa)], [alpha-equiv-FreeVar])). % 20.06/3.32 cnf(c156, plain, sK355 = sK358, inference(clausification, [status(esa)], [negated_conjecture])). % 20.06/3.32 cnf(c158, plain, vtcheck(sK357,vabs(sK358,sK359,veabs),sK360), inference(clausification, [status(esa)], [negated_conjecture])). % 20.06/3.32 cnf(c159, plain, ~vtcheck(vbind(sK355,sK356,sK357),vabs(sK358,sK359,veabs),sK360), inference(clausification, [status(esa)], [negated_conjecture])). % 20.06/3.32 cnf(d0, plain, X0 != X1 | X2 != X1 | visFreeVar(X0,vvar(X2)), inference(equality_resolution, [status(thm)], [c18])). % 20.06/3.32 cnf(d1, plain, X0 != X1 | visFreeVar(X1,vvar(X0)), inference(equality_resolution, [status(thm)], [d0])). % 20.06/3.32 cnf(d2, plain, visFreeVar(X0,vvar(X0)), inference(equality_resolution, [status(thm)], [d1])). % 20.06/3.32 cnf(d3, plain, ~visFreeVar(vgensym(X0),X0), inference(equality_resolution, [status(thm)], [c55])). % 20.06/3.32 cnf(d4, plain, X0 != X1 | visFreeVar(X0,vapp(X2,X3)) | ~visFreeVar(X1,X2), inference(equality_resolution, [status(thm)], [c23])). % 20.06/3.32 cnf(d5, plain, ~visFreeVar(X0,X1) | visFreeVar(X0,vapp(X1,X2)), inference(equality_resolution, [status(thm)], [d4])). % 20.06/3.32 cnf(d6, plain, ~visFreeVar(vgensym(vapp(X0,X1)),X0), inference(resolution, [status(thm)], [d5,d3])). % 20.06/3.32 cnf(d7, plain, X0 != X1 | ~visFreeVar(X1,X2) | visFreeVar(X0,vapp(X3,X2)), inference(equality_resolution, [status(thm)], [c24])). % 20.06/3.32 cnf(d8, plain, ~visFreeVar(X0,X1) | visFreeVar(X0,vapp(X2,X1)), inference(equality_resolution, [status(thm)], [d7])). % 20.06/3.32 cnf(d9, plain, ~visFreeVar(vgensym(vapp(X0,X1)),X1), inference(resolution, [status(thm)], [d8,d3])). % 20.06/3.32 cnf(d10, plain, visFreeVar(X0,X1) | visFreeVar(X2,vabs(X3,X4,X1)) | ~visFreeVar(X2,vabs(X0,X4,vsubst(X3,vvar(X0),X1))), inference(resolution, [status(thm)], [c153,c155])). % 20.06/3.32 cnf(d11, plain, ~vtcheck(vbind(sK358,sK356,sK357),vabs(sK358,sK359,veabs),sK360), inference(demodulation, [status(thm)], [c159,c156])). % 20.06/3.32 cnf(d12, plain, visFreeVar(X0,X1) | valphaEquivalent(vabs(X0,X2,vsubst(X3,vvar(X0),X1)),vabs(X3,X2,X1)), inference(resolution, [status(thm)], [c153,c151])). % 20.06/3.32 cnf(d13, plain, vtcheck(sK357,X0,sK360) | ~valphaEquivalent(vabs(sK358,sK359,veabs),X0), inference(resolution, [status(thm)], [c154,c158])). % 20.06/3.32 cnf(d14, plain, visFreeVar(X0,veabs) | vtcheck(sK357,vabs(X0,sK359,vsubst(sK358,vvar(X0),veabs)),sK360), inference(resolution, [status(thm)], [c153,d13])). % 20.06/3.32 cnf(d15, plain, vtcheck(vbind(X0,X1,X2),X3,X4) | ~valphaEquivalent(vabs(X5,X6,X7),X3) | X0 = X5 | ~vtcheck(X2,vabs(X5,X6,X7),X4) | visFreeVar(X0,vabs(X5,X6,X7)), inference(resolution, [status(thm)], [c154,c2])). % 20.06/3.32 cnf(d16, plain, X0 = X1 | vtcheck(vbind(X0,X2,sK357),X3,sK360) | visFreeVar(X0,vabs(X1,sK359,vsubst(sK358,vvar(X1),veabs))) | ~valphaEquivalent(vabs(X1,sK359,vsubst(sK358,vvar(X1),veabs)),X3) | visFreeVar(X1,veabs), inference(resolution, [status(thm)], [d15,d14])). % 20.06/3.32 cnf(d17, plain, X0 = X1 | vtcheck(vbind(X0,X2,sK357),vabs(sK358,sK359,veabs),sK360) | visFreeVar(X1,veabs) | visFreeVar(X0,vabs(X1,sK359,vsubst(sK358,vvar(X1),veabs))) | visFreeVar(X1,veabs), inference(resolution, [status(thm)], [d16,d12])). % 20.06/3.32 cnf(d18, plain, sK358 = X0 | visFreeVar(X0,veabs) | visFreeVar(sK358,vabs(X0,sK359,vsubst(sK358,vvar(X0),veabs))), inference(resolution, [status(thm)], [d17,d11])). % 20.06/3.32 cnf(d19, plain, sK358 = X0 | visFreeVar(X0,veabs) | visFreeVar(sK358,vabs(sK358,sK359,veabs)) | visFreeVar(X0,veabs), inference(resolution, [status(thm)], [d18,d10])). % 20.06/3.32 cnf(d20, plain, X0 != X1 | X2 != X1 | ~visFreeVar(X2,vabs(X0,X3,X4)), inference(equality_resolution, [status(thm)], [c21])). % 20.06/3.32 cnf(d21, plain, X0 != X1 | ~visFreeVar(X0,vabs(X1,X2,X3)), inference(equality_resolution, [status(thm)], [d20])). % 20.06/3.32 cnf(d22, plain, ~visFreeVar(X0,vabs(X0,X1,X2)), inference(equality_resolution, [status(thm)], [d21])). % 20.06/3.32 cnf(d23, plain, sK358 = X0 | visFreeVar(X0,veabs), inference(resolution, [status(thm)], [d22,d19])). % 20.06/3.32 cnf(d24, plain, sK358 = vgensym(vapp(X0,veabs)), inference(resolution, [status(thm)], [d23,d9])). % 20.06/3.32 cnf(d25, plain, ~visFreeVar(sK358,X0), inference(superposition, [status(thm)], [d24,d6])). % 20.06/3.32 cnf(d26, plain, $false, inference(resolution, [status(thm)], [d25,d2])). % 20.06/3.32 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------