%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM924+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 01:41:59 PM UTC 2026
% Result : Theorem 16.80s 3.29s
% Output : CNFRefutation 17.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 21
% Syntax : Number of formulae : 80 ( 44 unt; 4 def)
% Number of atoms : 134 ( 62 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 101 ( 47 ~; 40 |; 6 &)
% ( 6 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 9 con; 0-4 aty)
% Number of variables : 45 ( 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f74,axiom,
! [X_a] :
( one(X_a)
=> ti(X_a,one_one(X_a)) = one_one(X_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f276,axiom,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f296,axiom,
! [Z_1,W] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z_1),W) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f335,axiom,
! [W] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),W) = pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f339,axiom,
! [Z_1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),Z_1) = ti(int,Z_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f370,axiom,
! [Z1,Z2,Z3] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2)),Z3) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z2),Z3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f372,axiom,
! [Z_1,W] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z_1),W) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),W),Z_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f387,axiom,
! [N_1,Ma] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),Ma))
=> ( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Ma),N_1) = one_one(int)
<=> ( ti(int,N_1) = one_one(int)
& ti(int,Ma) = one_one(int) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f395,axiom,
hAPP(int,int,bit0,pls) = pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f396,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f403,axiom,
! [K_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),pls) = ti(int,K_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f406,axiom,
! [K_4] : hAPP(int,int,bit0,K_4) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),K_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f437,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),one_one(int))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f438,axiom,
! [K_4] : hAPP(int,int,bit1,K_4) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),K_4)),K_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5339,axiom,
one(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5738,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5739,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(negated_conjecture,[status(cth)],[f5738]) ).
fof(f5829,plain,
! [X_a] :
( ti(X_a,one_one(X_a)) = one_one(X_a)
| ~ one(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f5830,plain,
! [X0] :
( ti(X0,one_one(X0)) = one_one(X0)
| ~ one(X0) ),
inference(cnf_transformation,[status(thm)],[f5829]) ).
fof(f6093,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f6094,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f6141,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X1),X0),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f6265,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),X0) = pls,
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f6272,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f6370,plain,
! [X0,X1,X2] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1)),X2) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X2)),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f6372,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X0),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f6407,plain,
! [N_1,Ma] :
( ( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Ma),N_1) = one_one(int)
<=> ( ti(int,N_1) = one_one(int)
& ti(int,Ma) = one_one(int) ) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),Ma)) ),
inference(pre_NNF_transformation,[status(thm)],[f387]) ).
fof(f6408,plain,
! [N_1,Ma] :
( ( ( ti(int,N_1) != one_one(int)
| ti(int,Ma) != one_one(int)
| hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Ma),N_1) = one_one(int) )
& ( ( ti(int,N_1) = one_one(int)
& ti(int,Ma) = one_one(int) )
| hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Ma),N_1) != one_one(int) ) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),Ma)) ),
inference(NNF_transformation,[status(thm)],[f6407]) ).
fof(f6409,plain,
! [Ma] :
( ( ! [N_1] :
( ti(int,N_1) != one_one(int)
| ti(int,Ma) != one_one(int)
| hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Ma),N_1) = one_one(int) )
& ! [N_1] :
( ( ti(int,N_1) = one_one(int)
& ti(int,Ma) = one_one(int) )
| hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Ma),N_1) != one_one(int) ) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),Ma)) ),
inference(miniscoping,[status(thm)],[f6408]) ).
fof(f6410,plain,
! [X0,X1] :
( ti(int,X0) = one_one(int)
| hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1) != one_one(int)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),X0)) ),
inference(cnf_transformation,[status(thm)],[f6409]) ).
fof(f6430,plain,
hAPP(int,int,bit0,pls) = pls,
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f6431,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f396]) ).
fof(f6450,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f6453,plain,
! [X0] : hAPP(int,int,bit0,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X0),
inference(cnf_transformation,[status(thm)],[f406]) ).
fof(f6530,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),one_one(int))),
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f6531,plain,
! [X0] : hAPP(int,int,bit1,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X0),
inference(cnf_transformation,[status(thm)],[f438]) ).
fof(f20562,plain,
one(int),
inference(cnf_transformation,[status(thm)],[f5339]) ).
fof(f20972,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(cnf_transformation,[status(thm)],[f5739]) ).
fof(f21543,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),pls)),
inference(backward_demodulation,[status(thm)],[f6431,f20972]) ).
fof(f21941,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),one_one(int))),
inference(forward_demodulation,[status(thm)],[f6431,f6530]) ).
fof(f22207,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))),pls)),
inference(backward_demodulation,[status(thm)],[f6372,f21543]) ).
fof(f22295,plain,
! [X0,X1] :
( ti(int,X0) = one_one(int)
| hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1) != one_one(int)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),X0)) ),
inference(forward_demodulation,[status(thm)],[f6431,f6410]) ).
fof(f22296,plain,
! [X0] :
( ti(int,one_one(int)) = one_one(int)
| ti(int,X0) != one_one(int)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),one_one(int))) ),
inference(paramodulation,[status(thm)],[f6272,f22295]) ).
fof(f22302,definition,
( sQ51_spl
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),one_one(int))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f22304,plain,
( sQ51_spl
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),one_one(int))) ),
inference(component_clause,[status(thm)],[f22302]) ).
fof(f22305,definition,
! [X0] :
( sQ52_spl
<=> ti(int,X0) != one_one(int) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f22306,plain,
! [X0] :
( ~ sQ52_spl
| ti(int,X0) != one_one(int) ),
inference(component_clause,[status(thm)],[f22305]) ).
fof(f22308,definition,
( sQ53_spl
<=> ti(int,one_one(int)) = one_one(int) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f22309,plain,
( ~ sQ53_spl
| ti(int,one_one(int)) = one_one(int) ),
inference(component_clause,[status(thm)],[f22308]) ).
fof(f22311,plain,
( sQ53_spl
| sQ52_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f22296,f22302,f22305,f22308]) ).
fof(f22325,definition,
( sQ56_spl
<=> one(int) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f22327,plain,
( sQ56_spl
| ~ one(int) ),
inference(component_clause,[status(thm)],[f22325]) ).
fof(f22332,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22327,f20562]) ).
fof(f22333,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f22332]) ).
fof(f22335,plain,
( ~ sQ52_spl
| ~ one(int) ),
inference(resolution,[status(thm)],[f22306,f5830]) ).
fof(f22339,plain,
( ~ sQ52_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f22335,f22325,f22305]) ).
fof(f22340,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22304,f21941]) ).
fof(f22341,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f22340]) ).
fof(f22687,plain,
! [X0] : hAPP(int,int,bit1,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X0)),
inference(forward_demodulation,[status(thm)],[f6370,f6531]) ).
fof(f22688,plain,
! [X0] : hAPP(int,int,bit1,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,X0)),
inference(forward_demodulation,[status(thm)],[f6453,f22687]) ).
fof(f22691,plain,
hAPP(int,int,bit1,pls) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),pls),
inference(paramodulation,[status(thm)],[f6430,f22688]) ).
fof(f22706,plain,
hAPP(int,int,bit1,pls) = ti(int,one_one(int)),
inference(forward_demodulation,[status(thm)],[f6450,f22691]) ).
fof(f22707,plain,
( ~ sQ53_spl
| hAPP(int,int,bit1,pls) = one_one(int) ),
inference(forward_demodulation,[status(thm)],[f22309,f22706]) ).
fof(f22713,plain,
( ~ sQ53_spl
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int)))))),pls)) ),
inference(backward_demodulation,[status(thm)],[f22707,f22207]) ).
fof(f28499,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f6372,f6093]) ).
fof(f28500,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))) ),
inference(forward_demodulation,[status(thm)],[f22707,f28499]) ).
fof(f28501,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m))),zero_zero(int)))) ),
inference(forward_demodulation,[status(thm)],[f6372,f28500]) ).
fof(f28502,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),zero_zero(int)))) ),
inference(forward_demodulation,[status(thm)],[f22707,f28501]) ).
fof(f28503,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),pls))) ),
inference(forward_demodulation,[status(thm)],[f6431,f28502]) ).
fof(f28504,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f6372,f6094]) ).
fof(f28505,plain,
( ~ sQ53_spl
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t) ),
inference(forward_demodulation,[status(thm)],[f22707,f28504]) ).
fof(f28506,plain,
( ~ sQ53_spl
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m))),t) ),
inference(forward_demodulation,[status(thm)],[f6372,f28505]) ).
fof(f28507,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int)))))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),pls))) ),
inference(backward_demodulation,[status(thm)],[f28508,f28503]) ).
fof(f28508,plain,
( ~ sQ53_spl
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))),t) ),
inference(forward_demodulation,[status(thm)],[f22707,f28506]) ).
fof(f30689,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int)))))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m))))) ),
inference(forward_demodulation,[status(thm)],[f6141,f28507]) ).
fof(f30690,plain,
( ~ sQ53_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int)))))),pls)) ),
inference(forward_demodulation,[status(thm)],[f6265,f30689]) ).
fof(f30691,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30690,f22713]) ).
fof(f30692,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f30691]) ).
fof(f30693,plain,
$false,
inference(sat_refutation,[status(thm)],[f22311,f22333,f22339,f22341,f30692]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.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 : Mon Sep 21 03:16:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.87/1.18 % Drodi V4.1.1
% 16.80/3.29 % Refutation found
% 16.80/3.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.80/3.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.05/3.48 % Elapsed time: 3.116269 seconds
% 13.05/3.48 % CPU time: 18.082436 seconds
% 13.05/3.48 % Total memory used: 1.223 GB
% 13.05/3.48 % Net memory used: 1.215 GB
%------------------------------------------------------------------------------