%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM924+8 : 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 : n006.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 23.42s 4.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+8 : 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.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 03:16:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 1.14/1.46 % Drodi V4.1.1
% 23.42/4.52 % Refutation found
% 23.42/4.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 23.42/4.52 % SZS output start CNFRefutation for theBenchmark
% 23.42/4.52 fof(f106,hypothesis,(
% 23.42/4.52 ti(int,pls) = pls ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f265,axiom,(
% 23.42/4.52 (! [X_a,X_c,B_1_1,B_2_1] : hAPP(X_a,X_c,B_1_1,ti(X_a,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f275,axiom,(
% 23.42/4.52 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)))) ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f276,axiom,(
% 23.42/4.52 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) ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f295,axiom,(
% 23.42/4.52 (! [K_4] : hAPP(int,int,number_number_of(int),K_4) = ti(int,K_4) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f296,axiom,(
% 23.42/4.52 (! [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) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f335,axiom,(
% 23.42/4.52 (! [W] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),W) = pls )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f336,axiom,(
% 23.42/4.52 (! [K_4,L_4] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,K_4)),L_4) = hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),K_4),L_4)) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f339,axiom,(
% 23.42/4.52 (! [Z_1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),Z_1) = ti(int,Z_1) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f365,axiom,(
% 23.42/4.52 (! [K,L] :( hAPP(int,int,bit0,K) = hAPP(int,int,bit0,L)<=> ti(int,K) = ti(int,L) ) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f370,axiom,(
% 23.42/4.52 (! [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)) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f395,axiom,(
% 23.42/4.52 hAPP(int,int,bit0,pls) = pls ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f396,axiom,(
% 23.42/4.52 pls = zero_zero(int) ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f403,axiom,(
% 23.42/4.52 (! [K_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),pls) = ti(int,K_4) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f406,axiom,(
% 23.42/4.52 (! [K_4] : hAPP(int,int,bit0,K_4) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),K_4) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f435,axiom,(
% 23.42/4.52 (! [K_4,L_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit1,K_4)),hAPP(int,int,bit0,L_4)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),L_4)) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f438,axiom,(
% 23.42/4.52 (! [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) )),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f740,axiom,(
% 23.42/4.52 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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,number_number_of(int),min_1)) = 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)) ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f5738,conjecture,(
% 23.42/4.52 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))) ),
% 23.42/4.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.42/4.52 fof(f5739,negated_conjecture,(
% 23.42/4.52 ~(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))) )),
% 23.42/4.52 inference(negated_conjecture,[status(cth)],[f5738])).
% 23.42/4.52 fof(f5878,plain,(
% 23.42/4.52 ti(int,pls)=pls),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f106])).
% 23.42/4.52 fof(f6080,plain,(
% 23.42/4.52 ![X0,X1,X2,X3]: (hAPP(X0,X1,X2,ti(X0,X3))=hAPP(X0,X1,X2,X3))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f265])).
% 23.42/4.52 fof(f6093,plain,(
% 23.42/4.52 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))))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f275])).
% 23.42/4.52 fof(f6094,plain,(
% 23.42/4.52 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)),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f276])).
% 23.42/4.52 fof(f6140,plain,(
% 23.42/4.52 ![X0]: (hAPP(int,int,number_number_of(int),X0)=ti(int,X0))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f295])).
% 23.42/4.52 fof(f6141,plain,(
% 23.42/4.52 ![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))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f296])).
% 23.42/4.52 fof(f6265,plain,(
% 23.42/4.52 ![X0]: (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),X0)=pls)),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f335])).
% 23.42/4.52 fof(f6266,plain,(
% 23.42/4.52 ![X0,X1]: (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,X0)),X1)=hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1)))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f336])).
% 23.42/4.52 fof(f6272,plain,(
% 23.42/4.52 ![X0]: (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0)=ti(int,X0))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f339])).
% 23.42/4.52 fof(f6355,plain,(
% 23.42/4.52 ![K,L]: ((~hAPP(int,int,bit0,K)=hAPP(int,int,bit0,L)|ti(int,K)=ti(int,L))&(hAPP(int,int,bit0,K)=hAPP(int,int,bit0,L)|~ti(int,K)=ti(int,L)))),
% 23.42/4.52 inference(NNF_transformation,[status(thm)],[f365])).
% 23.42/4.52 fof(f6356,plain,(
% 23.42/4.52 (![K,L]: (~hAPP(int,int,bit0,K)=hAPP(int,int,bit0,L)|ti(int,K)=ti(int,L)))&(![K,L]: (hAPP(int,int,bit0,K)=hAPP(int,int,bit0,L)|~ti(int,K)=ti(int,L)))),
% 23.42/4.52 inference(miniscoping,[status(thm)],[f6355])).
% 23.42/4.52 fof(f6358,plain,(
% 23.42/4.52 ![X0,X1]: (hAPP(int,int,bit0,X0)=hAPP(int,int,bit0,X1)|~ti(int,X0)=ti(int,X1))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f6356])).
% 23.42/4.52 fof(f6370,plain,(
% 23.42/4.52 ![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)))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f370])).
% 23.42/4.52 fof(f6430,plain,(
% 23.42/4.52 hAPP(int,int,bit0,pls)=pls),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f395])).
% 23.42/4.52 fof(f6431,plain,(
% 23.42/4.52 pls=zero_zero(int)),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f396])).
% 23.42/4.52 fof(f6450,plain,(
% 23.42/4.52 ![X0]: (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)=ti(int,X0))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f403])).
% 23.42/4.52 fof(f6453,plain,(
% 23.42/4.52 ![X0]: (hAPP(int,int,bit0,X0)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X0))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f406])).
% 23.42/4.52 fof(f6528,plain,(
% 23.42/4.52 ![X0,X1]: (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,X1))=hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1)))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f435])).
% 23.42/4.52 fof(f6531,plain,(
% 23.42/4.52 ![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))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f438])).
% 23.42/4.52 fof(f7384,plain,(
% 23.42/4.52 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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,number_number_of(int),min_1))=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))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f740])).
% 23.42/4.52 fof(f20972,plain,(
% 23.42/4.52 ~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)))),
% 23.42/4.52 inference(cnf_transformation,[status(thm)],[f5739])).
% 23.42/4.52 fof(f21726,plain,(
% 23.42/4.52 ~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))),
% 23.42/4.52 inference(backward_demodulation,[status(thm)],[f6431,f20972])).
% 23.42/4.52 fof(f22804,plain,(
% 23.42/4.52 ![X0]: (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit1,X0)),pls)=hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)))),
% 23.42/4.52 inference(paramodulation,[status(thm)],[f6430,f6528])).
% 23.42/4.52 fof(f22810,plain,(
% 23.42/4.52 ![X0]: (ti(int,hAPP(int,int,bit1,X0))=hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6450,f22804])).
% 23.42/4.52 fof(f22811,plain,(
% 23.42/4.52 ![X0]: (ti(int,hAPP(int,int,bit1,X0))=hAPP(int,int,bit1,ti(int,X0)))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6450,f22810])).
% 23.42/4.52 fof(f22905,plain,(
% 23.42/4.52 ![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)))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6370,f6531])).
% 23.42/4.52 fof(f22906,plain,(
% 23.42/4.52 ![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)))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6453,f22905])).
% 23.42/4.52 fof(f22907,plain,(
% 23.42/4.52 hAPP(int,int,bit1,pls)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),pls)),
% 23.42/4.52 inference(paramodulation,[status(thm)],[f6430,f22906])).
% 23.42/4.52 fof(f22911,plain,(
% 23.42/4.52 hAPP(int,int,bit1,pls)=ti(int,one_one(int))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6450,f22907])).
% 23.42/4.52 fof(f23016,plain,(
% 23.42/4.52 ~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,ti(int,one_one(int)))))),one_one(int))),pls))),
% 23.42/4.52 inference(backward_demodulation,[status(thm)],[f22911,f21726])).
% 23.42/4.52 fof(f23017,plain,(
% 23.42/4.52 ti(int,ti(int,one_one(int)))=hAPP(int,int,bit1,ti(int,pls))),
% 23.42/4.52 inference(paramodulation,[status(thm)],[f22911,f22811])).
% 23.42/4.52 fof(f23057,plain,(
% 23.42/4.52 ti(int,ti(int,one_one(int)))=hAPP(int,int,bit1,pls)),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f5878,f23017])).
% 23.42/4.52 fof(f23058,plain,(
% 23.42/4.52 ti(int,ti(int,one_one(int)))=ti(int,one_one(int))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f22911,f23057])).
% 23.42/4.52 fof(f23209,plain,(
% 23.42/4.52 hAPP(int,int,bit0,ti(int,one_one(int)))=hAPP(int,int,bit0,one_one(int))),
% 23.42/4.52 inference(resolution,[status(thm)],[f23058,f6358])).
% 23.42/4.52 fof(f24406,plain,(
% 23.42/4.52 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))),hAPP(int,int,number_number_of(int),min_1))=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))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f22911,f7384])).
% 23.42/4.52 fof(f24408,plain,(
% 23.42/4.52 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))),hAPP(int,int,number_number_of(int),min_1))=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,ti(int,one_one(int)))))),one_one(int))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f22911,f24406])).
% 23.42/4.52 fof(f24472,plain,(
% 23.42/4.52 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))),hAPP(int,int,number_number_of(int),min_1))=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,one_one(int))))),one_one(int))),
% 23.42/4.52 inference(backward_demodulation,[status(thm)],[f23209,f24408])).
% 23.42/4.52 fof(f24504,plain,(
% 23.42/4.52 ~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,one_one(int))))),one_one(int))),pls))),
% 23.42/4.52 inference(backward_demodulation,[status(thm)],[f23209,f23016])).
% 23.42/4.52 fof(f24540,plain,(
% 23.42/4.52 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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,number_number_of(int),min_1))=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,one_one(int))))),one_one(int))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f23209,f24472])).
% 23.42/4.52 fof(f27010,plain,(
% 23.42/4.52 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,ti(int,one_one(int)))))),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))))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f22911,f6093])).
% 23.42/4.52 fof(f27011,plain,(
% 23.42/4.52 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,one_one(int))))),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))))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6080,f27010])).
% 23.42/4.52 fof(f27012,plain,(
% 23.42/4.52 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,one_one(int))))),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,ti(int,one_one(int)))))),m)),one_one(int))),zero_zero(int))))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f22911,f27011])).
% 23.42/4.52 fof(f27013,plain,(
% 23.42/4.52 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,one_one(int))))),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,one_one(int))))),m)),one_one(int))),zero_zero(int))))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6080,f27012])).
% 23.42/4.52 fof(f27014,plain,(
% 23.42/4.52 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,one_one(int))))),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,one_one(int))))),m)),one_one(int))),pls)))),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6431,f27013])).
% 23.42/4.52 fof(f27028,plain,(
% 23.42/4.52 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,ti(int,one_one(int)))))),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)),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f22911,f6094])).
% 23.42/4.52 fof(f27029,plain,(
% 23.42/4.52 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,one_one(int))))),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)),
% 23.42/4.52 inference(forward_demodulation,[status(thm)],[f6080,f27028])).
% 23.42/4.52 fof(f27030,plain,(
% 23.42/4.52 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,one_one(int))))),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,ti(int,one_one(int)))))),m)),one_one(int))),t)),
% 23.42/4.53 inference(forward_demodulation,[status(thm)],[f22911,f27029])).
% 23.42/4.53 fof(f27031,plain,(
% 23.42/4.53 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,one_one(int))))),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,one_one(int))))),m)),one_one(int))),pls)))),
% 23.42/4.53 inference(backward_demodulation,[status(thm)],[f27032,f27014])).
% 23.42/4.53 fof(f27032,plain,(
% 23.42/4.53 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,one_one(int))))),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,one_one(int))))),m)),one_one(int))),t)),
% 23.42/4.53 inference(forward_demodulation,[status(thm)],[f6080,f27030])).
% 23.42/4.53 fof(f30779,plain,(
% 23.42/4.53 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),ti(int,min_1))=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,one_one(int))))),one_one(int))),
% 23.42/4.53 inference(forward_demodulation,[status(thm)],[f6140,f24540])).
% 23.42/4.53 fof(f30802,plain,(
% 23.42/4.53 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),pls))),
% 23.42/4.53 inference(backward_demodulation,[status(thm)],[f30803,f24504])).
% 23.42/4.53 fof(f30803,plain,(
% 23.42/4.53 hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)=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,one_one(int))))),one_one(int))),
% 23.42/4.53 inference(forward_demodulation,[status(thm)],[f6080,f30779])).
% 23.42/4.53 fof(f32016,plain,(
% 23.42/4.53 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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,one_one(int))))),m)),one_one(int))),pls)))),
% 23.42/4.53 inference(forward_demodulation,[status(thm)],[f30803,f27031])).
% 23.42/4.53 fof(f32017,plain,(
% 23.42/4.53 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),pls)))),
% 23.42/4.53 inference(forward_demodulation,[status(thm)],[f6140,f32016])).
% 23.42/4.53 fof(f32018,plain,(
% 23.42/4.53 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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,bit0,hAPP(int,int,bit0,one_one(int)))),m)),one_one(int))),pls)))),
% 25.28/4.64 inference(forward_demodulation,[status(thm)],[f6080,f32017])).
% 25.28/4.64 fof(f32019,plain,(
% 25.28/4.64 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),m))),one_one(int))),pls)))),
% 25.28/4.64 inference(forward_demodulation,[status(thm)],[f6266,f32018])).
% 25.28/4.64 fof(f32020,plain,(
% 25.28/4.64 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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,bit0,hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),m)))),one_one(int))),pls)))),
% 25.28/4.64 inference(forward_demodulation,[status(thm)],[f6266,f32019])).
% 25.28/4.64 fof(f32021,plain,(
% 25.28/4.64 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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,bit0,hAPP(int,int,bit0,ti(int,m)))),one_one(int))),pls)))),
% 25.28/4.64 inference(forward_demodulation,[status(thm)],[f6272,f32020])).
% 25.28/4.64 fof(f32022,plain,(
% 25.28/4.64 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),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,bit0,hAPP(int,int,bit0,m))),one_one(int))),pls)))),
% 25.28/4.64 inference(forward_demodulation,[status(thm)],[f6080,f32021])).
% 25.28/4.64 fof(f32033,plain,(
% 25.28/4.64 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int)))))),
% 25.28/4.64 inference(paramodulation,[status(thm)],[f6141,f32022])).
% 25.28/4.64 fof(f32039,plain,(
% 25.28/4.64 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(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))))),min_1)),pls))),
% 25.28/4.64 inference(forward_demodulation,[status(thm)],[f6265,f32033])).
% 25.28/4.64 fof(f32040,plain,(
% 25.28/4.64 $false),
% 25.28/4.64 inference(forward_subsumption_resolution,[status(thm)],[f32039,f30802])).
% 25.28/4.64 % SZS output end CNFRefutation for theBenchmark.p
% 12.27/4.69 % Elapsed time: 4.303846 seconds
% 12.27/4.69 % CPU time: 25.689858 seconds
% 12.27/4.69 % Total memory used: 1.195 GB
% 12.27/4.69 % Net memory used: 1.187 GB
%------------------------------------------------------------------------------