%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW350+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:08 AM UTC 2026
% Result : Theorem 13.23s 17.40s
% Output : CNFRefutation 13.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 88 ( 55 unt; 0 def)
% Number of atoms : 135 ( 71 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 84 ( 37 ~; 32 |; 4 &)
% ( 6 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 145 ( 33 sgn 52 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_ext,axiom,
! [V_g_2,V_f_2] :
( ! [B_x] : hAPP(V_f_2,B_x) = hAPP(V_g_2,B_x)
=> V_f_2 = V_g_2 ),
file('theBenchmark.p',fact_ext) ).
fof(fact_diff__Suc__Suc,axiom,
! [V_n,V_m] : hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,V_m)),hAPP(c_Nat_OSuc,V_n)) = hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),V_m),V_n),
file('theBenchmark.p',fact_diff__Suc__Suc) ).
fof(fact_Suc__eq__plus1__left,axiom,
! [V_n] : hAPP(c_Nat_OSuc,V_n) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),V_n),
file('theBenchmark.p',fact_Suc__eq__plus1__left) ).
fof(fact_diff__Suc__1,axiom,
! [V_n] : hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,V_n)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = V_n,
file('theBenchmark.p',fact_diff__Suc__1) ).
fof(fact_zero__less__Suc,axiom,
! [V_n] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,V_n))),
file('theBenchmark.p',fact_zero__less__Suc) ).
fof(fact_Suc__lessI,axiom,
! [V_n,V_m] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_m),V_n))
=> ( hAPP(c_Nat_OSuc,V_m) != V_n
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(c_Nat_OSuc,V_m)),V_n)) ) ),
file('theBenchmark.p',fact_Suc__lessI) ).
fof(fact_not__add__less1,axiom,
! [V_j,V_i] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_i),V_j)),V_i)),
file('theBenchmark.p',fact_not__add__less1) ).
fof(fact_gr0__conv__Suc,axiom,
! [V_n_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n_2))
<=> ? [B_m] : V_n_2 = hAPP(c_Nat_OSuc,B_m) ),
file('theBenchmark.p',fact_gr0__conv__Suc) ).
fof(fact_add__gr__0,axiom,
! [V_n_2,V_m_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_m_2),V_n_2)))
<=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n_2))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_m_2)) ) ),
file('theBenchmark.p',fact_add__gr__0) ).
fof(fact_less__add__Suc2,axiom,
! [V_m,V_i] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_i),hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_m),V_i)))),
file('theBenchmark.p',fact_less__add__Suc2) ).
fof(fact_le__0__eq,axiom,
! [V_n_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),V_n_2),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))
<=> V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('theBenchmark.p',fact_le__0__eq) ).
fof(fact_Suc__le__mono,axiom,
! [V_m_2,V_n_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Nat_OSuc,V_n_2)),hAPP(c_Nat_OSuc,V_m_2)))
<=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),V_n_2),V_m_2)) ),
file('theBenchmark.p',fact_Suc__le__mono) ).
fof(fact_nat__less__le,axiom,
! [V_n_2,V_m_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_m_2),V_n_2))
<=> ( V_m_2 != V_n_2
& hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),V_m_2),V_n_2)) ) ),
file('theBenchmark.p',fact_nat__less__le) ).
fof(fact_le__add1,axiom,
! [V_m,V_n] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),V_n),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_n),V_m))),
file('theBenchmark.p',fact_le__add1) ).
fof(fact_le__less__Suc__eq,axiom,
! [V_n_2,V_m_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),V_m_2),V_n_2))
=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_n_2),hAPP(c_Nat_OSuc,V_m_2)))
<=> V_n_2 = V_m_2 ) ),
file('theBenchmark.p',fact_le__less__Suc__eq) ).
fof(fact_le__add__diff__inverse,axiom,
! [V_m,V_n] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),V_n),V_m))
=> hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_n),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),V_m),V_n)) = V_m ),
file('theBenchmark.p',fact_le__add__diff__inverse) ).
fof(fact_less__eq__Suc__le__raw,axiom,
! [V_n_2] : hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_n_2) = hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Nat_OSuc,V_n_2)),
file('theBenchmark.p',fact_less__eq__Suc__le__raw) ).
fof(help_c__COMBB__1,axiom,
! [V_R_2,V_Q_2,V_P_2,T_c,T_a,T_b] : hAPP(hAPP(hAPP(c_COMBB(T_b,T_a,T_c),V_P_2),V_Q_2),V_R_2) = hAPP(V_P_2,hAPP(V_Q_2,V_R_2)),
file('theBenchmark.p',help_c__COMBB__1) ).
fof(help_c__COMBS__1,axiom,
! [V_R_2,V_Q_2,V_P_2,T_a,T_c,T_b] : hAPP(hAPP(hAPP(c_COMBS(T_b,T_c,T_a),V_P_2),V_Q_2),V_R_2) = hAPP(hAPP(V_P_2,V_R_2),hAPP(V_Q_2,V_R_2)),
file('theBenchmark.p',help_c__COMBS__1) ).
fof(fact_bot__nat__def,axiom,
c_Orderings_Obot__class_Obot(tc_Nat_Onat) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('theBenchmark.p',fact_bot__nat__def) ).
cnf(c_878,plain,
c_Orderings_Obot__class_Obot(tc_Nat_Onat) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(clausify,[status(thm)],[fact_bot__nat__def]) ).
cnf(c_1033,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),hAPP(c_Nat_OSuc,B)) = hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),B),
inference(clausify,[status(thm)],[fact_diff__Suc__Suc]) ).
cnf(c_1097,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),A) = hAPP(c_Nat_OSuc,A),
inference(clausify,[status(thm)],[fact_Suc__eq__plus1__left]) ).
cnf(c_1099,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = A,
inference(clausify,[status(thm)],[fact_diff__Suc__1]) ).
cnf(c_1115,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,A))),
inference(clausify,[status(thm)],[fact_zero__less__Suc]) ).
cnf(c_1203,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),B))
| hAPP(c_Nat_OSuc,A) = B
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_Suc__lessI]) ).
cnf(c_1221,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B)),A)),
inference(clausify,[status(thm)],[fact_not__add__less1]) ).
fof(nnf_426,plain,
! [V_n_2] :
( ( ! [B_m] : hAPP(c_Nat_OSuc,B_m) != V_n_2
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n_2)) )
& ( ? [X0] : hAPP(c_Nat_OSuc,X0) = V_n_2
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n_2)) ) ),
inference(fof_nnf,[status(thm)],[fact_gr0__conv__Suc]) ).
fof(sk_fact_gr0__conv__Suc_sk,plain,
! [V_n_2] :
( ( ! [B_m] : hAPP(c_Nat_OSuc,B_m) != V_n_2
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n_2)) )
& ( hAPP(c_Nat_OSuc,sK0(V_n_2)) = V_n_2
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n_2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0(V_n_2))],[nnf_426]) ).
fof(sk_fact_gr0__conv__Suc,plain,
( ! [VAR_0,VAR_1] :
( hAPP(c_Nat_OSuc,VAR_1) != VAR_0
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),VAR_0)) )
& ! [VAR_0] :
( hAPP(c_Nat_OSuc,sK0(VAR_0)) = VAR_0
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),VAR_0)) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_gr0__conv__Suc_sk]) ).
cnf(c_1263,plain,
( hAPP(c_Nat_OSuc,sK0(A)) = A
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),A)) ),
inference(split_conjunct,[status(thm)],[sk_fact_gr0__conv__Suc]) ).
cnf(c_1271,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),B))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),A))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B))) ),
inference(clausify,[status(thm)],[fact_add__gr__0]) ).
cnf(c_1275,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),A)))),
inference(clausify,[status(thm)],[fact_less__add__Suc2]) ).
cnf(c_1351,plain,
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = A
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),A),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) ),
inference(clausify,[status(thm)],[fact_le__0__eq]) ).
cnf(c_1360,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),A),B))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),hAPP(c_Nat_OSuc,B))) ),
inference(clausify,[status(thm)],[fact_Suc__le__mono]) ).
cnf(c_1374,plain,
( A != B
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_nat__less__le]) ).
cnf(c_1388,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B))),
inference(clausify,[status(thm)],[fact_le__add1]) ).
cnf(c_1408,plain,
( A != B
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B),hAPP(c_Nat_OSuc,A)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_le__less__Suc__eq]) ).
cnf(c_1433,plain,
( hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),B),A)) = B
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_le__add__diff__inverse]) ).
cnf(c_1438,plain,
hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)) = hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),
inference(clausify,[status(thm)],[fact_less__eq__Suc__le__raw]) ).
cnf(c_1803,plain,
hAPP(hAPP(hAPP(c_COMBB(A,B,C),D),E),F) = hAPP(D,hAPP(E,F)),
inference(clausify,[status(thm)],[help_c__COMBB__1]) ).
cnf(c_1804,plain,
hAPP(hAPP(hAPP(c_COMBS(A,B,C),D),E),F) = hAPP(hAPP(D,F),hAPP(E,F)),
inference(clausify,[status(thm)],[help_c__COMBS__1]) ).
fof(nnf_1,plain,
! [V_g_2,V_f_2] :
( V_g_2 = V_f_2
| ? [B_x] : hAPP(V_g_2,B_x) != hAPP(V_f_2,B_x) ),
inference(fof_nnf,[status(thm)],[fact_ext]) ).
fof(sk_fact_ext,plain,
! [V_g_2,V_f_2] :
( V_g_2 = V_f_2
| hAPP(V_g_2,sK1(V_g_2,V_f_2)) != hAPP(V_f_2,sK1(V_g_2,V_f_2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(B_x,sK1(V_g_2,V_f_2))],[nnf_1]) ).
cnf(c_1805,plain,
( A = B
| hAPP(A,sK1(A,B)) != hAPP(B,sK1(A,B)) ),
inference(split_conjunct,[status(thm)],[sk_fact_ext]) ).
cnf(c_1806,plain,
( B = A
| hAPP(A,sK1(B,A)) != hAPP(B,sK1(B,A)) ),
inference(copy,[status(thm)],[c_1805]) ).
cnf(c_4811,plain,
c_Nat_OSuc = hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_1806,c_1097]) ).
cnf(c_1974,plain,
hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Nat_OSuc,
inference(copy,[status(thm)],[c_4811]) ).
cnf(c_2110,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),c_Groups_Oone__class_Oone(tc_Nat_Onat))),
inference(paramod,[status(thm)],[c_1974,c_1221]) ).
cnf(c_4812,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),A))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,A))) ),
inference(paramod,[status(thm)],[c_1974,c_1271]) ).
cnf(c_2114,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),A))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),c_Groups_Oone__class_Oone(tc_Nat_Onat))) ),
inference(resolve,[status(thm)],[c_1115,c_4812]) ).
cnf(c_2116,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)))),
inference(paramod,[status(thm)],[c_1974,c_1275]) ).
cnf(c_2121,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),hAPP(c_Nat_OSuc,A))),
inference(paramod,[status(thm)],[c_1974,c_1388]) ).
cnf(c_2147,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),c_Groups_Oone__class_Oone(tc_Nat_Onat))),
inference(factor,[status(thm)],[c_2114]) ).
cnf(c_2275,plain,
hAPP(c_Nat_OSuc,sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
inference(resolve,[status(thm)],[c_2147,c_1263]) ).
cnf(c_2324,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))),
inference(paramod,[status(thm)],[c_2275,c_1033]) ).
cnf(c_4813,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))),A))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),hAPP(c_Nat_OSuc,A))) ),
inference(paramod,[status(thm)],[c_2275,c_1360]) ).
cnf(c_2347,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))),A)),
inference(resolve,[status(thm)],[c_2121,c_4813]) ).
cnf(c_4814,plain,
hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))),
inference(paramod,[status(thm)],[c_2275,c_1438]) ).
cnf(c_2353,plain,
hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))) = hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(copy,[status(thm)],[c_4814]) ).
cnf(c_2386,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))) = A,
inference(paramod,[status(thm)],[c_2324,c_1099]) ).
cnf(c_2392,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = A,
inference(paramod,[status(thm)],[c_2386,c_2324]) ).
cnf(c_4815,plain,
( sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)) != A
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),hAPP(c_Nat_OSuc,sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat))))) ),
inference(resolve,[status(thm)],[c_2347,c_1408]) ).
cnf(c_2405,plain,
( sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)) != A
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),c_Groups_Oone__class_Oone(tc_Nat_Onat))) ),
inference(paramod,[status(thm)],[c_2275,c_4815]) ).
cnf(c_4816,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_2347,c_1351]) ).
cnf(c_2411,plain,
sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(copy,[status(thm)],[c_4816]) ).
cnf(c_2430,plain,
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != A
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),c_Groups_Oone__class_Oone(tc_Nat_Onat))) ),
inference(paramod,[status(thm)],[c_2411,c_2405]) ).
cnf(c_4817,plain,
hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_2411,c_2353]) ).
cnf(c_2450,plain,
hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(copy,[status(thm)],[c_4817]) ).
cnf(c_4818,plain,
A != hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)),
inference(resolve,[status(thm)],[c_2116,c_1374]) ).
cnf(c_3424,plain,
hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)) != A,
inference(copy,[status(thm)],[c_4818]) ).
cnf(c_3531,plain,
hAPP(hAPP(hAPP(c_COMBB(A,B,C),c_Nat_OSuc),c_Nat_OSuc),D) != D,
inference(paramod,[status(thm)],[c_1803,c_3424]) ).
cnf(c_3562,plain,
hAPP(hAPP(hAPP(c_COMBB(A,B,C),hAPP(hAPP(c_COMBB(D,E,F),c_Nat_OSuc),c_Nat_OSuc)),V6),V7) != hAPP(V6,V7),
inference(paramod,[status(thm)],[c_1803,c_3531]) ).
cnf(c_4819,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Orderings_Obot__class_Obot(tc_Nat_Onat),
inference(copy,[status(thm)],[c_878]) ).
cnf(c_4574,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),c_Groups_Oone__class_Oone(tc_Nat_Onat))),
inference(resolve,[status(thm)],[c_2430,c_4819]) ).
cnf(c_4820,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(c_Nat_OSuc,c_Orderings_Obot__class_Obot(tc_Nat_Onat))),c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| hAPP(c_Nat_OSuc,c_Orderings_Obot__class_Obot(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(tc_Nat_Onat) ),
inference(resolve,[status(thm)],[c_4574,c_1203]) ).
cnf(c_4635,plain,
hAPP(c_Nat_OSuc,c_Orderings_Obot__class_Obot(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
inference(resolve,[status(thm)],[c_2110,c_4820]) ).
cnf(c_4821,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_4635,c_1033]) ).
cnf(c_4822,plain,
A = hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_2392,c_4821]) ).
cnf(c_4654,plain,
hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat)) = A,
inference(copy,[status(thm)],[c_4822]) ).
cnf(c_4823,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),A))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),hAPP(c_Nat_OSuc,A))) ),
inference(paramod,[status(thm)],[c_4635,c_1360]) ).
cnf(c_4824,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),A))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,A))) ),
inference(paramod,[status(thm)],[c_2450,c_4823]) ).
cnf(c_4668,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),A)),
inference(resolve,[status(thm)],[c_1115,c_4824]) ).
cnf(c_4825,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat))) = A,
inference(resolve,[status(thm)],[c_4668,c_1433]) ).
cnf(c_4699,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),A) = A,
inference(paramod,[status(thm)],[c_4654,c_4825]) ).
cnf(c_4809,plain,
hAPP(hAPP(hAPP(c_COMBS(A,B,C),D),hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat))),E) = hAPP(hAPP(D,E),E),
inference(paramod,[status(thm)],[c_4699,c_1804]) ).
cnf(c_4826,plain,
hAPP(V6,V7) != hAPP(hAPP(hAPP(c_COMBB(A,B,C),hAPP(hAPP(c_COMBB(D,E,F),c_Nat_OSuc),c_Nat_OSuc)),V6),V7),
inference(copy,[status(thm)],[c_3562]) ).
cnf(c_4810,plain,
$false,
inference(resolve,[status(thm)],[c_4809,c_4826]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW350+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/15.40 % Computer : n008.cluster.edu
% 0.12/15.40 % Model : x86_64 x86_64
% 0.12/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/15.40 % Memory : 8046.5625MB
% 0.12/15.40 % OS : Linux 6.8.0-71-generic
% 0.16/15.40 % CPULimit : 300
% 0.16/15.40 % WCLimit : 300
% 0.16/15.40 % DateTime : Sat Sep 26 15:43:40 UTC 2026
% 0.16/15.40 % CPUTime :
% 0.16/15.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/15.40 % Process 3990093 was started by sandbox2 on n008,
% 0.16/15.40 % Sat Sep 26 15:43:40 2026
% 0.16/15.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 13.23/17.40
% 13.23/17.40 % SInE (scan): 590 to sos (tol 1.5x), 195 to usable (tol 2.0x), 4443 zapped, of 5228 axioms (depth 3).
% 13.23/17.40
% 13.23/17.40 % From the command line: assign(max_seconds, 300).
% 13.23/17.40
% 13.23/17.40 % SZS status Theorem for theBenchmark
% 13.23/17.40
% 13.23/17.40 % Proof 1 at 1.44 (+ 0.33) seconds.
% 13.23/17.40 % Length of proof is 66.
% 13.23/17.40 % Level of proof is 15.
% 13.23/17.40 % Maximum clause weight is 21.000.
% 13.23/17.40 % Given clauses 161.
% 13.23/17.40
% 13.23/17.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------