%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NUM926+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:10 AM UTC 2026
% Result : Theorem 38.21s 5.26s
% Output : CNFRefutation 38.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 10
% Syntax : Number of formulae : 44 ( 20 unt; 0 def)
% Number of atoms : 96 ( 36 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 89 ( 37 ~; 36 |; 8 &)
% ( 1 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 3 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-2 aty)
% Number of variables : 28 ( 8 sgn 6 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(gsy_c_Groups_Oone__class_Oone_000tc__Int__Oint,hypothesis,
'is$uint'('one$uone$uint') ).
fof(gsy_v_t____,axiom,
'is$uint'(t) ).
fof(fact_0_tpos,axiom,
hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint','one$uone$uint'),t)) ).
fof(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( t = 'one$uone$uint'
=> ? [X0,X1] :
( 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint')
& 'is$uint'(X1)
& 'is$uint'(X0) ) ) ).
fof(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint','one$uone$uint'),t))
=> ? [X0,X1] :
( 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint')
& 'is$uint'(X1)
& 'is$uint'(X0) ) ) ).
fof(fact_37_zless__le,axiom,
! [X0,X1] :
( ( 'is$uint'(X1)
& 'is$uint'(X0) )
=> ( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',X0),X1))
<=> ( X0 != X1
& hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',X0),X1)) ) ) ) ).
fof(fact_38_zless__linear,axiom,
! [X0,X1] :
( ( 'is$uint'(X1)
& 'is$uint'(X0) )
=> ( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',X1),X0))
| X0 = X1
| hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',X0),X1)) ) ) ).
fof(fact_40_zle__antisym,axiom,
! [X0,X1] :
( ( 'is$uint'(X1)
& 'is$uint'(X0) )
=> ( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',X0),X1))
=> ( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',X1),X0))
=> X0 = X1 ) ) ) ).
fof(fact_358_Pls__def,axiom,
pls = 'zero$uzero$uint' ).
fof(conj_0,conjecture,
? [X0,X1] : 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint') ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1] : 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint'),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c0,plain,
'is$uint'('one$uone$uint'),
inference(clausification,[status(esa)],[gsy_c_Groups_Oone__class_Oone_000tc__Int__Oint]) ).
cnf(c24,plain,
'is$uint'(t),
inference(clausification,[status(esa)],[gsy_v_t____]) ).
cnf(c25,plain,
hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint','one$uone$uint'),t)),
inference(clausification,[status(esa)],[fact_0_tpos]) ).
cnf(c28,plain,
( 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK27),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(sK28),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint')
| t != 'one$uone$uint' ),
inference(clausification,[status(esa)],[fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
cnf(c31,plain,
( 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK29),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(sK30),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint')
| ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint','one$uone$uint'),t)) ),
inference(clausification,[status(esa)],[fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
cnf(c67,plain,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',X0),X1))
| ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',X0),X1))
| ~ 'is$uint'(X1)
| ~ 'is$uint'(X0) ),
inference(clausification,[status(esa)],[fact_37_zless__le]) ).
cnf(c70,plain,
( ~ 'is$uint'(X1)
| hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',X1),X0))
| ~ 'is$uint'(X0)
| X0 = X1
| hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',X0),X1)) ),
inference(clausification,[status(esa)],[fact_38_zless__linear]) ).
cnf(c72,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',X0),X1))
| ~ 'is$uint'(X0)
| ~ 'is$uint'(X1)
| ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',X1),X0))
| X0 = X1 ),
inference(clausification,[status(esa)],[fact_40_zle__antisym]) ).
cnf(c485,plain,
pls = 'zero$uzero$uint',
inference(clausification,[status(esa)],[fact_358_Pls__def]) ).
cnf(c1767,plain,
'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1(pls))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1(pls))))) != 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint'),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint','one$uone$uint'),t))
| 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK29),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(sK30),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint') ),
inference(demodulation,[status(thm)],[c31,c485]) ).
cnf(d1,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint','one$uone$uint'),t))
| 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK29),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(sK30),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint') ),
inference(demodulation,[status(thm)],[d0,c485]) ).
cnf(d2,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint','one$uone$uint'),t))
| 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK29),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(sK30),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1('zero$uzero$uint'))))),m)),'one$uone$uint') ),
inference(demodulation,[status(thm)],[d1,c485]) ).
cnf(d3,plain,
'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1(pls))))) != 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint'),
inference(demodulation,[status(thm)],[c1767,c485]) ).
cnf(d4,plain,
'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))) != 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint'),
inference(demodulation,[status(thm)],[d3,c485]) ).
cnf(d5,plain,
'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(X0),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(X1),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))) != 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1('zero$uzero$uint'))))),m)),'one$uone$uint'),
inference(demodulation,[status(thm)],[d4,c485]) ).
cnf(d6,plain,
~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint','one$uone$uint'),t)),
inference(resolution,[status(thm)],[d5,d2]) ).
cnf(d7,plain,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',t),'one$uone$uint'))
| ~ 'is$uint'(t)
| ~ 'is$uint'('one$uone$uint')
| t = 'one$uone$uint' ),
inference(resolution,[status(thm)],[c70,d6]) ).
cnf(d8,plain,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',t),'one$uone$uint'))
| ~ 'is$uint'(t)
| t = 'one$uone$uint' ),
inference(resolution,[status(thm)],[c0,d7]) ).
cnf(d9,plain,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',t),'one$uone$uint'))
| t = 'one$uone$uint' ),
inference(resolution,[status(thm)],[c24,d8]) ).
cnf(d10,plain,
( t != 'one$uone$uint'
| 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK27),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(sK28),'number$unumber$uof$unat'(bit0(bit1(pls))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint') ),
inference(demodulation,[status(thm)],[c28,c485]) ).
cnf(d11,plain,
( t != 'one$uone$uint'
| 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK27),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(sK28),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1(pls))))),m)),'one$uone$uint') ),
inference(demodulation,[status(thm)],[d10,c485]) ).
cnf(d12,plain,
( t != 'one$uone$uint'
| 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$unat$uint'('power$upower$uint'(sK27),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))),'hAPP$unat$uint'('power$upower$uint'(sK28),'number$unumber$uof$unat'(bit0(bit1('zero$uzero$uint'))))) = 'hAPP$uint$uint'('plus$uplus$uint'('hAPP$uint$uint'('times$utimes$uint'('number$unumber$uof$uint'(bit0(bit0(bit1('zero$uzero$uint'))))),m)),'one$uone$uint') ),
inference(demodulation,[status(thm)],[d11,c485]) ).
cnf(d13,plain,
t != 'one$uone$uint',
inference(resolution,[status(thm)],[d5,d12]) ).
cnf(d14,plain,
hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$uint',t),'one$uone$uint')),
inference(resolution,[status(thm)],[d13,d9]) ).
cnf(d15,plain,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',t),'one$uone$uint'))
| ~ 'is$uint'('one$uone$uint')
| ~ 'is$uint'(t) ),
inference(resolution,[status(thm)],[d14,c67]) ).
cnf(d16,plain,
( hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',t),'one$uone$uint'))
| ~ 'is$uint'(t) ),
inference(resolution,[status(thm)],[c0,d15]) ).
cnf(d17,plain,
hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint',t),'one$uone$uint')),
inference(resolution,[status(thm)],[c24,d16]) ).
cnf(d18,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint','one$uone$uint'),t))
| ~ 'is$uint'(t)
| ~ 'is$uint'('one$uone$uint')
| t = 'one$uone$uint' ),
inference(resolution,[status(thm)],[c72,d17]) ).
cnf(d19,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint','one$uone$uint'),t))
| ~ 'is$uint'(t)
| t = 'one$uone$uint' ),
inference(resolution,[status(thm)],[c0,d18]) ).
cnf(d20,plain,
( ~ hBOOL('hAPP$uint$ubool'('hAPP$ui1948725293t$ubool'('ord$uless$ueq$uint','one$uone$uint'),t))
| t = 'one$uone$uint' ),
inference(resolution,[status(thm)],[c24,d19]) ).
cnf(d21,plain,
t = 'one$uone$uint',
inference(resolution,[status(thm)],[c25,d20]) ).
cnf(d22,plain,
$false,
inference(resolution,[status(thm)],[d13,d21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM926+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 04:22:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.21/5.26 % SZS status Theorem for theBenchmark.p
% 38.21/5.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------