%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM926+4 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:42:02 PM UTC 2026
% Result : Theorem 0.66s 1.06s
% Output : CNFRefutation 0.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 10
% Syntax : Number of formulae : 50 ( 19 unt; 0 def)
% Number of atoms : 134 ( 45 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 139 ( 55 ~; 56 |; 19 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 17 con; 0-2 aty)
% Number of variables : 42 ( 30 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,hypothesis,
is_int(one_one_int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
is_int(t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
( t = one_one_int
=> ? [X,Y] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
& is_int(Y)
& is_int(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
=> ? [X,Y] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
& is_int(Y)
& is_int(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [X_49] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X_49),X_49) = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X_49),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [Z_2,W_1] :
( ( is_int(W_1)
& is_int(Z_2) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))
<=> ( Z_2 != W_1
& hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,axiom,
! [X_1,Y_1] :
( ( is_int(Y_1)
& is_int(X_1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Y_1),X_1))
| X_1 = Y_1
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X_1),Y_1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [Z_1,W] :
( ( is_int(W)
& is_int(Z_1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_1),W))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,W),Z_1))
=> Z_1 = W ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5480,conjecture,
? [X,Y] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5481,negated_conjecture,
~ ? [X,Y] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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),
inference(negated_conjecture,[status(cth)],[f5480]) ).
fof(f5487,plain,
is_int(one_one_int),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f5547,plain,
is_int(t),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f5548,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f5549,plain,
( ? [X,Y] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
& is_int(Y)
& is_int(X) )
| t != one_one_int ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f5550,plain,
( ( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK0_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK1_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
& is_int(sK1_skl)
& is_int(sK0_skl) )
| t != one_one_int ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f5549]) ).
fof(f5553,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK0_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK1_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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 != one_one_int ),
inference(cnf_transformation,[status(thm)],[f5550]) ).
fof(f5554,plain,
( ? [X,Y] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
& is_int(Y)
& is_int(X) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f5555,plain,
( ( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK2_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
& is_int(sK3_skl)
& is_int(sK2_skl) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f5554]) ).
fof(f5558,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK2_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(cnf_transformation,[status(thm)],[f5555]) ).
fof(f5588,plain,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),X0) = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f5624,plain,
! [Z_2,W_1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))
<=> ( Z_2 != W_1
& hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1)) ) )
| ~ is_int(W_1)
| ~ is_int(Z_2) ),
inference(pre_NNF_transformation,[status(thm)],[f125]) ).
fof(f5625,plain,
! [Z_2,W_1] :
( ( ( Z_2 = W_1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1)) )
& ( ( Z_2 != W_1
& hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1)) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1)) ) )
| ~ is_int(W_1)
| ~ is_int(Z_2) ),
inference(NNF_transformation,[status(thm)],[f5624]) ).
fof(f5626,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ is_int(X1)
| ~ is_int(X0) ),
inference(cnf_transformation,[status(thm)],[f5625]) ).
fof(f5629,plain,
! [X_1,Y_1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Y_1),X_1))
| X_1 = Y_1
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X_1),Y_1))
| ~ is_int(Y_1)
| ~ is_int(X_1) ),
inference(pre_NNF_transformation,[status(thm)],[f126]) ).
fof(f5630,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0))
| X0 = X1
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ is_int(X1)
| ~ is_int(X0) ),
inference(cnf_transformation,[status(thm)],[f5629]) ).
fof(f5634,plain,
! [Z_1,W] :
( Z_1 = W
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,W),Z_1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_1),W))
| ~ is_int(W)
| ~ is_int(Z_1) ),
inference(pre_NNF_transformation,[status(thm)],[f128]) ).
fof(f5635,plain,
! [X0,X1] :
( X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X1),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X1)
| ~ is_int(X0) ),
inference(cnf_transformation,[status(thm)],[f5634]) ).
fof(f19089,plain,
! [X,Y] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,Y),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) != 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),
inference(pre_NNF_transformation,[status(thm)],[f5481]) ).
fof(f19090,plain,
! [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) != 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),
inference(cnf_transformation,[status(thm)],[f19089]) ).
fof(f20155,plain,
! [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),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,X1),X1)) != 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),
inference(paramodulation,[status(thm)],[f5588,f19090]) ).
fof(f20227,plain,
! [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),X0)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X1),X1)) != 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),
inference(paramodulation,[status(thm)],[f5588,f20155]) ).
fof(f20758,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,sK0_skl),sK0_skl)),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK1_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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 != one_one_int ),
inference(forward_demodulation,[status(thm)],[f5588,f5553]) ).
fof(f20759,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,sK0_skl),sK0_skl)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,sK1_skl),sK1_skl)) = 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 != one_one_int ),
inference(forward_demodulation,[status(thm)],[f5588,f20758]) ).
fof(f20760,plain,
t != one_one_int,
inference(forward_subsumption_resolution,[status(thm)],[f20759,f20227]) ).
fof(f20789,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,sK2_skl),sK2_skl)),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3_skl),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = 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)
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(forward_demodulation,[status(thm)],[f5588,f5558]) ).
fof(f20790,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,sK2_skl),sK2_skl)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,sK3_skl),sK3_skl)) = 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)
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(forward_demodulation,[status(thm)],[f5588,f20789]) ).
fof(f20791,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)),
inference(forward_subsumption_resolution,[status(thm)],[f20790,f20227]) ).
fof(f23415,plain,
( t = one_one_int
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),one_one_int))
| ~ is_int(one_one_int)
| ~ is_int(t) ),
inference(resolution,[status(thm)],[f5630,f20791]) ).
fof(f23426,plain,
( t = one_one_int
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),one_one_int))
| ~ is_int(one_one_int) ),
inference(forward_subsumption_resolution,[status(thm)],[f23415,f5547]) ).
fof(f23430,plain,
( t = one_one_int
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),one_one_int)) ),
inference(forward_subsumption_resolution,[status(thm)],[f23426,f5487]) ).
fof(f23431,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,t),one_one_int))
| ~ is_int(one_one_int)
| ~ is_int(t)
| t = one_one_int ),
inference(resolution,[status(thm)],[f23430,f5626]) ).
fof(f23436,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,t),one_one_int))
| ~ is_int(one_one_int)
| ~ is_int(t) ),
inference(forward_subsumption_resolution,[status(thm)],[f23431,f20760]) ).
fof(f23442,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,t),one_one_int))
| ~ is_int(one_one_int) ),
inference(forward_subsumption_resolution,[status(thm)],[f23436,f5547]) ).
fof(f23443,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,t),one_one_int)),
inference(resolution,[status(thm)],[f23442,f5487]) ).
fof(f23520,plain,
( one_one_int = t
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t))
| ~ is_int(t)
| ~ is_int(one_one_int) ),
inference(resolution,[status(thm)],[f23443,f5635]) ).
fof(f23523,plain,
( one_one_int = t
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t))
| ~ is_int(t) ),
inference(forward_subsumption_resolution,[status(thm)],[f23520,f5487]) ).
fof(f23700,plain,
( one_one_int = t
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)) ),
inference(forward_subsumption_resolution,[status(thm)],[f23523,f5547]) ).
fof(f23701,plain,
one_one_int = t,
inference(resolution,[status(thm)],[f23700,f5548]) ).
fof(f23705,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f23701,f20760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n019.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 03:18:20 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.56/0.88 % Drodi V4.1.1
% 0.66/1.06 % Refutation found
% 0.66/1.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.66/1.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.09/1.21 % Elapsed time: 0.807941 seconds
% 1.09/1.21 % CPU time: 2.032121 seconds
% 1.09/1.21 % Total memory used: 624.387 MB
% 1.09/1.21 % Net memory used: 619.092 MB
%------------------------------------------------------------------------------