%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM926+7 : 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 : n005.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 1.05s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 03:18:33 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.21/0.50 % Drodi V4.1.1
% 1.05/0.87 % Refutation found
% 1.05/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.05/0.87 % SZS output start CNFRefutation for theBenchmark
% 1.05/0.87 fof(f16,axiom,(
% 1.05/0.87 (! [X_a] :( one(X_a)=> ti(X_a,one_one(X_a)) = one_one(X_a) ) )),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f97,axiom,(
% 1.05/0.87 ti(int,t) = t ),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f98,axiom,(
% 1.05/0.87 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)) ),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f99,axiom,(
% 1.05/0.87 ( t = one_one(int)=> (? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) )) ),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f100,axiom,(
% 1.05/0.87 ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))=> (? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) )) ),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f120,axiom,(
% 1.05/0.87 (! [Z_2,W_1] :( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))<=> ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))& ti(int,Z_2) != ti(int,W_1) ) ) )),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f1150,axiom,(
% 1.05/0.87 one(int) ),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f1255,conjecture,(
% 1.05/0.87 (? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) )),
% 1.05/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.05/0.87 fof(f1256,negated_conjecture,(
% 1.05/0.87 ~((? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) ))),
% 1.05/0.87 inference(negated_conjecture,[status(cth)],[f1255])).
% 1.05/0.87 fof(f1280,plain,(
% 1.05/0.87 ![X_a]: (~one(X_a)|ti(X_a,one_one(X_a))=one_one(X_a))),
% 1.05/0.87 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 1.05/0.87 fof(f1281,plain,(
% 1.05/0.87 ![X0]: (~one(X0)|ti(X0,one_one(X0))=one_one(X0))),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f1280])).
% 1.05/0.87 fof(f1417,plain,(
% 1.05/0.87 ti(int,t)=t),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f97])).
% 1.05/0.87 fof(f1418,plain,(
% 1.05/0.87 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t))),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f98])).
% 1.05/0.87 fof(f1419,plain,(
% 1.05/0.87 ~t=one_one(int)|(?[X,Y]: hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)))),
% 1.05/0.87 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 1.05/0.87 fof(f1420,plain,(
% 1.05/0.87 ~t=one_one(int)|hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
% 1.05/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f1419])).
% 1.05/0.87 fof(f1421,plain,(
% 1.05/0.87 ~t=one_one(int)|hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f1420])).
% 1.05/0.87 fof(f1422,plain,(
% 1.05/0.87 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|(?[X,Y]: hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)))),
% 1.05/0.87 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 1.05/0.87 fof(f1423,plain,(
% 1.05/0.87 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
% 1.05/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f1422])).
% 1.05/0.87 fof(f1424,plain,(
% 1.05/0.87 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f1423])).
% 1.05/0.87 fof(f1455,plain,(
% 1.05/0.87 ![Z_2,W_1]: ((~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))|(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))&~ti(int,Z_2)=ti(int,W_1)))&(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))|(~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))|ti(int,Z_2)=ti(int,W_1))))),
% 1.05/0.87 inference(NNF_transformation,[status(thm)],[f120])).
% 1.05/0.87 fof(f1456,plain,(
% 1.05/0.87 (![Z_2,W_1]: (~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))|(hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))&~ti(int,Z_2)=ti(int,W_1))))&(![Z_2,W_1]: (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))|(~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))|ti(int,Z_2)=ti(int,W_1))))),
% 1.05/0.87 inference(miniscoping,[status(thm)],[f1455])).
% 1.05/0.87 fof(f1459,plain,(
% 1.05/0.87 ![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))),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f1456])).
% 1.05/0.87 fof(f4395,plain,(
% 1.05/0.87 one(int)),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f1150])).
% 1.05/0.87 fof(f4502,plain,(
% 1.05/0.87 (![X,Y]: ~hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)))),
% 1.05/0.87 inference(pre_NNF_transformation,[status(thm)],[f1256])).
% 1.05/0.87 fof(f4503,plain,(
% 1.05/0.87 ![X0,X1]: (~hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(bit1(pls)))))=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)))),
% 1.05/0.87 inference(cnf_transformation,[status(thm)],[f4502])).
% 1.05/0.87 fof(f5968,plain,(
% 1.05/0.87 ~t=one_one(int)),
% 1.05/0.87 inference(forward_subsumption_resolution,[status(thm)],[f1421,f4503])).
% 1.05/0.87 fof(f5969,plain,(
% 1.05/0.87 ~hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))),
% 1.05/0.87 inference(forward_subsumption_resolution,[status(thm)],[f1424,f4503])).
% 1.05/0.87 fof(f6344,plain,(
% 1.05/0.87 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|ti(int,one_one(int))=ti(int,t)),
% 1.05/0.87 inference(resolution,[status(thm)],[f1459,f1418])).
% 1.05/0.90 fof(f6352,plain,(
% 1.05/0.90 hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))|ti(int,one_one(int))=t),
% 1.05/0.90 inference(forward_demodulation,[status(thm)],[f1417,f6344])).
% 1.05/0.90 fof(f6353,plain,(
% 1.05/0.90 ti(int,one_one(int))=t),
% 1.05/0.90 inference(forward_subsumption_resolution,[status(thm)],[f6352,f5969])).
% 1.05/0.90 fof(f6557,plain,(
% 1.05/0.90 ti(int,one_one(int))=one_one(int)),
% 1.05/0.90 inference(resolution,[status(thm)],[f4395,f1281])).
% 1.05/0.90 fof(f6558,plain,(
% 1.05/0.90 t=one_one(int)),
% 1.05/0.90 inference(forward_demodulation,[status(thm)],[f6353,f6557])).
% 1.05/0.90 fof(f6559,plain,(
% 1.05/0.90 $false),
% 1.05/0.90 inference(forward_subsumption_resolution,[status(thm)],[f6558,f5968])).
% 1.05/0.90 % SZS output end CNFRefutation for theBenchmark.p
% 0.35/0.90 % Elapsed time: 0.535288 seconds
% 0.35/0.90 % CPU time: 2.919736 seconds
% 0.35/0.90 % Total memory used: 263.807 MB
% 0.35/0.90 % Net memory used: 261.713 MB
%------------------------------------------------------------------------------