%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM146+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 : n019.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 22.01s 3.77s
% Output : CNFRefutation 22.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM146+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.10/0.59 % Computer : n019.cluster.edu
% 0.10/0.59 % Model : x86_64 x86_64
% 0.10/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.59 % Memory : 8046.5625MB
% 0.10/0.59 % OS : Linux 6.8.0-71-generic
% 0.10/0.59 % CPULimit : 300
% 0.10/0.59 % WCLimit : 300
% 0.10/0.59 % DateTime : Sat Sep 26 23:35:06 UTC 2026
% 0.10/0.59 % CPUTime :
% 0.10/0.59 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.59 % Process 2498668 was started by sandbox2 on n019,
% 0.10/0.59 % Sat Sep 26 23:35:06 2026
% 0.10/0.59 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.89
% 0.15/0.89 % From the command line: assign(max_seconds, 300).
% 22.01/3.77
% 22.01/3.77 % SZS status Theorem for theBenchmark
% 22.01/3.77
% 22.01/3.77 % Proof 1 at 2.63 (+ 0.10) seconds.
% 22.01/3.77 % Length of proof is 8.
% 22.01/3.77 % Level of proof is 3.
% 22.01/3.77 % Maximum clause weight is 21.000.
% 22.01/3.77 % Given clauses 448.
% 22.01/3.77
% 22.01/3.77 % SZS output start CNFRefutation for theBenchmark
% 22.01/3.77 fof(DIFF-noExp-someExp, axiom, ! [VExp0] : ~ (vnoExp = vsomeExp(VExp0)), file('theBenchmark.p',DIFF-noExp-someExp)).
% 22.01/3.77 fof(reduce0, axiom, ! [Vx,VExp0,RESULT] : (VExp0 = vvar(Vx) => (RESULT = vreduce(VExp0) => RESULT = vnoExp)), file('theBenchmark.p',reduce0)).
% 22.01/3.77 fof(T-Preservation-T-var, conjecture, ! [Vx,VC,Veout,VT] : ((vreduce(vvar(Vx)) = vsomeExp(Veout) & vtcheck(VC,vvar(Vx),VT)) => vtcheck(VC,Veout,VT)), file('theBenchmark.p',T-Preservation-T-var)).
% 22.01/3.77 fof(T-Preservation-T-var_neg, negated_conjecture, ~(! [Vx,VC,Veout,VT] : ((vreduce(vvar(Vx)) = vsomeExp(Veout) & vtcheck(VC,vvar(Vx),VT)) => vtcheck(VC,Veout,VT))), inference(assume_negation, [status(cth)], [T-Preservation-T-var])).
% 22.01/3.77 cnf(c_651, plain, vsomeExp(A) != vnoExp, inference(clausify, [status(thm)], [DIFF-noExp-someExp])).
% 22.01/3.77 cnf(c_656, plain, vvar(A) != B | vreduce(B) != C | vnoExp = C, inference(clausify, [status(thm)], [reduce0])).
% 22.01/3.77 fof(nnf_59, plain, ? [Vx,VC,Veout,VT] : (vreduce(vvar(Vx)) = vsomeExp(Veout) & vtcheck(VC,vvar(Vx),VT) & ~ (vtcheck(VC,Veout,VT))), inference(fof_nnf, [status(thm)], [T-Preservation-T-var_neg])).
% 22.01/3.77 fof(sk_T-Preservation-T-var_neg, plain, (vreduce(vvar(sK0)) = vsomeExp(sK1) & vtcheck(sK2,vvar(sK0),sK3) & ~ (vtcheck(sK2,sK1,sK3))), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3]), skolemize(Vx,sK0), skolemize(VC,sK2), skolemize(Veout,sK1), skolemize(VT,sK3)], [nnf_59])).
% 22.01/3.77 cnf(c_837, negated_conjecture, vreduce(vvar(sK0)) = vsomeExp(sK1), inference(split_conjunct, [status(thm)], [sk_T-Preservation-T-var_neg])).
% 22.01/3.77 cnf(c_838, negated_conjecture, vsomeExp(sK1) = vreduce(vvar(sK0)),
% 22.01/3.77 inference(copy, [status(thm)], [c_837])).
% 22.01/3.77 cnf(c_4192, plain, vvar(A) != B | C != vreduce(B) | vnoExp = C,
% 22.01/3.77 inference(copy, [status(thm)], [c_656])).
% 22.01/3.77 cnf(c_4193, negated_conjecture, vvar(A) != vvar(sK0) | vnoExp = vsomeExp(sK1),
% 22.01/3.77 inference(resolve, [status(thm)], [c_838, c_4192])).
% 22.01/3.77 cnf(c_4194, negated_conjecture, vvar(sK0) != vvar(A) | vnoExp = vsomeExp(sK1),
% 22.01/3.77 inference(copy, [status(thm)], [c_4193])).
% 22.01/3.77 cnf(c_4195, negated_conjecture, vvar(sK0) != vvar(A) | vsomeExp(sK1) = vnoExp,
% 22.01/3.77 inference(copy, [status(thm)], [c_4194])).
% 22.01/3.77 cnf(c_4196, negated_conjecture, vsomeExp(sK1) = vnoExp,
% 22.01/3.77 inference(copy, [status(thm)], [c_4195])).
% 22.01/3.77 cnf(c_4191, negated_conjecture, $false,
% 22.01/3.77 inference(resolve, [status(thm)], [c_651, c_4196])).
% 22.01/3.77 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------