%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM149+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:59:49 AM UTC 2026
% Result : Theorem 24.07s 4.20s
% Output : CNFRefutation 24.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM149+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 23:36:45 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 314803 was started by sandbox2 on n010,
% 0.08/0.35 % Sat Sep 26 23:36:45 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.38/0.68
% 0.38/0.68 % From the command line: assign(max_seconds, 300).
% 24.07/4.20
% 24.07/4.20 % given #500 (I,wt=26): 1057 -defn_00(A,B,C,D) | f28(A,B,C,D) != f25(A,B,C,D) # tptp_name(subst-INV). [clausify(35)].
% 24.07/4.20
% 24.07/4.20 % SZS status Theorem for theBenchmark
% 24.07/4.20
% 24.07/4.20 % Proof 1 at 3.28 (+ 0.10) seconds.
% 24.07/4.20 % Length of proof is 16.
% 24.07/4.20 % Level of proof is 4.
% 24.07/4.20 % Maximum clause weight is 54.000.
% 24.07/4.20 % Given clauses 725.
% 24.07/4.20
% 24.07/4.20 % SZS output start CNFRefutation for theBenchmark
% 24.07/4.20 fof(DIFF-var-abs, axiom, ! [VVar0,VVar1,VTyp0,VExp0] : ~ (vvar(VVar0) = vabs(VVar1,VTyp0,VExp0)), file('theBenchmark.p',DIFF-var-abs)).
% 24.07/4.20 fof(DIFF-var-app, axiom, ! [VVar0,VExp0,VExp1] : ~ (vvar(VVar0) = vapp(VExp0,VExp1)), file('theBenchmark.p',DIFF-var-app)).
% 24.07/4.20 fof(DIFF-noType-someType, axiom, ! [VTyp0] : ~ (vnoType = vsomeType(VTyp0)), file('theBenchmark.p',DIFF-noType-someType)).
% 24.07/4.20 fof(lookup0, axiom, ! [Vx,VVar0,VCtx0,RESULT] : ((VVar0 = Vx & VCtx0 = vempty) => (RESULT = vlookup(VVar0,VCtx0) => RESULT = vnoType)), file('theBenchmark.p',lookup0)).
% 24.07/4.20 fof(T-inv, axiom, ! [Ve,VT,VC] : (vtcheck(VC,Ve,VT) => (? [Vx] : (Ve = vvar(Vx) & vlookup(Vx,VC) = vsomeType(VT)) | ? [Vx,Ve2,VT1,VT2] : (Ve = vabs(Vx,VT1,Ve2) & VT = varrow(VT1,VT2) & vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)) | ? [Ve1,Ve2,VS] : (Ve = vapp(Ve1,Ve2) & vtcheck(VC,Ve1,varrow(VS,VT)) & vtcheck(VC,Ve2,VS)))), file('theBenchmark.p',T-inv)).
% 24.07/4.20 fof(T-Progress-T-var, conjecture, ! [VT,Vx] : ((vtcheck(vempty,vvar(Vx),VT) & ~ (visValue(vvar(Vx)))) => ? [Veout] : vreduce(vvar(Vx)) = vsomeExp(Veout)), file('theBenchmark.p',T-Progress-T-var)).
% 24.07/4.20 fof(T-Progress-T-var_neg, negated_conjecture, ~(! [VT,Vx] : ((vtcheck(vempty,vvar(Vx),VT) & ~ (visValue(vvar(Vx)))) => ? [Veout] : vreduce(vvar(Vx)) = vsomeExp(Veout))), inference(assume_negation, [status(cth)], [T-Progress-T-var])).
% 24.07/4.20 fof(nnf_54, plain, ! [Ve,VT,VC] : (~ (vtcheck(VC,Ve,VT)) | ? [X0] : (vvar(X0) = Ve & vlookup(X0,VC) = vsomeType(VT)) | ? [Vx,X1,VT1,VT2] : (vabs(Vx,VT1,X1) = Ve & varrow(VT1,VT2) = VT & vtcheck(vbind(Vx,VT1,VC),X1,VT2)) | ? [Ve1,Ve2,VS] : (vapp(Ve1,Ve2) = Ve & vtcheck(VC,Ve1,varrow(VS,VT)) & vtcheck(VC,Ve2,VS))), inference(fof_nnf, [status(thm)], [T-inv])).
% 24.07/4.20 fof(sk_T-inv_sk, plain, ! [Ve,VT,VC] : (~ (vtcheck(VC,Ve,VT)) | (vvar(sK0(Ve,VT,VC)) = Ve & vlookup(sK0(Ve,VT,VC),VC) = vsomeType(VT)) | (vabs(sK1(Ve,VT,VC),sK2(Ve,VT,VC),sK3(Ve,VT,VC)) = Ve & varrow(sK2(Ve,VT,VC),sK8(Ve,VT,VC)) = VT & vtcheck(vbind(sK1(Ve,VT,VC),sK2(Ve,VT,VC),VC),sK3(Ve,VT,VC),sK8(Ve,VT,VC))) | (vapp(sK4(Ve,VT,VC),sK5(Ve,VT,VC)) = Ve & vtcheck(VC,sK4(Ve,VT,VC),varrow(sK9(Ve,VT,VC),VT)) & vtcheck(VC,sK5(Ve,VT,VC),sK9(Ve,VT,VC)))), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3,sK8,sK4,sK5,sK9]), skolemize(X0,sK0(Ve,VT,VC)), skolemize(Vx,sK1(Ve,VT,VC)), skolemize(X1,sK3(Ve,VT,VC)), skolemize(VT1,sK2(Ve,VT,VC)), skolemize(VT2,sK8(Ve,VT,VC)), skolemize(Ve1,sK4(Ve,VT,VC)), skolemize(Ve2,sK5(Ve,VT,VC)), skolemize(VS,sK9(Ve,VT,VC))], [nnf_54])).
% 24.07/4.20 fof(sk_T-inv, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK9(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK9(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK2(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) = VAR_2 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK2(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK9(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK2(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK9(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK9(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK9(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK9(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK9(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK2(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) = VAR_2 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK2(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK9(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK2(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK9(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK9(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK8(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK9(VAR_1,VAR_2,VAR_0)))), inference(cnf_transformation, [status(thm)], [sk_T-inv_sk])).
% 24.07/4.20 cnf(c_1236, plain, ~vtcheck(A,B,C) | vlookup(sK0(B,C,A),A) = vsomeType(C) | vabs(sK1(B,C,A),sK2(B,C,A),sK3(B,C,A)) = B | vapp(sK4(B,C,A),sK5(B,C,A)) = B, inference(split_conjunct, [status(thm)], [sk_T-inv])).
% 24.07/4.20 fof(nnf_57, plain, ? [VT,Vx] : (vtcheck(vempty,vvar(Vx),VT) & ~ (visValue(vvar(Vx))) & ! [Veout] : ~ (vreduce(vvar(Vx)) = vsomeExp(Veout))), inference(fof_nnf, [status(thm)], [T-Progress-T-var_neg])).
% 24.07/4.20 fof(sk_T-Progress-T-var_neg, plain, (vtcheck(vempty,vvar(sK6),sK7) & ~ (visValue(vvar(sK6))) & ! [Veout] : ~ (vreduce(vvar(sK6)) = vsomeExp(Veout))), inference(skolemize, [status(esa), new_symbols(skolem, [sK6,sK7]), skolemize(VT,sK7), skolemize(Vx,sK6)], [nnf_57])).
% 24.07/4.20 cnf(c_1247, negated_conjecture, vtcheck(vempty,vvar(sK6),sK7), inference(split_conjunct, [status(thm)], [sk_T-Progress-T-var_neg])).
% 24.07/4.20 cnf(c_1359, plain, A != B | C != vempty | vlookup(B,C) != D | D = vnoType, inference(clausify, [status(thm)], [lookup0])).
% 24.07/4.20 cnf(c_6731, plain, A != B | vempty != C | vlookup(B,C) != D | D = vnoType,
% 24.07/4.20 inference(copy, [status(thm)], [c_1359])).
% 24.07/4.20 cnf(c_6732, plain, A != B | vempty != C | vlookup(B,C) != D | vnoType = D,
% 24.07/4.20 inference(copy, [status(thm)], [c_6731])).
% 24.07/4.20 cnf(c_1360, plain, vempty != A | vlookup(B,A) != C | vnoType = C,
% 24.07/4.20 inference(copy, [status(thm)], [c_6732])).
% 24.07/4.20 cnf(c_1362, plain, vsomeType(A) != vnoType, inference(clausify, [status(thm)], [DIFF-noType-someType])).
% 24.07/4.20 cnf(c_1382, plain, vapp(A,B) != vvar(C), inference(clausify, [status(thm)], [DIFF-var-app])).
% 24.07/4.20 cnf(c_1383, plain, vabs(A,B,C) != vvar(D), inference(clausify, [status(thm)], [DIFF-var-abs])).
% 24.07/4.20 cnf(c_6733, negated_conjecture, vlookup(sK0(vvar(sK6),sK7,vempty),vempty) = vsomeType(sK7) | vabs(sK1(vvar(sK6),sK7,vempty),sK2(vvar(sK6),sK7,vempty),sK3(vvar(sK6),sK7,vempty)) = vvar(sK6) | vapp(sK4(vvar(sK6),sK7,vempty),sK5(vvar(sK6),sK7,vempty)) = vvar(sK6),
% 24.07/4.20 inference(resolve, [status(thm)], [c_1247, c_1236])).
% 24.07/4.20 cnf(c_6734, negated_conjecture, vlookup(sK0(vvar(sK6),sK7,vempty),vempty) = vsomeType(sK7) | vapp(sK4(vvar(sK6),sK7,vempty),sK5(vvar(sK6),sK7,vempty)) = vvar(sK6),
% 24.07/4.20 inference(resolve, [status(thm)], [c_1383, c_6733])).
% 24.07/4.20 cnf(c_5912, negated_conjecture, vlookup(sK0(vvar(sK6),sK7,vempty),vempty) = vsomeType(sK7),
% 24.07/4.20 inference(resolve, [status(thm)], [c_1382, c_6734])).
% 24.07/4.20 cnf(c_6735, plain, vlookup(A,vempty) != B | vnoType = B,
% 24.07/4.20 inference(xxres, [status(thm)], [c_1360])).
% 24.07/4.20 cnf(c_6736, plain, vnoType = vlookup(A,vempty),
% 24.07/4.20 inference(xxres, [status(thm)], [c_6735])).
% 24.07/4.20 cnf(c_6729, plain, vlookup(A,vempty) = vnoType,
% 24.07/4.20 inference(copy, [status(thm)], [c_6736])).
% 24.07/4.20 cnf(c_6737, negated_conjecture, vnoType = vsomeType(sK7),
% 24.07/4.20 inference(paramod, [status(thm)], [c_6729, c_5912])).
% 24.07/4.20 cnf(c_6738, negated_conjecture, vsomeType(sK7) = vnoType,
% 24.07/4.20 inference(copy, [status(thm)], [c_6737])).
% 24.07/4.20 cnf(c_6730, negated_conjecture, $false,
% 24.07/4.20 inference(resolve, [status(thm)], [c_1362, c_6738])).
% 24.07/4.20 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------