%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM925+5 : 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.12s 0.39s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 16
% Syntax : Number of formulae : 67 ( 29 unt; 5 def)
% Number of atoms : 135 ( 59 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 124 ( 56 ~; 48 |; 10 &)
% ( 8 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 62 ( 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [B_1,B_2,X_a] :
( linord219039673up_add(X_a)
=> plus_plus(X_a,ti(X_a,B_1),B_2) = plus_plus(X_a,B_1,B_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X_a] :
( linordered_idom(X_a)
=> ! [Xa,Ya] :
( plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(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(f80,axiom,
! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [Wa,Z_1] :
( ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))
<=> ( Wa = Z_1
| ord_less(int,Wa,Z_1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [K] : ~ ord_less(int,semiring_1_of_nat(int,K),zero_zero(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [K] : plus_plus(int,K,pls) = K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [K] : bit1(K) = plus_plus(int,plus_plus(int,one_one(int),K),K),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,axiom,
linord219039673up_add(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,axiom,
linordered_idom(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,negated_conjecture,
~ ( power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ),
inference(negated_conjecture,[status(cth)],[f153]) ).
fof(f157,plain,
! [B_1,B_2,X_a] :
( plus_plus(X_a,ti(X_a,B_1),B_2) = plus_plus(X_a,B_1,B_2)
| ~ linord219039673up_add(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f158,plain,
! [X_a] :
( ! [B_1,B_2] : plus_plus(X_a,ti(X_a,B_1),B_2) = plus_plus(X_a,B_1,B_2)
| ~ linord219039673up_add(X_a) ),
inference(miniscoping,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0,X1,X2] :
( plus_plus(X0,ti(X0,X1),X2) = plus_plus(X0,X1,X2)
| ~ linord219039673up_add(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f239,plain,
! [X_a] :
( ! [Xa,Ya] :
( plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(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)],[f35]) ).
fof(f240,plain,
! [X_a] :
( ! [Xa,Ya] :
( ( ti(X_a,Ya) != zero_zero(X_a)
| ti(X_a,Xa) != zero_zero(X_a)
| plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a) )
& ( ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) )
| plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(NNF_transformation,[status(thm)],[f239]) ).
fof(f241,plain,
! [X_a] :
( ( ! [Xa,Ya] :
( ti(X_a,Ya) != zero_zero(X_a)
| ti(X_a,Xa) != zero_zero(X_a)
| plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a) )
& ! [Xa,Ya] :
( ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) )
| plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(miniscoping,[status(thm)],[f240]) ).
fof(f243,plain,
! [X0,X1,X2] :
( ti(X0,X2) = zero_zero(X0)
| plus_plus(X0,power_power(X0,X1,number_number_of(nat,bit0(bit1(pls)))),power_power(X0,X2,number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f350,plain,
! [X0,X1] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f395,plain,
! [Wa,Z_1] :
( ( ( Wa != Z_1
& ~ ord_less(int,Wa,Z_1) )
| ord_less(int,Wa,plus_plus(int,Z_1,one_one(int))) )
& ( Wa = Z_1
| ord_less(int,Wa,Z_1)
| ~ ord_less(int,Wa,plus_plus(int,Z_1,one_one(int))) ) ),
inference(NNF_transformation,[status(thm)],[f93]) ).
fof(f396,plain,
( ! [Wa,Z_1] :
( ( Wa != Z_1
& ~ ord_less(int,Wa,Z_1) )
| ord_less(int,Wa,plus_plus(int,Z_1,one_one(int))) )
& ! [Wa,Z_1] :
( Wa = Z_1
| ord_less(int,Wa,Z_1)
| ~ ord_less(int,Wa,plus_plus(int,Z_1,one_one(int))) ) ),
inference(miniscoping,[status(thm)],[f395]) ).
fof(f399,plain,
! [X0,X1] :
( X0 != X1
| ord_less(int,X0,plus_plus(int,X1,one_one(int))) ),
inference(cnf_transformation,[status(thm)],[f396]) ).
fof(f400,plain,
! [X0] : ~ ord_less(int,semiring_1_of_nat(int,X0),zero_zero(int)),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f433,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f435,plain,
! [X0] : plus_plus(int,X0,pls) = X0,
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f465,plain,
! [X0] : bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f482,plain,
linord219039673up_add(int),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f485,plain,
linordered_idom(int),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f504,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f506,plain,
! [X0] : ord_less(int,X0,plus_plus(int,X0,one_one(int))),
inference(destructive_equality_resolution,[status(thm)],[f399]) ).
fof(f510,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = pls,
inference(backward_demodulation,[status(thm)],[f433,f504]) ).
fof(f538,plain,
! [X0] :
( ti(int,X0) = plus_plus(int,X0,pls)
| ~ linord219039673up_add(int) ),
inference(paramodulation,[status(thm)],[f435,f159]) ).
fof(f539,definition,
( sQ4_spl
<=> linord219039673up_add(int) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f541,plain,
( sQ4_spl
| ~ linord219039673up_add(int) ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,definition,
! [X0] :
( sQ5_spl
<=> ti(int,X0) = plus_plus(int,X0,pls) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f543,plain,
! [X0] :
( ~ sQ5_spl
| ti(int,X0) = plus_plus(int,X0,pls) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f538,f539,f542]) ).
fof(f546,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f541,f482]) ).
fof(f547,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f546]) ).
fof(f548,plain,
! [X0] :
( ~ sQ5_spl
| ti(int,X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f435,f543]) ).
fof(f802,plain,
! [X0] : ~ ord_less(int,semiring_1_of_nat(int,X0),pls),
inference(forward_demodulation,[status(thm)],[f433,f400]) ).
fof(f978,plain,
! [X0] : ord_less(int,X0,plus_plus(int,one_one(int),X0)),
inference(paramodulation,[status(thm)],[f350,f506]) ).
fof(f1141,definition,
( sQ62_spl
<=> linordered_idom(int) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1143,plain,
( sQ62_spl
| ~ linordered_idom(int) ),
inference(component_clause,[status(thm)],[f1141]) ).
fof(f1167,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1143,f485]) ).
fof(f1168,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f1167]) ).
fof(f1541,plain,
bit1(pls) = plus_plus(int,one_one(int),pls),
inference(paramodulation,[status(thm)],[f435,f465]) ).
fof(f1559,plain,
bit1(pls) = one_one(int),
inference(forward_demodulation,[status(thm)],[f435,f1541]) ).
fof(f1591,plain,
! [X0] : ord_less(int,X0,plus_plus(int,bit1(pls),X0)),
inference(backward_demodulation,[status(thm)],[f1559,f978]) ).
fof(f1600,plain,
power_power(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = pls,
inference(backward_demodulation,[status(thm)],[f1559,f510]) ).
fof(f1890,plain,
! [X0] :
( ti(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n))) = zero_zero(int)
| plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),pls) != zero_zero(int)
| ~ linordered_idom(int) ),
inference(paramodulation,[status(thm)],[f1600,f243]) ).
fof(f1899,definition,
( sQ137_spl
<=> ti(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n))) = zero_zero(int) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1900,plain,
( ~ sQ137_spl
| ti(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n))) = zero_zero(int) ),
inference(component_clause,[status(thm)],[f1899]) ).
fof(f1907,definition,
! [X0] :
( sQ139_spl
<=> plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),pls) != zero_zero(int) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1908,plain,
! [X0] :
( ~ sQ139_spl
| plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),pls) != zero_zero(int) ),
inference(component_clause,[status(thm)],[f1907]) ).
fof(f1910,plain,
( sQ137_spl
| sQ139_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f1890,f1141,f1907,f1899]) ).
fof(f1947,plain,
! [X0] :
( ~ sQ139_spl
| power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ),
inference(forward_demodulation,[status(thm)],[f435,f1908]) ).
fof(f1948,plain,
! [X0] :
( ~ sQ139_spl
| power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))) != pls ),
inference(forward_demodulation,[status(thm)],[f433,f1947]) ).
fof(f1951,plain,
( ~ sQ139_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1600,f1948]) ).
fof(f1953,plain,
~ sQ139_spl,
inference(contradiction_clause,[status(thm)],[f1951]) ).
fof(f1954,plain,
( ~ sQ137_spl
| ~ sQ5_spl
| plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)) = zero_zero(int) ),
inference(forward_demodulation,[status(thm)],[f548,f1900]) ).
fof(f1955,plain,
( ~ sQ137_spl
| ~ sQ5_spl
| plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)) = pls ),
inference(forward_demodulation,[status(thm)],[f433,f1954]) ).
fof(f1956,plain,
( ~ sQ137_spl
| ~ sQ5_spl
| ord_less(int,semiring_1_of_nat(int,n),pls) ),
inference(paramodulation,[status(thm)],[f1955,f1591]) ).
fof(f1962,plain,
( ~ sQ137_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1956,f802]) ).
fof(f1963,plain,
( ~ sQ137_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1962]) ).
fof(f1964,plain,
$false,
inference(sat_refutation,[status(thm)],[f545,f547,f1168,f1910,f1953,f1963]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925+5 : 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.34 % Computer : n018.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 03:19:58 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.43 % Elapsed time: 0.076583 seconds
% 0.12/0.43 % CPU time: 0.247804 seconds
% 0.12/0.43 % Total memory used: 112.118 MB
% 0.12/0.43 % Net memory used: 111.856 MB
%------------------------------------------------------------------------------