%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM926+4 : 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 : n007.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 7.50s 1.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40 % Computer : n007.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 21 03:16:05 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.63/0.90 % Drodi V4.1.1
% 7.50/1.84 % Refutation found
% 7.50/1.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.50/1.84 % SZS output start CNFRefutation for theBenchmark
% 7.50/1.84 fof(f6,hypothesis,(
% 7.50/1.84 is_int(one_one_int) ),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f59,axiom,(
% 7.50/1.84 is_int(t) ),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f60,axiom,(
% 7.50/1.84 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)) ),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f61,axiom,(
% 7.50/1.84 ( t = one_one_int=> (? [X,Y] :( is_int(X)& is_int(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) ) )) ),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f62,axiom,(
% 7.50/1.84 ( 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(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) ) )) ),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f125,axiom,(
% 7.50/1.84 (! [Z_2,W_1] :( ( is_int(Z_2)& is_int(W_1) )=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))& Z_2 != W_1 ) ) ) )),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f5480,conjecture,(
% 7.50/1.84 (? [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) )),
% 7.50/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.50/1.84 fof(f5481,negated_conjecture,(
% 7.50/1.84 ~((? [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) ))),
% 7.50/1.84 inference(negated_conjecture,[status(cth)],[f5480])).
% 7.50/1.84 fof(f5487,plain,(
% 7.50/1.84 is_int(one_one_int)),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f6])).
% 7.50/1.84 fof(f5547,plain,(
% 7.50/1.84 is_int(t)),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f59])).
% 7.50/1.84 fof(f5548,plain,(
% 7.50/1.84 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t))),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f60])).
% 7.50/1.84 fof(f5549,plain,(
% 7.50/1.84 ~t=one_one_int|(?[X,Y]: ((is_int(X)&is_int(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)))),
% 7.50/1.84 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 7.50/1.84 fof(f5550,plain,(
% 7.50/1.84 ~t=one_one_int|((is_int(sK0_skl)&is_int(sK1_skl))&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))),
% 7.50/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f5549])).
% 7.50/1.84 fof(f5553,plain,(
% 7.50/1.84 ~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)),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f5550])).
% 7.50/1.84 fof(f5554,plain,(
% 7.50/1.84 ~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(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)))),
% 7.50/1.84 inference(pre_NNF_transformation,[status(thm)],[f62])).
% 7.50/1.84 fof(f5555,plain,(
% 7.50/1.84 ~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(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))),
% 7.50/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f5554])).
% 7.50/1.84 fof(f5558,plain,(
% 7.50/1.84 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_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)),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f5555])).
% 7.50/1.84 fof(f5624,plain,(
% 7.50/1.84 ![Z_2,W_1]: ((~is_int(Z_2)|~is_int(W_1))|(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))<=>(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))&~Z_2=W_1)))),
% 7.50/1.84 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 7.50/1.84 fof(f5625,plain,(
% 7.50/1.84 ![Z_2,W_1]: ((~is_int(Z_2)|~is_int(W_1))|((~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))|(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))&~Z_2=W_1))&(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))|(~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))|Z_2=W_1))))),
% 7.50/1.84 inference(NNF_transformation,[status(thm)],[f5624])).
% 7.50/1.84 fof(f5628,plain,(
% 7.50/1.84 ![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)),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f5625])).
% 7.50/1.84 fof(f19089,plain,(
% 7.50/1.84 (![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))),
% 7.50/1.84 inference(pre_NNF_transformation,[status(thm)],[f5481])).
% 7.50/1.84 fof(f19090,plain,(
% 7.50/1.84 ![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))),
% 7.50/1.84 inference(cnf_transformation,[status(thm)],[f19089])).
% 7.50/1.84 fof(f19491,definition,(
% 7.50/1.84 sQ0_spl <=> (t=one_one_int)),
% 7.50/1.84 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.50/1.84 fof(f19502,definition,(
% 7.50/1.84 sQ3_spl <=> (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))),
% 7.50/1.84 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 7.50/1.84 fof(f19503,plain,(
% 7.50/1.84 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)|~sQ3_spl),
% 7.50/1.84 inference(component_clause,[status(thm)],[f19502])).
% 7.50/1.84 fof(f19505,plain,(
% 7.50/1.84 ~sQ0_spl|sQ3_spl),
% 7.50/1.84 inference(split_clause,[status(thm)],[f5553,f19491,f19502])).
% 7.50/1.84 fof(f19506,definition,(
% 7.50/1.84 sQ4_spl <=> (hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)))),
% 7.50/1.84 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 7.50/1.84 fof(f19517,definition,(
% 7.50/1.84 sQ7_spl <=> (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))),
% 7.50/1.90 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 7.50/1.90 fof(f19518,plain,(
% 7.50/1.90 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)|~sQ7_spl),
% 7.50/1.90 inference(component_clause,[status(thm)],[f19517])).
% 7.50/1.90 fof(f19520,plain,(
% 7.50/1.90 ~sQ4_spl|sQ7_spl),
% 7.50/1.90 inference(split_clause,[status(thm)],[f5558,f19506,f19517])).
% 7.50/1.90 fof(f25171,definition,(
% 7.50/1.90 sQ17_spl <=> (is_int(t))),
% 7.50/1.90 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 7.50/1.90 fof(f25173,plain,(
% 7.50/1.90 ~is_int(t)|sQ17_spl),
% 7.50/1.90 inference(component_clause,[status(thm)],[f25171])).
% 7.50/1.90 fof(f25184,definition,(
% 7.50/1.90 sQ21_spl <=> (is_int(one_one_int))),
% 7.50/1.90 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 7.50/1.90 fof(f25186,plain,(
% 7.50/1.90 ~is_int(one_one_int)|sQ21_spl),
% 7.50/1.90 inference(component_clause,[status(thm)],[f25184])).
% 7.50/1.90 fof(f25191,plain,(
% 7.50/1.90 $false|sQ21_spl),
% 7.50/1.90 inference(forward_subsumption_resolution,[status(thm)],[f25186,f5487])).
% 7.50/1.90 fof(f25192,plain,(
% 7.50/1.90 sQ21_spl),
% 7.50/1.90 inference(contradiction_clause,[status(thm)],[f25191])).
% 7.50/1.90 fof(f25197,plain,(
% 7.50/1.90 ~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),
% 7.50/1.90 inference(resolution,[status(thm)],[f5628,f5548])).
% 7.50/1.90 fof(f25204,plain,(
% 7.50/1.90 ~sQ21_spl|~sQ17_spl|sQ4_spl|sQ0_spl),
% 7.50/1.90 inference(split_clause,[status(thm)],[f25197,f25184,f25171,f19506,f19491])).
% 7.50/1.90 fof(f25212,plain,(
% 7.50/1.90 $false|sQ17_spl),
% 7.50/1.90 inference(forward_subsumption_resolution,[status(thm)],[f25173,f5547])).
% 7.50/1.90 fof(f25213,plain,(
% 7.50/1.90 sQ17_spl),
% 7.50/1.90 inference(contradiction_clause,[status(thm)],[f25212])).
% 7.50/1.90 fof(f25214,plain,(
% 7.50/1.90 $false|~sQ7_spl),
% 7.50/1.90 inference(forward_subsumption_resolution,[status(thm)],[f19518,f19090])).
% 7.50/1.90 fof(f25215,plain,(
% 7.50/1.90 ~sQ7_spl),
% 7.50/1.90 inference(contradiction_clause,[status(thm)],[f25214])).
% 7.50/1.90 fof(f25218,plain,(
% 7.50/1.90 $false|~sQ3_spl),
% 7.50/1.90 inference(forward_subsumption_resolution,[status(thm)],[f19503,f19090])).
% 7.50/1.90 fof(f25219,plain,(
% 7.50/1.90 ~sQ3_spl),
% 7.50/1.90 inference(contradiction_clause,[status(thm)],[f25218])).
% 7.50/1.90 fof(f25220,plain,(
% 7.50/1.90 $false),
% 7.50/1.90 inference(sat_refutation,[status(thm)],[f19505,f19520,f25192,f25204,f25213,f25215,f25219])).
% 7.50/1.90 % SZS output end CNFRefutation for theBenchmark.p
% 3.37/1.97 % Elapsed time: 1.556098 seconds
% 3.37/1.97 % CPU time: 8.058986 seconds
% 3.37/1.97 % Total memory used: 694.101 MB
% 3.37/1.97 % Net memory used: 687.943 MB
%------------------------------------------------------------------------------