%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM924+4 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:41:58 PM UTC 2026
% Result : Theorem 18.25s 3.26s
% Output : CNFRefutation 18.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 37 ( 33 unt; 0 def)
% Number of atoms : 41 ( 22 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 11 ( 7 ~; 3 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 14 con; 0-2 aty)
% Number of variables : 15 ( 15 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,hypothesis,
is_int(one_one_int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
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))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,axiom,
! [W] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,pls),W) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f316,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,axiom,
! [K_2] :
( is_int(K_2)
=> hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,K_2),pls) = K_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f416,axiom,
! [K_2] : hAPP_int_int(bit1,K_2) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),K_2)),K_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5480,conjecture,
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)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5481,negated_conjecture,
~ 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)),
inference(negated_conjecture,[status(cth)],[f5480]) ).
fof(f5487,plain,
is_int(one_one_int),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f5550,plain,
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))),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f5551,plain,
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),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f5652,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f5858,plain,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,pls),X0) = pls,
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f6182,plain,
pls = zero_zero_int,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f6201,plain,
! [K_2] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,K_2),pls) = K_2
| ~ is_int(K_2) ),
inference(pre_NNF_transformation,[status(thm)],[f323]) ).
fof(f6202,plain,
! [X0] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X0),pls) = X0
| ~ is_int(X0) ),
inference(cnf_transformation,[status(thm)],[f6201]) ).
fof(f6341,plain,
! [X0] : hAPP_int_int(bit1,X0) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),X0)),X0),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f19074,plain,
~ 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)),
inference(cnf_transformation,[status(thm)],[f5481]) ).
fof(f20032,plain,
~ 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)),
inference(backward_demodulation,[status(thm)],[f6182,f19074]) ).
fof(f20414,plain,
! [X0] :
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X0),zero_zero_int) = X0
| ~ is_int(X0) ),
inference(forward_demodulation,[status(thm)],[f6182,f6202]) ).
fof(f20439,plain,
hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),zero_zero_int) = one_one_int,
inference(resolution,[status(thm)],[f20414,f5487]) ).
fof(f20646,plain,
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))),
inference(forward_demodulation,[status(thm)],[f6182,f5550]) ).
fof(f20647,plain,
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))),
inference(forward_demodulation,[status(thm)],[f6182,f20646]) ).
fof(f20648,plain,
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),
inference(forward_demodulation,[status(thm)],[f6182,f5551]) ).
fof(f20649,plain,
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))),
inference(backward_demodulation,[status(thm)],[f20650,f20647]) ).
fof(f20650,plain,
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),
inference(forward_demodulation,[status(thm)],[f6182,f20648]) ).
fof(f23007,plain,
hAPP_int_int(bit1,zero_zero_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),zero_zero_int),
inference(paramodulation,[status(thm)],[f20439,f6341]) ).
fof(f23031,plain,
hAPP_int_int(bit1,zero_zero_int) = one_one_int,
inference(forward_demodulation,[status(thm)],[f20439,f23007]) ).
fof(f23142,plain,
~ 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,one_one_int)))),one_one_int)),zero_zero_int)),
inference(backward_demodulation,[status(thm)],[f23031,f20032]) ).
fof(f28834,plain,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,zero_zero_int),X0) = pls,
inference(forward_demodulation,[status(thm)],[f6182,f5858]) ).
fof(f28837,plain,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,zero_zero_int),X0) = zero_zero_int,
inference(forward_demodulation,[status(thm)],[f6182,f28834]) ).
fof(f28838,plain,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),zero_zero_int) = zero_zero_int,
inference(paramodulation,[status(thm)],[f5652,f28837]) ).
fof(f35902,plain,
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,one_one_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))),
inference(forward_demodulation,[status(thm)],[f23031,f20649]) ).
fof(f35903,plain,
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,one_one_int)))),one_one_int)),zero_zero_int)),
inference(forward_demodulation,[status(thm)],[f28838,f35902]) ).
fof(f35904,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f35903,f23142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n015.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 03:20:21 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.57/0.85 % Drodi V4.1.1
% 18.25/3.26 % Refutation found
% 18.25/3.26 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.25/3.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.43/3.40 % Elapsed time: 3.037022 seconds
% 8.43/3.40 % CPU time: 20.005819 seconds
% 8.43/3.40 % Total memory used: 837.069 MB
% 8.43/3.40 % Net memory used: 823.255 MB
%------------------------------------------------------------------------------