%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NUM926+8 : 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 : n020.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:11 AM UTC 2026
% Result : Theorem 223.99s 33.06s
% Output : CNFRefutation 223.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 16
% Syntax : Number of formulae : 58 ( 31 unt; 0 def)
% Number of atoms : 95 ( 56 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 59 ( 22 ~; 30 |; 1 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 14 con; 0-4 aty)
% Number of variables : 52 ( 6 sgn 17 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_hAPP_arg2,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3) ).
fof(tsy_c_hAPP_res,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3) ).
fof(tsy_c_hBOOL_arg1,axiom,
! [X0] :
( hBOOL(ti(bool,X0))
<=> hBOOL(X0) ) ).
fof(tsy_v_t_____res,axiom,
ti(int,t) = t ).
fof(fact_0_tpos,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),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'(int)
=> ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) ) ).
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(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),t))
=> ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) ) ).
fof(fact_22_zless__le,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),X1))
<=> ( ti(int,X0) != ti(int,X1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1)) ) ) ).
fof(fact_23_zless__linear,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X1),X0))
| ti(int,X0) = ti(int,X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),X1)) ) ).
fof(fact_25_zle__antisym,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1))
=> ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X1),X0))
=> ti(int,X0) = ti(int,X1) ) ) ).
fof(fact_89_number__of__is__id,axiom,
! [X0] : hAPP(int,int,'number$unumber$uof'(int),X0) = ti(int,X0) ).
fof(fact_3184_fact__1__int,axiom,
hAPP(int,int,'fact$ufact'(int),'one$uone'(int)) = 'one$uone'(int) ).
fof(help_fTrue_1_1_U,axiom,
hBOOL(fTrue) ).
fof(help_fFalse_1_1_U,axiom,
~ hBOOL(fFalse) ).
fof(help_fFalse_1_1_T,axiom,
! [X0] :
( ti(bool,X0) = fFalse
| ti(bool,X0) = fTrue ) ).
fof(conj_0,conjecture,
? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c165,plain,
hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
inference(clausification,[status(esa)],[tsy_c_hAPP_arg2]) ).
cnf(c166,plain,
hAPP(X0,X1,X2,X3) = ti(X1,hAPP(X0,X1,X2,X3)),
inference(clausification,[status(esa)],[tsy_c_hAPP_res]) ).
cnf(c167,plain,
( hBOOL(X0)
| ~ hBOOL(ti(bool,X0)) ),
inference(clausification,[status(esa)],[tsy_c_hBOOL_arg1]) ).
cnf(c173,plain,
ti(int,t) = t,
inference(clausification,[status(esa)],[tsy_v_t_____res]) ).
cnf(c174,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),t)),
inference(clausification,[status(esa)],[fact_0_tpos]) ).
cnf(c175,plain,
( hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK107),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK108),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| 'one$uone'(int) != t ),
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(c176,plain,
( hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK109),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK110),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),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(c196,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),X1)) ),
inference(clausification,[status(esa)],[fact_22_zless__le]) ).
cnf(c199,plain,
( ti(int,X1) = ti(int,X0)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X1),X0))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),X0),X1)) ),
inference(clausification,[status(esa)],[fact_23_zless__linear]) ).
cnf(c201,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X1),X0))
| ti(int,X1) = ti(int,X0)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),X0),X1)) ),
inference(clausification,[status(esa)],[fact_25_zle__antisym]) ).
cnf(c291,plain,
ti(int,X0) = hAPP(int,int,'number$unumber$uof'(int),X0),
inference(clausification,[status(esa)],[fact_89_number__of__is__id]) ).
cnf(c4420,plain,
hAPP(int,int,'fact$ufact'(int),'one$uone'(int)) = 'one$uone'(int),
inference(clausification,[status(esa)],[fact_3184_fact__1__int]) ).
cnf(c7161,plain,
hBOOL(fTrue),
inference(clausification,[status(esa)],[help_fTrue_1_1_U]) ).
cnf(c7169,plain,
~ hBOOL(fFalse),
inference(clausification,[status(esa)],[help_fFalse_1_1_U]) ).
cnf(c7170,plain,
( ti(bool,X0) = fFalse
| ti(bool,X0) = fTrue ),
inference(clausification,[status(esa)],[help_fFalse_1_1_T]) ).
cnf(c7176,plain,
hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,'number$unumber$uof'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) != hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ti(bool,X0) = fFalse
| hBOOL(X0)
| ~ hBOOL(fTrue) ),
inference(superposition,[status(thm)],[c7170,c167]) ).
cnf(d1,plain,
( hBOOL(X0)
| ti(bool,X0) = fFalse ),
inference(resolution,[status(thm)],[c7161,d0]) ).
cnf(d2,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),t))
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK109),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK110),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(demodulation,[status(thm)],[c176,c291]) ).
cnf(d3,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),t))
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),m)),'one$uone'(int)) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK109),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK110),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(demodulation,[status(thm)],[d2,c165]) ).
cnf(d4,plain,
hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) != hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),
inference(demodulation,[status(thm)],[c7176,c291]) ).
cnf(d5,plain,
hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),m)),'one$uone'(int)) != hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X0),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),X1),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),
inference(demodulation,[status(thm)],[d4,c165]) ).
cnf(d6,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),t)),
inference(resolution,[status(thm)],[d5,d3]) ).
cnf(d7,plain,
ti(bool,hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),t)) = fFalse,
inference(resolution,[status(thm)],[d6,d1]) ).
cnf(d8,plain,
hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),'one$uone'(int)),t) = fFalse,
inference(demodulation,[status(thm)],[d7,c166]) ).
cnf(d9,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),t),'one$uone'(int)))
| ti(int,t) = ti(int,'one$uone'(int))
| hBOOL(fFalse) ),
inference(superposition,[status(thm)],[d8,c199]) ).
cnf(d10,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),t),'one$uone'(int)))
| hBOOL(fFalse)
| t = ti(int,'one$uone'(int)) ),
inference(demodulation,[status(thm)],[d9,c173]) ).
cnf(d11,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless'(int),t),'one$uone'(int)))
| t = ti(int,'one$uone'(int)) ),
inference(resolution,[status(thm)],[c7169,d10]) ).
cnf(d12,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),t),'one$uone'(int)))
| t = ti(int,'one$uone'(int)) ),
inference(resolution,[status(thm)],[d11,c196]) ).
cnf(d13,plain,
( t = ti(int,'one$uone'(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),t))
| ti(int,t) = ti(int,'one$uone'(int)) ),
inference(resolution,[status(thm)],[c201,d12]) ).
cnf(d14,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),'ord$uless$ueq'(int),'one$uone'(int)),t))
| t = ti(int,'one$uone'(int))
| t = ti(int,'one$uone'(int)) ),
inference(demodulation,[status(thm)],[d13,c173]) ).
cnf(d15,plain,
( t = ti(int,'one$uone'(int))
| t = ti(int,'one$uone'(int)) ),
inference(resolution,[status(thm)],[c174,d14]) ).
cnf(d16,plain,
hAPP(int,X0,X1,'one$uone'(int)) = hAPP(int,X0,X1,t),
inference(superposition,[status(thm)],[d15,c165]) ).
cnf(d17,plain,
hAPP(int,int,'fact$ufact'(int),t) = 'one$uone'(int),
inference(demodulation,[status(thm)],[c4420,d16]) ).
cnf(d18,plain,
hAPP(int,int,'fact$ufact'(int),t) = ti(int,'one$uone'(int)),
inference(superposition,[status(thm)],[d17,c166]) ).
cnf(d19,plain,
'one$uone'(int) = ti(int,'one$uone'(int)),
inference(demodulation,[status(thm)],[d18,d17]) ).
cnf(d20,plain,
'one$uone'(int) = t,
inference(demodulation,[status(thm)],[d19,d15]) ).
cnf(d21,plain,
( 'one$uone'(int) != t
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),'one$uone'(int)) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK107),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK108),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(demodulation,[status(thm)],[c175,c291]) ).
cnf(d22,plain,
( 'one$uone'(int) != t
| hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(int,int,hAPP(int,fun(int,int),'times$utimes'(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),m)),'one$uone'(int)) = hAPP(int,int,hAPP(int,fun(int,int),'plus$uplus'(int),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK107),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),'power$upower'(int),sK108),hAPP(int,nat,'number$unumber$uof'(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(demodulation,[status(thm)],[d21,c165]) ).
cnf(d23,plain,
'one$uone'(int) != t,
inference(resolution,[status(thm)],[d5,d22]) ).
cnf(d24,plain,
$false,
inference(resolution,[status(thm)],[d23,d20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 04:21:34 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 223.99/33.06 % SZS status Theorem for theBenchmark.p
% 223.99/33.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------