%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NUM925+8 : 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 : n014.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 80.72s 13.42s
% Output : CNFRefutation 80.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 11
% Syntax : Number of formulae : 43 ( 22 unt; 0 def)
% Number of atoms : 76 ( 38 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 60 ( 27 ~; 27 |; 0 &)
% ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-4 aty)
% Number of variables : 26 ( 1 sgn 11 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Int_OPls_res,hypothesis,
ti(int,pls) = pls ).
fof(tsy_c_hAPP_res,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3) ).
fof(fact_5_zero__eq__power2,axiom,
! [X0] :
( 'ring$u11004092258visors'(X0)
=> ! [X1] :
( hAPP(nat,X0,hAPP(X0,fun(nat,X0),'power$upower'(X0),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,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_76_Pls__def,axiom,
pls = 'zero$uzero'(int) ).
fof(fact_98_zero__less__power2,axiom,
! [X0] :
( 'linordered$uidom'(X0)
=> ! [X1] :
( hBOOL(hAPP(X0,bool,hAPP(X0,fun(X0,bool),'ord$uless'(X0),'zero$uzero'(X0)),hAPP(nat,X0,hAPP(X0,fun(nat,X0),'power$upower'(X0),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))))
<=> ti(X0,X1) != 'zero$uzero'(X0) ) ) ).
fof(fact_269_zle__iff__zadd,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1))
<=> ? [X2] : ti(int,X1) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),X0),hAPP(nat,int,'semiring$u1$uof$unat'(int),X2)) ) ).
fof(fact_282_int__one__le__iff__zero__less,axiom,
! [X0] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),X0))
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),X0)) ) ).
fof(arity_Int_Oint___Rings_Oring__1__no__zero__divisors,axiom,
'ring$u11004092258visors'(int) ).
fof(arity_Int_Oint___Rings_Olinordered__idom,axiom,
'linordered$uidom'(int) ).
fof(conj_0,conjecture,
hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != 'zero$uzero'(int) ).
fof(negated_conjecture,negated_conjecture,
~ ( hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != 'zero$uzero'(int) ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c105,plain,
ti(int,pls) = pls,
inference(clausification,[status(esa)],[tsy_c_Int_OPls_res]) ).
cnf(c265,plain,
ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
inference(clausification,[status(esa)],[tsy_c_hAPP_res]) ).
cnf(c289,plain,
( ti(X0,X1) = 'zero$uzero'(X0)
| hAPP(nat,X0,hAPP(X0,fun(nat,X0),'power$upower'(X0),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != 'zero$uzero'(X0)
| ~ 'ring$u11004092258visors'(X0) ),
inference(clausification,[status(esa)],[fact_5_zero__eq__power2]) ).
cnf(c323,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(c395,plain,
pls = 'zero$uzero'(int),
inference(clausification,[status(esa)],[fact_76_Pls__def]) ).
cnf(c420,plain,
( ti(X0,X1) = 'zero$uzero'(X0)
| hBOOL(hAPP(X0,bool,hAPP(X0,fun(X0,bool),'ord$uless'(X0),'zero$uzero'(X0)),hAPP(nat,X0,hAPP(X0,fun(nat,X0),'power$upower'(X0),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))))
| ~ 'linordered$uidom'(X0) ),
inference(clausification,[status(esa)],[fact_98_zero__less__power2]) ).
cnf(c673,plain,
( ti(int,X1) != hAPP(int,int,hAPP(int,fun(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_269_zle__iff__zadd]) ).
cnf(c695,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),X0))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),X0)) ),
inference(clausification,[status(esa)],[fact_282_int__one__le__iff__zero__less]) ).
cnf(c7866,plain,
'ring$u11004092258visors'(int),
inference(clausification,[status(esa)],[arity_Int_Oint___Rings_Oring__1__no__zero__divisors]) ).
cnf(c7884,plain,
'linordered$uidom'(int),
inference(clausification,[status(esa)],[arity_Int_Oint___Rings_Olinordered__idom]) ).
cnf(c8320,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),hAPP(int,nat,'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,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),X0))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),X0)) ),
inference(demodulation,[status(thm)],[c695,c395]) ).
cnf(d1,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n))),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = pls,
inference(demodulation,[status(thm)],[c8320,c395]) ).
cnf(d2,plain,
( ~ 'ring$u11004092258visors'(int)
| ti(int,hAPP(int,int,hAPP(int,fun(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)],[d1,c289]) ).
cnf(d3,plain,
( ~ 'ring$u11004092258visors'(int)
| pls != 'zero$uzero'(int)
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = 'zero$uzero'(int) ),
inference(demodulation,[status(thm)],[d2,c265]) ).
cnf(d4,plain,
( ~ 'ring$u11004092258visors'(int)
| pls != 'zero$uzero'(int)
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d3,c395]) ).
cnf(d5,plain,
( ~ 'ring$u11004092258visors'(int)
| pls != pls
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(demodulation,[status(thm)],[d4,c395]) ).
cnf(d6,plain,
( pls != pls
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls ),
inference(resolution,[status(thm)],[c7866,d5]) ).
cnf(d7,plain,
hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),'one$uone'(int)),hAPP(nat,int,'semiring$u1$uof$unat'(int),n)) = pls,
inference(equality_resolution,[status(thm)],[d6]) ).
cnf(d8,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),X0))
| ti(int,X0) != pls ),
inference(superposition,[status(thm)],[d7,c673]) ).
cnf(d9,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),pls))
| pls != pls ),
inference(superposition,[status(thm)],[c105,d8]) ).
cnf(d10,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),pls),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = pls,
inference(demodulation,[status(thm)],[d1,d7]) ).
cnf(d11,plain,
( ~ 'linordered$uidom'(int)
| ti(int,pls) = 'zero$uzero'(int)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),pls)) ),
inference(superposition,[status(thm)],[d10,c420]) ).
cnf(d12,plain,
( ~ 'linordered$uidom'(int)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),pls))
| pls = 'zero$uzero'(int) ),
inference(demodulation,[status(thm)],[d11,c105]) ).
cnf(d13,plain,
( ~ 'linordered$uidom'(int)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'zero$uzero'(int)),pls))
| pls = pls ),
inference(demodulation,[status(thm)],[d12,c395]) ).
cnf(d14,plain,
( ~ 'linordered$uidom'(int)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),pls))
| pls = pls ),
inference(demodulation,[status(thm)],[d13,c395]) ).
cnf(d15,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),pls))
| pls = pls ),
inference(resolution,[status(thm)],[c7884,d14]) ).
cnf(d16,plain,
pls = pls,
inference(resolution,[status(thm)],[c323,d15]) ).
cnf(d17,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),pls)),
inference(resolution,[status(thm)],[d16,d9]) ).
cnf(d18,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),pls),pls)),
inference(resolution,[status(thm)],[d17,d0]) ).
cnf(d19,plain,
$false,
inference(resolution,[status(thm)],[c323,d18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n014.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sat Sep 26 04:19:48 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 80.72/13.42 % SZS status Theorem for theBenchmark.p
% 80.72/13.42 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------