%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:03 PM UTC 2026
% Result : Theorem 1.28s 2.19s
% Output : CNFRefutation 1.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 46
% Syntax : Number of formulae : 149 ( 63 unt; 22 def)
% Number of atoms : 246 ( 50 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 152 ( 55 ~; 66 |; 5 &)
% ( 23 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 31 ( 29 usr; 23 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 20 con; 0-4 aty)
% Number of variables : 31 ( 19 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f74,axiom,
! [X_a] :
( one(X_a)
=> ti(X_a,one_one(X_a)) = one_one(X_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,axiom,
ti(int,min_1) = min_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,axiom,
ti(int,t) = t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f274,axiom,
( t = one_one(int)
=> ? [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,axiom,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
=> ? [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f295,axiom,
! [Z,W_1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1))
<=> ( ti(int,Z) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2194,axiom,
pi != zero_zero(real),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5314,axiom,
monoid_mult(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5317,axiom,
semiring_1(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5330,axiom,
abs_if(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5339,axiom,
one(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5369,axiom,
monoid_mult(nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5432,axiom,
monoid_mult(rat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5449,axiom,
abs_if(rat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5505,axiom,
sgn_div_norm(real),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5532,axiom,
monoid_mult(real),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5549,axiom,
abs_if(real),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5556,axiom,
banach(real),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5602,axiom,
monoid_mult(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5622,axiom,
banach(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5655,axiom,
monoid_mult(code_code_numeral),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5696,axiom,
monoid_mult(quickcheck_code_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5738,conjecture,
? [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5739,negated_conjecture,
~ ? [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)),
inference(negated_conjecture,[status(cth)],[f5738]) ).
fof(f5829,plain,
! [X_a] :
( ti(X_a,one_one(X_a)) = one_one(X_a)
| ~ one(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f5830,plain,
! [X0] :
( ti(X0,one_one(X0)) = one_one(X0)
| ~ one(X0) ),
inference(cnf_transformation,[status(thm)],[f5829]) ).
fof(f5877,plain,
ti(int,min_1) = min_1,
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f6090,plain,
ti(int,t) = t,
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f6091,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f6092,plain,
( ? [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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 != one_one(int) ),
inference(pre_NNF_transformation,[status(thm)],[f274]) ).
fof(f6093,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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 != one_one(int) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f6092]) ).
fof(f6094,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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 != one_one(int) ),
inference(cnf_transformation,[status(thm)],[f6093]) ).
fof(f6095,plain,
( ? [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(pre_NNF_transformation,[status(thm)],[f275]) ).
fof(f6096,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f6095]) ).
fof(f6097,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(cnf_transformation,[status(thm)],[f6096]) ).
fof(f6128,plain,
! [Z,W_1] :
( ( ti(int,Z) = ti(int,W_1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1)) )
& ( ( ti(int,Z) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1)) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1)) ) ),
inference(NNF_transformation,[status(thm)],[f295]) ).
fof(f6129,plain,
( ! [Z,W_1] :
( ti(int,Z) = ti(int,W_1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1)) )
& ! [Z,W_1] :
( ( ti(int,Z) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z),W_1)) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z),W_1)) ) ),
inference(miniscoping,[status(thm)],[f6128]) ).
fof(f6132,plain,
! [X0,X1] :
( ti(int,X0) = ti(int,X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f6129]) ).
fof(f11852,plain,
pi != zero_zero(real),
inference(cnf_transformation,[status(thm)],[f2194]) ).
fof(f20541,plain,
monoid_mult(int),
inference(cnf_transformation,[status(thm)],[f5314]) ).
fof(f20544,plain,
semiring_1(int),
inference(cnf_transformation,[status(thm)],[f5317]) ).
fof(f20557,plain,
abs_if(int),
inference(cnf_transformation,[status(thm)],[f5330]) ).
fof(f20566,plain,
one(int),
inference(cnf_transformation,[status(thm)],[f5339]) ).
fof(f20596,plain,
monoid_mult(nat),
inference(cnf_transformation,[status(thm)],[f5369]) ).
fof(f20659,plain,
monoid_mult(rat),
inference(cnf_transformation,[status(thm)],[f5432]) ).
fof(f20676,plain,
abs_if(rat),
inference(cnf_transformation,[status(thm)],[f5449]) ).
fof(f20732,plain,
sgn_div_norm(real),
inference(cnf_transformation,[status(thm)],[f5505]) ).
fof(f20759,plain,
monoid_mult(real),
inference(cnf_transformation,[status(thm)],[f5532]) ).
fof(f20776,plain,
abs_if(real),
inference(cnf_transformation,[status(thm)],[f5549]) ).
fof(f20783,plain,
banach(real),
inference(cnf_transformation,[status(thm)],[f5556]) ).
fof(f20830,plain,
monoid_mult(complex),
inference(cnf_transformation,[status(thm)],[f5602]) ).
fof(f20850,plain,
banach(complex),
inference(cnf_transformation,[status(thm)],[f5622]) ).
fof(f20884,plain,
monoid_mult(code_code_numeral),
inference(cnf_transformation,[status(thm)],[f5655]) ).
fof(f20925,plain,
monoid_mult(quickcheck_code_int),
inference(cnf_transformation,[status(thm)],[f5696]) ).
fof(f20976,plain,
! [X,Y] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),Y),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != 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)),
inference(pre_NNF_transformation,[status(thm)],[f5739]) ).
fof(f20977,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(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))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != 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)),
inference(cnf_transformation,[status(thm)],[f20976]) ).
fof(f21483,definition,
( sQ0_spl
<=> t = one_one(int) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21485,plain,
( sQ0_spl
| t != one_one(int) ),
inference(component_clause,[status(thm)],[f21483]) ).
fof(f21486,definition,
( sQ1_spl
<=> hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21487,plain,
( ~ sQ1_spl
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)) ),
inference(component_clause,[status(thm)],[f21486]) ).
fof(f21489,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f6094,f21483,f21486]) ).
fof(f21490,definition,
( sQ2_spl
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21493,definition,
( sQ3_spl
<=> hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f21494,plain,
( ~ sQ3_spl
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3_skl),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = 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)) ),
inference(component_clause,[status(thm)],[f21493]) ).
fof(f21496,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f6097,f21490,f21493]) ).
fof(f23198,plain,
ti(int,one_one(int)) = one_one(int),
inference(resolution,[status(thm)],[f5830,f20566]) ).
fof(f27697,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21494,f20977]) ).
fof(f27698,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f27697]) ).
fof(f27699,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21487,f20977]) ).
fof(f27700,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f27699]) ).
fof(f28205,definition,
( sQ170_spl
<=> s = s ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f28207,plain,
( sQ170_spl
| s != s ),
inference(component_clause,[status(thm)],[f28205]) ).
fof(f28256,plain,
( sQ170_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f28207]) ).
fof(f28257,plain,
sQ170_spl,
inference(contradiction_clause,[status(thm)],[f28256]) ).
fof(f28430,definition,
( sQ184_spl
<=> banach(complex) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f28432,plain,
( sQ184_spl
| ~ banach(complex) ),
inference(component_clause,[status(thm)],[f28430]) ).
fof(f28437,definition,
( sQ186_spl
<=> banach(real) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f28439,plain,
( sQ186_spl
| ~ banach(real) ),
inference(component_clause,[status(thm)],[f28437]) ).
fof(f28444,plain,
( sQ186_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28439,f20783]) ).
fof(f28445,plain,
sQ186_spl,
inference(contradiction_clause,[status(thm)],[f28444]) ).
fof(f28446,plain,
( sQ184_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28432,f20850]) ).
fof(f28447,plain,
sQ184_spl,
inference(contradiction_clause,[status(thm)],[f28446]) ).
fof(f29317,definition,
( sQ198_spl
<=> monoid_mult(quickcheck_code_int) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f29319,plain,
( sQ198_spl
| ~ monoid_mult(quickcheck_code_int) ),
inference(component_clause,[status(thm)],[f29317]) ).
fof(f29324,definition,
( sQ200_spl
<=> monoid_mult(code_code_numeral) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f29326,plain,
( sQ200_spl
| ~ monoid_mult(code_code_numeral) ),
inference(component_clause,[status(thm)],[f29324]) ).
fof(f29331,definition,
( sQ202_spl
<=> monoid_mult(complex) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f29333,plain,
( sQ202_spl
| ~ monoid_mult(complex) ),
inference(component_clause,[status(thm)],[f29331]) ).
fof(f29338,definition,
( sQ204_spl
<=> monoid_mult(real) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f29340,plain,
( sQ204_spl
| ~ monoid_mult(real) ),
inference(component_clause,[status(thm)],[f29338]) ).
fof(f29345,definition,
( sQ206_spl
<=> monoid_mult(rat) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f29347,plain,
( sQ206_spl
| ~ monoid_mult(rat) ),
inference(component_clause,[status(thm)],[f29345]) ).
fof(f29352,definition,
( sQ208_spl
<=> monoid_mult(nat) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f29354,plain,
( sQ208_spl
| ~ monoid_mult(nat) ),
inference(component_clause,[status(thm)],[f29352]) ).
fof(f29359,definition,
( sQ210_spl
<=> monoid_mult(int) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f29361,plain,
( sQ210_spl
| ~ monoid_mult(int) ),
inference(component_clause,[status(thm)],[f29359]) ).
fof(f29366,plain,
( sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29361,f20541]) ).
fof(f29367,plain,
sQ210_spl,
inference(contradiction_clause,[status(thm)],[f29366]) ).
fof(f29368,plain,
( sQ208_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29354,f20596]) ).
fof(f29369,plain,
sQ208_spl,
inference(contradiction_clause,[status(thm)],[f29368]) ).
fof(f29370,plain,
( sQ206_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29347,f20659]) ).
fof(f29371,plain,
sQ206_spl,
inference(contradiction_clause,[status(thm)],[f29370]) ).
fof(f29372,plain,
( sQ204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29340,f20759]) ).
fof(f29373,plain,
sQ204_spl,
inference(contradiction_clause,[status(thm)],[f29372]) ).
fof(f29374,plain,
( sQ202_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29333,f20830]) ).
fof(f29375,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f29374]) ).
fof(f29376,plain,
( sQ200_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29326,f20884]) ).
fof(f29377,plain,
sQ200_spl,
inference(contradiction_clause,[status(thm)],[f29376]) ).
fof(f29378,plain,
( sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29319,f20925]) ).
fof(f29379,plain,
sQ198_spl,
inference(contradiction_clause,[status(thm)],[f29378]) ).
fof(f29519,definition,
! [X0] :
( sQ220_spl
<=> X0 = zero_zero(real) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f29520,plain,
! [X0] :
( ~ sQ220_spl
| X0 = zero_zero(real) ),
inference(component_clause,[status(thm)],[f29519]) ).
fof(f29526,plain,
( ~ sQ220_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f11852,f29520]) ).
fof(f29537,plain,
~ sQ220_spl,
inference(contradiction_clause,[status(thm)],[f29526]) ).
fof(f29669,definition,
( sQ225_spl
<=> semiring_1(int) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f29671,plain,
( sQ225_spl
| ~ semiring_1(int) ),
inference(component_clause,[status(thm)],[f29669]) ).
fof(f29676,plain,
( sQ225_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29671,f20544]) ).
fof(f29677,plain,
sQ225_spl,
inference(contradiction_clause,[status(thm)],[f29676]) ).
fof(f30156,definition,
( sQ234_spl
<=> ti(int,min_1) = min_1 ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f30158,plain,
( sQ234_spl
| ti(int,min_1) != min_1 ),
inference(component_clause,[status(thm)],[f30156]) ).
fof(f30162,plain,
( sQ234_spl
| min_1 != min_1 ),
inference(forward_demodulation,[status(thm)],[f5877,f30158]) ).
fof(f30163,plain,
( sQ234_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f30162]) ).
fof(f30164,plain,
sQ234_spl,
inference(contradiction_clause,[status(thm)],[f30163]) ).
fof(f30187,definition,
( sQ235_spl
<=> abs_if(real) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f30189,plain,
( sQ235_spl
| ~ abs_if(real) ),
inference(component_clause,[status(thm)],[f30187]) ).
fof(f30194,plain,
( sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30189,f20776]) ).
fof(f30195,plain,
sQ235_spl,
inference(contradiction_clause,[status(thm)],[f30194]) ).
fof(f30200,definition,
( sQ237_spl
<=> abs_if(rat) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f30202,plain,
( sQ237_spl
| ~ abs_if(rat) ),
inference(component_clause,[status(thm)],[f30200]) ).
fof(f30207,plain,
( sQ237_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30202,f20676]) ).
fof(f30208,plain,
sQ237_spl,
inference(contradiction_clause,[status(thm)],[f30207]) ).
fof(f30213,definition,
( sQ239_spl
<=> abs_if(int) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f30215,plain,
( sQ239_spl
| ~ abs_if(int) ),
inference(component_clause,[status(thm)],[f30213]) ).
fof(f30220,plain,
( sQ239_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30215,f20557]) ).
fof(f30221,plain,
sQ239_spl,
inference(contradiction_clause,[status(thm)],[f30220]) ).
fof(f30226,definition,
( sQ241_spl
<=> sgn_div_norm(real) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f30228,plain,
( sQ241_spl
| ~ sgn_div_norm(real) ),
inference(component_clause,[status(thm)],[f30226]) ).
fof(f30233,plain,
( sQ241_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30228,f20732]) ).
fof(f30234,plain,
sQ241_spl,
inference(contradiction_clause,[status(thm)],[f30233]) ).
fof(f30257,plain,
( ti(int,one_one(int)) = ti(int,t)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(resolution,[status(thm)],[f6132,f6091]) ).
fof(f30263,definition,
( sQ247_spl
<=> ti(int,one_one(int)) = ti(int,t) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f30264,plain,
( ~ sQ247_spl
| ti(int,one_one(int)) = ti(int,t) ),
inference(component_clause,[status(thm)],[f30263]) ).
fof(f30266,plain,
( sQ247_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f30257,f21490,f30263]) ).
fof(f30272,plain,
( ~ sQ247_spl
| one_one(int) = ti(int,t) ),
inference(forward_demodulation,[status(thm)],[f23198,f30264]) ).
fof(f30273,plain,
( ~ sQ247_spl
| one_one(int) = t ),
inference(forward_demodulation,[status(thm)],[f6090,f30272]) ).
fof(f30274,plain,
( ~ sQ247_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30273,f21485]) ).
fof(f30275,plain,
( ~ sQ247_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f30274]) ).
fof(f30276,plain,
$false,
inference(sat_refutation,[status(thm)],[f21489,f21496,f27698,f27700,f28257,f28445,f28447,f29367,f29369,f29371,f29373,f29375,f29377,f29379,f29537,f29677,f30164,f30195,f30208,f30221,f30234,f30266,f30275]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.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:18:42 UTC 2026
% 0.08/0.35 % CPUTime :
% 1.15/1.45 % Drodi V4.1.1
% 1.28/2.19 % Refutation found
% 1.28/2.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.28/2.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.40/2.37 % Elapsed time: 2.000594 seconds
% 6.40/2.37 % CPU time: 7.205771 seconds
% 6.40/2.37 % Total memory used: 995.680 MB
% 6.40/2.37 % Net memory used: 992.035 MB
%------------------------------------------------------------------------------