%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : COM141+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:05 AM UTC 2025
% Result : Theorem 102.70s 13.18s
% Output : CNFRefutation 102.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : COM141+1 : TPTP v9.0.0. Released v6.4.0.
% 0.00/0.09 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.28 % Computer : n017.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Sun Jul 20 06:19:19 EDT 2025
% 0.08/0.29 % CPUTime :
% 0.14/0.29 % launching worker at depth: 1
% 0.14/0.29 % launching worker at depth: 3
% 0.14/0.29 % launching worker at depth: 2
% 0.14/0.29 % launching worker at depth: 4
% 0.14/0.29 % launching worker at depth: 5
% 0.14/0.29 % launching worker at depth: 6
% 0.14/0.29 % launching worker at depth: 7
% 0.14/0.29 % launching worker at depth: 8
% 0.14/0.30 % launching worker at depth: 9
% 0.14/0.41 % launching worker at depth: 10
% 102.70/13.18 % SZS status Theorem for theBenchmark
% 102.70/13.18 % SZS output start CNFRefutation
% 102.70/13.18 fof('T-Weak-abs', plain, ![Vx,VS,VC,Vy,VS1,VT]:((vlookup(Vx,VC)=vnoType&vtcheck(VC,vabs(Vy,VS1,veabs),VT))=>vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-Weak-abs')).
% 102.70/13.18 fof('T-Weak-abs'_negated, plain, ~(![Vx,VS,VC,Vy,VS1,VT]:((vlookup(Vx,VC)=vnoType&vtcheck(VC,vabs(Vy,VS1,veabs),VT))=>vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT))), inference(negate_conjecture, [status(cth)], ['T-Weak-abs'])).
% 102.70/13.18 cnf(147, plain, vlookup(sK75,sK77) = vnoType, inference(cnf, [status(esa)], ['T-Weak-abs'_negated])).
% 102.70/13.18 cnf(l0, plain, vlookup(sK75,sK77) = vnoType, inference(instantiation, [status(thm)], [147])).
% 102.70/13.18 fof('T-Weak-abs-2', plain, ![Vx,VS,VC,Vy,VS1,VT]:((Vx=Vy&vlookup(Vx,VC)=vnoType&vtcheck(VC,vabs(Vy,VS1,veabs),VT))=>vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-Weak-abs-2')).
% 102.70/13.18 cnf(146, 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(cnf, [status(esa)], ['T-Weak-abs-2'])).
% 102.70/13.18 cnf(l1, plain, sK75 != sK78 | vlookup(sK75,sK77) != vnoType | ~vtcheck(sK77,vabs(sK78,sK79,veabs),sK80) | vtcheck(vbind(sK75,sK76,sK77),vabs(sK78,sK79,veabs),sK80), inference(instantiation, [status(thm)], [146])).
% 102.70/13.18 cnf(148, plain, vtcheck(sK77,vabs(sK78,sK79,veabs),sK80), inference(cnf, [status(esa)], ['T-Weak-abs'_negated])).
% 102.70/13.18 cnf(l29, plain, vtcheck(sK77,vabs(sK78,sK79,veabs),sK80), inference(instantiation, [status(thm)], [148])).
% 102.70/13.18 fof('T-Weak-abs-1', plain, ![Vx,VS,VC,Vy,VS1,VT]:((Vx!=Vy&vlookup(Vx,VC)=vnoType&vtcheck(VC,vabs(Vy,VS1,veabs),VT))=>vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-Weak-abs-1')).
% 102.70/13.18 cnf(145, plain, vlookup(X0,X1) != vnoType | ~vtcheck(X1,vabs(X2,X3,veabs),X4) | X0 = X2 | vtcheck(vbind(X0,X5,X1),vabs(X2,X3,veabs),X4), inference(cnf, [status(esa)], ['T-Weak-abs-1'])).
% 102.70/13.18 cnf(l19, plain, vlookup(sK75,sK77) != vnoType | ~vtcheck(sK77,vabs(sK78,sK79,veabs),sK80) | sK75 = sK78 | vtcheck(vbind(sK75,sK76,sK77),vabs(sK78,sK79,veabs),sK80), inference(instantiation, [status(thm)], [145])).
% 102.70/13.18 cnf(149, plain, ~vtcheck(vbind(sK75,sK76,sK77),vabs(sK78,sK79,veabs),sK80), inference(cnf, [status(esa)], ['T-Weak-abs'_negated])).
% 102.70/13.18 cnf(l24, plain, ~vtcheck(vbind(sK75,sK76,sK77),vabs(sK78,sK79,veabs),sK80), inference(instantiation, [status(thm)], [149])).
% 102.70/13.18 cnf(l27, plain, vtcheck(sK77,vabs(sK78,sK79,veabs),sK80), inference(instantiation, [status(thm)], [148])).
% 102.70/13.18 cnf(l2, plain, ~vtcheck(vbind(sK75,sK76,sK77),vabs(sK78,sK79,veabs),sK80), inference(instantiation, [status(thm)], [149])).
% 102.70/13.18 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l29, l19, l24, l27, l2])).
% 102.70/13.18 % SZS output end CNFRefutation
%------------------------------------------------------------------------------