%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM925+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:01 PM UTC 2026
% Result : Theorem 0.22s 0.49s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 15
% Syntax : Number of formulae : 60 ( 30 unt; 4 def)
% Number of atoms : 109 ( 55 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 93 ( 44 ~; 35 |; 6 &)
% ( 6 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-4 aty)
% Number of variables : 43 ( 43 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [B_1_1,X_a] :
( number(X_a)
=> ti(X_a,number_number_of(X_a,B_1_1)) = number_number_of(X_a,B_1_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X_a] :
( linordered_idom(X_a)
=> ! [Xa,Ya] :
( hAPP(X_a,X_a,plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = zero_zero(X_a)
<=> ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
one_one(int) = number_number_of(int,hAPP(int,int,bit1,pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [K] : hAPP(int,int,plus_plus(int,pls),K) = K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,axiom,
! [K] : number_number_of(int,K) = K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f563,axiom,
linordered_idom(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f581,axiom,
number(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f660,conjecture,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f661,negated_conjecture,
~ ( hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != zero_zero(int) ),
inference(negated_conjecture,[status(cth)],[f660]) ).
fof(f694,plain,
! [B_1_1,X_a] :
( ti(X_a,number_number_of(X_a,B_1_1)) = number_number_of(X_a,B_1_1)
| ~ number(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f695,plain,
! [X_a] :
( ! [B_1_1] : ti(X_a,number_number_of(X_a,B_1_1)) = number_number_of(X_a,B_1_1)
| ~ number(X_a) ),
inference(miniscoping,[status(thm)],[f694]) ).
fof(f696,plain,
! [X0,X1] :
( ti(X0,number_number_of(X0,X1)) = number_number_of(X0,X1)
| ~ number(X0) ),
inference(cnf_transformation,[status(thm)],[f695]) ).
fof(f748,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f750,plain,
! [X_a] :
( ! [Xa,Ya] :
( hAPP(X_a,X_a,plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = zero_zero(X_a)
<=> ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f751,plain,
! [X_a] :
( ! [Xa,Ya] :
( ( ti(X_a,Ya) != zero_zero(X_a)
| ti(X_a,Xa) != zero_zero(X_a)
| hAPP(X_a,X_a,plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = zero_zero(X_a) )
& ( ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) )
| hAPP(X_a,X_a,plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(NNF_transformation,[status(thm)],[f750]) ).
fof(f752,plain,
! [X_a] :
( ( ! [Xa,Ya] :
( ti(X_a,Ya) != zero_zero(X_a)
| ti(X_a,Xa) != zero_zero(X_a)
| hAPP(X_a,X_a,plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = zero_zero(X_a) )
& ! [Xa,Ya] :
( ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) )
| hAPP(X_a,X_a,plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(miniscoping,[status(thm)],[f751]) ).
fof(f753,plain,
! [X0,X1,X2] :
( ti(X0,X1) = zero_zero(X0)
| hAPP(X0,X0,plus_plus(X0,hAPP(nat,X0,power_power(X0,X1),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,X0,power_power(X0,X2),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[status(thm)],[f752]) ).
fof(f816,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f833,plain,
one_one(int) = number_number_of(int,hAPP(int,int,bit1,pls)),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f944,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f947,plain,
! [X0] : hAPP(int,int,plus_plus(int,pls),X0) = X0,
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f1040,plain,
! [X0] : number_number_of(int,X0) = X0,
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f2264,plain,
linordered_idom(int),
inference(cnf_transformation,[status(thm)],[f563]) ).
fof(f2282,plain,
number(int),
inference(cnf_transformation,[status(thm)],[f581]) ).
fof(f2361,plain,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f661]) ).
fof(f2427,plain,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = pls,
inference(backward_demodulation,[status(thm)],[f944,f2361]) ).
fof(f2430,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(forward_demodulation,[status(thm)],[f944,f748]) ).
fof(f2483,plain,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,one_one(int)))) = pls,
inference(backward_demodulation,[status(thm)],[f2484,f2427]) ).
fof(f2484,plain,
one_one(int) = hAPP(int,int,bit1,pls),
inference(forward_demodulation,[status(thm)],[f1040,f833]) ).
fof(f2560,plain,
! [X0] : ti(int,number_number_of(int,X0)) = number_number_of(int,X0),
inference(resolution,[status(thm)],[f2282,f696]) ).
fof(f2562,plain,
! [X0] : ti(int,X0) = number_number_of(int,X0),
inference(forward_demodulation,[status(thm)],[f1040,f2560]) ).
fof(f2563,plain,
! [X0] : ti(int,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1040,f2562]) ).
fof(f2839,definition,
( sQ14_spl
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f2840,plain,
( ~ sQ14_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
inference(component_clause,[status(thm)],[f2839]) ).
fof(f2850,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2840,f816]) ).
fof(f2851,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f2850]) ).
fof(f3245,plain,
! [X0,X1,X2] :
( ti(X0,X1) = zero_zero(X0)
| hAPP(X0,X0,plus_plus(X0,hAPP(nat,X0,power_power(X0,X1),number_number_of(nat,hAPP(int,int,bit0,one_one(int))))),hAPP(nat,X0,power_power(X0,X2),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(forward_demodulation,[status(thm)],[f2484,f753]) ).
fof(f3246,plain,
! [X0,X1,X2] :
( ti(X0,X1) = zero_zero(X0)
| hAPP(X0,X0,plus_plus(X0,hAPP(nat,X0,power_power(X0,X1),number_number_of(nat,hAPP(int,int,bit0,one_one(int))))),hAPP(nat,X0,power_power(X0,X2),number_number_of(nat,hAPP(int,int,bit0,one_one(int))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(forward_demodulation,[status(thm)],[f2484,f3245]) ).
fof(f3254,plain,
! [X0] :
( ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))) = zero_zero(int)
| hAPP(int,int,plus_plus(int,pls),hAPP(nat,int,power_power(int,X0),number_number_of(nat,hAPP(int,int,bit0,one_one(int))))) != zero_zero(int)
| ~ linordered_idom(int) ),
inference(paramodulation,[status(thm)],[f2483,f3246]) ).
fof(f3260,definition,
( sQ20_spl
<=> linordered_idom(int) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f3262,plain,
( sQ20_spl
| ~ linordered_idom(int) ),
inference(component_clause,[status(thm)],[f3260]) ).
fof(f3294,definition,
! [X0] :
( sQ29_spl
<=> hAPP(int,int,plus_plus(int,pls),hAPP(nat,int,power_power(int,X0),number_number_of(nat,hAPP(int,int,bit0,one_one(int))))) != zero_zero(int) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f3295,plain,
! [X0] :
( ~ sQ29_spl
| hAPP(int,int,plus_plus(int,pls),hAPP(nat,int,power_power(int,X0),number_number_of(nat,hAPP(int,int,bit0,one_one(int))))) != zero_zero(int) ),
inference(component_clause,[status(thm)],[f3294]) ).
fof(f3297,definition,
( sQ30_spl
<=> ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))) = zero_zero(int) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f3298,plain,
( ~ sQ30_spl
| ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))) = zero_zero(int) ),
inference(component_clause,[status(thm)],[f3297]) ).
fof(f3300,plain,
( sQ30_spl
| sQ29_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f3254,f3260,f3294,f3297]) ).
fof(f3321,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3262,f2264]) ).
fof(f3322,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f3321]) ).
fof(f3339,plain,
! [X0] :
( ~ sQ29_spl
| hAPP(nat,int,power_power(int,X0),number_number_of(nat,hAPP(int,int,bit0,one_one(int)))) != zero_zero(int) ),
inference(forward_demodulation,[status(thm)],[f947,f3295]) ).
fof(f3340,plain,
! [X0] :
( ~ sQ29_spl
| hAPP(nat,int,power_power(int,X0),number_number_of(nat,hAPP(int,int,bit0,one_one(int)))) != pls ),
inference(forward_demodulation,[status(thm)],[f944,f3339]) ).
fof(f3399,plain,
( ~ sQ30_spl
| hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)) = zero_zero(int) ),
inference(forward_demodulation,[status(thm)],[f2563,f3298]) ).
fof(f3400,plain,
( ~ sQ30_spl
| hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)) = pls ),
inference(forward_demodulation,[status(thm)],[f944,f3399]) ).
fof(f3416,plain,
( ~ sQ30_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
inference(backward_demodulation,[status(thm)],[f3400,f2430]) ).
fof(f3422,plain,
( ~ sQ30_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f3416,f2839,f3297]) ).
fof(f3553,plain,
( ~ sQ29_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2483,f3340]) ).
fof(f3555,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f3553]) ).
fof(f3556,plain,
$false,
inference(sat_refutation,[status(thm)],[f2851,f3300,f3322,f3422,f3555]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 03:17:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.22/0.49 % Refutation found
% 0.22/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.22/0.54 % Elapsed time: 0.162022 seconds
% 0.22/0.54 % CPU time: 0.492108 seconds
% 0.22/0.54 % Total memory used: 166.850 MB
% 0.22/0.54 % Net memory used: 166.154 MB
%------------------------------------------------------------------------------