%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 0.39s 1.11s
% Output : CNFRefutation 3.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 13
% Syntax : Number of formulae : 61 ( 56 unt; 0 def)
% Number of atoms : 66 ( 34 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 9 ~; 4 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-4 aty)
% Number of variables : 23 ( 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,hypothesis,
! [B_1_1] : bit0(ti(int,B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
! [B_1_1] : ti(int,bit0(B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
! [B_1_1] : ti(int,bit1(B_1_1)) = bit1(B_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [K_1] : number_number_of(int,K_1) = ti(int,K_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [K_1,L_1] : hAPP(int,int,times_times(int,bit0(K_1)),L_1) = bit0(hAPP(int,int,times_times(int,K_1),L_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,axiom,
! [Z_1] : hAPP(int,int,times_times(int,one_one(int)),Z_1) = ti(int,Z_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f333,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1] : hAPP(X_a,X_a,times_times(X_a,A_1),zero_zero(X_a)) = zero_zero(X_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1122,axiom,
comm_semiring_1(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1255,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1256,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(negated_conjecture,[status(cth)],[f1255]) ).
fof(f1356,plain,
! [X0] : bit0(ti(int,X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f1357,plain,
! [X0] : ti(int,bit0(X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f1359,plain,
! [X0] : ti(int,bit1(X0)) = bit1(X0),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f1420,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f1421,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f1467,plain,
! [X0] : number_number_of(int,X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f1593,plain,
! [X0,X1] : hAPP(int,int,times_times(int,bit0(X0)),X1) = bit0(hAPP(int,int,times_times(int,X0),X1)),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f1599,plain,
! [X0] : hAPP(int,int,times_times(int,one_one(int)),X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f1729,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f1755,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f2036,plain,
! [X_a] :
( ! [A_1] : hAPP(X_a,X_a,times_times(X_a,A_1),zero_zero(X_a)) = zero_zero(X_a)
| ~ comm_semiring_1(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f333]) ).
fof(f2037,plain,
! [X0,X1] :
( hAPP(X0,X0,times_times(X0,X1),zero_zero(X0)) = zero_zero(X0)
| ~ comm_semiring_1(X0) ),
inference(cnf_transformation,[status(thm)],[f2036]) ).
fof(f4358,plain,
comm_semiring_1(int),
inference(cnf_transformation,[status(thm)],[f1122]) ).
fof(f4493,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(cnf_transformation,[status(thm)],[f1256]) ).
fof(f4607,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),pls)),
inference(backward_demodulation,[status(thm)],[f1755,f4493]) ).
fof(f5845,plain,
one_one(int) = ti(int,bit1(pls)),
inference(backward_demodulation,[status(thm)],[f1467,f1729]) ).
fof(f5850,plain,
one_one(int) = bit1(pls),
inference(forward_demodulation,[status(thm)],[f1359,f5845]) ).
fof(f5866,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int))),pls)),
inference(backward_demodulation,[status(thm)],[f5850,f4607]) ).
fof(f8612,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,ti(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1467,f1420]) ).
fof(f8613,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1357,f8612]) ).
fof(f8614,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1593,f8613]) ).
fof(f8615,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(hAPP(int,int,times_times(int,bit1(pls)),m)))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1593,f8614]) ).
fof(f8616,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(hAPP(int,int,times_times(int,one_one(int)),m)))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f5850,f8615]) ).
fof(f8617,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(ti(int,m)))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1599,f8616]) ).
fof(f8618,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1356,f8617]) ).
fof(f8619,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,ti(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1467,f8618]) ).
fof(f8620,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m)),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1357,f8619]) ).
fof(f8621,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m))),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1593,f8620]) ).
fof(f8622,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(hAPP(int,int,times_times(int,bit1(pls)),m)))),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1593,f8621]) ).
fof(f8623,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(hAPP(int,int,times_times(int,one_one(int)),m)))),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f5850,f8622]) ).
fof(f8624,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(ti(int,m)))),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1599,f8623]) ).
fof(f8625,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),zero_zero(int)))),
inference(forward_demodulation,[status(thm)],[f1356,f8624]) ).
fof(f8626,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),pls))),
inference(forward_demodulation,[status(thm)],[f1755,f8625]) ).
fof(f8631,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f5850,f1421]) ).
fof(f8632,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,ti(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f1467,f8631]) ).
fof(f8633,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m)),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f1357,f8632]) ).
fof(f8634,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m))),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f1593,f8633]) ).
fof(f8635,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(hAPP(int,int,times_times(int,bit1(pls)),m)))),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f1593,f8634]) ).
fof(f8636,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(hAPP(int,int,times_times(int,one_one(int)),m)))),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f5850,f8635]) ).
fof(f8637,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(ti(int,m)))),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f1599,f8636]) ).
fof(f8638,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),pls)),
inference(backward_demodulation,[status(thm)],[f8639,f5866]) ).
fof(f8639,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t),
inference(forward_demodulation,[status(thm)],[f1356,f8637]) ).
fof(f10167,plain,
! [X0] :
( hAPP(int,int,times_times(int,X0),pls) = zero_zero(int)
| ~ comm_semiring_1(int) ),
inference(paramodulation,[status(thm)],[f1755,f2037]) ).
fof(f10173,plain,
! [X0] :
( hAPP(int,int,times_times(int,X0),pls) = pls
| ~ comm_semiring_1(int) ),
inference(forward_demodulation,[status(thm)],[f1755,f10167]) ).
fof(f10174,plain,
! [X0] : hAPP(int,int,times_times(int,X0),pls) = pls,
inference(forward_subsumption_resolution,[status(thm)],[f10173,f4358]) ).
fof(f10175,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit0(bit0(m))),one_one(int))),t)),pls)),
inference(backward_demodulation,[status(thm)],[f10174,f8626]) ).
fof(f10194,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10175,f8638]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:14:51 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.23/0.57 % Drodi V4.1.1
% 0.39/1.11 % Refutation found
% 0.39/1.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.39/1.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.92/1.15 % Elapsed time: 0.774451 seconds
% 3.92/1.15 % CPU time: 4.282517 seconds
% 3.92/1.15 % Total memory used: 282.459 MB
% 3.92/1.15 % Net memory used: 279.881 MB
%------------------------------------------------------------------------------