%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM924+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 : n026.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:04 PM UTC 2026
% Result : Theorem 12.86s 2.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+4 : 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.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 21 03:19:52 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.64/0.90 % Drodi V4.1.1
% 12.86/2.60 % Refutation found
% 12.86/2.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.86/2.60 % SZS output start CNFRefutation for theBenchmark
% 12.86/2.60 fof(f62,axiom,(
% 12.86/2.60 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),t)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),zero_zero_int))) ),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f63,axiom,(
% 12.86/2.60 hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),t) ),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f114,axiom,(
% 12.86/2.60 (! [Z_1,W] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,Z_1),W) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,W),Z_1) )),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f184,axiom,(
% 12.86/2.60 hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,one_one_nat),one_one_nat) = hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))) ),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f185,axiom,(
% 12.86/2.60 (! [W] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,pls),W) = pls )),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f316,axiom,(
% 12.86/2.60 pls = zero_zero_int ),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f5480,conjecture,(
% 12.86/2.60 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),one_one_int)),zero_zero_int)) ),
% 12.86/2.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.86/2.60 fof(f5481,negated_conjecture,(
% 12.86/2.60 ~(hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),one_one_int)),zero_zero_int)) )),
% 12.86/2.60 inference(negated_conjecture,[status(cth)],[f5480])).
% 12.86/2.60 fof(f5550,plain,(
% 12.86/2.60 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),t)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),zero_zero_int)))),
% 12.86/2.60 inference(cnf_transformation,[status(thm)],[f62])).
% 12.86/2.60 fof(f5551,plain,(
% 12.86/2.60 hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),one_one_int)=hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),t)),
% 12.86/2.60 inference(cnf_transformation,[status(thm)],[f63])).
% 12.86/2.60 fof(f5652,plain,(
% 12.86/2.60 ![X0,X1]: (hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),X1)=hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X1),X0))),
% 12.86/2.61 inference(cnf_transformation,[status(thm)],[f114])).
% 12.86/2.61 fof(f5857,plain,(
% 12.86/2.61 hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,one_one_nat),one_one_nat)=hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))),
% 12.86/2.61 inference(cnf_transformation,[status(thm)],[f184])).
% 12.86/2.61 fof(f5858,plain,(
% 12.86/2.61 ![X0]: (hAPP_int_int(hAPP_int_fun_int_int(times_times_int,pls),X0)=pls)),
% 12.86/2.61 inference(cnf_transformation,[status(thm)],[f185])).
% 12.86/2.61 fof(f6182,plain,(
% 12.86/2.61 pls=zero_zero_int),
% 12.86/2.61 inference(cnf_transformation,[status(thm)],[f316])).
% 12.86/2.61 fof(f19074,plain,(
% 12.86/2.61 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),one_one_int)),zero_zero_int))),
% 12.86/2.61 inference(cnf_transformation,[status(thm)],[f5481])).
% 12.86/2.61 fof(f20011,plain,(
% 12.86/2.61 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,zero_zero_int))))),one_one_int)),zero_zero_int))),
% 12.86/2.61 inference(backward_demodulation,[status(thm)],[f6182,f19074])).
% 12.86/2.61 fof(f20528,plain,(
% 12.86/2.61 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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,zero_zero_int))))),m)),one_one_int)),t)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),zero_zero_int)))),
% 12.86/2.61 inference(forward_demodulation,[status(thm)],[f6182,f5550])).
% 12.86/2.61 fof(f20529,plain,(
% 12.86/2.61 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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,zero_zero_int))))),m)),one_one_int)),t)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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,zero_zero_int))))),m)),one_one_int)),zero_zero_int)))),
% 12.86/2.61 inference(forward_demodulation,[status(thm)],[f6182,f20528])).
% 12.86/2.61 fof(f20534,plain,(
% 12.86/2.61 hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,zero_zero_int))))),one_one_int)=hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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)),t)),
% 12.86/2.61 inference(forward_demodulation,[status(thm)],[f6182,f5551])).
% 12.86/2.61 fof(f20535,plain,(
% 12.86/2.61 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,zero_zero_int))))),one_one_int)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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,zero_zero_int))))),m)),one_one_int)),zero_zero_int)))),
% 12.86/2.61 inference(backward_demodulation,[status(thm)],[f20536,f20529])).
% 12.86/2.61 fof(f20536,plain,(
% 12.86/2.61 hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,zero_zero_int))))),one_one_int)=hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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,zero_zero_int))))),m)),one_one_int)),t)),
% 13.69/2.69 inference(forward_demodulation,[status(thm)],[f6182,f20534])).
% 13.69/2.69 fof(f25042,plain,(
% 13.69/2.69 ~hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,one_one_nat),one_one_nat))),one_one_int)),zero_zero_int))),
% 13.69/2.69 inference(backward_demodulation,[status(thm)],[f25046,f20011])).
% 13.69/2.69 fof(f25046,plain,(
% 13.69/2.69 hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,one_one_nat),one_one_nat)=hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,zero_zero_int)))),
% 13.69/2.69 inference(forward_demodulation,[status(thm)],[f6182,f5857])).
% 13.69/2.69 fof(f25087,plain,(
% 13.69/2.69 ![X0]: (hAPP_int_int(hAPP_int_fun_int_int(times_times_int,zero_zero_int),X0)=pls)),
% 13.69/2.69 inference(forward_demodulation,[status(thm)],[f6182,f5858])).
% 13.69/2.69 fof(f25090,plain,(
% 13.69/2.69 ![X0]: (hAPP_int_int(hAPP_int_fun_int_int(times_times_int,zero_zero_int),X0)=zero_zero_int)),
% 13.69/2.69 inference(forward_demodulation,[status(thm)],[f6182,f25087])).
% 13.69/2.69 fof(f25091,plain,(
% 13.69/2.69 ![X0]: (hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),zero_zero_int)=zero_zero_int)),
% 13.69/2.69 inference(paramodulation,[status(thm)],[f5652,f25090])).
% 13.69/2.69 fof(f29791,plain,(
% 13.69/2.69 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,one_one_nat),one_one_nat))),one_one_int)),hAPP_int_int(hAPP_int_fun_int_int(times_times_int,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,zero_zero_int))))),m)),one_one_int)),zero_zero_int)))),
% 13.69/2.69 inference(forward_demodulation,[status(thm)],[f25046,f20535])).
% 13.69/2.69 fof(f29792,plain,(
% 13.69/2.69 hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,one_one_nat),one_one_nat))),one_one_int)),zero_zero_int))),
% 13.69/2.69 inference(forward_demodulation,[status(thm)],[f25091,f29791])).
% 13.69/2.69 fof(f29793,plain,(
% 13.69/2.69 $false),
% 13.69/2.69 inference(forward_subsumption_resolution,[status(thm)],[f29792,f25042])).
% 13.69/2.69 % SZS output end CNFRefutation for theBenchmark.p
% 2.36/2.72 % Elapsed time: 2.314159 seconds
% 2.36/2.72 % CPU time: 14.137809 seconds
% 2.36/2.72 % Total memory used: 790.503 MB
% 2.36/2.72 % Net memory used: 776.658 MB
%------------------------------------------------------------------------------