%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NUM925+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 08:14:09 AM UTC 2026
% Result : Theorem 23.85s 6.09s
% Output : CNFRefutation 23.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 30
% Syntax : Number of formulae : 105 ( 66 unt; 0 def)
% Number of atoms : 158 ( 114 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 98 ( 45 ~; 33 |; 4 &)
% ( 4 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-4 aty)
% Number of variables : 73 ( 4 sgn 28 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Groups_Oplus__class_Oplus_2_arg1,axiom,
! [X0,X1] :
( 'cancel$usemigroup$uadd'(X1)
=> 'plus$uplus'(X1,ti(X1,X0)) = 'plus$uplus'(X1,X0) ) ).
fof(tsy_c_Groups_Ozero__class_Ozero_res,axiom,
! [X0] :
( zero(X0)
=> ti(X0,'zero$uzero'(X0)) = 'zero$uzero'(X0) ) ).
fof(tsy_c_Int_Onumber__class_Onumber__of_res,axiom,
! [X0,X1] :
( number(X1)
=> ti(X1,'number$unumber$uof'(X1,X0)) = 'number$unumber$uof'(X1,X0) ) ).
fof(tsy_c_hAPP_4_res,axiom,
! [X0,X1,X2] : ti(X0,hAPP(X0,X0,X1,X2)) = hAPP(X0,X0,X1,X2) ).
fof(fact_19_zero__is__num__zero,axiom,
'zero$uzero'(int) = 'number$unumber$uof'(int,pls) ).
fof(fact_25_nat__number__of__Pls,axiom,
'number$unumber$uof'(nat,pls) = 'zero$uzero'(nat) ).
fof(fact_29_nat__1__add__1,axiom,
hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'one$uone'(nat)) = 'number$unumber$uof'(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))) ).
fof(fact_36_add__nat__number__of,axiom,
! [X0,X1] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X1),pls))
=> ( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls))
=> hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X1)),'number$unumber$uof'(nat,X0)) = 'number$unumber$uof'(nat,hAPP(int,int,'plus$uplus'(int,X1),X0)) )
& ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls))
=> hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X1)),'number$unumber$uof'(nat,X0)) = 'number$unumber$uof'(nat,X1) ) ) )
& ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X1),pls))
=> hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X1)),'number$unumber$uof'(nat,X0)) = 'number$unumber$uof'(nat,X0) ) ) ).
fof(fact_37_one__is__num__one,axiom,
'one$uone'(int) = 'number$unumber$uof'(int,hAPP(int,int,bit1,pls)) ).
fof(fact_38_nat__numeral__1__eq__1,axiom,
'number$unumber$uof'(nat,hAPP(int,int,bit1,pls)) = 'one$uone'(nat) ).
fof(fact_39_Numeral1__eq1__nat,axiom,
'one$uone'(nat) = 'number$unumber$uof'(nat,hAPP(int,int,bit1,pls)) ).
fof(fact_73_Pls__def,axiom,
pls = 'zero$uzero'(int) ).
fof(fact_102_mn,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),m1),hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))) ).
fof(fact_119_number__of__is__id,axiom,
! [X0] : 'number$unumber$uof'(int,X0) = X0 ).
fof(fact_121_nat__add__commute,axiom,
! [X0,X1] : hAPP(nat,nat,'plus$uplus'(nat,X0),X1) = hAPP(nat,nat,'plus$uplus'(nat,X1),X0) ).
fof(fact_125_nat__add__right__cancel,axiom,
! [X0,X1,X2] :
( hAPP(nat,nat,'plus$uplus'(nat,X0),X1) = hAPP(nat,nat,'plus$uplus'(nat,X2),X1)
<=> X0 = X2 ) ).
fof(fact_153_add__is__0,axiom,
! [X0,X1] :
( hAPP(nat,nat,'plus$uplus'(nat,X0),X1) = 'zero$uzero'(nat)
<=> ( X1 = 'zero$uzero'(nat)
& X0 = 'zero$uzero'(nat) ) ) ).
fof(fact_154_Nat_Oadd__0__right,axiom,
! [X0] : hAPP(nat,nat,'plus$uplus'(nat,X0),'zero$uzero'(nat)) = X0 ).
fof(fact_155_plus__nat_Oadd__0,axiom,
! [X0] : hAPP(nat,nat,'plus$uplus'(nat,'zero$uzero'(nat)),X0) = X0 ).
fof(fact_163_zero__neq__one,axiom,
! [X0] :
( 'zero$uneq$uone'(X0)
=> 'zero$uzero'(X0) != 'one$uone'(X0) ) ).
fof(fact_164_field__power__not__zero,axiom,
! [X0] :
( 'ring$u11004092258visors'(X0)
=> ! [X1,X2] :
( ti(X0,X2) != 'zero$uzero'(X0)
=> hAPP(nat,X0,'power$upower'(X0,X2),X1) != 'zero$uzero'(X0) ) ) ).
fof(fact_232_nat__number__of__add__1,axiom,
! [X0] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls))
=> hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X0)),'one$uone'(nat)) = 'number$unumber$uof'(nat,hAPP(int,int,succ,X0)) )
& ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls))
=> hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X0)),'one$uone'(nat)) = 'one$uone'(nat) ) ) ).
fof(fact_294_zle__iff__zadd,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1))
<=> ? [X2] : X1 = hAPP(int,int,'plus$uplus'(int,X0),hAPP(nat,int,'semiring$u1$uof$unat'(int),X2)) ) ).
fof(fact_304_eq__0__number__of,axiom,
! [X0] :
( 'zero$uzero'(nat) = 'number$unumber$uof'(nat,X0)
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),pls)) ) ).
fof(arity_Int_Oint___Rings_Oring__1__no__zero__divisors,axiom,
'ring$u11004092258visors'(int) ).
fof(arity_Int_Oint___Int_Onumber,axiom,
number(int) ).
fof(arity_Nat_Onat___Groups_Ocancel__semigroup__add,axiom,
'cancel$usemigroup$uadd'(nat) ).
fof(arity_Nat_Onat___Rings_Ozero__neq__one,axiom,
'zero$uneq$uone'(nat) ).
fof(arity_Nat_Onat___Groups_Ozero,axiom,
zero(nat) ).
fof(conj_0,conjecture,
hAPP(nat,int,'power$upower'(int,hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),'number$unumber$uof'(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != 'zero$uzero'(int) ).
fof(negated_conjecture,negated_conjecture,
~ ( hAPP(nat,int,'power$upower'(int,hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),'number$unumber$uof'(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != 'zero$uzero'(int) ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c5,plain,
( 'plus$uplus'(X0,ti(X0,X1)) = 'plus$uplus'(X0,X1)
| ~ 'cancel$usemigroup$uadd'(X0) ),
inference(clausification,[status(esa)],[tsy_c_Groups_Oplus__class_Oplus_2_arg1]) ).
cnf(c8,plain,
( ti(X0,'zero$uzero'(X0)) = 'zero$uzero'(X0)
| ~ zero(X0) ),
inference(clausification,[status(esa)],[tsy_c_Groups_Ozero__class_Ozero_res]) ).
cnf(c15,plain,
( ti(X0,'number$unumber$uof'(X0,X1)) = 'number$unumber$uof'(X0,X1)
| ~ number(X0) ),
inference(clausification,[status(esa)],[tsy_c_Int_Onumber__class_Onumber__of_res]) ).
cnf(c39,plain,
ti(X0,hAPP(X0,X0,X1,X2)) = hAPP(X0,X0,X1,X2),
inference(clausification,[status(esa)],[tsy_c_hAPP_4_res]) ).
cnf(c71,plain,
'zero$uzero'(int) = 'number$unumber$uof'(int,pls),
inference(clausification,[status(esa)],[fact_19_zero__is__num__zero]) ).
cnf(c77,plain,
'number$unumber$uof'(nat,pls) = 'zero$uzero'(nat),
inference(clausification,[status(esa)],[fact_25_nat__number__of__Pls]) ).
cnf(c82,plain,
hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'one$uone'(nat)) = 'number$unumber$uof'(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),
inference(clausification,[status(esa)],[fact_29_nat__1__add__1]) ).
cnf(c93,plain,
( hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X0)),'number$unumber$uof'(nat,X1)) = 'number$unumber$uof'(nat,X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls)) ),
inference(clausification,[status(esa)],[fact_36_add__nat__number__of]) ).
cnf(c96,plain,
'one$uone'(int) = 'number$unumber$uof'(int,hAPP(int,int,bit1,pls)),
inference(clausification,[status(esa)],[fact_37_one__is__num__one]) ).
cnf(c97,plain,
'number$unumber$uof'(nat,hAPP(int,int,bit1,pls)) = 'one$uone'(nat),
inference(clausification,[status(esa)],[fact_38_nat__numeral__1__eq__1]) ).
cnf(c98,plain,
'one$uone'(nat) = 'number$unumber$uof'(nat,hAPP(int,int,bit1,pls)),
inference(clausification,[status(esa)],[fact_39_Numeral1__eq1__nat]) ).
cnf(c155,plain,
pls = 'zero$uzero'(int),
inference(clausification,[status(esa)],[fact_73_Pls__def]) ).
cnf(c189,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),m1),hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))),
inference(clausification,[status(esa)],[fact_102_mn]) ).
cnf(c212,plain,
'number$unumber$uof'(int,X0) = X0,
inference(clausification,[status(esa)],[fact_119_number__of__is__id]) ).
cnf(c216,plain,
hAPP(nat,nat,'plus$uplus'(nat,X0),X1) = hAPP(nat,nat,'plus$uplus'(nat,X1),X0),
inference(clausification,[status(esa)],[fact_121_nat__add__commute]) ).
cnf(c221,plain,
( X0 = X2
| hAPP(nat,nat,'plus$uplus'(nat,X0),X1) != hAPP(nat,nat,'plus$uplus'(nat,X2),X1) ),
inference(clausification,[status(esa)],[fact_125_nat__add__right__cancel]) ).
cnf(c270,plain,
( X0 = 'zero$uzero'(nat)
| hAPP(nat,nat,'plus$uplus'(nat,X0),X1) != 'zero$uzero'(nat) ),
inference(clausification,[status(esa)],[fact_153_add__is__0]) ).
cnf(c273,plain,
hAPP(nat,nat,'plus$uplus'(nat,X0),'zero$uzero'(nat)) = X0,
inference(clausification,[status(esa)],[fact_154_Nat_Oadd__0__right]) ).
cnf(c274,plain,
hAPP(nat,nat,'plus$uplus'(nat,'zero$uzero'(nat)),X0) = X0,
inference(clausification,[status(esa)],[fact_155_plus__nat_Oadd__0]) ).
cnf(c287,plain,
( 'zero$uzero'(X0) != 'one$uone'(X0)
| ~ 'zero$uneq$uone'(X0) ),
inference(clausification,[status(esa)],[fact_163_zero__neq__one]) ).
cnf(c288,plain,
( hAPP(nat,X0,'power$upower'(X0,X1),X2) != 'zero$uzero'(X0)
| ti(X0,X1) = 'zero$uzero'(X0)
| ~ 'ring$u11004092258visors'(X0) ),
inference(clausification,[status(esa)],[fact_164_field__power__not__zero]) ).
cnf(c380,plain,
( hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,X0)),'one$uone'(nat)) = 'one$uone'(nat)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls)) ),
inference(clausification,[status(esa)],[fact_232_nat__number__of__add__1]) ).
cnf(c475,plain,
( X1 != hAPP(int,int,'plus$uplus'(int,X0),hAPP(nat,int,'semiring$u1$uof$unat'(int),X2))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1)) ),
inference(clausification,[status(esa)],[fact_294_zle__iff__zadd]) ).
cnf(c486,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),pls))
| 'zero$uzero'(nat) = 'number$unumber$uof'(nat,X0) ),
inference(clausification,[status(esa)],[fact_304_eq__0__number__of]) ).
cnf(c789,plain,
'ring$u11004092258visors'(int),
inference(clausification,[status(esa)],[arity_Int_Oint___Rings_Oring__1__no__zero__divisors]) ).
cnf(c816,plain,
number(int),
inference(clausification,[status(esa)],[arity_Int_Oint___Int_Onumber]) ).
cnf(c826,plain,
'cancel$usemigroup$uadd'(nat),
inference(clausification,[status(esa)],[arity_Nat_Onat___Groups_Ocancel__semigroup__add]) ).
cnf(c835,plain,
'zero$uneq$uone'(nat),
inference(clausification,[status(esa)],[arity_Nat_Onat___Rings_Ozero__neq__one]) ).
cnf(c846,plain,
zero(nat),
inference(clausification,[status(esa)],[arity_Nat_Onat___Groups_Ozero]) ).
cnf(c895,plain,
hAPP(nat,int,'power$upower'(int,hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),'number$unumber$uof'(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = 'zero$uzero'(int),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
ti(int,'number$unumber$uof'(int,X0)) = 'number$unumber$uof'(int,X0),
inference(resolution,[status(thm)],[c816,c15]) ).
cnf(d1,plain,
ti(int,X0) = 'number$unumber$uof'(int,X0),
inference(demodulation,[status(thm)],[d0,c212]) ).
cnf(d2,plain,
ti(int,X0) = X0,
inference(demodulation,[status(thm)],[d1,c212]) ).
cnf(d3,plain,
hAPP(nat,int,'power$upower'(int,hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'one$uone'(nat))) = 'zero$uzero'(int),
inference(demodulation,[status(thm)],[c895,c82]) ).
cnf(d4,plain,
hAPP(nat,int,'power$upower'(int,hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'one$uone'(nat))) = pls,
inference(demodulation,[status(thm)],[d3,c155]) ).
cnf(d5,plain,
( ~ 'ring$u11004092258visors'(int)
| ti(int,hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))) = 'zero$uzero'(int)
| pls != 'zero$uzero'(int) ),
inference(superposition,[status(thm)],[d4,c288]) ).
cnf(d6,plain,
( ~ 'ring$u11004092258visors'(int)
| pls != 'zero$uzero'(int)
| hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = 'zero$uzero'(int) ),
inference(demodulation,[status(thm)],[d5,d2]) ).
cnf(d7,plain,
( ~ 'ring$u11004092258visors'(int)
| pls != 'zero$uzero'(int)
| hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d6,c155]) ).
cnf(d8,plain,
( ~ 'ring$u11004092258visors'(int)
| pls != pls
| hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d7,c155]) ).
cnf(d9,plain,
( pls != pls
| hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(resolution,[status(thm)],[c789,d8]) ).
cnf(d10,plain,
pls = 'number$unumber$uof'(int,pls),
inference(demodulation,[status(thm)],[c71,c155]) ).
cnf(d11,plain,
pls = pls,
inference(demodulation,[status(thm)],[d10,c212]) ).
cnf(d12,plain,
hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls,
inference(resolution,[status(thm)],[d11,d9]) ).
cnf(d13,plain,
ti(int,pls) = hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)),
inference(superposition,[status(thm)],[d12,c39]) ).
cnf(d14,plain,
pls = hAPP(int,int,'plus$uplus'(int,'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)),
inference(demodulation,[status(thm)],[d13,d2]) ).
cnf(d15,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),X0))
| X0 != pls ),
inference(superposition,[status(thm)],[d14,c475]) ).
cnf(d16,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),pls)),
inference(equality_resolution,[status(thm)],[d15]) ).
cnf(d17,plain,
'zero$uzero'(nat) = 'number$unumber$uof'(nat,'one$uone'(int)),
inference(resolution,[status(thm)],[d16,c486]) ).
cnf(d18,plain,
'one$uone'(int) = hAPP(int,int,bit1,pls),
inference(demodulation,[status(thm)],[c96,c212]) ).
cnf(d19,plain,
'number$unumber$uof'(nat,'one$uone'(int)) = 'one$uone'(nat),
inference(demodulation,[status(thm)],[c97,d18]) ).
cnf(d20,plain,
'zero$uzero'(nat) = 'one$uone'(nat),
inference(demodulation,[status(thm)],[d19,d17]) ).
cnf(d21,plain,
( ~ 'zero$uneq$uone'(nat)
| 'zero$uzero'(nat) != 'zero$uzero'(nat) ),
inference(superposition,[status(thm)],[d20,c287]) ).
cnf(d22,plain,
'zero$uzero'(nat) != 'zero$uzero'(nat),
inference(resolution,[status(thm)],[c835,d21]) ).
cnf(d23,plain,
ti(nat,'zero$uzero'(nat)) = 'zero$uzero'(nat),
inference(resolution,[status(thm)],[c846,c8]) ).
cnf(d24,plain,
'one$uone'(nat) = 'number$unumber$uof'(nat,'one$uone'(int)),
inference(demodulation,[status(thm)],[c98,d18]) ).
cnf(d25,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),m1),pls)),
inference(demodulation,[status(thm)],[c189,d12]) ).
cnf(d26,plain,
hAPP(nat,nat,'plus$uplus'(nat,'number$unumber$uof'(nat,m1)),'number$unumber$uof'(nat,X0)) = 'number$unumber$uof'(nat,X0),
inference(resolution,[status(thm)],[d25,c93]) ).
cnf(d27,plain,
( 'number$unumber$uof'(nat,m1) = 'zero$uzero'(nat)
| 'number$unumber$uof'(nat,X0) != 'zero$uzero'(nat) ),
inference(superposition,[status(thm)],[d26,c270]) ).
cnf(d28,plain,
( 'number$unumber$uof'(nat,m1) = 'zero$uzero'(nat)
| 'zero$uzero'(nat) != 'zero$uzero'(nat) ),
inference(superposition,[status(thm)],[c77,d27]) ).
cnf(d29,plain,
'number$unumber$uof'(nat,m1) = 'zero$uzero'(nat),
inference(equality_resolution,[status(thm)],[d28]) ).
cnf(d30,plain,
( 'number$unumber$uof'(nat,m1) = X1
| 'number$unumber$uof'(nat,X0) != hAPP(nat,nat,'plus$uplus'(nat,X1),'number$unumber$uof'(nat,X0)) ),
inference(superposition,[status(thm)],[d26,c221]) ).
cnf(d31,plain,
( 'zero$uzero'(nat) = X1
| 'number$unumber$uof'(nat,X0) != hAPP(nat,nat,'plus$uplus'(nat,X1),'number$unumber$uof'(nat,X0)) ),
inference(demodulation,[status(thm)],[d30,d29]) ).
cnf(d32,plain,
( 'zero$uzero'(nat) = X0
| 'number$unumber$uof'(nat,'one$uone'(int)) != hAPP(nat,nat,'plus$uplus'(nat,X0),'one$uone'(nat)) ),
inference(superposition,[status(thm)],[d19,d31]) ).
cnf(d33,plain,
( 'one$uone'(nat) != hAPP(nat,nat,'plus$uplus'(nat,X0),'one$uone'(nat))
| 'zero$uzero'(nat) = X0 ),
inference(demodulation,[status(thm)],[d32,d24]) ).
cnf(d34,plain,
'plus$uplus'(nat,ti(nat,X0)) = 'plus$uplus'(nat,X0),
inference(resolution,[status(thm)],[c826,c5]) ).
cnf(d35,plain,
( 'zero$uzero'(nat) = ti(nat,X0)
| 'one$uone'(nat) != hAPP(nat,nat,'plus$uplus'(nat,X0),'one$uone'(nat)) ),
inference(superposition,[status(thm)],[d34,d33]) ).
cnf(d36,plain,
( 'zero$uzero'(nat) = ti(nat,'zero$uzero'(nat))
| 'one$uone'(nat) != 'one$uone'(nat) ),
inference(superposition,[status(thm)],[c274,d35]) ).
cnf(d37,plain,
( 'zero$uzero'(nat) = 'zero$uzero'(nat)
| 'one$uone'(nat) != 'one$uone'(nat) ),
inference(demodulation,[status(thm)],[d36,d23]) ).
cnf(d38,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),pls))
| hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'number$unumber$uof'(nat,X0)) = 'one$uone'(nat) ),
inference(demodulation,[status(thm)],[c380,c216]) ).
cnf(d39,plain,
hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'number$unumber$uof'(nat,m1)) = 'one$uone'(nat),
inference(resolution,[status(thm)],[d38,d25]) ).
cnf(d40,plain,
hAPP(nat,nat,'plus$uplus'(nat,'one$uone'(nat)),'zero$uzero'(nat)) = 'one$uone'(nat),
inference(demodulation,[status(thm)],[d39,d29]) ).
cnf(d41,plain,
'one$uone'(nat) = 'one$uone'(nat),
inference(demodulation,[status(thm)],[d40,c273]) ).
cnf(d42,plain,
'zero$uzero'(nat) = 'zero$uzero'(nat),
inference(resolution,[status(thm)],[d41,d37]) ).
cnf(d43,plain,
$false,
inference(resolution,[status(thm)],[d42,d22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n015.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sat Sep 26 04:22:44 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.85/6.09 % SZS status Theorem for theBenchmark.p
% 23.85/6.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------