%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:08 PM UTC 2026
% Result : Theorem 9.70s 2.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 03:20:15 UTC 2026
% 0.11/0.38 % CPUTime :
% 1.25/1.51 % Drodi V4.1.1
% 9.70/2.66 % Refutation found
% 9.70/2.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.70/2.66 % SZS output start CNFRefutation for theBenchmark
% 9.70/2.66 fof(f106,hypothesis,(
% 9.70/2.66 ti(int,pls) = pls ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f265,axiom,(
% 9.70/2.66 (! [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) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f272,axiom,(
% 9.70/2.66 ti(int,t) = t ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f273,axiom,(
% 9.70/2.66 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)) ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f274,axiom,(
% 9.70/2.66 ( 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)) )) ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f275,axiom,(
% 9.70/2.66 ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,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)) )) ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f295,axiom,(
% 9.70/2.66 (! [Z,W_1] :( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1))<=> ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))& ti(int,Z) != ti(int,W_1) ) ) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f359,axiom,(
% 9.70/2.66 (! [K,L] :( hAPP(int,int,bit0,K) = hAPP(int,int,bit0,L)<=> ti(int,K) = ti(int,L) ) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f362,axiom,(
% 9.70/2.66 (! [K_4] : hAPP(int,int,number_number_of(int),K_4) = ti(int,K_4) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f363,axiom,(
% 9.70/2.66 (! [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)) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f396,axiom,(
% 9.70/2.66 hAPP(int,int,bit0,pls) = pls ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f399,axiom,(
% 9.70/2.66 (! [K_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),pls) = ti(int,K_4) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f402,axiom,(
% 9.70/2.66 (! [K_4] : hAPP(int,int,bit0,K_4) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),K_4) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f425,axiom,(
% 9.70/2.66 (! [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)) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f427,axiom,(
% 9.70/2.66 (! [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) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f431,axiom,(
% 9.70/2.66 (! [X_a] :( number_semiring(X_a)=> hAPP(int,X_a,number_number_of(X_a),hAPP(int,int,bit1,pls)) = one_one(X_a) ) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f5308,axiom,(
% 9.70/2.66 number_semiring(int) ),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f5738,conjecture,(
% 9.70/2.66 (? [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)) )),
% 9.70/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.70/2.66 fof(f5739,negated_conjecture,(
% 9.70/2.66 ~((? [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)) ))),
% 9.70/2.66 inference(negated_conjecture,[status(cth)],[f5738])).
% 9.70/2.66 fof(f5878,plain,(
% 9.70/2.66 ti(int,pls)=pls),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f106])).
% 9.70/2.66 fof(f6080,plain,(
% 9.70/2.66 ![X0,X1,X2,X3]: (hAPP(X0,X1,X2,ti(X0,X3))=hAPP(X0,X1,X2,X3))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f265])).
% 9.70/2.66 fof(f6090,plain,(
% 9.70/2.66 ti(int,t)=t),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f272])).
% 9.70/2.66 fof(f6091,plain,(
% 9.70/2.66 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f273])).
% 9.70/2.66 fof(f6092,plain,(
% 9.70/2.66 ~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)))),
% 9.70/2.66 inference(pre_NNF_transformation,[status(thm)],[f274])).
% 9.70/2.66 fof(f6093,plain,(
% 9.70/2.66 ~t=one_one(int)|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))),
% 9.70/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f6092])).
% 9.70/2.66 fof(f6094,plain,(
% 9.70/2.66 ~t=one_one(int)|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))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f6093])).
% 9.70/2.66 fof(f6095,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,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)))),
% 9.70/2.66 inference(pre_NNF_transformation,[status(thm)],[f275])).
% 9.70/2.66 fof(f6096,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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))),
% 9.70/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f6095])).
% 9.70/2.66 fof(f6097,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f6096])).
% 9.70/2.66 fof(f6128,plain,(
% 9.70/2.66 ![Z,W_1]: ((~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1))|(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))&~ti(int,Z)=ti(int,W_1)))&(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1))|(~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))|ti(int,Z)=ti(int,W_1))))),
% 9.70/2.66 inference(NNF_transformation,[status(thm)],[f295])).
% 9.70/2.66 fof(f6129,plain,(
% 9.70/2.66 (![Z,W_1]: (~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1))|(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))&~ti(int,Z)=ti(int,W_1))))&(![Z,W_1]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1))|(~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))|ti(int,Z)=ti(int,W_1))))),
% 9.70/2.66 inference(miniscoping,[status(thm)],[f6128])).
% 9.70/2.66 fof(f6132,plain,(
% 9.70/2.66 ![X0,X1]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1))|~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))|ti(int,X0)=ti(int,X1))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f6129])).
% 9.70/2.66 fof(f6311,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(NNF_transformation,[status(thm)],[f359])).
% 9.70/2.66 fof(f6312,plain,(
% 9.70/2.66 (![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)))),
% 9.70/2.66 inference(miniscoping,[status(thm)],[f6311])).
% 9.70/2.66 fof(f6314,plain,(
% 9.70/2.66 ![X0,X1]: (hAPP(int,int,bit0,X0)=hAPP(int,int,bit0,X1)|~ti(int,X0)=ti(int,X1))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f6312])).
% 9.70/2.66 fof(f6317,plain,(
% 9.70/2.66 ![X0]: (hAPP(int,int,number_number_of(int),X0)=ti(int,X0))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f362])).
% 9.70/2.66 fof(f6318,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f363])).
% 9.70/2.66 fof(f6424,plain,(
% 9.70/2.66 hAPP(int,int,bit0,pls)=pls),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f396])).
% 9.70/2.66 fof(f6427,plain,(
% 9.70/2.66 ![X0]: (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)=ti(int,X0))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f399])).
% 9.70/2.66 fof(f6430,plain,(
% 9.70/2.66 ![X0]: (hAPP(int,int,bit0,X0)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X0))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f402])).
% 9.70/2.66 fof(f6470,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f425])).
% 9.70/2.66 fof(f6472,plain,(
% 9.70/2.66 ![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))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f427])).
% 9.70/2.66 fof(f6479,plain,(
% 9.70/2.66 ![X_a]: (~number_semiring(X_a)|hAPP(int,X_a,number_number_of(X_a),hAPP(int,int,bit1,pls))=one_one(X_a))),
% 9.70/2.66 inference(pre_NNF_transformation,[status(thm)],[f431])).
% 9.70/2.66 fof(f6480,plain,(
% 9.70/2.66 ![X0]: (~number_semiring(X0)|hAPP(int,X0,number_number_of(X0),hAPP(int,int,bit1,pls))=one_one(X0))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f6479])).
% 9.70/2.66 fof(f20535,plain,(
% 9.70/2.66 number_semiring(int)),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f5308])).
% 9.70/2.66 fof(f20976,plain,(
% 9.70/2.66 (![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)))),
% 9.70/2.66 inference(pre_NNF_transformation,[status(thm)],[f5739])).
% 9.70/2.66 fof(f20977,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(cnf_transformation,[status(thm)],[f20976])).
% 9.70/2.66 fof(f22806,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(paramodulation,[status(thm)],[f6424,f6470])).
% 9.70/2.66 fof(f22812,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6427,f22806])).
% 9.70/2.66 fof(f22813,plain,(
% 9.70/2.66 ![X0]: (ti(int,hAPP(int,int,bit1,X0))=hAPP(int,int,bit1,ti(int,X0)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6427,f22812])).
% 9.70/2.66 fof(f22833,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6318,f6472])).
% 9.70/2.66 fof(f22834,plain,(
% 9.70/2.66 ![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)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6430,f22833])).
% 9.70/2.66 fof(f22835,plain,(
% 9.70/2.66 hAPP(int,int,bit1,pls)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),pls)),
% 9.70/2.66 inference(paramodulation,[status(thm)],[f6424,f22834])).
% 9.70/2.66 fof(f22839,plain,(
% 9.70/2.66 hAPP(int,int,bit1,pls)=ti(int,one_one(int))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6427,f22835])).
% 9.70/2.66 fof(f23004,plain,(
% 9.70/2.66 ![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,ti(int,one_one(int)))))),m)),one_one(int)))),
% 9.70/2.66 inference(backward_demodulation,[status(thm)],[f22839,f20977])).
% 9.70/2.66 fof(f23073,plain,(
% 9.70/2.66 ![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,ti(int,one_one(int)))))),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,ti(int,one_one(int)))))),m)),one_one(int)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f23004])).
% 9.70/2.66 fof(f23074,plain,(
% 9.70/2.66 ![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,ti(int,one_one(int)))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(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)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f23073])).
% 9.70/2.66 fof(f23373,plain,(
% 9.70/2.66 ti(int,ti(int,one_one(int)))=hAPP(int,int,bit1,ti(int,pls))),
% 9.70/2.66 inference(paramodulation,[status(thm)],[f22839,f22813])).
% 9.70/2.66 fof(f23383,plain,(
% 9.70/2.66 ti(int,ti(int,one_one(int)))=hAPP(int,int,bit1,pls)),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f5878,f23373])).
% 9.70/2.66 fof(f23384,plain,(
% 9.70/2.66 ti(int,ti(int,one_one(int)))=ti(int,one_one(int))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f23383])).
% 9.70/2.66 fof(f23457,plain,(
% 9.70/2.66 hAPP(int,int,bit0,ti(int,one_one(int)))=hAPP(int,int,bit0,one_one(int))),
% 9.70/2.66 inference(resolution,[status(thm)],[f23384,f6314])).
% 9.70/2.66 fof(f24156,plain,(
% 9.70/2.66 ![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,ti(int,one_one(int)))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(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)))),
% 9.70/2.66 inference(backward_demodulation,[status(thm)],[f23457,f23074])).
% 9.70/2.66 fof(f24216,plain,(
% 9.70/2.66 ![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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(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)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f23457,f24156])).
% 9.70/2.66 fof(f24217,plain,(
% 9.70/2.66 ![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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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)))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f23457,f24216])).
% 9.70/2.66 fof(f25469,plain,(
% 9.70/2.66 ~t=one_one(int)|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,ti(int,one_one(int)))))),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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f6094])).
% 9.70/2.66 fof(f25470,plain,(
% 9.70/2.66 ~t=one_one(int)|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,one_one(int))))),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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6080,f25469])).
% 9.70/2.66 fof(f25471,plain,(
% 9.70/2.66 ~t=one_one(int)|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f25470])).
% 9.70/2.66 fof(f25472,plain,(
% 9.70/2.66 ~t=one_one(int)|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6080,f25471])).
% 9.70/2.66 fof(f25473,plain,(
% 9.70/2.66 ~t=one_one(int)|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f25472])).
% 9.70/2.66 fof(f25474,plain,(
% 9.70/2.66 ~t=one_one(int)|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6080,f25473])).
% 9.70/2.66 fof(f25475,plain,(
% 9.70/2.66 ~t=one_one(int)),
% 9.70/2.66 inference(forward_subsumption_resolution,[status(thm)],[f25474,f24217])).
% 9.70/2.66 fof(f25476,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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,ti(int,one_one(int)))))),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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f6097])).
% 9.70/2.66 fof(f25477,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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,one_one(int))))),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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6080,f25476])).
% 9.70/2.66 fof(f25478,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f25477])).
% 9.70/2.66 fof(f25479,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f6080,f25478])).
% 9.70/2.66 fof(f25480,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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))),
% 9.70/2.66 inference(forward_demodulation,[status(thm)],[f22839,f25479])).
% 9.70/2.66 fof(f25481,plain,(
% 9.70/2.66 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|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,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(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))),
% 8.89/2.75 inference(forward_demodulation,[status(thm)],[f6080,f25480])).
% 8.89/2.75 fof(f25482,plain,(
% 8.89/2.75 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))),
% 8.89/2.75 inference(forward_subsumption_resolution,[status(thm)],[f25481,f24217])).
% 8.89/2.75 fof(f26056,plain,(
% 8.89/2.75 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|ti(int,one_one(int))=ti(int,t)),
% 8.89/2.75 inference(resolution,[status(thm)],[f6132,f6091])).
% 8.89/2.75 fof(f26066,plain,(
% 8.89/2.75 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|ti(int,one_one(int))=t),
% 8.89/2.75 inference(forward_demodulation,[status(thm)],[f6090,f26056])).
% 8.89/2.75 fof(f26067,plain,(
% 8.89/2.75 ti(int,one_one(int))=t),
% 8.89/2.75 inference(forward_subsumption_resolution,[status(thm)],[f26066,f25482])).
% 8.89/2.75 fof(f26313,plain,(
% 8.89/2.75 hAPP(int,int,bit1,pls)=t),
% 8.89/2.75 inference(backward_demodulation,[status(thm)],[f26067,f22839])).
% 8.89/2.75 fof(f28965,plain,(
% 8.89/2.75 ![X0]: (~number_semiring(X0)|hAPP(int,X0,number_number_of(X0),t)=one_one(X0))),
% 8.89/2.75 inference(forward_demodulation,[status(thm)],[f26313,f6480])).
% 8.89/2.75 fof(f28968,plain,(
% 8.89/2.75 hAPP(int,int,number_number_of(int),t)=one_one(int)),
% 8.89/2.75 inference(resolution,[status(thm)],[f28965,f20535])).
% 8.89/2.75 fof(f28969,plain,(
% 8.89/2.75 ti(int,t)=one_one(int)),
% 8.89/2.75 inference(forward_demodulation,[status(thm)],[f6317,f28968])).
% 8.89/2.75 fof(f28970,plain,(
% 8.89/2.75 t=one_one(int)),
% 8.89/2.75 inference(forward_demodulation,[status(thm)],[f6090,f28969])).
% 8.89/2.75 fof(f28971,plain,(
% 8.89/2.75 $false),
% 8.89/2.75 inference(forward_subsumption_resolution,[status(thm)],[f28970,f25475])).
% 8.89/2.75 % SZS output end CNFRefutation for theBenchmark.p
% 1.62/2.82 % Elapsed time: 2.417885 seconds
% 1.62/2.82 % CPU time: 10.448539 seconds
% 1.62/2.82 % Total memory used: 1.025 GB
% 1.62/2.82 % Net memory used: 1.019 GB
%------------------------------------------------------------------------------