%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM144+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 21.94s 3.55s
% Output : CNFRefutation 21.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM144+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n004.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 26 23:35:07 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 2899860 was started by sandbox on n004,
% 0.08/0.35 % Sat Sep 26 23:35:07 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.40/0.65
% 0.40/0.65 % From the command line: assign(max_seconds, 300).
% 21.94/3.55
% 21.94/3.55 % given #500 (I,wt=80): 1023 vreduce(A) != B | vvar(f42(A,B)) = A | vabs(f43(A,B),f44(A,B),f45(A,B)) = A | vreduce(f46(A,B)) = f50(A,B) | defn_20(A,B) | defn_30(A,B) | vsomeExp(vapp(vgetSomeExp(f62(A,B)),f63(A,B))) = B | f65(A,B) != vabs(C,D,E). [copy(1022),flip(h)].
% 21.94/3.55
% 21.94/3.55 % SZS status Theorem for theBenchmark
% 21.94/3.55
% 21.94/3.55 % Proof 1 at 2.38 (+ 0.07) seconds.
% 21.94/3.55 % Length of proof is 7.
% 21.94/3.55 % Level of proof is 2.
% 21.94/3.55 % Maximum clause weight is 23.000.
% 21.94/3.55 % Given clauses 602.
% 21.94/3.55
% 21.94/3.55 % SZS output start CNFRefutation for theBenchmark
% 21.94/3.55 fof(DIFF-noExp-someExp, axiom, ! [VExp0] : ~ (vnoExp = vsomeExp(VExp0)), file('theBenchmark.p',DIFF-noExp-someExp)).
% 21.94/3.55 fof(reduce1, axiom, ! [Vx,VS,Ve,VExp0,RESULT] : (VExp0 = vabs(Vx,VS,Ve) => (RESULT = vreduce(VExp0) => RESULT = vnoExp)), file('theBenchmark.p',reduce1)).
% 21.94/3.55 fof(T-Preservation-T-abs, conjecture, ! [Vx,VS,VC,Veout,VT] : ((vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) & vtcheck(VC,vabs(Vx,VS,ve1),VT)) => vtcheck(VC,Veout,VT)), file('theBenchmark.p',T-Preservation-T-abs)).
% 21.94/3.55 fof(T-Preservation-T-abs_neg, negated_conjecture, ~(! [Vx,VS,VC,Veout,VT] : ((vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) & vtcheck(VC,vabs(Vx,VS,ve1),VT)) => vtcheck(VC,Veout,VT))), inference(assume_negation, [status(cth)], [T-Preservation-T-abs])).
% 21.94/3.55 cnf(c_958, plain, vsomeExp(A) != vnoExp, inference(clausify, [status(thm)], [DIFF-noExp-someExp])).
% 21.94/3.55 cnf(c_964, plain, vabs(A,B,C) != D | vreduce(D) != E | vnoExp = E, inference(clausify, [status(thm)], [reduce1])).
% 21.94/3.55 fof(nnf_60, plain, ? [Vx,VS,VC,Veout,VT] : (vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) & vtcheck(VC,vabs(Vx,VS,ve1),VT) & ~ (vtcheck(VC,Veout,VT))), inference(fof_nnf, [status(thm)], [T-Preservation-T-abs_neg])).
% 21.94/3.55 fof(sk_T-Preservation-T-abs_neg, plain, (vreduce(vabs(sK0,sK1,ve1)) = vsomeExp(sK2) & vtcheck(sK3,vabs(sK0,sK1,ve1),sK4) & ~ (vtcheck(sK3,sK2,sK4))), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3,sK4]), skolemize(Vx,sK0), skolemize(VS,sK1), skolemize(VC,sK3), skolemize(Veout,sK2), skolemize(VT,sK4)], [nnf_60])).
% 21.94/3.55 cnf(c_1146, negated_conjecture, vreduce(vabs(sK0,sK1,ve1)) = vsomeExp(sK2), inference(split_conjunct, [status(thm)], [sk_T-Preservation-T-abs_neg])).
% 21.94/3.55 cnf(c_5491, negated_conjecture, vabs(A,B,C) != vabs(sK0,sK1,ve1) | vnoExp = vsomeExp(sK2),
% 21.94/3.55 inference(resolve, [status(thm)], [c_1146, c_964])).
% 21.94/3.55 cnf(c_5492, negated_conjecture, vabs(sK0,sK1,ve1) != vabs(A,B,C) | vnoExp = vsomeExp(sK2),
% 21.94/3.55 inference(copy, [status(thm)], [c_5491])).
% 21.94/3.55 cnf(c_5493, negated_conjecture, vabs(sK0,sK1,ve1) != vabs(A,B,C) | vsomeExp(sK2) = vnoExp,
% 21.94/3.55 inference(copy, [status(thm)], [c_5492])).
% 21.94/3.55 cnf(c_5494, negated_conjecture, vsomeExp(sK2) = vnoExp,
% 21.94/3.55 inference(copy, [status(thm)], [c_5493])).
% 21.94/3.55 cnf(c_5490, negated_conjecture, $false,
% 21.94/3.55 inference(resolve, [status(thm)], [c_958, c_5494])).
% 21.94/3.55 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------