%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:44:05 PM UTC 2026
% Result : Theorem 0.14s 1.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.57 % Computer : n007.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Mon Sep 21 03:14:51 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.14/0.71 % Drodi V4.1.1
% 0.14/1.22 % Refutation found
% 0.14/1.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/1.22 % SZS output start CNFRefutation for theBenchmark
% 0.14/1.22 fof(f25,axiom,(
% 0.14/1.22 (! [B_1_1,X_a] :( ab_semigroup_mult(X_a)=> times_times(X_a,ti(X_a,B_1_1)) = times_times(X_a,B_1_1) ) )),
% 0.14/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.22 fof(f50,hypothesis,(
% 0.14/1.22 (! [B_1_1] : bit0(ti(int,B_1_1)) = bit0(B_1_1) )),
% 0.14/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.22 fof(f52,hypothesis,(
% 0.14/1.22 (! [B_1_1] : bit1(ti(int,B_1_1)) = bit1(B_1_1) )),
% 0.14/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.22 fof(f53,hypothesis,(
% 0.14/1.22 (! [B_1_1] : ti(int,bit1(B_1_1)) = bit1(B_1_1) )),
% 0.14/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.22 fof(f100,axiom,(
% 0.14/1.22 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)))) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f101,axiom,(
% 0.14/1.23 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) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f120,axiom,(
% 0.14/1.23 (! [K_1] : number_number_of(int,K_1) = ti(int,K_1) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f161,axiom,(
% 0.14/1.23 (! [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)) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f164,axiom,(
% 0.14/1.23 (! [Z_1] : hAPP(int,int,times_times(int,one_one(int)),Z_1) = ti(int,Z_1) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f188,axiom,(
% 0.14/1.23 (! [K,L] :( bit1(K) = bit1(L)<=> ti(int,K) = ti(int,L) ) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f189,axiom,(
% 0.14/1.23 (! [K,L] :( bit0(K) = bit0(L)<=> ti(int,K) = ti(int,L) ) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f196,axiom,(
% 0.14/1.23 (! [Z_1,W] : hAPP(int,int,plus_plus(int,Z_1),W) = hAPP(int,int,plus_plus(int,W),Z_1) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f209,axiom,(
% 0.14/1.23 one_one(int) = number_number_of(int,bit1(pls)) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f220,axiom,(
% 0.14/1.23 pls = zero_zero(int) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f227,axiom,(
% 0.14/1.23 (! [K_1] : hAPP(int,int,plus_plus(int,K_1),pls) = ti(int,K_1) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f228,axiom,(
% 0.14/1.23 (! [K_1] : hAPP(int,int,plus_plus(int,pls),K_1) = ti(int,K_1) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f262,axiom,(
% 0.14/1.23 (! [K_1] : bit1(K_1) = hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),K_1)),K_1) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f333,axiom,(
% 0.14/1.23 (! [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) )) )),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f1114,axiom,(
% 0.14/1.23 ab_semigroup_mult(int) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f1122,axiom,(
% 0.14/1.23 comm_semiring_1(int) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f1255,conjecture,(
% 0.14/1.23 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))) ),
% 0.14/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/1.23 fof(f1256,negated_conjecture,(
% 0.14/1.23 ~(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))) )),
% 0.14/1.23 inference(negated_conjecture,[status(cth)],[f1255])).
% 0.14/1.23 fof(f1306,plain,(
% 0.14/1.23 ![B_1_1,X_a]: (~ab_semigroup_mult(X_a)|times_times(X_a,ti(X_a,B_1_1))=times_times(X_a,B_1_1))),
% 0.14/1.23 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.14/1.23 fof(f1307,plain,(
% 0.14/1.23 ![X_a]: (~ab_semigroup_mult(X_a)|(![B_1_1]: times_times(X_a,ti(X_a,B_1_1))=times_times(X_a,B_1_1)))),
% 0.14/1.23 inference(miniscoping,[status(thm)],[f1306])).
% 0.14/1.23 fof(f1308,plain,(
% 0.14/1.23 ![X0,X1]: (~ab_semigroup_mult(X0)|times_times(X0,ti(X0,X1))=times_times(X0,X1))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f1307])).
% 0.14/1.23 fof(f1356,plain,(
% 0.14/1.23 ![X0]: (bit0(ti(int,X0))=bit0(X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/1.23 fof(f1358,plain,(
% 0.14/1.23 ![X0]: (bit1(ti(int,X0))=bit1(X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/1.23 fof(f1359,plain,(
% 0.14/1.23 ![X0]: (ti(int,bit1(X0))=bit1(X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/1.23 fof(f1420,plain,(
% 0.14/1.23 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))))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/1.23 fof(f1421,plain,(
% 0.14/1.23 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)),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f101])).
% 0.14/1.23 fof(f1467,plain,(
% 0.14/1.23 ![X0]: (number_number_of(int,X0)=ti(int,X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f120])).
% 0.14/1.23 fof(f1593,plain,(
% 0.14/1.23 ![X0,X1]: (hAPP(int,int,times_times(int,bit0(X0)),X1)=bit0(hAPP(int,int,times_times(int,X0),X1)))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f161])).
% 0.14/1.23 fof(f1599,plain,(
% 0.14/1.23 ![X0]: (hAPP(int,int,times_times(int,one_one(int)),X0)=ti(int,X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f164])).
% 0.14/1.23 fof(f1675,plain,(
% 0.14/1.23 ![K,L]: ((~bit1(K)=bit1(L)|ti(int,K)=ti(int,L))&(bit1(K)=bit1(L)|~ti(int,K)=ti(int,L)))),
% 0.14/1.23 inference(NNF_transformation,[status(thm)],[f188])).
% 0.14/1.23 fof(f1676,plain,(
% 0.14/1.23 (![K,L]: (~bit1(K)=bit1(L)|ti(int,K)=ti(int,L)))&(![K,L]: (bit1(K)=bit1(L)|~ti(int,K)=ti(int,L)))),
% 0.14/1.23 inference(miniscoping,[status(thm)],[f1675])).
% 0.14/1.23 fof(f1677,plain,(
% 0.14/1.23 ![X0,X1]: (~bit1(X0)=bit1(X1)|ti(int,X0)=ti(int,X1))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f1676])).
% 0.14/1.23 fof(f1679,plain,(
% 0.14/1.23 ![K,L]: ((~bit0(K)=bit0(L)|ti(int,K)=ti(int,L))&(bit0(K)=bit0(L)|~ti(int,K)=ti(int,L)))),
% 0.14/1.23 inference(NNF_transformation,[status(thm)],[f189])).
% 0.14/1.23 fof(f1680,plain,(
% 0.14/1.23 (![K,L]: (~bit0(K)=bit0(L)|ti(int,K)=ti(int,L)))&(![K,L]: (bit0(K)=bit0(L)|~ti(int,K)=ti(int,L)))),
% 0.14/1.23 inference(miniscoping,[status(thm)],[f1679])).
% 0.14/1.23 fof(f1682,plain,(
% 0.14/1.23 ![X0,X1]: (bit0(X0)=bit0(X1)|~ti(int,X0)=ti(int,X1))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f1680])).
% 0.14/1.23 fof(f1696,plain,(
% 0.14/1.23 ![X0,X1]: (hAPP(int,int,plus_plus(int,X0),X1)=hAPP(int,int,plus_plus(int,X1),X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f196])).
% 0.14/1.23 fof(f1729,plain,(
% 0.14/1.23 one_one(int)=number_number_of(int,bit1(pls))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f209])).
% 0.14/1.23 fof(f1755,plain,(
% 0.14/1.23 pls=zero_zero(int)),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f220])).
% 0.14/1.23 fof(f1774,plain,(
% 0.14/1.23 ![X0]: (hAPP(int,int,plus_plus(int,X0),pls)=ti(int,X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f227])).
% 0.14/1.23 fof(f1775,plain,(
% 0.14/1.23 ![X0]: (hAPP(int,int,plus_plus(int,pls),X0)=ti(int,X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f228])).
% 0.14/1.23 fof(f1855,plain,(
% 0.14/1.23 ![X0]: (bit1(X0)=hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),X0)),X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f262])).
% 0.14/1.23 fof(f2036,plain,(
% 0.14/1.23 ![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)))),
% 0.14/1.23 inference(pre_NNF_transformation,[status(thm)],[f333])).
% 0.14/1.23 fof(f2037,plain,(
% 0.14/1.23 ![X0,X1]: (~comm_semiring_1(X0)|hAPP(X0,X0,times_times(X0,X1),zero_zero(X0))=zero_zero(X0))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f2036])).
% 0.14/1.23 fof(f4350,plain,(
% 0.14/1.23 ab_semigroup_mult(int)),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f1114])).
% 0.14/1.23 fof(f4358,plain,(
% 0.14/1.23 comm_semiring_1(int)),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f1122])).
% 0.14/1.23 fof(f4493,plain,(
% 0.14/1.23 ~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)))),
% 0.14/1.23 inference(cnf_transformation,[status(thm)],[f1256])).
% 0.14/1.23 fof(f4560,plain,(
% 0.14/1.23 ~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))),
% 0.14/1.23 inference(backward_demodulation,[status(thm)],[f1755,f4493])).
% 0.14/1.23 fof(f4611,plain,(
% 0.14/1.23 ![X0]: (ti(int,ti(int,X0))=ti(int,X0))),
% 0.14/1.23 inference(resolution,[status(thm)],[f1677,f1358])).
% 0.14/1.23 fof(f4699,plain,(
% 0.14/1.23 ![X0,X1]: (bit0(bit1(X0))=bit0(X1)|~bit1(X0)=ti(int,X1))),
% 0.14/1.23 inference(paramodulation,[status(thm)],[f1359,f1682])).
% 0.14/1.23 fof(f4934,plain,(
% 0.14/1.23 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls)))))),pls))),
% 0.14/1.23 inference(backward_demodulation,[status(thm)],[f1696,f4560])).
% 0.14/1.23 fof(f5187,plain,(
% 0.14/1.23 ![X0]: (bit1(X0)=hAPP(int,int,plus_plus(int,X0),hAPP(int,int,plus_plus(int,one_one(int)),X0)))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1696,f1855])).
% 0.14/1.23 fof(f5188,plain,(
% 0.14/1.23 bit1(pls)=ti(int,hAPP(int,int,plus_plus(int,one_one(int)),pls))),
% 0.14/1.23 inference(paramodulation,[status(thm)],[f1775,f5187])).
% 0.14/1.23 fof(f5195,plain,(
% 0.14/1.23 bit1(pls)=ti(int,ti(int,one_one(int)))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1774,f5188])).
% 0.14/1.23 fof(f5196,plain,(
% 0.14/1.23 bit1(pls)=ti(int,one_one(int))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f4611,f5195])).
% 0.14/1.23 fof(f5205,plain,(
% 0.14/1.23 bit0(bit1(pls))=bit0(one_one(int))),
% 0.14/1.23 inference(resolution,[status(thm)],[f5196,f4699])).
% 0.14/1.23 fof(f5227,plain,(
% 0.14/1.23 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))),pls))),
% 0.14/1.23 inference(backward_demodulation,[status(thm)],[f5205,f4934])).
% 0.14/1.23 fof(f5342,plain,(
% 0.14/1.23 ![X0]: (times_times(int,ti(int,X0))=times_times(int,X0))),
% 0.14/1.23 inference(resolution,[status(thm)],[f1308,f4350])).
% 0.14/1.23 fof(f5604,plain,(
% 0.14/1.23 one_one(int)=ti(int,bit1(pls))),
% 0.14/1.23 inference(backward_demodulation,[status(thm)],[f1467,f1729])).
% 0.14/1.23 fof(f5610,plain,(
% 0.14/1.23 one_one(int)=bit1(pls)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1359,f5604])).
% 0.14/1.23 fof(f7800,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1696,f1420])).
% 0.14/1.23 fof(f7801,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,ti(int,bit0(bit0(bit1(pls))))),m))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1467,f7800])).
% 0.14/1.23 fof(f7802,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5342,f7801])).
% 0.14/1.23 fof(f7803,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m)))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1593,f7802])).
% 0.14/1.23 fof(f7804,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(hAPP(int,int,times_times(int,bit1(pls)),m))))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1593,f7803])).
% 0.14/1.23 fof(f7805,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(hAPP(int,int,times_times(int,one_one(int)),m))))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5610,f7804])).
% 0.14/1.23 fof(f7806,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(ti(int,m))))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1599,f7805])).
% 0.14/1.23 fof(f7807,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),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))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1356,f7806])).
% 0.14/1.23 fof(f7808,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1696,f7807])).
% 0.14/1.23 fof(f7809,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,ti(int,bit0(bit0(bit1(pls))))),m))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1467,f7808])).
% 0.14/1.23 fof(f7810,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5342,f7809])).
% 0.14/1.23 fof(f7811,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m)))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1593,f7810])).
% 0.14/1.23 fof(f7812,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(hAPP(int,int,times_times(int,bit1(pls)),m))))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1593,f7811])).
% 0.14/1.23 fof(f7813,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(hAPP(int,int,times_times(int,one_one(int)),m))))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5610,f7812])).
% 0.14/1.23 fof(f7814,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(ti(int,m))))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1599,f7813])).
% 0.14/1.23 fof(f7815,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),zero_zero(int))))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1356,f7814])).
% 0.14/1.23 fof(f7816,plain,(
% 0.14/1.23 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),pls)))),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1755,f7815])).
% 0.14/1.23 fof(f7821,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls)))))=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)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1696,f1421])).
% 0.14/1.23 fof(f7822,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(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)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5610,f7821])).
% 0.14/1.23 fof(f7823,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m))),t)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1696,f7822])).
% 0.14/1.23 fof(f7824,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,ti(int,bit0(bit0(bit1(pls))))),m))),t)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1467,f7823])).
% 0.14/1.23 fof(f7825,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m))),t)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5342,f7824])).
% 0.14/1.23 fof(f7826,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m)))),t)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1593,f7825])).
% 0.14/1.23 fof(f7827,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(hAPP(int,int,times_times(int,bit1(pls)),m))))),t)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f1593,f7826])).
% 0.14/1.23 fof(f7828,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(hAPP(int,int,times_times(int,one_one(int)),m))))),t)),
% 0.14/1.23 inference(forward_demodulation,[status(thm)],[f5610,f7827])).
% 0.14/1.23 fof(f7829,plain,(
% 0.14/1.23 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(ti(int,m))))),t)),
% 0.14/1.27 inference(forward_demodulation,[status(thm)],[f1599,f7828])).
% 0.14/1.27 fof(f7830,plain,(
% 0.14/1.27 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),pls))),
% 0.14/1.27 inference(backward_demodulation,[status(thm)],[f7831,f5227])).
% 0.14/1.27 fof(f7831,plain,(
% 0.14/1.27 hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(one_one(int)))))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),
% 0.14/1.27 inference(forward_demodulation,[status(thm)],[f1356,f7829])).
% 0.14/1.27 fof(f8153,plain,(
% 0.14/1.27 ![X0]: (hAPP(int,int,times_times(int,X0),zero_zero(int))=zero_zero(int))),
% 0.14/1.27 inference(resolution,[status(thm)],[f2037,f4358])).
% 0.14/1.27 fof(f8154,plain,(
% 0.14/1.27 ![X0]: (hAPP(int,int,times_times(int,X0),pls)=zero_zero(int))),
% 0.14/1.27 inference(forward_demodulation,[status(thm)],[f1755,f8153])).
% 0.14/1.27 fof(f8155,plain,(
% 0.14/1.27 ![X0]: (hAPP(int,int,times_times(int,X0),pls)=pls)),
% 0.14/1.27 inference(forward_demodulation,[status(thm)],[f1755,f8154])).
% 0.14/1.27 fof(f8156,plain,(
% 0.14/1.27 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),bit0(bit0(m)))),t)),pls))),
% 0.14/1.27 inference(backward_demodulation,[status(thm)],[f8155,f7816])).
% 0.14/1.27 fof(f8169,plain,(
% 0.14/1.27 $false),
% 0.14/1.27 inference(forward_subsumption_resolution,[status(thm)],[f8156,f7830])).
% 0.14/1.27 % SZS output end CNFRefutation for theBenchmark.p
% 3.71/1.29 % Elapsed time: 0.706695 seconds
% 3.71/1.29 % CPU time: 4.195680 seconds
% 3.71/1.29 % Total memory used: 273.450 MB
% 3.71/1.29 % Net memory used: 270.585 MB
%------------------------------------------------------------------------------