%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW297+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 09:14:03 AM UTC 2026
% Result : Theorem 14.48s 2.78s
% Output : CNFRefutation 14.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 2
% Syntax : Number of formulae : 15 ( 6 unt; 0 def)
% Number of atoms : 45 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 45 ( 15 ~; 10 |; 9 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 36 ( 0 sgn 25 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_evaln__Suc,axiom,
! [V_s_H,V_n,V_s,V_c] :
( c_Natural_Oevaln(V_c,V_s,V_n,V_s_H)
=> c_Natural_Oevaln(V_c,V_s,hAPP(c_Nat_OSuc,V_n),V_s_H) ),
file('theBenchmark.p',fact_evaln__Suc) ).
fof(conj_0,conjecture,
( ! [B_Z,B_s] :
( v_fun1(B_Z,B_s)
=> ! [B_s_H] :
( c_Natural_Oevaln(v_com,B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)
=> v_fun2(B_Z,B_s_H) ) )
=> ! [B_Z,B_s] :
( v_fun1(B_Z,B_s)
=> ! [B_s_H] :
( c_Natural_Oevaln(v_com,B_s,v_n,B_s_H)
=> v_fun2(B_Z,B_s_H) ) ) ),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ( ! [B_Z,B_s] :
( v_fun1(B_Z,B_s)
=> ! [B_s_H] :
( c_Natural_Oevaln(v_com,B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)
=> v_fun2(B_Z,B_s_H) ) )
=> ! [B_Z,B_s] :
( v_fun1(B_Z,B_s)
=> ! [B_s_H] :
( c_Natural_Oevaln(v_com,B_s,v_n,B_s_H)
=> v_fun2(B_Z,B_s_H) ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_2861,plain,
( c_Natural_Oevaln(A,B,hAPP(c_Nat_OSuc,C),D)
| ~ c_Natural_Oevaln(A,B,C,D) ),
inference(clausify,[status(thm)],[fact_evaln__Suc]) ).
fof(nnf_1373,plain,
( ? [B_Z,B_s] :
( ? [B_s_H] :
( ~ v_fun2(B_Z,B_s_H)
& c_Natural_Oevaln(v_com,B_s,v_n,B_s_H) )
& v_fun1(B_Z,B_s) )
& ! [X0,X1] :
( ! [X2] :
( v_fun2(X0,X2)
| ~ c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2) )
| ~ v_fun1(X0,X1) ) ),
inference(fof_nnf,[status(thm)],[conj_0_neg]) ).
fof(sk_conj_0_neg_sk,plain,
( ~ v_fun2(sK0,sK2)
& c_Natural_Oevaln(v_com,sK1,v_n,sK2)
& v_fun1(sK0,sK1)
& ! [X0,X1] :
( ! [X2] :
( v_fun2(X0,X2)
| ~ c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2) )
| ~ v_fun1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(B_Z,sK0),skolemize(B_s,sK1),skolemize(B_s_H,sK2)],[nnf_1373]) ).
fof(sk_conj_0_neg,plain,
( ~ v_fun2(sK0,sK2)
& c_Natural_Oevaln(v_com,sK1,v_n,sK2)
& v_fun1(sK0,sK1)
& ! [VAR_0,VAR_1,VAR_2] :
( v_fun2(VAR_0,VAR_2)
| ~ c_Natural_Oevaln(v_com,VAR_1,hAPP(c_Nat_OSuc,v_n),VAR_2)
| ~ v_fun1(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_conj_0_neg_sk]) ).
cnf(c_3913,negated_conjecture,
( v_fun2(A,C)
| ~ c_Natural_Oevaln(v_com,B,hAPP(c_Nat_OSuc,v_n),C)
| ~ v_fun1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_conj_0_neg]) ).
cnf(c_3914,negated_conjecture,
v_fun1(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_conj_0_neg]) ).
cnf(c_3915,negated_conjecture,
c_Natural_Oevaln(v_com,sK1,v_n,sK2),
inference(split_conjunct,[status(thm)],[sk_conj_0_neg]) ).
cnf(c_3916,negated_conjecture,
~ v_fun2(sK0,sK2),
inference(split_conjunct,[status(thm)],[sk_conj_0_neg]) ).
cnf(c_4194,plain,
c_Natural_Oevaln(v_com,sK1,hAPP(c_Nat_OSuc,v_n),sK2),
inference(resolve,[status(thm)],[c_2861,c_3915]) ).
cnf(c_4636,plain,
( v_fun2(A,sK2)
| ~ v_fun1(A,sK1) ),
inference(resolve,[status(thm)],[c_3913,c_4194]) ).
cnf(c_4638,negated_conjecture,
v_fun2(sK0,sK2),
inference(resolve,[status(thm)],[c_4636,c_3914]) ).
cnf(c_4637,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3916,c_4638]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW297+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n020.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Sat Sep 26 15:37:33 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.46 % Process 1913208 was started by sandbox on n020,
% 0.18/0.46 % Sat Sep 26 15:37:33 2026
% 0.18/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 14.48/2.78
% 14.48/2.78 % SInE (scan): 1166 to sos (tol 1.5x), 264 to usable (tol 2.0x), 3794 zapped, of 5224 axioms (depth 3).
% 14.48/2.78
% 14.48/2.78 % From the command line: assign(max_seconds, 300).
% 14.48/2.78
% 14.48/2.78 % SZS status Theorem for theBenchmark
% 14.48/2.78
% 14.48/2.78 % Proof 1 at 1.34 (+ 0.40) seconds.
% 14.48/2.78 % Length of proof is 10.
% 14.48/2.78 % Level of proof is 4.
% 14.48/2.78 % Maximum clause weight is 23.000.
% 14.48/2.78 % Given clauses 73.
% 14.48/2.78
% 14.48/2.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------