%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM926+3 : 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 : n011.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 0.21s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+3 : 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.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 03:18:26 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.21/0.47 % Drodi V4.1.1
% 0.21/0.56 % Refutation found
% 0.21/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.21/0.56 fof(f1,hypothesis,(
% 0.21/0.56 is_int(one_one_int) ),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f25,axiom,(
% 0.21/0.56 is_int(t) ),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f26,axiom,(
% 0.21/0.56 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)) ),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f27,axiom,(
% 0.21/0.56 ( t = one_one_int=> (? [X,Y] :( is_int(X)& is_int(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) ) )) ),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f28,axiom,(
% 0.21/0.56 ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))=> (? [X,Y] :( is_int(X)& is_int(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) ) )) ),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f45,axiom,(
% 0.21/0.56 (! [X_26] : hAPP_int_int(times_times_int(X_26),X_26) = hAPP_nat_int(power_power_int(X_26),number_number_of_nat(bit0(bit1(pls)))) )),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f63,axiom,(
% 0.21/0.56 (! [Z_1,W_1] :( ( is_int(Z_1)& is_int(W_1) )=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_1),W_1))<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_1),W_1))& Z_1 != W_1 ) ) ) )),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f384,axiom,(
% 0.21/0.56 pls = zero_zero_int ),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f1230,conjecture,(
% 0.21/0.56 (? [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) )),
% 0.21/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.56 fof(f1231,negated_conjecture,(
% 0.21/0.56 ~((? [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) ))),
% 0.21/0.56 inference(negated_conjecture,[status(cth)],[f1230])).
% 0.21/0.56 fof(f1232,plain,(
% 0.21/0.56 is_int(one_one_int)),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f1])).
% 0.21/0.56 fof(f1272,plain,(
% 0.21/0.56 is_int(t)),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f25])).
% 0.21/0.56 fof(f1273,plain,(
% 0.21/0.56 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t))),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f26])).
% 0.21/0.56 fof(f1274,plain,(
% 0.21/0.56 ~t=one_one_int|(?[X,Y]: ((is_int(X)&is_int(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)))),
% 0.21/0.56 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.21/0.56 fof(f1275,plain,(
% 0.21/0.56 ~t=one_one_int|((is_int(sK0_skl)&is_int(sK1_skl))&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))),
% 0.21/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f1274])).
% 0.21/0.56 fof(f1278,plain,(
% 0.21/0.56 ~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)),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f1275])).
% 0.21/0.56 fof(f1279,plain,(
% 0.21/0.56 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))|(?[X,Y]: ((is_int(X)&is_int(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)))),
% 0.21/0.56 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.21/0.56 fof(f1280,plain,(
% 0.21/0.56 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))|((is_int(sK2_skl)&is_int(sK3_skl))&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))),
% 0.21/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f1279])).
% 0.21/0.56 fof(f1283,plain,(
% 0.21/0.56 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_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)),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f1280])).
% 0.21/0.56 fof(f1300,plain,(
% 0.21/0.56 ![X0]: (hAPP_int_int(times_times_int(X0),X0)=hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))))),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f45])).
% 0.21/0.56 fof(f1321,plain,(
% 0.21/0.56 ![Z_1,W_1]: ((~is_int(Z_1)|~is_int(W_1))|(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_1),W_1))<=>(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_1),W_1))&~Z_1=W_1)))),
% 0.21/0.56 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.21/0.56 fof(f1322,plain,(
% 0.21/0.56 ![Z_1,W_1]: ((~is_int(Z_1)|~is_int(W_1))|((~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_1),W_1))|(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_1),W_1))&~Z_1=W_1))&(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_1),W_1))|(~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_1),W_1))|Z_1=W_1))))),
% 0.21/0.56 inference(NNF_transformation,[status(thm)],[f1321])).
% 0.21/0.56 fof(f1325,plain,(
% 0.21/0.56 ![X0,X1]: (~is_int(X0)|~is_int(X1)|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))|~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))|X0=X1)),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f1322])).
% 0.21/0.56 fof(f2002,plain,(
% 0.21/0.56 pls=zero_zero_int),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f384])).
% 0.21/0.56 fof(f4442,plain,(
% 0.21/0.56 (![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))),
% 0.21/0.56 inference(pre_NNF_transformation,[status(thm)],[f1231])).
% 0.21/0.56 fof(f4443,plain,(
% 0.21/0.56 ![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))),
% 0.21/0.56 inference(cnf_transformation,[status(thm)],[f4442])).
% 0.21/0.56 fof(f4494,definition,(
% 0.21/0.56 sQ0_spl <=> (t=one_one_int)),
% 0.21/0.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.21/0.56 fof(f4505,definition,(
% 0.21/0.56 sQ3_spl <=> (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))),
% 0.21/0.56 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.21/0.56 fof(f4506,plain,(
% 0.21/0.56 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)|~sQ3_spl),
% 0.21/0.56 inference(component_clause,[status(thm)],[f4505])).
% 0.21/0.56 fof(f4508,plain,(
% 0.21/0.56 ~sQ0_spl|sQ3_spl),
% 0.21/0.56 inference(split_clause,[status(thm)],[f1278,f4494,f4505])).
% 0.21/0.56 fof(f4509,definition,(
% 0.21/0.56 sQ4_spl <=> (hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)))),
% 0.21/0.56 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.21/0.56 fof(f4520,definition,(
% 0.21/0.56 sQ7_spl <=> (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))),
% 0.21/0.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.21/0.56 fof(f4521,plain,(
% 0.21/0.56 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)|~sQ7_spl),
% 0.21/0.56 inference(component_clause,[status(thm)],[f4520])).
% 0.21/0.56 fof(f4523,plain,(
% 0.21/0.56 ~sQ4_spl|sQ7_spl),
% 0.21/0.56 inference(split_clause,[status(thm)],[f1283,f4509,f4520])).
% 0.21/0.56 fof(f4573,plain,(
% 0.21/0.56 ![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(zero_zero_int))))),m)),one_one_int))),
% 0.21/0.56 inference(backward_demodulation,[status(thm)],[f2002,f4443])).
% 0.21/0.56 fof(f4574,plain,(
% 0.21/0.56 ![X0,X1]: (~hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int))))),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(zero_zero_int))))),m)),one_one_int))),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f4573])).
% 0.21/0.56 fof(f4575,plain,(
% 0.21/0.56 ![X0,X1]: (~hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(zero_zero_int)))))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(zero_zero_int))))),m)),one_one_int))),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f4574])).
% 0.21/0.56 fof(f4739,plain,(
% 0.21/0.56 ![X0]: (hAPP_int_int(times_times_int(X0),X0)=hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int)))))),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f1300])).
% 0.21/0.56 fof(f4756,plain,(
% 0.21/0.56 ![X0,X1]: (~hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int))))),hAPP_int_int(times_times_int(X1),X1))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(zero_zero_int))))),m)),one_one_int))),
% 0.21/0.56 inference(paramodulation,[status(thm)],[f4739,f4575])).
% 0.21/0.56 fof(f4884,plain,(
% 0.21/0.56 ![X0,X1]: (~hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(X0),X0)),hAPP_int_int(times_times_int(X1),X1))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(zero_zero_int))))),m)),one_one_int))),
% 0.21/0.56 inference(paramodulation,[status(thm)],[f4739,f4756])).
% 0.21/0.56 fof(f5371,definition,(
% 0.21/0.56 sQ12_spl <=> (is_int(t))),
% 0.21/0.56 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.21/0.56 fof(f5373,plain,(
% 0.21/0.56 ~is_int(t)|sQ12_spl),
% 0.21/0.56 inference(component_clause,[status(thm)],[f5371])).
% 0.21/0.56 fof(f5429,plain,(
% 0.21/0.56 ~is_int(one_one_int)|~is_int(t)|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))|one_one_int=t),
% 0.21/0.56 inference(resolution,[status(thm)],[f1325,f1273])).
% 0.21/0.56 fof(f5435,definition,(
% 0.21/0.56 sQ15_spl <=> (is_int(one_one_int))),
% 0.21/0.56 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.21/0.56 fof(f5437,plain,(
% 0.21/0.56 ~is_int(one_one_int)|sQ15_spl),
% 0.21/0.56 inference(component_clause,[status(thm)],[f5435])).
% 0.21/0.56 fof(f5438,plain,(
% 0.21/0.56 ~sQ15_spl|~sQ12_spl|sQ4_spl|sQ0_spl),
% 0.21/0.56 inference(split_clause,[status(thm)],[f5429,f5435,f5371,f4509,f4494])).
% 0.21/0.56 fof(f5439,plain,(
% 0.21/0.56 $false|sQ12_spl),
% 0.21/0.56 inference(forward_subsumption_resolution,[status(thm)],[f5373,f1272])).
% 0.21/0.56 fof(f5440,plain,(
% 0.21/0.56 sQ12_spl),
% 0.21/0.56 inference(contradiction_clause,[status(thm)],[f5439])).
% 0.21/0.56 fof(f5441,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK0_skl),number_number_of_nat(bit0(bit1(zero_zero_int))))),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)|~sQ3_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f4506])).
% 0.21/0.56 fof(f5442,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK0_skl),sK0_skl)),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)|~sQ3_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f4739,f5441])).
% 0.21/0.56 fof(f5443,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK0_skl),sK0_skl)),hAPP_nat_int(power_power_int(sK1_skl),number_number_of_nat(bit0(bit1(zero_zero_int)))))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)|~sQ3_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f5442])).
% 0.21/0.56 fof(f5444,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK0_skl),sK0_skl)),hAPP_int_int(times_times_int(sK1_skl),sK1_skl))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)|~sQ3_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f4739,f5443])).
% 0.21/0.56 fof(f5445,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK0_skl),sK0_skl)),hAPP_int_int(times_times_int(sK1_skl),sK1_skl))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(zero_zero_int))))),m)),one_one_int)|~sQ3_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f5444])).
% 0.21/0.56 fof(f5446,plain,(
% 0.21/0.56 $false|~sQ3_spl),
% 0.21/0.56 inference(forward_subsumption_resolution,[status(thm)],[f5445,f4884])).
% 0.21/0.56 fof(f5447,plain,(
% 0.21/0.56 ~sQ3_spl),
% 0.21/0.56 inference(contradiction_clause,[status(thm)],[f5446])).
% 0.21/0.56 fof(f5448,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK2_skl),number_number_of_nat(bit0(bit1(zero_zero_int))))),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)|~sQ7_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f2002,f4521])).
% 0.21/0.56 fof(f5449,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK2_skl),sK2_skl)),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)|~sQ7_spl),
% 0.21/0.56 inference(forward_demodulation,[status(thm)],[f4739,f5448])).
% 0.21/0.56 fof(f5450,plain,(
% 0.21/0.56 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK2_skl),sK2_skl)),hAPP_nat_int(power_power_int(sK3_skl),number_number_of_nat(bit0(bit1(zero_zero_int)))))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)|~sQ7_spl),
% 0.21/0.57 inference(forward_demodulation,[status(thm)],[f2002,f5449])).
% 0.21/0.57 fof(f5451,plain,(
% 0.21/0.57 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK2_skl),sK2_skl)),hAPP_int_int(times_times_int(sK3_skl),sK3_skl))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)|~sQ7_spl),
% 0.21/0.57 inference(forward_demodulation,[status(thm)],[f4739,f5450])).
% 0.21/0.57 fof(f5452,plain,(
% 0.21/0.57 hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(sK2_skl),sK2_skl)),hAPP_int_int(times_times_int(sK3_skl),sK3_skl))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(zero_zero_int))))),m)),one_one_int)|~sQ7_spl),
% 0.21/0.57 inference(forward_demodulation,[status(thm)],[f2002,f5451])).
% 0.21/0.57 fof(f5453,plain,(
% 0.21/0.57 $false|~sQ7_spl),
% 0.21/0.57 inference(forward_subsumption_resolution,[status(thm)],[f5452,f4884])).
% 0.21/0.57 fof(f5454,plain,(
% 0.21/0.57 ~sQ7_spl),
% 0.21/0.57 inference(contradiction_clause,[status(thm)],[f5453])).
% 0.21/0.57 fof(f5460,plain,(
% 0.21/0.57 $false|sQ15_spl),
% 0.21/0.57 inference(forward_subsumption_resolution,[status(thm)],[f5437,f1232])).
% 0.21/0.57 fof(f5461,plain,(
% 0.21/0.57 sQ15_spl),
% 0.21/0.57 inference(contradiction_clause,[status(thm)],[f5460])).
% 0.21/0.57 fof(f5462,plain,(
% 0.21/0.57 $false),
% 0.21/0.57 inference(sat_refutation,[status(thm)],[f4508,f4523,f5438,f5440,f5447,f5454,f5461])).
% 0.21/0.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.59 % Elapsed time: 0.208961 seconds
% 0.21/0.59 % CPU time: 0.655904 seconds
% 0.21/0.59 % Total memory used: 167.606 MB
% 0.21/0.59 % Net memory used: 166.667 MB
%------------------------------------------------------------------------------