%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM925+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 : n012.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:07 PM UTC 2026
% Result : Theorem 10.50s 2.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM925+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Mon Sep 21 03:17:52 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.43/0.78 % Drodi V4.1.1
% 10.50/2.12 % Refutation found
% 10.50/2.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.50/2.12 % SZS output start CNFRefutation for theBenchmark
% 10.50/2.12 fof(f106,hypothesis,(
% 10.50/2.12 ti(int,pls) = pls ),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f309,axiom,(
% 10.50/2.12 (! [Na] :( hAPP(nat,int,semiring_1_of_nat(int),Na) = zero_zero(int)<=> Na = zero_zero(nat) ) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f314,axiom,(
% 10.50/2.12 ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f325,axiom,(
% 10.50/2.12 (! [K,L] :( hAPP(int,int,bit0,K) = hAPP(int,int,bit0,L)<=> ti(int,K) = ti(int,L) ) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f327,axiom,(
% 10.50/2.12 (! [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)) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f354,axiom,(
% 10.50/2.12 hAPP(int,int,bit0,pls) = pls ),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f358,axiom,(
% 10.50/2.12 pls = zero_zero(int) ),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f360,axiom,(
% 10.50/2.12 (! [K_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),pls) = ti(int,K_4) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f363,axiom,(
% 10.50/2.12 (! [K_4] : hAPP(int,int,bit0,K_4) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),K_4) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f375,axiom,(
% 10.50/2.12 (! [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)) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f377,axiom,(
% 10.50/2.12 (! [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) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f555,axiom,(
% 10.50/2.12 (! [Va] :( hAPP(int,nat,number_number_of(nat),Va) = zero_zero(nat)<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Va),pls)) ) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f565,axiom,(
% 10.50/2.12 (! [Na] :( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),Na)),zero_zero(int)))<=> Na = zero_zero(nat) ) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f594,axiom,(
% 10.50/2.12 (! [X] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X),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)))))) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f1732,axiom,(
% 10.50/2.12 (! [M] : hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,suc,M)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),M)) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f2356,axiom,(
% 10.50/2.12 (! [Na,Ma] :( hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),Na)) = hAPP(nat,int,semiring_1_of_nat(int),Ma)<=> ( Na = zero_zero(nat)& Ma = zero_zero(nat) ) ) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f2377,axiom,(
% 10.50/2.12 (! [N] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,suc,N)))),zero_zero(int))) )),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f5747,conjecture,(
% 10.50/2.12 hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != zero_zero(int) ),
% 10.50/2.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.50/2.12 fof(f5748,negated_conjecture,(
% 10.50/2.12 ~(hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != zero_zero(int) )),
% 10.50/2.12 inference(negated_conjecture,[status(cth)],[f5747])).
% 10.50/2.12 fof(f5887,plain,(
% 10.50/2.12 ti(int,pls)=pls),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f106])).
% 10.50/2.12 fof(f6163,plain,(
% 10.50/2.12 ![Na]: ((~hAPP(nat,int,semiring_1_of_nat(int),Na)=zero_zero(int)|Na=zero_zero(nat))&(hAPP(nat,int,semiring_1_of_nat(int),Na)=zero_zero(int)|~Na=zero_zero(nat)))),
% 10.50/2.12 inference(NNF_transformation,[status(thm)],[f309])).
% 10.50/2.12 fof(f6164,plain,(
% 10.50/2.12 (![Na]: (~hAPP(nat,int,semiring_1_of_nat(int),Na)=zero_zero(int)|Na=zero_zero(nat)))&(![Na]: (hAPP(nat,int,semiring_1_of_nat(int),Na)=zero_zero(int)|~Na=zero_zero(nat)))),
% 10.50/2.12 inference(miniscoping,[status(thm)],[f6163])).
% 10.50/2.12 fof(f6166,plain,(
% 10.50/2.12 ![X0]: (hAPP(nat,int,semiring_1_of_nat(int),X0)=zero_zero(int)|~X0=zero_zero(nat))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f6164])).
% 10.50/2.12 fof(f6177,plain,(
% 10.50/2.12 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f314])).
% 10.50/2.12 fof(f6211,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(NNF_transformation,[status(thm)],[f325])).
% 10.50/2.12 fof(f6212,plain,(
% 10.50/2.12 (![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)))),
% 10.50/2.12 inference(miniscoping,[status(thm)],[f6211])).
% 10.50/2.12 fof(f6214,plain,(
% 10.50/2.12 ![X0,X1]: (hAPP(int,int,bit0,X0)=hAPP(int,int,bit0,X1)|~ti(int,X0)=ti(int,X1))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f6212])).
% 10.50/2.12 fof(f6220,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f327])).
% 10.50/2.12 fof(f6304,plain,(
% 10.50/2.12 hAPP(int,int,bit0,pls)=pls),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f354])).
% 10.50/2.12 fof(f6313,plain,(
% 10.50/2.12 pls=zero_zero(int)),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f358])).
% 10.50/2.12 fof(f6315,plain,(
% 10.50/2.12 ![X0]: (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)=ti(int,X0))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f360])).
% 10.50/2.12 fof(f6318,plain,(
% 10.50/2.12 ![X0]: (hAPP(int,int,bit0,X0)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X0))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f363])).
% 10.50/2.12 fof(f6343,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f375])).
% 10.50/2.12 fof(f6345,plain,(
% 10.50/2.12 ![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))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f377])).
% 10.50/2.12 fof(f6888,plain,(
% 10.50/2.12 ![Va]: ((~hAPP(int,nat,number_number_of(nat),Va)=zero_zero(nat)|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Va),pls)))&(hAPP(int,nat,number_number_of(nat),Va)=zero_zero(nat)|~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Va),pls))))),
% 10.50/2.12 inference(NNF_transformation,[status(thm)],[f555])).
% 10.50/2.12 fof(f6889,plain,(
% 10.50/2.12 (![Va]: (~hAPP(int,nat,number_number_of(nat),Va)=zero_zero(nat)|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Va),pls))))&(![Va]: (hAPP(int,nat,number_number_of(nat),Va)=zero_zero(nat)|~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Va),pls))))),
% 10.50/2.12 inference(miniscoping,[status(thm)],[f6888])).
% 10.50/2.12 fof(f6890,plain,(
% 10.50/2.12 ![X0]: (~hAPP(int,nat,number_number_of(nat),X0)=zero_zero(nat)|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),pls)))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f6889])).
% 10.50/2.12 fof(f6891,plain,(
% 10.50/2.12 ![X0]: (hAPP(int,nat,number_number_of(nat),X0)=zero_zero(nat)|~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),pls)))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f6889])).
% 10.50/2.12 fof(f6929,plain,(
% 10.50/2.12 ![Na]: ((~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),Na)),zero_zero(int)))|Na=zero_zero(nat))&(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),Na)),zero_zero(int)))|~Na=zero_zero(nat)))),
% 10.50/2.12 inference(NNF_transformation,[status(thm)],[f565])).
% 10.50/2.12 fof(f6930,plain,(
% 10.50/2.12 (![Na]: (~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),Na)),zero_zero(int)))|Na=zero_zero(nat)))&(![Na]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),Na)),zero_zero(int)))|~Na=zero_zero(nat)))),
% 10.50/2.12 inference(miniscoping,[status(thm)],[f6929])).
% 10.50/2.12 fof(f6931,plain,(
% 10.50/2.12 ![X0]: (~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),X0)),zero_zero(int)))|X0=zero_zero(nat))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f6930])).
% 10.50/2.12 fof(f7000,plain,(
% 10.50/2.12 ![X0]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f594])).
% 10.50/2.12 fof(f10296,plain,(
% 10.50/2.12 ![X0]: (hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,suc,X0))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),X0)))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f1732])).
% 10.50/2.12 fof(f12283,plain,(
% 10.50/2.12 ![Na,Ma]: ((~hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),Na))=hAPP(nat,int,semiring_1_of_nat(int),Ma)|(Na=zero_zero(nat)&Ma=zero_zero(nat)))&(hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),Na))=hAPP(nat,int,semiring_1_of_nat(int),Ma)|(~Na=zero_zero(nat)|~Ma=zero_zero(nat))))),
% 10.50/2.12 inference(NNF_transformation,[status(thm)],[f2356])).
% 10.50/2.12 fof(f12284,plain,(
% 10.50/2.12 (![Na,Ma]: (~hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),Na))=hAPP(nat,int,semiring_1_of_nat(int),Ma)|(Na=zero_zero(nat)&Ma=zero_zero(nat))))&(![Na,Ma]: (hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),Na))=hAPP(nat,int,semiring_1_of_nat(int),Ma)|(~Na=zero_zero(nat)|~Ma=zero_zero(nat))))),
% 10.50/2.12 inference(miniscoping,[status(thm)],[f12283])).
% 10.50/2.12 fof(f12287,plain,(
% 10.50/2.12 ![X0,X1]: (hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),X0))=hAPP(nat,int,semiring_1_of_nat(int),X1)|~X0=zero_zero(nat)|~X1=zero_zero(nat))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f12284])).
% 10.50/2.12 fof(f12325,plain,(
% 10.50/2.12 ![X0]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,suc,X0)))),zero_zero(int))))),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f2377])).
% 10.50/2.12 fof(f20963,plain,(
% 10.50/2.12 hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))=zero_zero(int)),
% 10.50/2.12 inference(cnf_transformation,[status(thm)],[f5748])).
% 10.50/2.12 fof(f21469,plain,(
% 10.50/2.12 hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat))=zero_zero(int)),
% 10.50/2.12 inference(destructive_equality_resolution,[status(thm)],[f6166])).
% 10.50/2.12 fof(f21587,plain,(
% 10.50/2.12 hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat)))=hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat))),
% 10.50/2.12 inference(destructive_equality_resolution,[status(thm)],[f12287])).
% 10.50/2.12 fof(f21717,plain,(
% 10.50/2.12 hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))=pls),
% 10.50/2.12 inference(backward_demodulation,[status(thm)],[f6313,f20963])).
% 10.50/2.12 fof(f21746,plain,(
% 10.50/2.12 hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat))=pls),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6313,f21469])).
% 10.50/2.12 fof(f22101,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(paramodulation,[status(thm)],[f6304,f6343])).
% 10.50/2.12 fof(f22107,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6315,f22101])).
% 10.50/2.12 fof(f22108,plain,(
% 10.50/2.12 ![X0]: (ti(int,hAPP(int,int,bit1,X0))=hAPP(int,int,bit1,ti(int,X0)))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6315,f22107])).
% 10.50/2.12 fof(f22119,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6220,f6345])).
% 10.50/2.12 fof(f22120,plain,(
% 10.50/2.12 ![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)))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6318,f22119])).
% 10.50/2.12 fof(f22121,plain,(
% 10.50/2.12 hAPP(int,int,bit1,pls)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),pls)),
% 10.50/2.12 inference(paramodulation,[status(thm)],[f6304,f22120])).
% 10.50/2.12 fof(f22125,plain,(
% 10.50/2.12 hAPP(int,int,bit1,pls)=ti(int,one_one(int))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6315,f22121])).
% 10.50/2.12 fof(f22138,plain,(
% 10.50/2.12 hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))=pls),
% 10.50/2.12 inference(backward_demodulation,[status(thm)],[f22125,f21717])).
% 10.50/2.12 fof(f22407,plain,(
% 10.50/2.12 ti(int,ti(int,one_one(int)))=hAPP(int,int,bit1,ti(int,pls))),
% 10.50/2.12 inference(paramodulation,[status(thm)],[f22125,f22108])).
% 10.50/2.12 fof(f22413,plain,(
% 10.50/2.12 ti(int,ti(int,one_one(int)))=hAPP(int,int,bit1,pls)),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f5887,f22407])).
% 10.50/2.12 fof(f22414,plain,(
% 10.50/2.12 ti(int,ti(int,one_one(int)))=ti(int,one_one(int))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f22125,f22413])).
% 10.50/2.12 fof(f22423,plain,(
% 10.50/2.12 hAPP(int,int,bit0,ti(int,one_one(int)))=hAPP(int,int,bit0,one_one(int))),
% 10.50/2.12 inference(resolution,[status(thm)],[f22414,f6214])).
% 10.50/2.12 fof(f22706,plain,(
% 10.50/2.12 hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))=pls),
% 10.50/2.12 inference(backward_demodulation,[status(thm)],[f22423,f22138])).
% 10.50/2.12 fof(f23024,plain,(
% 10.50/2.12 ![X0]: (~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),X0)),pls))|X0=zero_zero(nat))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f6313,f6931])).
% 10.50/2.12 fof(f23025,plain,(
% 10.50/2.12 ![X0]: (X0=zero_zero(nat)|~hAPP(int,nat,number_number_of(nat),hAPP(nat,int,semiring_1_of_nat(int),X0))=zero_zero(nat))),
% 10.50/2.12 inference(resolution,[status(thm)],[f23024,f6890])).
% 10.50/2.12 fof(f23163,plain,(
% 10.50/2.12 ![X0]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),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))))))))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f22125,f7000])).
% 10.50/2.12 fof(f23164,plain,(
% 10.50/2.12 ![X0]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),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)))))))),
% 10.50/2.12 inference(forward_demodulation,[status(thm)],[f22423,f23163])).
% 10.50/2.12 fof(f23181,plain,(
% 10.50/2.12 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),pls))),
% 10.50/2.12 inference(paramodulation,[status(thm)],[f22706,f23164])).
% 10.50/2.12 fof(f23206,plain,(
% 10.50/2.12 hAPP(int,nat,number_number_of(nat),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))=zero_zero(nat)),
% 10.50/2.12 inference(resolution,[status(thm)],[f23181,f6891])).
% 10.50/2.12 fof(f28663,plain,(
% 10.50/2.12 hAPP(int,nat,number_number_of(nat),hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,suc,n)))=zero_zero(nat)),
% 9.39/2.22 inference(backward_demodulation,[status(thm)],[f10296,f23206])).
% 9.39/2.22 fof(f28855,plain,(
% 9.39/2.22 hAPP(nat,nat,suc,n)=zero_zero(nat)),
% 9.39/2.22 inference(resolution,[status(thm)],[f28663,f23025])).
% 9.39/2.22 fof(f28973,plain,(
% 9.39/2.22 hAPP(int,int,uminus_uminus(int),pls)=hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat))),
% 9.39/2.22 inference(forward_demodulation,[status(thm)],[f21746,f21587])).
% 9.39/2.22 fof(f28974,plain,(
% 9.39/2.22 hAPP(int,int,uminus_uminus(int),pls)=pls),
% 9.39/2.22 inference(forward_demodulation,[status(thm)],[f21746,f28973])).
% 9.39/2.22 fof(f29407,plain,(
% 9.39/2.22 ![X0]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,suc,X0)))),pls)))),
% 9.39/2.22 inference(forward_demodulation,[status(thm)],[f6313,f12325])).
% 9.39/2.22 fof(f29421,plain,(
% 9.39/2.22 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,uminus_uminus(int),hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat)))),pls))),
% 9.39/2.22 inference(paramodulation,[status(thm)],[f28855,f29407])).
% 9.39/2.22 fof(f29427,plain,(
% 9.39/2.22 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,uminus_uminus(int),pls)),pls))),
% 9.39/2.22 inference(forward_demodulation,[status(thm)],[f21746,f29421])).
% 9.39/2.22 fof(f29428,plain,(
% 9.39/2.22 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls))),
% 9.39/2.22 inference(forward_demodulation,[status(thm)],[f28974,f29427])).
% 9.39/2.22 fof(f29429,plain,(
% 9.39/2.22 $false),
% 9.39/2.22 inference(forward_subsumption_resolution,[status(thm)],[f29428,f6177])).
% 9.39/2.22 % SZS output end CNFRefutation for theBenchmark.p
% 9.39/2.25 % Elapsed time: 1.928461 seconds
% 9.39/2.25 % CPU time: 11.485947 seconds
% 9.39/2.25 % Total memory used: 1.183 GB
% 9.39/2.25 % Net memory used: 1.171 GB
%------------------------------------------------------------------------------