%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM925+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 : n018.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:42:00 PM UTC 2026
% Result : Theorem 0.63s 1.03s
% Output : CNFRefutation 0.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 32 ( 17 unt; 0 def)
% Number of atoms : 58 ( 34 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 50 ( 24 ~; 18 |; 3 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 12 con; 0-2 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34,hypothesis,
! [B_1_1,B_2_1] :
( is_int(B_2_1)
=> is_int(hAPP_int_int(B_1_1,B_2_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
! [B_1_1,B_2_1] : is_int(hAPP_nat_int(B_1_1,B_2_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [A_1] :
( is_int(A_1)
=> ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A_1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int
<=> A_1 = zero_zero_int ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [Na] :
( hAPP_nat_int(semiri1621563631at_int,Na) = zero_zero_int
<=> Na = zero_zero_nat ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,axiom,
! [K_2] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,K_2)),zero_zero_int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5487,conjecture,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5488,negated_conjecture,
~ ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int ),
inference(negated_conjecture,[status(cth)],[f5487]) ).
fof(f5527,plain,
! [B_1_1,B_2_1] :
( is_int(hAPP_int_int(B_1_1,B_2_1))
| ~ is_int(B_2_1) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f5528,plain,
! [B_2_1] :
( ! [B_1_1] : is_int(hAPP_int_int(B_1_1,B_2_1))
| ~ is_int(B_2_1) ),
inference(miniscoping,[status(thm)],[f5527]) ).
fof(f5529,plain,
! [X0,X1] :
( is_int(hAPP_int_int(X1,X0))
| ~ is_int(X0) ),
inference(cnf_transformation,[status(thm)],[f5528]) ).
fof(f5531,plain,
! [X0,X1] : is_int(hAPP_nat_int(X0,X1)),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f5562,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f5605,plain,
! [A_1] :
( ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A_1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int
<=> A_1 = zero_zero_int )
| ~ is_int(A_1) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f5606,plain,
! [A_1] :
( ( ( A_1 != zero_zero_int
| hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A_1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int )
& ( A_1 = zero_zero_int
| hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A_1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int ) )
| ~ is_int(A_1) ),
inference(NNF_transformation,[status(thm)],[f5605]) ).
fof(f5607,plain,
! [X0] :
( X0 = zero_zero_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)))) != zero_zero_int
| ~ is_int(X0) ),
inference(cnf_transformation,[status(thm)],[f5606]) ).
fof(f5691,plain,
! [Na] :
( ( Na != zero_zero_nat
| hAPP_nat_int(semiri1621563631at_int,Na) = zero_zero_int )
& ( Na = zero_zero_nat
| hAPP_nat_int(semiri1621563631at_int,Na) != zero_zero_int ) ),
inference(NNF_transformation,[status(thm)],[f138]) ).
fof(f5692,plain,
( ! [Na] :
( Na != zero_zero_nat
| hAPP_nat_int(semiri1621563631at_int,Na) = zero_zero_int )
& ! [Na] :
( Na = zero_zero_nat
| hAPP_nat_int(semiri1621563631at_int,Na) != zero_zero_int ) ),
inference(miniscoping,[status(thm)],[f5691]) ).
fof(f5694,plain,
! [X0] :
( X0 != zero_zero_nat
| hAPP_nat_int(semiri1621563631at_int,X0) = zero_zero_int ),
inference(cnf_transformation,[status(thm)],[f5692]) ).
fof(f5856,plain,
! [X0] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f5944,plain,
pls = zero_zero_int,
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f19302,plain,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int,
inference(cnf_transformation,[status(thm)],[f5488]) ).
fof(f19726,plain,
hAPP_nat_int(semiri1621563631at_int,zero_zero_nat) = zero_zero_int,
inference(destructive_equality_resolution,[status(thm)],[f5694]) ).
fof(f20340,plain,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,zero_zero_int)))) = zero_zero_int,
inference(backward_demodulation,[status(thm)],[f5944,f19302]) ).
fof(f20407,plain,
! [X0] :
( X0 = zero_zero_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,zero_zero_int)))) != zero_zero_int
| ~ is_int(X0) ),
inference(forward_demodulation,[status(thm)],[f5944,f5607]) ).
fof(f20409,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = zero_zero_int
| ~ is_int(hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))) ),
inference(resolution,[status(thm)],[f20407,f20340]) ).
fof(f20576,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = zero_zero_int
| ~ is_int(hAPP_nat_int(semiri1621563631at_int,n)) ),
inference(resolution,[status(thm)],[f5529,f20409]) ).
fof(f20581,plain,
hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = zero_zero_int,
inference(forward_subsumption_resolution,[status(thm)],[f20576,f5531]) ).
fof(f20584,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),zero_zero_int)),
inference(backward_demodulation,[status(thm)],[f20581,f5562]) ).
fof(f20915,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),zero_zero_int)),
inference(paramodulation,[status(thm)],[f19726,f5856]) ).
fof(f20917,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f20915,f20584]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+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.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:19:29 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.55/0.86 % Drodi V4.1.1
% 0.63/1.03 % Refutation found
% 0.63/1.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.63/1.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.74/1.13 % Elapsed time: 0.753263 seconds
% 0.74/1.13 % CPU time: 1.868852 seconds
% 0.74/1.13 % Total memory used: 620.711 MB
% 0.74/1.13 % Net memory used: 615.196 MB
%------------------------------------------------------------------------------