%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM925+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:59 PM UTC 2026
% Result : Theorem 0.12s 0.41s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 36 ( 25 unt; 0 def)
% Number of atoms : 51 ( 33 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 31 ( 16 ~; 11 |; 2 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-2 aty)
% Number of variables : 27 ( 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A_24] :
( hAPP_nat_int(power_power_int(A_24),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int
<=> A_24 = zero_zero_int ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
one_one_int = number_number_of_int(bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [K,I_2,J_2] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,I_2),J_2))
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(I_2),K)),hAPP_int_int(plus_plus_int(J_2),K))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
! [K] : hAPP_int_int(plus_plus_int(pls),K) = K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,axiom,
! [K] : number_number_of_int(K) = K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f708,conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f709,negated_conjecture,
~ ( hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
inference(negated_conjecture,[status(cth)],[f708]) ).
fof(f715,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f733,plain,
! [A_24] :
( ( A_24 != zero_zero_int
| hAPP_nat_int(power_power_int(A_24),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int )
& ( A_24 = zero_zero_int
| hAPP_nat_int(power_power_int(A_24),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f734,plain,
( ! [A_24] :
( A_24 != zero_zero_int
| hAPP_nat_int(power_power_int(A_24),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int )
& ! [A_24] :
( A_24 = zero_zero_int
| hAPP_nat_int(power_power_int(A_24),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ) ),
inference(miniscoping,[status(thm)],[f733]) ).
fof(f735,plain,
! [X0] :
( X0 = zero_zero_int
| hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
inference(cnf_transformation,[status(thm)],[f734]) ).
fof(f763,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f804,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f813,plain,
! [K,I_2,J_2] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(I_2),K)),hAPP_int_int(plus_plus_int(J_2),K)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,I_2),J_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f814,plain,
! [I_2,J_2] :
( ! [K] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(I_2),K)),hAPP_int_int(plus_plus_int(J_2),K)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,I_2),J_2)) ),
inference(miniscoping,[status(thm)],[f813]) ).
fof(f815,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(X0),X2)),hAPP_int_int(plus_plus_int(X1),X2)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f814]) ).
fof(f960,plain,
pls = zero_zero_int,
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f963,plain,
! [X0] : hAPP_int_int(plus_plus_int(pls),X0) = X0,
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f1103,plain,
! [X0] : number_number_of_int(X0) = X0,
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f2553,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(cnf_transformation,[status(thm)],[f709]) ).
fof(f2645,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = pls,
inference(backward_demodulation,[status(thm)],[f960,f2553]) ).
fof(f2649,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(forward_demodulation,[status(thm)],[f960,f715]) ).
fof(f2692,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(one_one_int))) = pls,
inference(backward_demodulation,[status(thm)],[f2693,f2645]) ).
fof(f2693,plain,
one_one_int = bit1(pls),
inference(forward_demodulation,[status(thm)],[f1103,f763]) ).
fof(f2705,plain,
! [X0] :
( X0 = zero_zero_int
| hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(one_one_int))) != zero_zero_int ),
inference(forward_demodulation,[status(thm)],[f2693,f735]) ).
fof(f2706,plain,
! [X0] :
( X0 = zero_zero_int
| hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(one_one_int))) != pls ),
inference(forward_demodulation,[status(thm)],[f960,f2705]) ).
fof(f2707,plain,
! [X0] :
( X0 = pls
| hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(one_one_int))) != pls ),
inference(forward_demodulation,[status(thm)],[f960,f2706]) ).
fof(f2717,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = pls,
inference(resolution,[status(thm)],[f2692,f2707]) ).
fof(f2743,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(backward_demodulation,[status(thm)],[f2717,f2649]) ).
fof(f2978,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(pls),X0)),hAPP_int_int(plus_plus_int(pls),X0))),
inference(resolution,[status(thm)],[f815,f2743]) ).
fof(f2984,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(plus_plus_int(pls),X0))),
inference(forward_demodulation,[status(thm)],[f963,f2978]) ).
fof(f2985,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X0)),
inference(forward_demodulation,[status(thm)],[f963,f2984]) ).
fof(f3033,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f804,f2985]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 03:17:33 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.41 % Refutation found
% 0.12/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.45 % Elapsed time: 0.092793 seconds
% 0.12/0.45 % CPU time: 0.301774 seconds
% 0.12/0.45 % Total memory used: 158.859 MB
% 0.12/0.45 % Net memory used: 158.118 MB
%------------------------------------------------------------------------------