%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : COM133+1 : TPTP v9.0.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 10:55:04 AM UTC 2025
% Result : Theorem 277.04s 35.05s
% Output : CNFRefutation 277.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.08 % Problem : COM133+1 : TPTP v9.0.0. Released v6.4.0.
% 0.02/0.09 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.28 % Computer : n017.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Sun Jul 20 06:18:19 EDT 2025
% 0.09/0.28 % CPUTime :
% 0.09/0.29 % launching worker at depth: 2
% 0.09/0.29 % launching worker at depth: 5
% 0.09/0.29 % launching worker at depth: 3
% 0.09/0.29 % launching worker at depth: 1
% 0.09/0.29 % launching worker at depth: 4
% 0.09/0.29 % launching worker at depth: 6
% 0.09/0.29 % launching worker at depth: 7
% 0.09/0.29 % launching worker at depth: 8
% 0.09/0.29 % launching worker at depth: 9
% 0.13/0.31 % launching worker at depth: 10
% 6.30/1.12 % launching worker at depth: 11
% 277.04/35.05 % SZS status Theorem for theBenchmark
% 277.04/35.05 % SZS output start CNFRefutation
% 277.04/35.05 fof('T-subst-abs', plain, ![VT,VC,Vx,Ve,Vy,VS,VT2]:((vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))=>vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-subst-abs')).
% 277.04/35.05 fof('T-subst-abs'_negated, plain, ~(![VT,VC,Vx,Ve,Vy,VS,VT2]:((vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))=>vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2))), inference(negate_conjecture, [status(cth)], ['T-subst-abs'])).
% 277.04/35.05 cnf(151, plain, vtcheck(sK76,sK78,sK75), inference(cnf, [status(esa)], ['T-subst-abs'_negated])).
% 277.04/35.05 cnf(l0, plain, vtcheck(sK76,sK78,sK75), inference(instantiation, [status(thm)], [151])).
% 277.04/35.05 fof('T-subst-abs-3', plain, ![VT,VC,Vx,Ve,Vy,VS,VT2]:((Vx!=Vy&visFreeVar(Vy,Ve)&vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))=>vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-subst-abs-3')).
% 277.04/35.05 cnf(150, plain, ~visFreeVar(X0,X1) | ~vtcheck(X2,X1,X3) | ~vtcheck(vbind(X4,X3,X2),vabs(X0,X5,veabs),X6) | X4 = X0 | vtcheck(X2,vsubst(X4,X1,vabs(X0,X5,veabs)),X6), inference(cnf, [status(esa)], ['T-subst-abs-3'])).
% 277.04/35.05 cnf(l1, plain, ~visFreeVar(sK79,sK78) | ~vtcheck(sK76,sK78,sK75) | ~vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81) | sK77 = sK79 | vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [150])).
% 277.04/35.05 cnf(152, plain, vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81), inference(cnf, [status(esa)], ['T-subst-abs'_negated])).
% 277.04/35.05 cnf(l3, plain, vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81), inference(instantiation, [status(thm)], [152])).
% 277.04/35.05 cnf(153, plain, ~vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(cnf, [status(esa)], ['T-subst-abs'_negated])).
% 277.04/35.05 cnf(l122, plain, ~vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [153])).
% 277.04/35.05 fof('T-subst-abs-2', plain, ![VT,VC,Vx,Ve,Vy,VS,VT2]:((Vx!=Vy&~visFreeVar(Vy,Ve)&vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))=>vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-subst-abs-2')).
% 277.04/35.05 cnf(149, plain, ~vtcheck(X0,X1,X2) | ~vtcheck(vbind(X3,X2,X0),vabs(X4,X5,veabs),X6) | X3 = X4 | visFreeVar(X4,X1) | vtcheck(X0,vsubst(X3,X1,vabs(X4,X5,veabs)),X6), inference(cnf, [status(esa)], ['T-subst-abs-2'])).
% 277.04/35.05 cnf(l98, plain, ~vtcheck(sK76,sK78,sK75) | ~vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81) | sK77 = sK79 | visFreeVar(sK79,sK78) | vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [149])).
% 277.04/35.05 cnf(l110, plain, vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81), inference(instantiation, [status(thm)], [152])).
% 277.04/35.05 fof('T-subst-abs-1', plain, ![VT,VC,Vx,Ve,Vy,VS,Ve1,VT2]:((Vx=Vy&vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2))=>vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-subst-abs-1')).
% 277.04/35.05 cnf(148, plain, X0 != X1 | ~vtcheck(X2,X3,X4) | ~vtcheck(vbind(X0,X4,X2),vabs(X1,X5,X6),X7) | vtcheck(X2,vsubst(X0,X3,vabs(X1,X5,X6)),X7), inference(cnf, [status(esa)], ['T-subst-abs-1'])).
% 277.04/35.05 cnf(l107, plain, sK77 != sK79 | ~vtcheck(sK76,sK78,sK75) | ~vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81) | vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [148])).
% 277.04/35.05 cnf(l128, plain, vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81), inference(instantiation, [status(thm)], [152])).
% 277.04/35.05 cnf(l151, plain, ~vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [153])).
% 277.04/35.05 cnf(l109, plain, ~vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [153])).
% 277.04/35.05 cnf(l79, plain, sK77 != sK79 | ~vtcheck(sK76,sK78,sK75) | ~vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81) | vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [148])).
% 277.04/35.05 cnf(l129, plain, vtcheck(vbind(sK77,sK75,sK76),vabs(sK79,sK80,veabs),sK81), inference(instantiation, [status(thm)], [152])).
% 277.04/35.05 cnf(l135, plain, ~vtcheck(sK76,vsubst(sK77,sK78,vabs(sK79,sK80,veabs)),sK81), inference(instantiation, [status(thm)], [153])).
% 277.04/35.05 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l3, l122, l98, l110, l107, l128, l151, l109, l79, l129, l135])).
% 277.04/35.05 % SZS output end CNFRefutation
%------------------------------------------------------------------------------