%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM925+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 : 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:06 PM UTC 2026
% Result : Theorem 0.08s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM925+3 : 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.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 03:17:08 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.08/0.34 % Drodi V4.1.1
% 0.08/0.37 % Refutation found
% 0.08/0.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.37 fof(f3,hypothesis,(
% 0.08/0.37 is_int(one_one_int) ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f4,hypothesis,(
% 0.08/0.37 (! [B_1_1,B_2_1] :( ( is_int(B_1_1)& is_int(B_2_1) )=> is_int(plus_plus_int(B_1_1,B_2_1)) ) )),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f6,hypothesis,(
% 0.08/0.37 is_int(zero_zero_int) ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f20,hypothesis,(
% 0.08/0.37 (! [B_1_1,B_2_1] : is_int(hAPP_nat_int(B_1_1,B_2_1)) )),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f29,axiom,(
% 0.08/0.37 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)))) ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f31,axiom,(
% 0.08/0.37 (! [Xa,Ya] :( ( is_int(Xa)& is_int(Ya) )=> ( plus_plus_int(hAPP_nat_int(power_power_int(Xa),number_number_of_nat(bit0(bit1(pls)))),hAPP_nat_int(power_power_int(Ya),number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int<=> ( Xa = zero_zero_int& Ya = zero_zero_int ) ) ) )),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f36,axiom,(
% 0.08/0.37 hAPP_nat_int(power_power_int(zero_zero_int),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f77,axiom,(
% 0.08/0.37 ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)) ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f126,axiom,(
% 0.08/0.37 bit0(pls) = pls ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f127,axiom,(
% 0.08/0.37 pls = zero_zero_int ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f132,axiom,(
% 0.08/0.37 (! [K_1] : bit0(K_1) = plus_plus_int(K_1,K_1) )),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f1233,conjecture,(
% 0.08/0.37 hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f1234,negated_conjecture,(
% 0.08/0.37 ~(hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int )),
% 0.08/0.37 inference(negated_conjecture,[status(cth)],[f1233])).
% 0.08/0.37 fof(f1239,plain,(
% 0.08/0.37 is_int(one_one_int)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.37 fof(f1240,plain,(
% 0.08/0.37 ![B_1_1,B_2_1]: ((~is_int(B_1_1)|~is_int(B_2_1))|is_int(plus_plus_int(B_1_1,B_2_1)))),
% 0.08/0.37 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.08/0.37 fof(f1241,plain,(
% 0.08/0.37 ![X0,X1]: (~is_int(X0)|~is_int(X1)|is_int(plus_plus_int(X0,X1)))),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f1240])).
% 0.08/0.37 fof(f1244,plain,(
% 0.08/0.37 is_int(zero_zero_int)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f6])).
% 0.08/0.37 fof(f1266,plain,(
% 0.08/0.37 ![X0,X1]: (is_int(hAPP_nat_int(X0,X1)))),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f20])).
% 0.08/0.37 fof(f1275,plain,(
% 0.08/0.37 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))))),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f29])).
% 0.08/0.37 fof(f1277,plain,(
% 0.08/0.37 ![Xa,Ya]: ((~is_int(Xa)|~is_int(Ya))|(plus_plus_int(hAPP_nat_int(power_power_int(Xa),number_number_of_nat(bit0(bit1(pls)))),hAPP_nat_int(power_power_int(Ya),number_number_of_nat(bit0(bit1(pls)))))=zero_zero_int<=>(Xa=zero_zero_int&Ya=zero_zero_int)))),
% 0.08/0.37 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.08/0.37 fof(f1278,plain,(
% 0.08/0.37 ![Xa,Ya]: ((~is_int(Xa)|~is_int(Ya))|((~plus_plus_int(hAPP_nat_int(power_power_int(Xa),number_number_of_nat(bit0(bit1(pls)))),hAPP_nat_int(power_power_int(Ya),number_number_of_nat(bit0(bit1(pls)))))=zero_zero_int|(Xa=zero_zero_int&Ya=zero_zero_int))&(plus_plus_int(hAPP_nat_int(power_power_int(Xa),number_number_of_nat(bit0(bit1(pls)))),hAPP_nat_int(power_power_int(Ya),number_number_of_nat(bit0(bit1(pls)))))=zero_zero_int|(~Xa=zero_zero_int|~Ya=zero_zero_int))))),
% 0.08/0.37 inference(NNF_transformation,[status(thm)],[f1277])).
% 0.08/0.37 fof(f1279,plain,(
% 0.08/0.37 ![X0,X1]: (~is_int(X0)|~is_int(X1)|~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)))))=zero_zero_int|X0=zero_zero_int)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f1278])).
% 0.08/0.37 fof(f1290,plain,(
% 0.08/0.37 hAPP_nat_int(power_power_int(zero_zero_int),number_number_of_nat(bit0(bit1(pls))))=zero_zero_int),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f36])).
% 0.08/0.37 fof(f1365,plain,(
% 0.08/0.37 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls))),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f77])).
% 0.08/0.37 fof(f1521,plain,(
% 0.08/0.37 bit0(pls)=pls),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f126])).
% 0.08/0.37 fof(f1522,plain,(
% 0.08/0.37 pls=zero_zero_int),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f127])).
% 0.08/0.37 fof(f1529,plain,(
% 0.08/0.37 ![X0]: (bit0(X0)=plus_plus_int(X0,X0))),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f132])).
% 0.08/0.37 fof(f4524,plain,(
% 0.08/0.37 hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))=zero_zero_int),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f1234])).
% 0.08/0.37 fof(f4724,plain,(
% 0.08/0.37 hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(zero_zero_int))))=zero_zero_int),
% 0.08/0.37 inference(backward_demodulation,[status(thm)],[f1522,f4524])).
% 0.08/0.37 fof(f4725,plain,(
% 0.08/0.37 ![X0,X1]: (~is_int(X0)|~is_int(X1)|~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)))))=zero_zero_int|X0=zero_zero_int)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f1279])).
% 0.08/0.37 fof(f4726,plain,(
% 0.08/0.37 ![X0,X1]: (~is_int(X0)|~is_int(X1)|~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)))))=zero_zero_int|X0=zero_zero_int)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f4725])).
% 0.08/0.37 fof(f4742,plain,(
% 0.08/0.37 ![X0]: (~is_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)))|~is_int(X0)|~plus_plus_int(zero_zero_int,hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int)))))=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int)),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f4724,f4726])).
% 0.08/0.37 fof(f4745,plain,(
% 0.08/0.37 ![X0]: (~is_int(X0)|~plus_plus_int(zero_zero_int,hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int)))))=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int|~is_int(one_one_int)|~is_int(hAPP_nat_int(semiri1621563631at_int,n)))),
% 0.08/0.37 inference(resolution,[status(thm)],[f4742,f1241])).
% 0.08/0.37 fof(f4746,plain,(
% 0.08/0.37 ![X0]: (~is_int(X0)|~plus_plus_int(zero_zero_int,hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int)))))=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int|~is_int(hAPP_nat_int(semiri1621563631at_int,n)))),
% 0.08/0.37 inference(forward_subsumption_resolution,[status(thm)],[f4745,f1239])).
% 0.08/0.37 fof(f4760,plain,(
% 0.08/0.37 hAPP_nat_int(power_power_int(zero_zero_int),number_number_of_nat(bit0(bit1(zero_zero_int))))=zero_zero_int),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f1290])).
% 0.08/0.37 fof(f4798,plain,(
% 0.08/0.37 ![X0]: (~is_int(X0)|~plus_plus_int(zero_zero_int,hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(zero_zero_int)))))=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int)),
% 0.08/0.37 inference(forward_subsumption_resolution,[status(thm)],[f4746,f1266])).
% 0.08/0.37 fof(f4799,plain,(
% 0.08/0.37 ~is_int(zero_zero_int)|~plus_plus_int(zero_zero_int,zero_zero_int)=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f4760,f4798])).
% 0.08/0.37 fof(f4802,plain,(
% 0.08/0.37 ~plus_plus_int(zero_zero_int,zero_zero_int)=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int),
% 0.08/0.37 inference(forward_subsumption_resolution,[status(thm)],[f4799,f1244])).
% 0.08/0.37 fof(f4923,plain,(
% 0.08/0.37 bit0(zero_zero_int)=pls),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f1521])).
% 0.08/0.37 fof(f4924,plain,(
% 0.08/0.37 bit0(zero_zero_int)=zero_zero_int),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f4923])).
% 0.08/0.37 fof(f4927,plain,(
% 0.08/0.37 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),pls))),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f1365])).
% 0.08/0.37 fof(f4928,plain,(
% 0.08/0.37 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),zero_zero_int))),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f1522,f4927])).
% 0.08/0.37 fof(f5005,plain,(
% 0.08/0.37 ~bit0(zero_zero_int)=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int),
% 0.08/0.37 inference(backward_demodulation,[status(thm)],[f1529,f4802])).
% 0.08/0.37 fof(f5015,plain,(
% 0.08/0.37 ~zero_zero_int=zero_zero_int|plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f4924,f5005])).
% 0.08/0.37 fof(f5016,plain,(
% 0.08/0.37 plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))=zero_zero_int),
% 0.08/0.37 inference(trivial_equality_resolution,[status(thm)],[f5015])).
% 0.08/0.37 fof(f5054,plain,(
% 0.08/0.37 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),zero_zero_int))),
% 0.08/0.37 inference(backward_demodulation,[status(thm)],[f5016,f1275])).
% 0.08/0.37 fof(f5056,plain,(
% 0.08/0.37 $false),
% 0.08/0.37 inference(forward_subsumption_resolution,[status(thm)],[f5054,f4928])).
% 0.08/0.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.40 % Elapsed time: 0.095999 seconds
% 0.08/0.40 % CPU time: 0.260884 seconds
% 0.08/0.40 % Total memory used: 204.243 MB
% 0.08/0.40 % Net memory used: 202.639 MB
%------------------------------------------------------------------------------