%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NUM925+7 : 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 : n004.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 38.19s 15.86s
% Output : CNFRefutation 38.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 32
% Syntax : Number of formulae : 129 ( 106 unt; 0 def)
% Number of atoms : 160 ( 132 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 58 ( 27 ~; 20 |; 2 &)
% ( 3 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-4 aty)
% Number of variables : 124 ( 6 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Groups_Oplus__class_Oplus_2_res,axiom,
! [X0,X1,X2] :
( 'cancel$usemigroup$uadd'(X2)
=> ti(X2,'plus$uplus'(X2,X0,X1)) = 'plus$uplus'(X2,X0,X1) ) ).
fof(tsy_c_Int_OBit0_arg1,hypothesis,
! [X0] : bit0(ti(int,X0)) = bit0(X0) ).
fof(tsy_c_Int_OBit1_arg1,hypothesis,
! [X0] : bit1(ti(int,X0)) = bit1(X0) ).
fof(tsy_c_Int_OBit1_res,hypothesis,
! [X0] : ti(int,bit1(X0)) = bit1(X0) ).
fof(tsy_c_Residues_OLegendre_arg1,axiom,
! [X0,X1] : legendre(ti(int,X0),X1) = legendre(X0,X1) ).
fof(tsy_c_Residues_OLegendre_arg2,axiom,
! [X0,X1] : legendre(X0,ti(int,X1)) = legendre(X0,X1) ).
fof(tsy_c_Residues_OLegendre_res,axiom,
! [X0,X1] : ti(int,legendre(X0,X1)) = legendre(X0,X1) ).
fof(fact_0_n1pos,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))) ).
fof(fact_5_zero__eq__power2,axiom,
! [X0] :
( 'ring$u11004092258visors'(X0)
=> ! [X1] :
( hAPP(nat,X0,'power$upower'(X0,X1),'number$unumber$uof'(nat,bit0(bit1(pls)))) = 'zero$uzero'(X0)
<=> ti(X0,X1) = 'zero$uzero'(X0) ) ) ).
fof(fact_32_rel__simps_I2_J,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),pls)) ).
fof(fact_37_one__is__num__one,axiom,
'one$uone'(int) = 'number$unumber$uof'(int,bit1(pls)) ).
fof(fact_45_zadd__assoc,axiom,
! [X0,X1,X2] : 'plus$uplus'(int,'plus$uplus'(int,X0,X1),X2) = 'plus$uplus'(int,X0,'plus$uplus'(int,X1,X2)) ).
fof(fact_46_zadd__left__commute,axiom,
! [X0,X1,X2] : 'plus$uplus'(int,X0,'plus$uplus'(int,X1,X2)) = 'plus$uplus'(int,X1,'plus$uplus'(int,X0,X2)) ).
fof(fact_47_zadd__commute,axiom,
! [X0,X1] : 'plus$uplus'(int,X0,X1) = 'plus$uplus'(int,X1,X0) ).
fof(fact_70_rel__simps_I44_J,axiom,
! [X0] :
( bit0(X0) = pls
<=> ti(int,X0) = pls ) ).
fof(fact_72_Bit0__Pls,axiom,
bit0(pls) = pls ).
fof(fact_73_Pls__def,axiom,
pls = 'zero$uzero'(int) ).
fof(fact_78_Bit0__def,axiom,
! [X0] : bit0(X0) = 'plus$uplus'(int,X0,X0) ).
fof(fact_90_add__Bit1__Bit0,axiom,
! [X0,X1] : 'plus$uplus'(int,bit1(X0),bit0(X1)) = bit1('plus$uplus'(int,X0,X1)) ).
fof(fact_91_add__Bit0__Bit1,axiom,
! [X0,X1] : 'plus$uplus'(int,bit0(X0),bit1(X1)) = bit1('plus$uplus'(int,X0,X1)) ).
fof(fact_92_Bit1__def,axiom,
! [X0] : bit1(X0) = 'plus$uplus'(int,'plus$uplus'(int,'one$uone'(int),X0),X0) ).
fof(fact_120_number__of__is__id,axiom,
! [X0] : 'number$unumber$uof'(int,X0) = ti(int,X0) ).
fof(fact_370_mult__Pls,axiom,
! [X0] : 'times$utimes'(int,pls,X0) = pls ).
fof(fact_379_zmult__1__right,axiom,
! [X0] : 'times$utimes'(int,X0,'one$uone'(int)) = ti(int,X0) ).
fof(fact_519_succ__def,axiom,
! [X0] : succ(X0) = 'plus$uplus'(int,X0,'one$uone'(int)) ).
fof(fact_769_Bit1__Min,axiom,
bit1(min) = min ).
fof(fact_770_rel__simps_I43_J,axiom,
! [X0] :
( min = bit1(X0)
<=> min = ti(int,X0) ) ).
fof(fact_877_Legendre__def,axiom,
! [X0,X1] :
( ( ~ hBOOL(hAPP(int,bool,zcong(X0,'zero$uzero'(int)),X1))
=> ( ( ~ hBOOL(hAPP(int,bool,quadRes(X1),X0))
=> legendre(X0,X1) = 'number$unumber$uof'(int,min) )
& ( hBOOL(hAPP(int,bool,quadRes(X1),X0))
=> legendre(X0,X1) = 'one$uone'(int) ) ) )
& ( hBOOL(hAPP(int,bool,zcong(X0,'zero$uzero'(int)),X1))
=> legendre(X0,X1) = 'zero$uzero'(int) ) ) ).
fof(fact_886_zcong__1,axiom,
! [X0,X1] : hBOOL(hAPP(int,bool,zcong(X0,X1),'one$uone'(int))) ).
fof(arity_Int_Oint___Rings_Oring__1__no__zero__divisors,axiom,
'ring$u11004092258visors'(int) ).
fof(arity_Int_Oint___Groups_Ocancel__semigroup__add,axiom,
'cancel$usemigroup$uadd'(int) ).
fof(conj_0,conjecture,
hAPP(nat,int,'power$upower'(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),'number$unumber$uof'(nat,bit0(bit1(pls)))) != 'zero$uzero'(int) ).
fof(negated_conjecture,negated_conjecture,
~ ( hAPP(nat,int,'power$upower'(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),'number$unumber$uof'(nat,bit0(bit1(pls)))) != 'zero$uzero'(int) ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c17,plain,
( ti(X0,'plus$uplus'(X0,X1,X2)) = 'plus$uplus'(X0,X1,X2)
| ~ 'cancel$usemigroup$uadd'(X0) ),
inference(clausification,[status(esa)],[tsy_c_Groups_Oplus__class_Oplus_2_res]) ).
cnf(c46,plain,
bit0(ti(int,X0)) = bit0(X0),
inference(clausification,[status(esa)],[tsy_c_Int_OBit0_arg1]) ).
cnf(c48,plain,
bit1(ti(int,X0)) = bit1(X0),
inference(clausification,[status(esa)],[tsy_c_Int_OBit1_arg1]) ).
cnf(c49,plain,
ti(int,bit1(X0)) = bit1(X0),
inference(clausification,[status(esa)],[tsy_c_Int_OBit1_res]) ).
cnf(c63,plain,
legendre(ti(int,X0),X1) = legendre(X0,X1),
inference(clausification,[status(esa)],[tsy_c_Residues_OLegendre_arg1]) ).
cnf(c64,plain,
legendre(X0,ti(int,X1)) = legendre(X0,X1),
inference(clausification,[status(esa)],[tsy_c_Residues_OLegendre_arg2]) ).
cnf(c65,plain,
ti(int,legendre(X0,X1)) = legendre(X0,X1),
inference(clausification,[status(esa)],[tsy_c_Residues_OLegendre_res]) ).
cnf(c98,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))),
inference(clausification,[status(esa)],[fact_0_n1pos]) ).
cnf(c105,plain,
( ti(X0,X1) = 'zero$uzero'(X0)
| hAPP(nat,X0,'power$upower'(X0,X1),'number$unumber$uof'(nat,bit0(bit1(pls)))) != 'zero$uzero'(X0)
| ~ 'ring$u11004092258visors'(X0) ),
inference(clausification,[status(esa)],[fact_5_zero__eq__power2]) ).
cnf(c139,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),pls)),
inference(clausification,[status(esa)],[fact_32_rel__simps_I2_J]) ).
cnf(c148,plain,
'one$uone'(int) = 'number$unumber$uof'(int,bit1(pls)),
inference(clausification,[status(esa)],[fact_37_one__is__num__one]) ).
cnf(c161,plain,
'plus$uplus'(int,'plus$uplus'(int,X0,X1),X2) = 'plus$uplus'(int,X0,'plus$uplus'(int,X1,X2)),
inference(clausification,[status(esa)],[fact_45_zadd__assoc]) ).
cnf(c162,plain,
'plus$uplus'(int,X0,'plus$uplus'(int,X1,X2)) = 'plus$uplus'(int,X1,'plus$uplus'(int,X0,X2)),
inference(clausification,[status(esa)],[fact_46_zadd__left__commute]) ).
cnf(c163,plain,
'plus$uplus'(int,X0,X1) = 'plus$uplus'(int,X1,X0),
inference(clausification,[status(esa)],[fact_47_zadd__commute]) ).
cnf(c202,plain,
( ti(int,X0) = pls
| bit0(X0) != pls ),
inference(clausification,[status(esa)],[fact_70_rel__simps_I44_J]) ).
cnf(c206,plain,
bit0(pls) = pls,
inference(clausification,[status(esa)],[fact_72_Bit0__Pls]) ).
cnf(c207,plain,
pls = 'zero$uzero'(int),
inference(clausification,[status(esa)],[fact_73_Pls__def]) ).
cnf(c212,plain,
bit0(X0) = 'plus$uplus'(int,X0,X0),
inference(clausification,[status(esa)],[fact_78_Bit0__def]) ).
cnf(c226,plain,
'plus$uplus'(int,bit1(X0),bit0(X1)) = bit1('plus$uplus'(int,X0,X1)),
inference(clausification,[status(esa)],[fact_90_add__Bit1__Bit0]) ).
cnf(c227,plain,
'plus$uplus'(int,bit0(X0),bit1(X1)) = bit1('plus$uplus'(int,X0,X1)),
inference(clausification,[status(esa)],[fact_91_add__Bit0__Bit1]) ).
cnf(c228,plain,
bit1(X0) = 'plus$uplus'(int,'plus$uplus'(int,'one$uone'(int),X0),X0),
inference(clausification,[status(esa)],[fact_92_Bit1__def]) ).
cnf(c265,plain,
'number$unumber$uof'(int,X0) = ti(int,X0),
inference(clausification,[status(esa)],[fact_120_number__of__is__id]) ).
cnf(c625,plain,
'times$utimes'(int,pls,X0) = pls,
inference(clausification,[status(esa)],[fact_370_mult__Pls]) ).
cnf(c638,plain,
'times$utimes'(int,X0,'one$uone'(int)) = ti(int,X0),
inference(clausification,[status(esa)],[fact_379_zmult__1__right]) ).
cnf(c875,plain,
succ(X0) = 'plus$uplus'(int,X0,'one$uone'(int)),
inference(clausification,[status(esa)],[fact_519_succ__def]) ).
cnf(c1216,plain,
bit1(min) = min,
inference(clausification,[status(esa)],[fact_769_Bit1__Min]) ).
cnf(c1217,plain,
( min = ti(int,X0)
| min != bit1(X0) ),
inference(clausification,[status(esa)],[fact_770_rel__simps_I43_J]) ).
cnf(c1385,plain,
( legendre(X0,X1) = 'zero$uzero'(int)
| ~ hBOOL(hAPP(int,bool,zcong(X0,'zero$uzero'(int)),X1)) ),
inference(clausification,[status(esa)],[fact_877_Legendre__def]) ).
cnf(c1399,plain,
hBOOL(hAPP(int,bool,zcong(X0,X1),'one$uone'(int))),
inference(clausification,[status(esa)],[fact_886_zcong__1]) ).
cnf(c1602,plain,
'ring$u11004092258visors'(int),
inference(clausification,[status(esa)],[arity_Int_Oint___Rings_Oring__1__no__zero__divisors]) ).
cnf(c1609,plain,
'cancel$usemigroup$uadd'(int),
inference(clausification,[status(esa)],[arity_Int_Oint___Groups_Ocancel__semigroup__add]) ).
cnf(c1749,plain,
hAPP(nat,int,'power$upower'(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),'number$unumber$uof'(nat,bit0(bit1(pls)))) = 'zero$uzero'(int),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'ring$u11004092258visors'(int)
| ti(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))) = 'zero$uzero'(int)
| 'zero$uzero'(int) != 'zero$uzero'(int) ),
inference(superposition,[status(thm)],[c1749,c105]) ).
cnf(d1,plain,
( 'zero$uzero'(int) != 'zero$uzero'(int)
| ti(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))) = 'zero$uzero'(int) ),
inference(resolution,[status(thm)],[c1602,d0]) ).
cnf(d2,plain,
ti(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))) = 'zero$uzero'(int),
inference(equality_resolution,[status(thm)],[d1]) ).
cnf(d3,plain,
bit1('zero$uzero'(int)) = bit1('plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),
inference(superposition,[status(thm)],[d2,c48]) ).
cnf(d4,plain,
bit1(pls) = bit1('plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),
inference(demodulation,[status(thm)],[d3,c207]) ).
cnf(d5,plain,
ti(int,bit1(pls)) = bit1('plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),
inference(superposition,[status(thm)],[d4,c49]) ).
cnf(d6,plain,
'number$unumber$uof'(int,bit1(pls)) = bit1('plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),
inference(demodulation,[status(thm)],[d5,c265]) ).
cnf(d7,plain,
'one$uone'(int) = bit1('plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),
inference(demodulation,[status(thm)],[d6,c148]) ).
cnf(d8,plain,
'one$uone'(int) = bit1(pls),
inference(demodulation,[status(thm)],[d7,d4]) ).
cnf(d9,plain,
succ(X0) = 'plus$uplus'(int,X0,bit1(pls)),
inference(demodulation,[status(thm)],[c875,d8]) ).
cnf(d10,plain,
succ(X0) = 'plus$uplus'(int,bit1(pls),X0),
inference(superposition,[status(thm)],[d9,c163]) ).
cnf(d11,plain,
ti(int,'plus$uplus'(int,X0,X1)) = 'plus$uplus'(int,X0,X1),
inference(resolution,[status(thm)],[c1609,c17]) ).
cnf(d12,plain,
'number$unumber$uof'(int,'plus$uplus'(int,X0,X1)) = 'plus$uplus'(int,X0,X1),
inference(demodulation,[status(thm)],[d11,c265]) ).
cnf(d13,plain,
bit0('zero$uzero'(int)) = bit0('plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),
inference(superposition,[status(thm)],[d2,c46]) ).
cnf(d14,plain,
( ti(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))) = pls
| bit0('zero$uzero'(int)) != pls ),
inference(superposition,[status(thm)],[d13,c202]) ).
cnf(d15,plain,
( bit0('zero$uzero'(int)) != pls
| 'number$unumber$uof'(int,'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))) = pls ),
inference(demodulation,[status(thm)],[d14,c265]) ).
cnf(d16,plain,
( bit0('zero$uzero'(int)) != pls
| 'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d15,d12]) ).
cnf(d17,plain,
( bit0('zero$uzero'(int)) != pls
| 'plus$uplus'(int,bit1(pls),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d16,d8]) ).
cnf(d18,plain,
( bit0('zero$uzero'(int)) != pls
| succ(hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d17,d10]) ).
cnf(d19,plain,
( bit0(pls) != pls
| succ(hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d18,c207]) ).
cnf(d20,plain,
( pls != pls
| succ(hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d19,c206]) ).
cnf(d21,plain,
( ~ hBOOL(hAPP(int,bool,zcong(X0,'zero$uzero'(int)),X1))
| legendre(X0,X1) = pls ),
inference(demodulation,[status(thm)],[c1385,c207]) ).
cnf(d22,plain,
( ~ hBOOL(hAPP(int,bool,zcong(X0,pls),X1))
| legendre(X0,X1) = pls ),
inference(demodulation,[status(thm)],[d21,c207]) ).
cnf(d23,plain,
hBOOL(hAPP(int,bool,zcong(X0,X1),bit1(pls))),
inference(demodulation,[status(thm)],[c1399,d8]) ).
cnf(d24,plain,
legendre(X0,bit1(pls)) = pls,
inference(resolution,[status(thm)],[d23,d22]) ).
cnf(d25,plain,
'times$utimes'(int,X0,bit1(pls)) = ti(int,X0),
inference(demodulation,[status(thm)],[c638,d8]) ).
cnf(d26,plain,
'times$utimes'(int,X0,bit1(pls)) = 'number$unumber$uof'(int,X0),
inference(demodulation,[status(thm)],[d25,c265]) ).
cnf(d27,plain,
'number$unumber$uof'(int,pls) = pls,
inference(superposition,[status(thm)],[d26,c625]) ).
cnf(d28,plain,
ti(int,legendre(X0,X1)) = legendre(X0,ti(int,X1)),
inference(superposition,[status(thm)],[c64,c65]) ).
cnf(d29,plain,
'number$unumber$uof'(int,legendre(X0,X1)) = legendre(X0,ti(int,X1)),
inference(demodulation,[status(thm)],[d28,c265]) ).
cnf(d30,plain,
'number$unumber$uof'(int,legendre(X1,X0)) = legendre(X1,'number$unumber$uof'(int,X0)),
inference(demodulation,[status(thm)],[d29,c265]) ).
cnf(d31,plain,
legendre(X0,ti(int,X1)) = legendre(ti(int,X0),X1),
inference(superposition,[status(thm)],[c63,c64]) ).
cnf(d32,plain,
legendre(X1,'number$unumber$uof'(int,X0)) = legendre(ti(int,X1),X0),
inference(demodulation,[status(thm)],[d31,c265]) ).
cnf(d33,plain,
legendre(X0,'number$unumber$uof'(int,X1)) = legendre('number$unumber$uof'(int,X0),X1),
inference(demodulation,[status(thm)],[d32,c265]) ).
cnf(d34,plain,
( min != bit1(X0)
| min = 'number$unumber$uof'(int,X0) ),
inference(demodulation,[status(thm)],[c1217,c265]) ).
cnf(d35,plain,
bit1(X0) = 'plus$uplus'(int,'one$uone'(int),'plus$uplus'(int,X0,X0)),
inference(demodulation,[status(thm)],[c228,c161]) ).
cnf(d36,plain,
bit1(X0) = 'plus$uplus'(int,'one$uone'(int),bit0(X0)),
inference(demodulation,[status(thm)],[d35,c212]) ).
cnf(d37,plain,
bit1(X0) = 'plus$uplus'(int,bit1(pls),bit0(X0)),
inference(demodulation,[status(thm)],[d36,d8]) ).
cnf(d38,plain,
bit1(X0) = bit1('plus$uplus'(int,pls,X0)),
inference(demodulation,[status(thm)],[d37,c226]) ).
cnf(d39,plain,
bit1(X0) = bit1('plus$uplus'(int,X0,pls)),
inference(superposition,[status(thm)],[c163,d38]) ).
cnf(d40,plain,
bit1('plus$uplus'(int,X0,X1)) = bit1('plus$uplus'(int,X0,'plus$uplus'(int,pls,X1))),
inference(superposition,[status(thm)],[c162,d38]) ).
cnf(d41,plain,
bit1('plus$uplus'(int,X0,X1)) = bit1('plus$uplus'(int,pls,'plus$uplus'(int,X0,X1))),
inference(superposition,[status(thm)],[c162,d40]) ).
cnf(d42,plain,
bit1('plus$uplus'(int,X0,X1)) = bit1('plus$uplus'(int,X0,X1)),
inference(demodulation,[status(thm)],[d41,d38]) ).
cnf(d43,plain,
bit1(bit1('plus$uplus'(int,X0,X1))) = bit1('plus$uplus'(int,bit0(X0),bit1(X1))),
inference(superposition,[status(thm)],[c227,d42]) ).
cnf(d44,plain,
bit1(bit1('plus$uplus'(int,X0,X1))) = bit1(bit1('plus$uplus'(int,X0,X1))),
inference(demodulation,[status(thm)],[d43,c227]) ).
cnf(d45,plain,
bit1('plus$uplus'(int,X0,pls)) = bit1(X0),
inference(superposition,[status(thm)],[d39,d42]) ).
cnf(d46,plain,
bit1(bit1(X0)) = bit1(bit1('plus$uplus'(int,X0,pls))),
inference(superposition,[status(thm)],[d45,d44]) ).
cnf(d47,plain,
bit1(bit1(X0)) = bit1(bit1(X0)),
inference(demodulation,[status(thm)],[d46,d39]) ).
cnf(d48,plain,
bit1(min) = bit1(bit1(min)),
inference(superposition,[status(thm)],[c1216,d47]) ).
cnf(d49,plain,
min = bit1(bit1(min)),
inference(demodulation,[status(thm)],[d48,c1216]) ).
cnf(d50,plain,
min = bit1(min),
inference(demodulation,[status(thm)],[d49,c1216]) ).
cnf(d51,plain,
( min = 'number$unumber$uof'(int,min)
| min != min ),
inference(superposition,[status(thm)],[d50,d34]) ).
cnf(d52,plain,
min = 'number$unumber$uof'(int,min),
inference(equality_resolution,[status(thm)],[d51]) ).
cnf(d53,plain,
legendre(min,'number$unumber$uof'(int,X0)) = legendre(min,X0),
inference(superposition,[status(thm)],[d52,d33]) ).
cnf(d54,plain,
'number$unumber$uof'(int,legendre(min,X0)) = legendre(min,X0),
inference(demodulation,[status(thm)],[d53,d30]) ).
cnf(d55,plain,
'number$unumber$uof'(int,pls) = legendre(min,bit1(pls)),
inference(superposition,[status(thm)],[d24,d54]) ).
cnf(d56,plain,
pls = legendre(min,bit1(pls)),
inference(demodulation,[status(thm)],[d55,d27]) ).
cnf(d57,plain,
pls = pls,
inference(demodulation,[status(thm)],[d56,d24]) ).
cnf(d58,plain,
succ(hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls,
inference(resolution,[status(thm)],[d57,d20]) ).
cnf(d59,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),'plus$uplus'(int,'one$uone'(int),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))),
inference(demodulation,[status(thm)],[c98,c207]) ).
cnf(d60,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),'plus$uplus'(int,bit1(pls),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))),
inference(demodulation,[status(thm)],[d59,d8]) ).
cnf(d61,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),succ(hAPP(nat,int,'semiring$u1$uof$unat'(int),n)))),
inference(demodulation,[status(thm)],[d60,d10]) ).
cnf(d62,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),pls)),
inference(demodulation,[status(thm)],[d61,d58]) ).
cnf(d63,plain,
$false,
inference(resolution,[status(thm)],[c139,d62]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925+7 : 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.09/5.37 % Computer : n004.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sat Sep 26 04:19:28 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.19/15.86 % SZS status Theorem for theBenchmark.p
% 38.19/15.86 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------