%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW348+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 : n001.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:07 AM UTC 2026
% Result : Theorem 6.95s 1.51s
% Output : CNFRefutation 6.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 20
% Syntax : Number of formulae : 83 ( 49 unt; 0 def)
% Number of atoms : 133 ( 65 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 89 ( 39 ~; 33 |; 4 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 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 : 148 ( 33 sgn 54 !; 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_less__trans__Suc,axiom,
! [V_k,V_j,V_i] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_i),V_j))
=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_j),V_k))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(c_Nat_OSuc,V_i)),V_k)) ) ),
file('theBenchmark.p',fact_less__trans__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_add__diff__inverse,axiom,
! [V_n,V_m] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_m),V_n))
=> 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_add__diff__inverse) ).
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(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_876,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_1031,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_1095,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_1097,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_1113,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_1200,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(c_Nat_OSuc,A)),C))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B),C))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_less__trans__Suc]) ).
cnf(c_1201,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_1219,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_424,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_424]) ).
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_1261,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_1269,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_1273,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_1283,plain,
( hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),B)) = A
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_add__diff__inverse]) ).
cnf(c_1349,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_1358,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_1372,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_1386,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_1406,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_1801,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_1802,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_1803,plain,
( A = B
| hAPP(A,sK1(A,B)) != hAPP(B,sK1(A,B)) ),
inference(split_conjunct,[status(thm)],[sk_fact_ext]) ).
cnf(c_1804,plain,
( B = A
| hAPP(A,sK1(B,A)) != hAPP(B,sK1(B,A)) ),
inference(copy,[status(thm)],[c_1803]) ).
cnf(c_4775,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_1804,c_1095]) ).
cnf(c_1971,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_4775]) ).
cnf(c_2107,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_1971,c_1219]) ).
cnf(c_4776,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_1971,c_1269]) ).
cnf(c_2111,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_1113,c_4776]) ).
cnf(c_2113,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_1971,c_1273]) ).
cnf(c_2118,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_1971,c_1386]) ).
cnf(c_2144,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_2111]) ).
cnf(c_2277,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_2144,c_1261]) ).
cnf(c_2326,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_2277,c_1031]) ).
cnf(c_4777,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_2277,c_1358]) ).
cnf(c_2349,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_2118,c_4777]) ).
cnf(c_2388,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_2326,c_1097]) ).
cnf(c_2394,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_2388,c_2326]) ).
cnf(c_4778,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_2349,c_1406]) ).
cnf(c_2407,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_2277,c_4778]) ).
cnf(c_4779,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_2349,c_1349]) ).
cnf(c_2413,plain,
sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(copy,[status(thm)],[c_4779]) ).
cnf(c_2432,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_2413,c_2407]) ).
cnf(c_4780,plain,
A != hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)),
inference(resolve,[status(thm)],[c_2113,c_1372]) ).
cnf(c_3416,plain,
hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)) != A,
inference(copy,[status(thm)],[c_4780]) ).
cnf(c_3523,plain,
hAPP(hAPP(hAPP(c_COMBB(A,B,C),c_Nat_OSuc),c_Nat_OSuc),D) != D,
inference(paramod,[status(thm)],[c_1801,c_3416]) ).
cnf(c_3554,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_1801,c_3523]) ).
cnf(c_4781,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Orderings_Obot__class_Obot(tc_Nat_Onat),
inference(copy,[status(thm)],[c_876]) ).
cnf(c_4556,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_2432,c_4781]) ).
cnf(c_4782,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_4556,c_1201]) ).
cnf(c_4589,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_2107,c_4782]) ).
cnf(c_4783,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)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat))) ),
inference(resolve,[status(thm)],[c_4556,c_1200]) ).
cnf(c_4590,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat))),
inference(resolve,[status(thm)],[c_2107,c_4783]) ).
cnf(c_4602,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_4590,c_1283]) ).
cnf(c_4784,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_4589,c_1031]) ).
cnf(c_4785,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_2394,c_4784]) ).
cnf(c_4641,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_4785]) ).
cnf(c_4675,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_4641,c_4602]) ).
cnf(c_4773,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_4675,c_1802]) ).
cnf(c_4786,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_3554]) ).
cnf(c_4774,plain,
$false,
inference(resolve,[status(thm)],[c_4773,c_4786]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW348+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.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 15:48:28 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 2128308 was started by sandbox2 on n001,
% 0.12/0.36 % Sat Sep 26 15:48:28 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 6.95/1.51
% 6.95/1.51 % SInE (scan): 588 to sos (tol 1.5x), 195 to usable (tol 2.0x), 4443 zapped, of 5226 axioms (depth 3).
% 6.95/1.51
% 6.95/1.51 % From the command line: assign(max_seconds, 300).
% 6.95/1.51
% 6.95/1.51 % SZS status Theorem for theBenchmark
% 6.95/1.51
% 6.95/1.51 % Proof 1 at 0.77 (+ 0.19) seconds.
% 6.95/1.51 % Length of proof is 65.
% 6.95/1.51 % Level of proof is 15.
% 6.95/1.51 % Maximum clause weight is 21.000.
% 6.95/1.51 % Given clauses 154.
% 6.95/1.51
% 6.95/1.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------