%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW349+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 : n006.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 19.52s 3.43s
% Output : CNFRefutation 19.52s
% 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_877,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_1032,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_1096,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_1098,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_1114,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_1201,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_1202,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_1220,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_425,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_425]) ).
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_1262,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_1270,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_1274,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_1284,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_1350,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_1359,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_1373,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_1387,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_1407,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_1802,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_1803,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_1804,plain,
( A = B
| hAPP(A,sK1(A,B)) != hAPP(B,sK1(A,B)) ),
inference(split_conjunct,[status(thm)],[sk_fact_ext]) ).
cnf(c_1805,plain,
( B = A
| hAPP(A,sK1(B,A)) != hAPP(B,sK1(B,A)) ),
inference(copy,[status(thm)],[c_1804]) ).
cnf(c_4776,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_1805,c_1096]) ).
cnf(c_1972,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_4776]) ).
cnf(c_2108,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_1972,c_1220]) ).
cnf(c_4777,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_1972,c_1270]) ).
cnf(c_2112,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_1114,c_4777]) ).
cnf(c_2114,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_1972,c_1274]) ).
cnf(c_2119,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_1972,c_1387]) ).
cnf(c_2145,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_2112]) ).
cnf(c_2278,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_2145,c_1262]) ).
cnf(c_2327,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_2278,c_1032]) ).
cnf(c_4778,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_2278,c_1359]) ).
cnf(c_2350,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_2119,c_4778]) ).
cnf(c_2389,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_2327,c_1098]) ).
cnf(c_2395,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_2389,c_2327]) ).
cnf(c_4779,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_2350,c_1407]) ).
cnf(c_2408,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_2278,c_4779]) ).
cnf(c_4780,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_2350,c_1350]) ).
cnf(c_2414,plain,
sK0(c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(copy,[status(thm)],[c_4780]) ).
cnf(c_2433,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_2414,c_2408]) ).
cnf(c_4781,plain,
A != hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)),
inference(resolve,[status(thm)],[c_2114,c_1373]) ).
cnf(c_3417,plain,
hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)) != A,
inference(copy,[status(thm)],[c_4781]) ).
cnf(c_3524,plain,
hAPP(hAPP(hAPP(c_COMBB(A,B,C),c_Nat_OSuc),c_Nat_OSuc),D) != D,
inference(paramod,[status(thm)],[c_1802,c_3417]) ).
cnf(c_3555,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_1802,c_3524]) ).
cnf(c_4782,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Orderings_Obot__class_Obot(tc_Nat_Onat),
inference(copy,[status(thm)],[c_877]) ).
cnf(c_4557,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_2433,c_4782]) ).
cnf(c_4783,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_4557,c_1202]) ).
cnf(c_4590,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_2108,c_4783]) ).
cnf(c_4784,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_4557,c_1201]) ).
cnf(c_4591,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_2108,c_4784]) ).
cnf(c_4603,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_4591,c_1284]) ).
cnf(c_4785,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_4590,c_1032]) ).
cnf(c_4786,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_2395,c_4785]) ).
cnf(c_4642,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_4786]) ).
cnf(c_4676,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_4642,c_4603]) ).
cnf(c_4774,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_4676,c_1803]) ).
cnf(c_4787,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_3555]) ).
cnf(c_4775,plain,
$false,
inference(resolve,[status(thm)],[c_4774,c_4787]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW349+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.08 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.46 % Computer : n006.cluster.edu
% 0.21/0.46 % Model : x86_64 x86_64
% 0.21/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.46 % Memory : 8046.5625MB
% 0.21/0.46 % OS : Linux 6.8.0-71-generic
% 0.21/0.46 % CPULimit : 300
% 0.21/0.46 % WCLimit : 300
% 0.21/0.46 % DateTime : Sat Sep 26 15:42:43 UTC 2026
% 0.21/0.47 % CPUTime :
% 0.21/0.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.21/0.47 % Process 1581664 was started by sandbox2 on n006,
% 0.21/0.47 % Sat Sep 26 15:42:43 2026
% 0.21/0.47 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 19.52/3.43
% 19.52/3.43 % SInE (scan): 589 to sos (tol 1.5x), 195 to usable (tol 2.0x), 4443 zapped, of 5227 axioms (depth 3).
% 19.52/3.43
% 19.52/3.43 % From the command line: assign(max_seconds, 300).
% 19.52/3.43
% 19.52/3.43 % SZS status Theorem for theBenchmark
% 19.52/3.43
% 19.52/3.43 % Proof 1 at 2.14 (+ 0.50) seconds.
% 19.52/3.43 % Length of proof is 65.
% 19.52/3.43 % Level of proof is 15.
% 19.52/3.43 % Maximum clause weight is 21.000.
% 19.52/3.43 % Given clauses 154.
% 19.52/3.43
% 19.52/3.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------