%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : NUM925^1 : TPTP v9.2.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 09:25:06 AM UTC 2026
% Result : Theorem 0.29s 1.36s
% Output : Refutation 0.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 49 ( 30 unt; 0 typ; 1 def)
% Number of atoms : 147 ( 67 equ; 0 cnn)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 311 ( 34 ~; 22 |; 7 &; 241 @)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 23 ( 20 usr; 10 con; 0-2 aty)
% Number of variables : 34 ( 0 ^; 34 !; 0 ?; 34 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
int: $tType ).
thf(type_def_6,type,
nat: $tType ).
thf(func_def_0,type,
int: $tType ).
thf(func_def_1,type,
nat: $tType ).
thf(func_def_2,type,
one_one_int: int ).
thf(func_def_3,type,
one_one_nat: nat ).
thf(func_def_4,type,
plus_plus_int: int > int > int ).
thf(func_def_5,type,
plus_plus_nat: nat > nat > nat ).
thf(func_def_6,type,
zero_zero_int: int ).
thf(func_def_7,type,
zero_zero_nat: nat ).
thf(func_def_8,type,
bit0: int > int ).
thf(func_def_9,type,
bit1: int > int ).
thf(func_def_10,type,
pls: int ).
thf(func_def_11,type,
number_number_of_int: int > int ).
thf(func_def_12,type,
number_number_of_nat: int > nat ).
thf(func_def_13,type,
semiri1621563631at_int: nat > int ).
thf(func_def_14,type,
semiri984289939at_nat: nat > nat ).
thf(func_def_15,type,
ord_less_int: int > int > $o ).
thf(func_def_16,type,
ord_less_nat: nat > nat > $o ).
thf(func_def_17,type,
power_power_int: int > nat > int ).
thf(func_def_18,type,
power_power_nat: nat > nat > nat ).
thf(func_def_19,type,
n: nat ).
thf(func_def_20,type,
t: int ).
thf(f478,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f457,f475]) ).
thf(f475,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[status(thm)],[f474]) ).
thf(f474,plain,
( $false
| ~ spl0_1 ),
inference(subsumption_resolution,[status(thm)],[f467,f302]) ).
thf(f302,plain,
! [X0: nat] :
( ( ord_less_int @ ( semiri1621563631at_int @ X0 ) @ zero_zero_int )
!= $true ),
inference(cnf_transformation,[status(thm)],[f204]) ).
thf(f204,plain,
! [X0: nat] :
( ( ord_less_int @ ( semiri1621563631at_int @ X0 ) @ zero_zero_int )
!= $true ),
inference(flattening,[status(thm)],[f115]) ).
thf(f115,plain,
! [X0: nat] :
( ( ord_less_int @ ( semiri1621563631at_int @ X0 ) @ zero_zero_int )
!= $true ),
inference(fool_elimination,[status(thm)],[f114]) ).
thf(f114,plain,
! [X0: nat] :
~ ( ord_less_int @ ( semiri1621563631at_int @ X0 ) @ zero_zero_int ),
inference(rectify,[status(thm)],[f67]) ).
thf(f67,axiom,
! [X6: nat] :
~ ( ord_less_int @ ( semiri1621563631at_int @ X6 ) @ zero_zero_int ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_66_int__less__0__conv) ).
thf(f467,plain,
( ( $true
= ( ord_less_int @ ( semiri1621563631at_int @ n ) @ zero_zero_int ) )
| ~ spl0_1 ),
inference(superposition,[status(thm)],[f413,f444]) ).
thf(f444,plain,
( ( zero_zero_int
= ( plus_plus_int @ ( semiri1621563631at_int @ n ) @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) )
| ~ spl0_1 ),
inference(avatar_component_clause,[status(thm)],[f442]) ).
thf(f442,definition,
( spl0_1
<=> ( zero_zero_int
= ( plus_plus_int @ ( semiri1621563631at_int @ n ) @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition]) ).
thf(f413,plain,
! [X1: int] :
( ( ord_less_int @ X1 @ ( plus_plus_int @ X1 @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) )
= $true ),
inference(equality_resolution,[status(thm)],[f381]) ).
thf(f381,plain,
! [X0: int,X1: int] :
( ( ( ord_less_int @ X1 @ ( plus_plus_int @ X0 @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) )
= $true )
| ( X0 != X1 ) ),
inference(definition_unfolding,[status(thm)],[f299,f352]) ).
thf(f352,plain,
( one_one_int
= ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ),
inference(definition_unfolding,[status(thm)],[f278,f313]) ).
thf(f313,plain,
zero_zero_int = pls,
inference(cnf_transformation,[status(thm)],[f79]) ).
thf(f79,axiom,
zero_zero_int = pls,
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_78_Pls__def) ).
thf(f278,plain,
( one_one_int
= ( number_number_of_int @ ( bit1 @ pls ) ) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
thf(f18,axiom,
( one_one_int
= ( number_number_of_int @ ( bit1 @ pls ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_17_numeral__1__eq__1) ).
thf(f299,plain,
! [X0: int,X1: int] :
( ( $true
= ( ord_less_int @ X1 @ ( plus_plus_int @ X0 @ one_one_int ) ) )
| ( X0 != X1 ) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
thf(f231,plain,
! [X0: int,X1: int] :
( ( ( X0 = X1 )
| ( ( ord_less_int @ X1 @ X0 )
= $true )
| ( $true
!= ( ord_less_int @ X1 @ ( plus_plus_int @ X0 @ one_one_int ) ) ) )
& ( ( $true
= ( ord_less_int @ X1 @ ( plus_plus_int @ X0 @ one_one_int ) ) )
| ( ( X0 != X1 )
& ( ( ord_less_int @ X1 @ X0 )
!= $true ) ) ) ),
inference(rectify,[status(thm)],[f230]) ).
thf(f230,plain,
! [X1: int,X0: int] :
( ( ( X0 = X1 )
| ( ( ord_less_int @ X0 @ X1 )
= $true )
| ( $true
!= ( ord_less_int @ X0 @ ( plus_plus_int @ X1 @ one_one_int ) ) ) )
& ( ( $true
= ( ord_less_int @ X0 @ ( plus_plus_int @ X1 @ one_one_int ) ) )
| ( ( X0 != X1 )
& ( ( ord_less_int @ X0 @ X1 )
!= $true ) ) ) ),
inference(flattening,[status(thm)],[f229]) ).
thf(f229,plain,
! [X1: int,X0: int] :
( ( ( X0 = X1 )
| ( ( ord_less_int @ X0 @ X1 )
= $true )
| ( $true
!= ( ord_less_int @ X0 @ ( plus_plus_int @ X1 @ one_one_int ) ) ) )
& ( ( $true
= ( ord_less_int @ X0 @ ( plus_plus_int @ X1 @ one_one_int ) ) )
| ( ( X0 != X1 )
& ( ( ord_less_int @ X0 @ X1 )
!= $true ) ) ) ),
inference(nnf_transformation,[status(thm)],[f153]) ).
thf(f153,plain,
! [X1: int,X0: int] :
( ( ( X0 = X1 )
| ( ( ord_less_int @ X0 @ X1 )
= $true ) )
<=> ( $true
= ( ord_less_int @ X0 @ ( plus_plus_int @ X1 @ one_one_int ) ) ) ),
inference(fool_elimination,[status(thm)],[f152]) ).
thf(f152,plain,
! [X0: int,X1: int] :
( ( ( X0 = X1 )
| ( ord_less_int @ X0 @ X1 ) )
<=> ( ord_less_int @ X0 @ ( plus_plus_int @ X1 @ one_one_int ) ) ),
inference(rectify,[status(thm)],[f66]) ).
thf(f66,axiom,
! [X9: int,X14: int] :
( ( ( X9 = X14 )
| ( ord_less_int @ X9 @ X14 ) )
<=> ( ord_less_int @ X9 @ ( plus_plus_int @ X14 @ one_one_int ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_65_zless__add1__eq) ).
thf(f457,plain,
spl0_1,
inference(avatar_split_clause,[status(thm)],[f456,f442]) ).
thf(f456,plain,
( zero_zero_int
= ( plus_plus_int @ ( semiri1621563631at_int @ n ) @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) ),
inference(subsumption_resolution,[status(thm)],[f429,f379]) ).
thf(f379,plain,
( $true
!= ( ord_less_int @ zero_zero_int @ zero_zero_int ) ),
inference(definition_unfolding,[status(thm)],[f296,f313,f313]) ).
thf(f296,plain,
( ( ord_less_int @ pls @ pls )
!= $true ),
inference(cnf_transformation,[status(thm)],[f216]) ).
thf(f216,plain,
( ( ord_less_int @ pls @ pls )
!= $true ),
inference(flattening,[status(thm)],[f141]) ).
thf(f141,plain,
( ( ord_less_int @ pls @ pls )
!= $true ),
inference(fool_elimination,[status(thm)],[f140]) ).
thf(f140,plain,
~ ( ord_less_int @ pls @ pls ),
inference(rectify,[status(thm)],[f37]) ).
thf(f37,axiom,
~ ( ord_less_int @ pls @ pls ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_36_rel__simps_I2_J) ).
thf(f429,plain,
( ( $true
= ( ord_less_int @ zero_zero_int @ zero_zero_int ) )
| ( zero_zero_int
= ( plus_plus_int @ ( semiri1621563631at_int @ n ) @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) ) ),
inference(superposition,[status(thm)],[f374,f425]) ).
thf(f425,plain,
( zero_zero_int
= ( power_power_int @ ( plus_plus_int @ ( semiri1621563631at_int @ n ) @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ zero_zero_int ) ) ) ) ),
inference(forward_demodulation,[status(thm)],[f396,f320]) ).
thf(f320,plain,
! [X0: int,X1: int] :
( ( plus_plus_int @ X0 @ X1 )
= ( plus_plus_int @ X1 @ X0 ) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
thf(f183,plain,
! [X0: int,X1: int] :
( ( plus_plus_int @ X0 @ X1 )
= ( plus_plus_int @ X1 @ X0 ) ),
inference(rectify,[status(thm)],[f53]) ).
thf(f53,axiom,
! [X14: int,X9: int] :
( ( plus_plus_int @ X14 @ X9 )
= ( plus_plus_int @ X9 @ X14 ) ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_52_zadd__commute) ).
thf(f396,plain,
( zero_zero_int
= ( power_power_int @ ( plus_plus_int @ ( number_number_of_int @ ( bit1 @ zero_zero_int ) ) @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ zero_zero_int ) ) ) ) ),
inference(definition_unfolding,[status(thm)],[f325,f352,f313]) ).
thf(f325,plain,
( zero_zero_int
= ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
thf(f176,plain,
( zero_zero_int
= ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ),
inference(flattening,[status(thm)],[f108]) ).
thf(f108,negated_conjecture,
~ ( ( zero_zero_int
!= ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f107]) ).
thf(f107,conjecture,
( zero_zero_int
!= ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',conj_0) ).
thf(f374,plain,
! [X0: int] :
( ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ zero_zero_int ) ) ) ) )
= $true )
| ( zero_zero_int = X0 ) ),
inference(definition_unfolding,[status(thm)],[f290,f313]) ).
thf(f290,plain,
! [X0: int] :
( ( $true
= ( ord_less_int @ zero_zero_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
| ( zero_zero_int = X0 ) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
thf(f225,plain,
! [X0: int] :
( ( ( $true
= ( ord_less_int @ zero_zero_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
| ( zero_zero_int = X0 ) )
& ( ( zero_zero_int != X0 )
| ( $true
!= ( ord_less_int @ zero_zero_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ) ),
inference(nnf_transformation,[status(thm)],[f169]) ).
thf(f169,plain,
! [X0: int] :
( ( $true
= ( ord_less_int @ zero_zero_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
<=> ( zero_zero_int != X0 ) ),
inference(fool_elimination,[status(thm)],[f168]) ).
thf(f168,plain,
! [X0: int] :
( ( ord_less_int @ zero_zero_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
<=> ( zero_zero_int != X0 ) ),
inference(rectify,[status(thm)],[f104]) ).
thf(f104,axiom,
! [X45: int] :
( ( ord_less_int @ zero_zero_int @ ( power_power_int @ X45 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
<=> ( zero_zero_int != X45 ) ),
file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_103_zero__less__power2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM925^1 : TPTP v9.2.1. Released v5.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.33 % Computer : n019.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue Feb 24 11:17:54 EST 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.33 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/0.44 ---- Original DTF file ---
% 0.18/0.45 thf(spec,logic,$$dhol).
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 % File : NUM925^1 : TPTP v9.2.1. Released v5.3.0.
% 0.18/0.45 % Domain : Number Theory
% 0.18/0.45 % Problem : Sum of two squares line 192, 100 axioms selected
% 0.18/0.45 % Version : Especial.
% 0.18/0.45 % English :
% 0.18/0.45
% 0.18/0.45 % Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day
% 0.18/0.45 % : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe
% 0.18/0.45 % Source : [Bla11]
% 0.18/0.45 % Names : s2s_100_thf_l192 [Bla11]
% 0.18/0.45
% 0.18/0.45 % Status : Theorem
% 0.18/0.45 % Rating : 0.11 v9.1.0, 0.12 v9.0.0, 0.10 v8.2.0, 0.08 v8.1.0, 0.18 v7.5.0, 0.14 v7.4.0, 0.22 v7.2.0, 0.12 v7.1.0, 0.38 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.43 v5.5.0, 0.33 v5.4.0, 0.40 v5.3.0
% 0.18/0.45 % Syntax : Number of formulae : 128 ( 66 unt; 21 typ; 0 def)
% 0.18/0.45 % Number of atoms : 163 ( 105 equ; 0 cnn)
% 0.18/0.45 % Maximal formula atoms : 7 ( 1 avg)
% 0.18/0.45 % Number of connectives : 571 ( 20 ~; 4 |; 7 &; 495 @)
% 0.18/0.45 % ( 36 <=>; 9 =>; 0 <=; 0 <~>)
% 0.18/0.45 % Maximal formula depth : 11 ( 4 avg)
% 0.18/0.45 % Number of types : 3 ( 2 usr)
% 0.18/0.45 % Number of type conns : 18 ( 18 >; 0 *; 0 +; 0 <<)
% 0.18/0.45 % Number of symbols : 20 ( 19 usr; 7 con; 0-2 aty)
% 0.18/0.45 % Number of variables : 118 ( 0 ^; 118 !; 0 ?; 118 :)
% 0.18/0.45 % SPC : TH0_THM_EQU_NAR
% 0.18/0.45
% 0.18/0.45 % Comments : This file was generated by Isabelle (most likely Sledgehammer)
% 0.18/0.45 % 2011-08-09 19:10:38
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 %----Should-be-implicit typings (2)
% 0.18/0.45 thf(ty_ty_tc__Int__Oint,type,
% 0.18/0.45 int: $tType ).
% 0.18/0.45
% 0.18/0.45 thf(ty_ty_tc__Nat__Onat,type,
% 0.18/0.45 nat: $tType ).
% 0.18/0.45
% 0.18/0.45 %----Explicit typings (19)
% 0.18/0.45 thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,
% 0.18/0.45 one_one_int: int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,
% 0.18/0.45 one_one_nat: nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,
% 0.18/0.45 plus_plus_int: int > int > int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,
% 0.18/0.45 plus_plus_nat: nat > nat > nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Int__Oint,type,
% 0.18/0.45 zero_zero_int: int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Nat__Onat,type,
% 0.18/0.45 zero_zero_nat: nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Int_OBit0,type,
% 0.18/0.45 bit0: int > int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Int_OBit1,type,
% 0.18/0.45 bit1: int > int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Int_OPls,type,
% 0.18/0.45 pls: int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,
% 0.18/0.45 number_number_of_int: int > int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,
% 0.18/0.45 number_number_of_nat: int > nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Int__Oint,type,
% 0.18/0.45 semiri1621563631at_int: nat > int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Nat__Onat,type,
% 0.18/0.45 semiri984289939at_nat: nat > nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,
% 0.18/0.45 ord_less_int: int > int > $o ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,
% 0.18/0.45 ord_less_nat: nat > nat > $o ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,
% 0.18/0.45 power_power_int: int > nat > int ).
% 0.18/0.45
% 0.18/0.45 thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,
% 0.18/0.45 power_power_nat: nat > nat > nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_v_n____,type,
% 0.18/0.45 n: nat ).
% 0.18/0.45
% 0.18/0.45 thf(sy_v_t____,type,
% 0.18/0.45 t: int ).
% 0.18/0.45
% 0.18/0.45 %----Relevant facts (106)
% 0.18/0.45 thf(fact_0_n1pos,axiom,
% 0.18/0.45 ord_less_int @ zero_zero_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_1_t1,axiom,
% 0.18/0.45 ord_less_int @ one_one_int @ t ).
% 0.18/0.45
% 0.18/0.45 thf(fact_2_sum__power2__eq__zero__iff,axiom,
% 0.18/0.45 ! [X_3: int,Y_3: int] :
% 0.18/0.45 ( ( ( plus_plus_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.18/0.45 = zero_zero_int )
% 0.18/0.45 <=> ( ( X_3 = zero_zero_int )
% 0.18/0.45 & ( Y_3 = zero_zero_int ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_3_one__power2,axiom,
% 0.18/0.45 ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 = one_one_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_4_one__power2,axiom,
% 0.18/0.45 ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 = one_one_nat ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_5_zero__power2,axiom,
% 0.18/0.45 ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 = zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_6_zero__power2,axiom,
% 0.18/0.45 ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 = zero_zero_nat ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_7_zero__eq__power2,axiom,
% 0.18/0.45 ! [A_7: int] :
% 0.18/0.45 ( ( ( power_power_int @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 = zero_zero_int )
% 0.18/0.45 <=> ( A_7 = zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_8_add__special_I2_J,axiom,
% 0.18/0.45 ! [W_7: int] :
% 0.18/0.45 ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_7 ) )
% 0.18/0.45 = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_7 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_9_add__special_I3_J,axiom,
% 0.18/0.45 ! [V_5: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( number_number_of_int @ V_5 ) @ one_one_int )
% 0.18/0.45 = ( number_number_of_int @ ( plus_plus_int @ V_5 @ ( bit1 @ pls ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_10_one__add__one__is__two,axiom,
% 0.18/0.45 ( ( plus_plus_int @ one_one_int @ one_one_int )
% 0.18/0.45 = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_11_semiring__one__add__one__is__two,axiom,
% 0.18/0.45 ( ( plus_plus_int @ one_one_int @ one_one_int )
% 0.18/0.45 = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_12_semiring__one__add__one__is__two,axiom,
% 0.18/0.45 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 0.18/0.45 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_13_quartic__square__square,axiom,
% 0.18/0.45 ! [X_3: int] :
% 0.18/0.45 ( ( power_power_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 = ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_14_power__0__left__number__of,axiom,
% 0.18/0.45 ! [W_6: int] :
% 0.18/0.45 ( ( ( ( number_number_of_nat @ W_6 )
% 0.18/0.45 = zero_zero_nat )
% 0.18/0.45 => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) )
% 0.18/0.45 = one_one_int ) )
% 0.18/0.45 & ( ( ( number_number_of_nat @ W_6 )
% 0.18/0.45 != zero_zero_nat )
% 0.18/0.45 => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) )
% 0.18/0.45 = zero_zero_int ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_15_power__0__left__number__of,axiom,
% 0.18/0.45 ! [W_6: int] :
% 0.18/0.45 ( ( ( ( number_number_of_nat @ W_6 )
% 0.18/0.45 = zero_zero_nat )
% 0.18/0.45 => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) )
% 0.18/0.45 = one_one_nat ) )
% 0.18/0.45 & ( ( ( number_number_of_nat @ W_6 )
% 0.18/0.45 != zero_zero_nat )
% 0.18/0.45 => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) )
% 0.18/0.45 = zero_zero_nat ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_16_semiring__norm_I110_J,axiom,
% 0.18/0.45 ( one_one_int
% 0.18/0.45 = ( number_number_of_int @ ( bit1 @ pls ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_17_numeral__1__eq__1,axiom,
% 0.18/0.45 ( ( number_number_of_int @ ( bit1 @ pls ) )
% 0.18/0.45 = one_one_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_18_n0,axiom,
% 0.18/0.45 ord_less_nat @ zero_zero_nat @ n ).
% 0.18/0.45
% 0.18/0.45 thf(fact_19_zless__linear,axiom,
% 0.18/0.45 ! [X_3: int,Y_3: int] :
% 0.18/0.45 ( ( ord_less_int @ X_3 @ Y_3 )
% 0.18/0.45 | ( X_3 = Y_3 )
% 0.18/0.45 | ( ord_less_int @ Y_3 @ X_3 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_20_less__number__of__int__code,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 0.18/0.45 <=> ( ord_less_int @ K @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_21_plus__numeral__code_I9_J,axiom,
% 0.18/0.45 ! [V_3: int,W_4: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( number_number_of_int @ V_3 ) @ ( number_number_of_int @ W_4 ) )
% 0.18/0.45 = ( number_number_of_int @ ( plus_plus_int @ V_3 @ W_4 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_22_less__number__of,axiom,
% 0.18/0.45 ! [X_6: int,Y_5: int] :
% 0.18/0.45 ( ( ord_less_int @ ( number_number_of_int @ X_6 ) @ ( number_number_of_int @ Y_5 ) )
% 0.18/0.45 <=> ( ord_less_int @ X_6 @ Y_5 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_23_zero__is__num__zero,axiom,
% 0.18/0.45 ( zero_zero_int
% 0.18/0.45 = ( number_number_of_int @ pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_24_zpower__int,axiom,
% 0.18/0.45 ! [M: nat,N_1: nat] :
% 0.18/0.45 ( ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 )
% 0.18/0.45 = ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_25_int__power,axiom,
% 0.18/0.45 ! [M: nat,N_1: nat] :
% 0.18/0.45 ( ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) )
% 0.18/0.45 = ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_26_zadd__int__left,axiom,
% 0.18/0.45 ! [M: nat,N_1: nat,Z: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( plus_plus_int @ ( semiri1621563631at_int @ N_1 ) @ Z ) )
% 0.18/0.45 = ( plus_plus_int @ ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) @ Z ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_27_zadd__int,axiom,
% 0.18/0.45 ! [M: nat,N_1: nat] :
% 0.18/0.45 ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( semiri1621563631at_int @ N_1 ) )
% 0.18/0.45 = ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_28_int__1,axiom,
% 0.18/0.45 ( ( semiri1621563631at_int @ one_one_nat )
% 0.18/0.45 = one_one_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_29_nat__number__of__Pls,axiom,
% 0.18/0.45 ( ( number_number_of_nat @ pls )
% 0.18/0.45 = zero_zero_nat ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_30_semiring__norm_I113_J,axiom,
% 0.18/0.45 ( zero_zero_nat
% 0.18/0.45 = ( number_number_of_nat @ pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_31_int__eq__0__conv,axiom,
% 0.18/0.45 ! [N_1: nat] :
% 0.18/0.45 ( ( ( semiri1621563631at_int @ N_1 )
% 0.18/0.45 = zero_zero_int )
% 0.18/0.45 <=> ( N_1 = zero_zero_nat ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_32_int__0,axiom,
% 0.18/0.45 ( ( semiri1621563631at_int @ zero_zero_nat )
% 0.18/0.45 = zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_33_nat__1__add__1,axiom,
% 0.18/0.45 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 0.18/0.45 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_34_less__int__code_I16_J,axiom,
% 0.18/0.45 ! [K1: int,K2: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 0.18/0.45 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_35_rel__simps_I17_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 0.18/0.45 <=> ( ord_less_int @ K @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_36_rel__simps_I2_J,axiom,
% 0.18/0.45 ~ ( ord_less_int @ pls @ pls ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_37_less__int__code_I13_J,axiom,
% 0.18/0.45 ! [K1: int,K2: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 0.18/0.45 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_38_rel__simps_I14_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.18/0.45 <=> ( ord_less_int @ K @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_39_zadd__strict__right__mono,axiom,
% 0.18/0.45 ! [K: int,I: int,J: int] :
% 0.18/0.45 ( ( ord_less_int @ I @ J )
% 0.18/0.45 => ( ord_less_int @ ( plus_plus_int @ I @ K ) @ ( plus_plus_int @ J @ K ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_40_add__nat__number__of,axiom,
% 0.18/0.45 ! [V_4: int,V_3: int] :
% 0.18/0.45 ( ( ( ord_less_int @ V_3 @ pls )
% 0.18/0.45 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) )
% 0.18/0.45 = ( number_number_of_nat @ V_4 ) ) )
% 0.18/0.45 & ( ~ ( ord_less_int @ V_3 @ pls )
% 0.18/0.45 => ( ( ( ord_less_int @ V_4 @ pls )
% 0.18/0.45 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) )
% 0.18/0.45 = ( number_number_of_nat @ V_3 ) ) )
% 0.18/0.45 & ( ~ ( ord_less_int @ V_4 @ pls )
% 0.18/0.45 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) )
% 0.18/0.45 = ( number_number_of_nat @ ( plus_plus_int @ V_3 @ V_4 ) ) ) ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_41_one__is__num__one,axiom,
% 0.18/0.45 ( one_one_int
% 0.18/0.45 = ( number_number_of_int @ ( bit1 @ pls ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_42_nat__numeral__1__eq__1,axiom,
% 0.18/0.45 ( ( number_number_of_nat @ ( bit1 @ pls ) )
% 0.18/0.45 = one_one_nat ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_43_Numeral1__eq1__nat,axiom,
% 0.18/0.45 ( one_one_nat
% 0.18/0.45 = ( number_number_of_nat @ ( bit1 @ pls ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_44_eq__number__of,axiom,
% 0.18/0.45 ! [X_5: int,Y_4: int] :
% 0.18/0.45 ( ( ( number_number_of_int @ X_5 )
% 0.18/0.45 = ( number_number_of_int @ Y_4 ) )
% 0.18/0.45 <=> ( X_5 = Y_4 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_45_number__of__reorient,axiom,
% 0.18/0.45 ! [W_5: int,X_4: nat] :
% 0.18/0.45 ( ( ( number_number_of_nat @ W_5 )
% 0.18/0.45 = X_4 )
% 0.18/0.45 <=> ( X_4
% 0.18/0.45 = ( number_number_of_nat @ W_5 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_46_number__of__reorient,axiom,
% 0.18/0.45 ! [W_5: int,X_4: int] :
% 0.18/0.45 ( ( ( number_number_of_int @ W_5 )
% 0.18/0.45 = X_4 )
% 0.18/0.45 <=> ( X_4
% 0.18/0.45 = ( number_number_of_int @ W_5 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_47_rel__simps_I51_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( ( bit1 @ K )
% 0.18/0.45 = ( bit1 @ L ) )
% 0.18/0.45 <=> ( K = L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_48_rel__simps_I48_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( ( bit0 @ K )
% 0.18/0.45 = ( bit0 @ L ) )
% 0.18/0.45 <=> ( K = L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_49_even__less__0__iff,axiom,
% 0.18/0.45 ! [A_6: int] :
% 0.18/0.45 ( ( ord_less_int @ ( plus_plus_int @ A_6 @ A_6 ) @ zero_zero_int )
% 0.18/0.45 <=> ( ord_less_int @ A_6 @ zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_50_zadd__assoc,axiom,
% 0.18/0.45 ! [Z1: int,Z2: int,Z3: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 )
% 0.18/0.45 = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_51_zadd__left__commute,axiom,
% 0.18/0.45 ! [X_3: int,Y_3: int,Z: int] :
% 0.18/0.45 ( ( plus_plus_int @ X_3 @ ( plus_plus_int @ Y_3 @ Z ) )
% 0.18/0.45 = ( plus_plus_int @ Y_3 @ ( plus_plus_int @ X_3 @ Z ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_52_zadd__commute,axiom,
% 0.18/0.45 ! [Z: int,W_4: int] :
% 0.18/0.45 ( ( plus_plus_int @ Z @ W_4 )
% 0.18/0.45 = ( plus_plus_int @ W_4 @ Z ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_53_int__int__eq,axiom,
% 0.18/0.45 ! [M: nat,N_1: nat] :
% 0.18/0.45 ( ( ( semiri1621563631at_int @ M )
% 0.18/0.45 = ( semiri1621563631at_int @ N_1 ) )
% 0.18/0.45 <=> ( M = N_1 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_54_less__special_I3_J,axiom,
% 0.18/0.45 ! [X_2: int] :
% 0.18/0.45 ( ( ord_less_int @ ( number_number_of_int @ X_2 ) @ zero_zero_int )
% 0.18/0.45 <=> ( ord_less_int @ X_2 @ pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_55_less__special_I1_J,axiom,
% 0.18/0.45 ! [Y_2: int] :
% 0.18/0.45 ( ( ord_less_int @ zero_zero_int @ ( number_number_of_int @ Y_2 ) )
% 0.18/0.45 <=> ( ord_less_int @ pls @ Y_2 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_56_rel__simps_I12_J,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit1 @ K ) @ pls )
% 0.18/0.45 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_57_less__int__code_I15_J,axiom,
% 0.18/0.45 ! [K1: int,K2: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 0.18/0.45 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_58_rel__simps_I16_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.18/0.45 <=> ( ord_less_int @ K @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_59_rel__simps_I10_J,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit0 @ K ) @ pls )
% 0.18/0.45 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_60_rel__simps_I4_J,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( ord_less_int @ pls @ ( bit0 @ K ) )
% 0.18/0.45 <=> ( ord_less_int @ pls @ K ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_61_bin__less__0__simps_I4_J,axiom,
% 0.18/0.45 ! [W_4: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit1 @ W_4 ) @ zero_zero_int )
% 0.18/0.45 <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_62_bin__less__0__simps_I1_J,axiom,
% 0.18/0.45 ~ ( ord_less_int @ pls @ zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_63_bin__less__0__simps_I3_J,axiom,
% 0.18/0.45 ! [W_4: int] :
% 0.18/0.45 ( ( ord_less_int @ ( bit0 @ W_4 ) @ zero_zero_int )
% 0.18/0.45 <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_64_int__0__less__1,axiom,
% 0.18/0.45 ord_less_int @ zero_zero_int @ one_one_int ).
% 0.18/0.45
% 0.18/0.45 thf(fact_65_zless__add1__eq,axiom,
% 0.18/0.45 ! [W_4: int,Z: int] :
% 0.18/0.45 ( ( ord_less_int @ W_4 @ ( plus_plus_int @ Z @ one_one_int ) )
% 0.18/0.45 <=> ( ( ord_less_int @ W_4 @ Z )
% 0.18/0.45 | ( W_4 = Z ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_66_int__less__0__conv,axiom,
% 0.18/0.45 ! [K: nat] :
% 0.18/0.45 ~ ( ord_less_int @ ( semiri1621563631at_int @ K ) @ zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_67_less__special_I4_J,axiom,
% 0.18/0.45 ! [X_1: int] :
% 0.18/0.45 ( ( ord_less_int @ ( number_number_of_int @ X_1 ) @ one_one_int )
% 0.18/0.45 <=> ( ord_less_int @ X_1 @ ( bit1 @ pls ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_68_less__special_I2_J,axiom,
% 0.18/0.45 ! [Y_1: int] :
% 0.18/0.45 ( ( ord_less_int @ one_one_int @ ( number_number_of_int @ Y_1 ) )
% 0.18/0.45 <=> ( ord_less_int @ ( bit1 @ pls ) @ Y_1 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_69_odd__less__0,axiom,
% 0.18/0.45 ! [Z: int] :
% 0.18/0.45 ( ( ord_less_int @ ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z ) @ zero_zero_int )
% 0.18/0.45 <=> ( ord_less_int @ Z @ zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_70_double__eq__0__iff,axiom,
% 0.18/0.45 ! [A_5: int] :
% 0.18/0.45 ( ( ( plus_plus_int @ A_5 @ A_5 )
% 0.18/0.45 = zero_zero_int )
% 0.18/0.45 <=> ( A_5 = zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_71_rel__simps_I46_J,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( bit1 @ K )
% 0.18/0.45 != pls ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_72_rel__simps_I39_J,axiom,
% 0.18/0.45 ! [L: int] :
% 0.18/0.45 ( pls
% 0.18/0.45 != ( bit1 @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_73_rel__simps_I50_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( bit1 @ K )
% 0.18/0.45 != ( bit0 @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_74_rel__simps_I49_J,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( bit0 @ K )
% 0.18/0.45 != ( bit1 @ L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_75_rel__simps_I44_J,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( ( bit0 @ K )
% 0.18/0.45 = pls )
% 0.18/0.45 <=> ( K = pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_76_rel__simps_I38_J,axiom,
% 0.18/0.45 ! [L: int] :
% 0.18/0.45 ( ( pls
% 0.18/0.45 = ( bit0 @ L ) )
% 0.18/0.45 <=> ( pls = L ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_77_Bit0__Pls,axiom,
% 0.18/0.45 ( ( bit0 @ pls )
% 0.18/0.45 = pls ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_78_Pls__def,axiom,
% 0.18/0.45 pls = zero_zero_int ).
% 0.18/0.45
% 0.18/0.45 thf(fact_79_int__0__neq__1,axiom,
% 0.18/0.45 zero_zero_int != one_one_int ).
% 0.18/0.45
% 0.18/0.45 thf(fact_80_add__Pls__right,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( plus_plus_int @ K @ pls )
% 0.18/0.45 = K ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_81_add__Pls,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( plus_plus_int @ pls @ K )
% 0.18/0.45 = K ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_82_add__Bit0__Bit0,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.18/0.45 = ( bit0 @ ( plus_plus_int @ K @ L ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_83_Bit0__def,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( bit0 @ K )
% 0.18/0.45 = ( plus_plus_int @ K @ K ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_84_zadd__0__right,axiom,
% 0.18/0.45 ! [Z: int] :
% 0.18/0.45 ( ( plus_plus_int @ Z @ zero_zero_int )
% 0.18/0.45 = Z ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_85_zadd__0,axiom,
% 0.18/0.45 ! [Z: int] :
% 0.18/0.45 ( ( plus_plus_int @ zero_zero_int @ Z )
% 0.18/0.45 = Z ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_86_semiring__numeral__0__eq__0,axiom,
% 0.18/0.45 ( ( number_number_of_int @ pls )
% 0.18/0.45 = zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_87_semiring__numeral__0__eq__0,axiom,
% 0.18/0.45 ( ( number_number_of_nat @ pls )
% 0.18/0.45 = zero_zero_nat ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_88_number__of__Pls,axiom,
% 0.18/0.45 ( ( number_number_of_int @ pls )
% 0.18/0.45 = zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_89_semiring__norm_I112_J,axiom,
% 0.18/0.45 ( zero_zero_int
% 0.18/0.45 = ( number_number_of_int @ pls ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_90_add__numeral__0,axiom,
% 0.18/0.45 ! [A_4: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( number_number_of_int @ pls ) @ A_4 )
% 0.18/0.45 = A_4 ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_91_add__numeral__0__right,axiom,
% 0.18/0.45 ! [A_3: int] :
% 0.18/0.45 ( ( plus_plus_int @ A_3 @ ( number_number_of_int @ pls ) )
% 0.18/0.45 = A_3 ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_92_power__eq__0__iff__number__of,axiom,
% 0.18/0.45 ! [A_2: int,W_3: int] :
% 0.18/0.45 ( ( ( power_power_int @ A_2 @ ( number_number_of_nat @ W_3 ) )
% 0.18/0.45 = zero_zero_int )
% 0.18/0.45 <=> ( ( A_2 = zero_zero_int )
% 0.18/0.45 & ( ( number_number_of_nat @ W_3 )
% 0.18/0.45 != zero_zero_nat ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_93_power__eq__0__iff__number__of,axiom,
% 0.18/0.45 ! [A_2: nat,W_3: int] :
% 0.18/0.45 ( ( ( power_power_nat @ A_2 @ ( number_number_of_nat @ W_3 ) )
% 0.18/0.45 = zero_zero_nat )
% 0.18/0.45 <=> ( ( A_2 = zero_zero_nat )
% 0.18/0.45 & ( ( number_number_of_nat @ W_3 )
% 0.18/0.45 != zero_zero_nat ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_94_add__number__of__left,axiom,
% 0.18/0.45 ! [V_2: int,W_2: int,Z_1: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( number_number_of_int @ V_2 ) @ ( plus_plus_int @ ( number_number_of_int @ W_2 ) @ Z_1 ) )
% 0.18/0.45 = ( plus_plus_int @ ( number_number_of_int @ ( plus_plus_int @ V_2 @ W_2 ) ) @ Z_1 ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_95_add__number__of__eq,axiom,
% 0.18/0.45 ! [V_1: int,W_1: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( number_number_of_int @ V_1 ) @ ( number_number_of_int @ W_1 ) )
% 0.18/0.45 = ( number_number_of_int @ ( plus_plus_int @ V_1 @ W_1 ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_96_number__of__add,axiom,
% 0.18/0.45 ! [V: int,W: int] :
% 0.18/0.45 ( ( number_number_of_int @ ( plus_plus_int @ V @ W ) )
% 0.18/0.45 = ( plus_plus_int @ ( number_number_of_int @ V ) @ ( number_number_of_int @ W ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_97_add__Bit1__Bit0,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.18/0.45 = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_98_add__Bit0__Bit1,axiom,
% 0.18/0.45 ! [K: int,L: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 0.18/0.45 = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_99_Bit1__def,axiom,
% 0.18/0.45 ! [K: int] :
% 0.18/0.45 ( ( bit1 @ K )
% 0.18/0.45 = ( plus_plus_int @ ( plus_plus_int @ one_one_int @ K ) @ K ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_100_odd__nonzero,axiom,
% 0.18/0.45 ! [Z: int] :
% 0.18/0.45 ( ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z )
% 0.18/0.45 != zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_101_number__of__int,axiom,
% 0.18/0.45 ! [N: nat] :
% 0.18/0.45 ( ( number_number_of_nat @ ( semiri1621563631at_int @ N ) )
% 0.18/0.45 = ( semiri984289939at_nat @ N ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_102_number__of__int,axiom,
% 0.18/0.45 ! [N: nat] :
% 0.18/0.45 ( ( number_number_of_int @ ( semiri1621563631at_int @ N ) )
% 0.18/0.45 = ( semiri1621563631at_int @ N ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_103_zero__less__power2,axiom,
% 0.18/0.45 ! [A_1: int] :
% 0.18/0.45 ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ A_1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.18/0.45 <=> ( A_1 != zero_zero_int ) ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_104_power2__less__0,axiom,
% 0.18/0.45 ! [A: int] :
% 0.18/0.45 ~ ( ord_less_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 thf(fact_105_sum__power2__gt__zero__iff,axiom,
% 0.18/0.45 ! [X: int,Y: int] :
% 0.18/0.45 ( ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( power_power_int @ X @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
% 0.18/0.45 <=> ( ( X != zero_zero_int )
% 0.18/0.45 | ( Y != zero_zero_int ) ) ) ).
% 0.18/0.45
% 0.18/0.45 %----Conjectures (1)
% 0.18/0.45 thf(conj_0,conjecture,
% 0.18/0.45 ( ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.18/0.45 != zero_zero_int ) ).
% 0.18/0.45
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 ------------------------
% 0.29/1.30 ---- Embedded in THF ---
% 0.29/1.30 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 0.29/1.30 %%% Generated on Tue Feb 24 11:17:55 EST 2026
% 0.29/1.30 %%% using '$$dhol' embedding, version 1.3.0.
% 0.29/1.30 %%% Logic specification used:
% 0.29/1.30 %%% thf(spec, logic, $$dhol).
% 0.29/1.30
% 0.29/1.30 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2DTF846.p
% See solution above
% 0.29/1.30 ------------------------
% 0.29/1.32 ---- Cleaned THF ---
% 0.29/1.32 thf(ty_ty_tc__Int__Oint,type,
% 0.29/1.32 int: $tType ).
% 0.29/1.32
% 0.29/1.32 thf(ty_ty_tc__Nat__Onat,type,
% 0.29/1.32 nat: $tType ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,
% 0.29/1.32 one_one_int: int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,
% 0.29/1.32 one_one_nat: nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,
% 0.29/1.32 plus_plus_int: int > int > int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,
% 0.29/1.32 plus_plus_nat: nat > nat > nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Int__Oint,type,
% 0.29/1.32 zero_zero_int: int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Nat__Onat,type,
% 0.29/1.32 zero_zero_nat: nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Int_OBit0,type,
% 0.29/1.32 bit0: int > int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Int_OBit1,type,
% 0.29/1.32 bit1: int > int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Int_OPls,type,
% 0.29/1.32 pls: int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,
% 0.29/1.32 number_number_of_int: int > int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,
% 0.29/1.32 number_number_of_nat: int > nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Int__Oint,type,
% 0.29/1.32 semiri1621563631at_int: nat > int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Nat__Onat,type,
% 0.29/1.32 semiri984289939at_nat: nat > nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,
% 0.29/1.32 ord_less_int: int > int > $o ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,
% 0.29/1.32 ord_less_nat: nat > nat > $o ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,
% 0.29/1.32 power_power_int: int > nat > int ).
% 0.29/1.32
% 0.29/1.32 thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,
% 0.29/1.32 power_power_nat: nat > nat > nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_v_n____,type,
% 0.29/1.32 n: nat ).
% 0.29/1.32
% 0.29/1.32 thf(sy_v_t____,type,
% 0.29/1.32 t: int ).
% 0.29/1.32
% 0.29/1.32 thf(fact_0_n1pos,axiom,
% 0.29/1.32 ord_less_int @ zero_zero_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_1_t1,axiom,
% 0.29/1.32 ord_less_int @ one_one_int @ t ).
% 0.29/1.32
% 0.29/1.32 thf(fact_2_sum__power2__eq__zero__iff,axiom,
% 0.29/1.32 ! [X_3: int,Y_3: int] :
% 0.29/1.32 ( ( ( plus_plus_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.29/1.32 = zero_zero_int )
% 0.29/1.32 <=> ( ( X_3 = zero_zero_int )
% 0.29/1.32 & ( Y_3 = zero_zero_int ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_3_one__power2,axiom,
% 0.29/1.32 ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 = one_one_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_4_one__power2,axiom,
% 0.29/1.32 ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 = one_one_nat ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_5_zero__power2,axiom,
% 0.29/1.32 ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 = zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_6_zero__power2,axiom,
% 0.29/1.32 ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 = zero_zero_nat ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_7_zero__eq__power2,axiom,
% 0.29/1.32 ! [A_7: int] :
% 0.29/1.32 ( ( ( power_power_int @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 = zero_zero_int )
% 0.29/1.32 <=> ( A_7 = zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_8_add__special_I2_J,axiom,
% 0.29/1.32 ! [W_7: int] :
% 0.29/1.32 ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_7 ) )
% 0.29/1.32 = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_7 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_9_add__special_I3_J,axiom,
% 0.29/1.32 ! [V_5: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( number_number_of_int @ V_5 ) @ one_one_int )
% 0.29/1.32 = ( number_number_of_int @ ( plus_plus_int @ V_5 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_10_one__add__one__is__two,axiom,
% 0.29/1.32 ( ( plus_plus_int @ one_one_int @ one_one_int )
% 0.29/1.32 = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_11_semiring__one__add__one__is__two,axiom,
% 0.29/1.32 ( ( plus_plus_int @ one_one_int @ one_one_int )
% 0.29/1.32 = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_12_semiring__one__add__one__is__two,axiom,
% 0.29/1.32 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 0.29/1.32 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_13_quartic__square__square,axiom,
% 0.29/1.32 ! [X_3: int] :
% 0.29/1.32 ( ( power_power_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 = ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_14_power__0__left__number__of,axiom,
% 0.29/1.32 ! [W_6: int] :
% 0.29/1.32 ( ( ( ( number_number_of_nat @ W_6 )
% 0.29/1.32 = zero_zero_nat )
% 0.29/1.32 => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) )
% 0.29/1.32 = one_one_int ) )
% 0.29/1.32 & ( ( ( number_number_of_nat @ W_6 )
% 0.29/1.32 != zero_zero_nat )
% 0.29/1.32 => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) )
% 0.29/1.32 = zero_zero_int ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_15_power__0__left__number__of,axiom,
% 0.29/1.32 ! [W_6: int] :
% 0.29/1.32 ( ( ( ( number_number_of_nat @ W_6 )
% 0.29/1.32 = zero_zero_nat )
% 0.29/1.32 => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) )
% 0.29/1.32 = one_one_nat ) )
% 0.29/1.32 & ( ( ( number_number_of_nat @ W_6 )
% 0.29/1.32 != zero_zero_nat )
% 0.29/1.32 => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) )
% 0.29/1.32 = zero_zero_nat ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_16_semiring__norm_I110_J,axiom,
% 0.29/1.32 ( one_one_int
% 0.29/1.32 = ( number_number_of_int @ ( bit1 @ pls ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_17_numeral__1__eq__1,axiom,
% 0.29/1.32 ( ( number_number_of_int @ ( bit1 @ pls ) )
% 0.29/1.32 = one_one_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_18_n0,axiom,
% 0.29/1.32 ord_less_nat @ zero_zero_nat @ n ).
% 0.29/1.32
% 0.29/1.32 thf(fact_19_zless__linear,axiom,
% 0.29/1.32 ! [X_3: int,Y_3: int] :
% 0.29/1.32 ( ( ord_less_int @ X_3 @ Y_3 )
% 0.29/1.32 | ( X_3 = Y_3 )
% 0.29/1.32 | ( ord_less_int @ Y_3 @ X_3 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_20_less__number__of__int__code,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 0.29/1.32 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_21_plus__numeral__code_I9_J,axiom,
% 0.29/1.32 ! [V_3: int,W_4: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( number_number_of_int @ V_3 ) @ ( number_number_of_int @ W_4 ) )
% 0.29/1.32 = ( number_number_of_int @ ( plus_plus_int @ V_3 @ W_4 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_22_less__number__of,axiom,
% 0.29/1.32 ! [X_6: int,Y_5: int] :
% 0.29/1.32 ( ( ord_less_int @ ( number_number_of_int @ X_6 ) @ ( number_number_of_int @ Y_5 ) )
% 0.29/1.32 <=> ( ord_less_int @ X_6 @ Y_5 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_23_zero__is__num__zero,axiom,
% 0.29/1.32 ( zero_zero_int
% 0.29/1.32 = ( number_number_of_int @ pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_24_zpower__int,axiom,
% 0.29/1.32 ! [M: nat,N_1: nat] :
% 0.29/1.32 ( ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 )
% 0.29/1.32 = ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_25_int__power,axiom,
% 0.29/1.32 ! [M: nat,N_1: nat] :
% 0.29/1.32 ( ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) )
% 0.29/1.32 = ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_26_zadd__int__left,axiom,
% 0.29/1.32 ! [M: nat,N_1: nat,Z: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( plus_plus_int @ ( semiri1621563631at_int @ N_1 ) @ Z ) )
% 0.29/1.32 = ( plus_plus_int @ ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) @ Z ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_27_zadd__int,axiom,
% 0.29/1.32 ! [M: nat,N_1: nat] :
% 0.29/1.32 ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( semiri1621563631at_int @ N_1 ) )
% 0.29/1.32 = ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_28_int__1,axiom,
% 0.29/1.32 ( ( semiri1621563631at_int @ one_one_nat )
% 0.29/1.32 = one_one_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_29_nat__number__of__Pls,axiom,
% 0.29/1.32 ( ( number_number_of_nat @ pls )
% 0.29/1.32 = zero_zero_nat ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_30_semiring__norm_I113_J,axiom,
% 0.29/1.32 ( zero_zero_nat
% 0.29/1.32 = ( number_number_of_nat @ pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_31_int__eq__0__conv,axiom,
% 0.29/1.32 ! [N_1: nat] :
% 0.29/1.32 ( ( ( semiri1621563631at_int @ N_1 )
% 0.29/1.32 = zero_zero_int )
% 0.29/1.32 <=> ( N_1 = zero_zero_nat ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_32_int__0,axiom,
% 0.29/1.32 ( ( semiri1621563631at_int @ zero_zero_nat )
% 0.29/1.32 = zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_33_nat__1__add__1,axiom,
% 0.29/1.32 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 0.29/1.32 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_34_less__int__code_I16_J,axiom,
% 0.29/1.32 ! [K1: int,K2: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 0.29/1.32 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_35_rel__simps_I17_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 0.29/1.32 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_36_rel__simps_I2_J,axiom,
% 0.29/1.32 ~ ( ord_less_int @ pls @ pls ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_37_less__int__code_I13_J,axiom,
% 0.29/1.32 ! [K1: int,K2: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 0.29/1.32 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_38_rel__simps_I14_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.29/1.32 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_39_zadd__strict__right__mono,axiom,
% 0.29/1.32 ! [K: int,I: int,J: int] :
% 0.29/1.32 ( ( ord_less_int @ I @ J )
% 0.29/1.32 => ( ord_less_int @ ( plus_plus_int @ I @ K ) @ ( plus_plus_int @ J @ K ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_40_add__nat__number__of,axiom,
% 0.29/1.32 ! [V_4: int,V_3: int] :
% 0.29/1.32 ( ( ( ord_less_int @ V_3 @ pls )
% 0.29/1.32 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) )
% 0.29/1.32 = ( number_number_of_nat @ V_4 ) ) )
% 0.29/1.32 & ( ~ ( ord_less_int @ V_3 @ pls )
% 0.29/1.32 => ( ( ( ord_less_int @ V_4 @ pls )
% 0.29/1.32 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) )
% 0.29/1.32 = ( number_number_of_nat @ V_3 ) ) )
% 0.29/1.32 & ( ~ ( ord_less_int @ V_4 @ pls )
% 0.29/1.32 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) )
% 0.29/1.32 = ( number_number_of_nat @ ( plus_plus_int @ V_3 @ V_4 ) ) ) ) ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_41_one__is__num__one,axiom,
% 0.29/1.32 ( one_one_int
% 0.29/1.32 = ( number_number_of_int @ ( bit1 @ pls ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_42_nat__numeral__1__eq__1,axiom,
% 0.29/1.32 ( ( number_number_of_nat @ ( bit1 @ pls ) )
% 0.29/1.32 = one_one_nat ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_43_Numeral1__eq1__nat,axiom,
% 0.29/1.32 ( one_one_nat
% 0.29/1.32 = ( number_number_of_nat @ ( bit1 @ pls ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_44_eq__number__of,axiom,
% 0.29/1.32 ! [X_5: int,Y_4: int] :
% 0.29/1.32 ( ( ( number_number_of_int @ X_5 )
% 0.29/1.32 = ( number_number_of_int @ Y_4 ) )
% 0.29/1.32 <=> ( X_5 = Y_4 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_45_number__of__reorient,axiom,
% 0.29/1.32 ! [W_5: int,X_4: nat] :
% 0.29/1.32 ( ( ( number_number_of_nat @ W_5 )
% 0.29/1.32 = X_4 )
% 0.29/1.32 <=> ( X_4
% 0.29/1.32 = ( number_number_of_nat @ W_5 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_46_number__of__reorient,axiom,
% 0.29/1.32 ! [W_5: int,X_4: int] :
% 0.29/1.32 ( ( ( number_number_of_int @ W_5 )
% 0.29/1.32 = X_4 )
% 0.29/1.32 <=> ( X_4
% 0.29/1.32 = ( number_number_of_int @ W_5 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_47_rel__simps_I51_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( ( bit1 @ K )
% 0.29/1.32 = ( bit1 @ L ) )
% 0.29/1.32 <=> ( K = L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_48_rel__simps_I48_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( ( bit0 @ K )
% 0.29/1.32 = ( bit0 @ L ) )
% 0.29/1.32 <=> ( K = L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_49_even__less__0__iff,axiom,
% 0.29/1.32 ! [A_6: int] :
% 0.29/1.32 ( ( ord_less_int @ ( plus_plus_int @ A_6 @ A_6 ) @ zero_zero_int )
% 0.29/1.32 <=> ( ord_less_int @ A_6 @ zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_50_zadd__assoc,axiom,
% 0.29/1.32 ! [Z1: int,Z2: int,Z3: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 )
% 0.29/1.32 = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_51_zadd__left__commute,axiom,
% 0.29/1.32 ! [X_3: int,Y_3: int,Z: int] :
% 0.29/1.32 ( ( plus_plus_int @ X_3 @ ( plus_plus_int @ Y_3 @ Z ) )
% 0.29/1.32 = ( plus_plus_int @ Y_3 @ ( plus_plus_int @ X_3 @ Z ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_52_zadd__commute,axiom,
% 0.29/1.32 ! [Z: int,W_4: int] :
% 0.29/1.32 ( ( plus_plus_int @ Z @ W_4 )
% 0.29/1.32 = ( plus_plus_int @ W_4 @ Z ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_53_int__int__eq,axiom,
% 0.29/1.32 ! [M: nat,N_1: nat] :
% 0.29/1.32 ( ( ( semiri1621563631at_int @ M )
% 0.29/1.32 = ( semiri1621563631at_int @ N_1 ) )
% 0.29/1.32 <=> ( M = N_1 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_54_less__special_I3_J,axiom,
% 0.29/1.32 ! [X_2: int] :
% 0.29/1.32 ( ( ord_less_int @ ( number_number_of_int @ X_2 ) @ zero_zero_int )
% 0.29/1.32 <=> ( ord_less_int @ X_2 @ pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_55_less__special_I1_J,axiom,
% 0.29/1.32 ! [Y_2: int] :
% 0.29/1.32 ( ( ord_less_int @ zero_zero_int @ ( number_number_of_int @ Y_2 ) )
% 0.29/1.32 <=> ( ord_less_int @ pls @ Y_2 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_56_rel__simps_I12_J,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit1 @ K ) @ pls )
% 0.29/1.32 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_57_less__int__code_I15_J,axiom,
% 0.29/1.32 ! [K1: int,K2: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 0.29/1.32 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_58_rel__simps_I16_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.29/1.32 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_59_rel__simps_I10_J,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit0 @ K ) @ pls )
% 0.29/1.32 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_60_rel__simps_I4_J,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( ord_less_int @ pls @ ( bit0 @ K ) )
% 0.29/1.32 <=> ( ord_less_int @ pls @ K ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_61_bin__less__0__simps_I4_J,axiom,
% 0.29/1.32 ! [W_4: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit1 @ W_4 ) @ zero_zero_int )
% 0.29/1.32 <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_62_bin__less__0__simps_I1_J,axiom,
% 0.29/1.32 ~ ( ord_less_int @ pls @ zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_63_bin__less__0__simps_I3_J,axiom,
% 0.29/1.32 ! [W_4: int] :
% 0.29/1.32 ( ( ord_less_int @ ( bit0 @ W_4 ) @ zero_zero_int )
% 0.29/1.32 <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_64_int__0__less__1,axiom,
% 0.29/1.32 ord_less_int @ zero_zero_int @ one_one_int ).
% 0.29/1.32
% 0.29/1.32 thf(fact_65_zless__add1__eq,axiom,
% 0.29/1.32 ! [W_4: int,Z: int] :
% 0.29/1.32 ( ( ord_less_int @ W_4 @ ( plus_plus_int @ Z @ one_one_int ) )
% 0.29/1.32 <=> ( ( ord_less_int @ W_4 @ Z )
% 0.29/1.32 | ( W_4 = Z ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_66_int__less__0__conv,axiom,
% 0.29/1.32 ! [K: nat] :
% 0.29/1.32 ~ ( ord_less_int @ ( semiri1621563631at_int @ K ) @ zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_67_less__special_I4_J,axiom,
% 0.29/1.32 ! [X_1: int] :
% 0.29/1.32 ( ( ord_less_int @ ( number_number_of_int @ X_1 ) @ one_one_int )
% 0.29/1.32 <=> ( ord_less_int @ X_1 @ ( bit1 @ pls ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_68_less__special_I2_J,axiom,
% 0.29/1.32 ! [Y_1: int] :
% 0.29/1.32 ( ( ord_less_int @ one_one_int @ ( number_number_of_int @ Y_1 ) )
% 0.29/1.32 <=> ( ord_less_int @ ( bit1 @ pls ) @ Y_1 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_69_odd__less__0,axiom,
% 0.29/1.32 ! [Z: int] :
% 0.29/1.32 ( ( ord_less_int @ ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z ) @ zero_zero_int )
% 0.29/1.32 <=> ( ord_less_int @ Z @ zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_70_double__eq__0__iff,axiom,
% 0.29/1.32 ! [A_5: int] :
% 0.29/1.32 ( ( ( plus_plus_int @ A_5 @ A_5 )
% 0.29/1.32 = zero_zero_int )
% 0.29/1.32 <=> ( A_5 = zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_71_rel__simps_I46_J,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( bit1 @ K )
% 0.29/1.32 != pls ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_72_rel__simps_I39_J,axiom,
% 0.29/1.32 ! [L: int] :
% 0.29/1.32 ( pls
% 0.29/1.32 != ( bit1 @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_73_rel__simps_I50_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( bit1 @ K )
% 0.29/1.32 != ( bit0 @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_74_rel__simps_I49_J,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( bit0 @ K )
% 0.29/1.32 != ( bit1 @ L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_75_rel__simps_I44_J,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( ( bit0 @ K )
% 0.29/1.32 = pls )
% 0.29/1.32 <=> ( K = pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_76_rel__simps_I38_J,axiom,
% 0.29/1.32 ! [L: int] :
% 0.29/1.32 ( ( pls
% 0.29/1.32 = ( bit0 @ L ) )
% 0.29/1.32 <=> ( pls = L ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_77_Bit0__Pls,axiom,
% 0.29/1.32 ( ( bit0 @ pls )
% 0.29/1.32 = pls ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_78_Pls__def,axiom,
% 0.29/1.32 pls = zero_zero_int ).
% 0.29/1.32
% 0.29/1.32 thf(fact_79_int__0__neq__1,axiom,
% 0.29/1.32 zero_zero_int != one_one_int ).
% 0.29/1.32
% 0.29/1.32 thf(fact_80_add__Pls__right,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( plus_plus_int @ K @ pls )
% 0.29/1.32 = K ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_81_add__Pls,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( plus_plus_int @ pls @ K )
% 0.29/1.32 = K ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_82_add__Bit0__Bit0,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.29/1.32 = ( bit0 @ ( plus_plus_int @ K @ L ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_83_Bit0__def,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( bit0 @ K )
% 0.29/1.32 = ( plus_plus_int @ K @ K ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_84_zadd__0__right,axiom,
% 0.29/1.32 ! [Z: int] :
% 0.29/1.32 ( ( plus_plus_int @ Z @ zero_zero_int )
% 0.29/1.32 = Z ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_85_zadd__0,axiom,
% 0.29/1.32 ! [Z: int] :
% 0.29/1.32 ( ( plus_plus_int @ zero_zero_int @ Z )
% 0.29/1.32 = Z ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_86_semiring__numeral__0__eq__0,axiom,
% 0.29/1.32 ( ( number_number_of_int @ pls )
% 0.29/1.32 = zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_87_semiring__numeral__0__eq__0,axiom,
% 0.29/1.32 ( ( number_number_of_nat @ pls )
% 0.29/1.32 = zero_zero_nat ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_88_number__of__Pls,axiom,
% 0.29/1.32 ( ( number_number_of_int @ pls )
% 0.29/1.32 = zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_89_semiring__norm_I112_J,axiom,
% 0.29/1.32 ( zero_zero_int
% 0.29/1.32 = ( number_number_of_int @ pls ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_90_add__numeral__0,axiom,
% 0.29/1.32 ! [A_4: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( number_number_of_int @ pls ) @ A_4 )
% 0.29/1.32 = A_4 ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_91_add__numeral__0__right,axiom,
% 0.29/1.32 ! [A_3: int] :
% 0.29/1.32 ( ( plus_plus_int @ A_3 @ ( number_number_of_int @ pls ) )
% 0.29/1.32 = A_3 ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_92_power__eq__0__iff__number__of,axiom,
% 0.29/1.32 ! [A_2: int,W_3: int] :
% 0.29/1.32 ( ( ( power_power_int @ A_2 @ ( number_number_of_nat @ W_3 ) )
% 0.29/1.32 = zero_zero_int )
% 0.29/1.32 <=> ( ( A_2 = zero_zero_int )
% 0.29/1.32 & ( ( number_number_of_nat @ W_3 )
% 0.29/1.32 != zero_zero_nat ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_93_power__eq__0__iff__number__of,axiom,
% 0.29/1.32 ! [A_2: nat,W_3: int] :
% 0.29/1.32 ( ( ( power_power_nat @ A_2 @ ( number_number_of_nat @ W_3 ) )
% 0.29/1.32 = zero_zero_nat )
% 0.29/1.32 <=> ( ( A_2 = zero_zero_nat )
% 0.29/1.32 & ( ( number_number_of_nat @ W_3 )
% 0.29/1.32 != zero_zero_nat ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_94_add__number__of__left,axiom,
% 0.29/1.32 ! [V_2: int,W_2: int,Z_1: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( number_number_of_int @ V_2 ) @ ( plus_plus_int @ ( number_number_of_int @ W_2 ) @ Z_1 ) )
% 0.29/1.32 = ( plus_plus_int @ ( number_number_of_int @ ( plus_plus_int @ V_2 @ W_2 ) ) @ Z_1 ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_95_add__number__of__eq,axiom,
% 0.29/1.32 ! [V_1: int,W_1: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( number_number_of_int @ V_1 ) @ ( number_number_of_int @ W_1 ) )
% 0.29/1.32 = ( number_number_of_int @ ( plus_plus_int @ V_1 @ W_1 ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_96_number__of__add,axiom,
% 0.29/1.32 ! [V: int,W: int] :
% 0.29/1.32 ( ( number_number_of_int @ ( plus_plus_int @ V @ W ) )
% 0.29/1.32 = ( plus_plus_int @ ( number_number_of_int @ V ) @ ( number_number_of_int @ W ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_97_add__Bit1__Bit0,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.29/1.32 = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_98_add__Bit0__Bit1,axiom,
% 0.29/1.32 ! [K: int,L: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 0.29/1.32 = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_99_Bit1__def,axiom,
% 0.29/1.32 ! [K: int] :
% 0.29/1.32 ( ( bit1 @ K )
% 0.29/1.32 = ( plus_plus_int @ ( plus_plus_int @ one_one_int @ K ) @ K ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_100_odd__nonzero,axiom,
% 0.29/1.32 ! [Z: int] :
% 0.29/1.32 ( ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z )
% 0.29/1.32 != zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_101_number__of__int,axiom,
% 0.29/1.32 ! [N: nat] :
% 0.29/1.32 ( ( number_number_of_nat @ ( semiri1621563631at_int @ N ) )
% 0.29/1.32 = ( semiri984289939at_nat @ N ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_102_number__of__int,axiom,
% 0.29/1.32 ! [N: nat] :
% 0.29/1.32 ( ( number_number_of_int @ ( semiri1621563631at_int @ N ) )
% 0.29/1.32 = ( semiri1621563631at_int @ N ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_103_zero__less__power2,axiom,
% 0.29/1.32 ! [A_1: int] :
% 0.29/1.32 ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ A_1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.29/1.32 <=> ( A_1 != zero_zero_int ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_104_power2__less__0,axiom,
% 0.29/1.32 ! [A: int] :
% 0.29/1.32 ~ ( ord_less_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ zero_zero_int ) ).
% 0.29/1.32
% 0.29/1.32 thf(fact_105_sum__power2__gt__zero__iff,axiom,
% 0.29/1.32 ! [X: int,Y: int] :
% 0.29/1.32 ( ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( power_power_int @ X @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
% 0.29/1.32 <=> ( ( X != zero_zero_int )
% 0.29/1.32 | ( Y != zero_zero_int ) ) ) ).
% 0.29/1.32
% 0.29/1.32 thf(conj_0,conjecture,
% 0.29/1.32 ( ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/1.32 != zero_zero_int ) ).
% 0.29/1.32 ------------------------
% 0.29/1.33 % (984)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/18Mi)
% 0.29/1.33 % (982)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/2Mi)
% 0.29/1.33 % (978)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/183Mi)
% 0.29/1.33 % (979)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/4Mi)
% 0.29/1.33 % (982)Instruction limit reached!
% 0.29/1.33 % (982)------------------------------
% 0.29/1.33 % (982)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.33 % (982)Termination reason: Unknown
% 0.29/1.33 % (982)Termination phase: shuffling
% 0.29/1.33
% 0.29/1.33 % (982)Memory used [KB]: 1151
% 0.29/1.33 % (982)Time elapsed: 0.002 s
% 0.29/1.33 % (982)Instructions burned: 4 (million)
% 0.29/1.33 % (982)------------------------------
% 0.29/1.33 % (982)------------------------------
% 0.29/1.33 % (979)Instruction limit reached!
% 0.29/1.33 % (979)------------------------------
% 0.29/1.33 % (979)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.33 % (979)Termination reason: Unknown
% 0.29/1.33 % (979)Termination phase: shuffling
% 0.29/1.33
% 0.29/1.33 % (979)Memory used [KB]: 1151
% 0.29/1.33 % (979)Time elapsed: 0.003 s
% 0.29/1.33 % (979)Instructions burned: 7 (million)
% 0.29/1.33 % (979)------------------------------
% 0.29/1.33 % (979)------------------------------
% 0.29/1.34 % (984)Instruction limit reached!
% 0.29/1.34 % (984)------------------------------
% 0.29/1.34 % (984)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.34 % (984)Termination reason: Unknown
% 0.29/1.34 % (984)Termination phase: Saturation
% 0.29/1.34
% 0.29/1.34 % (984)Memory used [KB]: 5756
% 0.29/1.34 % (984)Time elapsed: 0.007 s
% 0.29/1.34 % (984)Instructions burned: 20 (million)
% 0.29/1.34 % (984)------------------------------
% 0.29/1.34 % (984)------------------------------
% 0.29/1.34 % (980)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/27Mi)
% 0.29/1.34 % (981)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/2Mi)
% 0.29/1.34 % (983)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/275Mi)
% 0.29/1.34 % (981)Instruction limit reached!
% 0.29/1.34 % (981)------------------------------
% 0.29/1.34 % (981)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.34 % (981)Termination reason: Unknown
% 0.29/1.34 % (981)Termination phase: shuffling
% 0.29/1.34
% 0.29/1.34 % (981)Memory used [KB]: 1023
% 0.29/1.34 % (981)Time elapsed: 0.003 s
% 0.29/1.34 % (981)Instructions burned: 2 (million)
% 0.29/1.34 % (981)------------------------------
% 0.29/1.34 % (981)------------------------------
% 0.29/1.34 % (985)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/3Mi)
% 0.29/1.34 % (986)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/37Mi)
% 0.29/1.34 % (985)Instruction limit reached!
% 0.29/1.34 % (985)------------------------------
% 0.29/1.34 % (985)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.34 % (985)Termination reason: Unknown
% 0.29/1.34 % (985)Termination phase: shuffling
% 0.29/1.34
% 0.29/1.34 % (985)Memory used [KB]: 1151
% 0.29/1.34 % (985)Time elapsed: 0.003 s
% 0.29/1.34 % (985)Instructions burned: 4 (million)
% 0.29/1.34 % (985)------------------------------
% 0.29/1.34 % (985)------------------------------
% 0.29/1.35 % (987)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/15Mi)
% 0.29/1.35 % (987)Instruction limit reached!
% 0.29/1.35 % (987)------------------------------
% 0.29/1.35 % (987)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.35 % (987)Termination reason: Unknown
% 0.29/1.35 % (987)Termination phase: Property scanning
% 0.29/1.35
% 0.29/1.35 % (987)Memory used [KB]: 1279
% 0.29/1.35 % (987)Time elapsed: 0.005 s
% 0.29/1.35 % (987)Instructions burned: 15 (million)
% 0.29/1.35 % (987)------------------------------
% 0.29/1.35 % (987)------------------------------
% 0.29/1.35 % (989)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/1041Mi)
% 0.29/1.35 % (980)Instruction limit reached!
% 0.29/1.35 % (980)------------------------------
% 0.29/1.35 % (980)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.35 % (980)Termination reason: Unknown
% 0.29/1.35 % (980)Termination phase: Saturation
% 0.29/1.35
% 0.29/1.35 % (980)Memory used [KB]: 5884
% 0.29/1.35 % (980)Time elapsed: 0.018 s
% 0.29/1.35 % (980)Instructions burned: 27 (million)
% 0.29/1.35 % (980)------------------------------
% 0.29/1.35 % (980)------------------------------
% 0.29/1.35 % (986)Instruction limit reached!
% 0.29/1.35 % (986)------------------------------
% 0.29/1.35 % (986)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.35 % (986)Termination reason: Unknown
% 0.29/1.35 % (986)Termination phase: Saturation
% 0.29/1.35
% 0.29/1.35 % (986)Memory used [KB]: 6012
% 0.29/1.35 % (986)Time elapsed: 0.013 s
% 0.29/1.35 % (986)Instructions burned: 39 (million)
% 0.29/1.35 % (986)------------------------------
% 0.29/1.35 % (986)------------------------------
% 0.29/1.36 % (988)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/3Mi)
% 0.29/1.36 % (983)First to succeed.
% 0.29/1.36 % (988)Instruction limit reached!
% 0.29/1.36 % (988)------------------------------
% 0.29/1.36 % (988)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.36 % (988)Termination reason: Unknown
% 0.29/1.36 % (988)Termination phase: shuffling
% 0.29/1.36
% 0.29/1.36 % (988)Memory used [KB]: 1151
% 0.29/1.36 % (988)Time elapsed: 0.004 s
% 0.29/1.36 % (988)Instructions burned: 4 (million)
% 0.29/1.36 % (988)------------------------------
% 0.29/1.36 % (988)------------------------------
% 0.29/1.36 % (990)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_846 for (2999ds/7Mi)
% 0.29/1.36 % (983)Refutation found. Thanks to Tanya!
% 0.29/1.36 % SZS status Theorem for DTF2THF_846
% 0.29/1.36 % SZS output start Proof for DTF2THF_846
% 0.29/1.36 thf(type_def_5, type, int: $tType).
% 0.29/1.36 thf(type_def_6, type, nat: $tType).
% 0.29/1.36 thf(func_def_0, type, int: $tType).
% 0.29/1.36 thf(func_def_1, type, nat: $tType).
% 0.29/1.36 thf(func_def_2, type, one_one_int: int).
% 0.29/1.36 thf(func_def_3, type, one_one_nat: nat).
% 0.29/1.36 thf(func_def_4, type, plus_plus_int: int > int > int).
% 0.29/1.36 thf(func_def_5, type, plus_plus_nat: nat > nat > nat).
% 0.29/1.36 thf(func_def_6, type, zero_zero_int: int).
% 0.29/1.36 thf(func_def_7, type, zero_zero_nat: nat).
% 0.29/1.36 thf(func_def_8, type, bit0: int > int).
% 0.29/1.36 thf(func_def_9, type, bit1: int > int).
% 0.29/1.36 thf(func_def_10, type, pls: int).
% 0.29/1.36 thf(func_def_11, type, number_number_of_int: int > int).
% 0.29/1.36 thf(func_def_12, type, number_number_of_nat: int > nat).
% 0.29/1.36 thf(func_def_13, type, semiri1621563631at_int: nat > int).
% 0.29/1.36 thf(func_def_14, type, semiri984289939at_nat: nat > nat).
% 0.29/1.36 thf(func_def_15, type, ord_less_int: int > int > $o).
% 0.29/1.36 thf(func_def_16, type, ord_less_nat: nat > nat > $o).
% 0.29/1.36 thf(func_def_17, type, power_power_int: int > nat > int).
% 0.29/1.36 thf(func_def_18, type, power_power_nat: nat > nat > nat).
% 0.29/1.36 thf(func_def_19, type, n: nat).
% 0.29/1.36 thf(func_def_20, type, t: int).
% 0.29/1.36 thf(f478,plain,(
% 0.29/1.36 $false),
% 0.29/1.36 inference(avatar_sat_refutation,[status(thm)],[f457,f475])).
% 0.29/1.36 thf(f475,plain,(
% 0.29/1.36 ~spl0_1),
% 0.29/1.36 inference(avatar_contradiction_clause,[status(thm)],[f474])).
% 0.29/1.36 thf(f474,plain,(
% 0.29/1.36 $false | ~spl0_1),
% 0.29/1.36 inference(subsumption_resolution,[status(thm)],[f467,f302])).
% 0.29/1.36 thf(f302,plain,(
% 0.29/1.36 ( ! [X0 : nat] : (((ord_less_int @ (semiri1621563631at_int @ X0) @ zero_zero_int) != $true)) )),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f204])).
% 0.29/1.36 thf(f204,plain,(
% 0.29/1.36 ! [X0 : nat] : ((ord_less_int @ (semiri1621563631at_int @ X0) @ zero_zero_int) != $true)),
% 0.29/1.36 inference(flattening,[status(thm)],[f115])).
% 0.29/1.36 thf(f115,plain,(
% 0.29/1.36 ! [X0 : nat] : ~((ord_less_int @ (semiri1621563631at_int @ X0) @ zero_zero_int) = $true)),
% 0.29/1.36 inference(fool_elimination,[status(thm)],[f114])).
% 0.29/1.36 thf(f114,plain,(
% 0.29/1.36 ! [X0 : nat] : ~(ord_less_int @ (semiri1621563631at_int @ X0) @ zero_zero_int)),
% 0.29/1.36 inference(rectify,[status(thm)],[f67])).
% 0.29/1.36 thf(f67,axiom,(
% 0.29/1.36 ! [X6 : nat] : ~(ord_less_int @ (semiri1621563631at_int @ X6) @ zero_zero_int)),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_66_int__less__0__conv)).
% 0.29/1.36 thf(f467,plain,(
% 0.29/1.36 ($true = (ord_less_int @ (semiri1621563631at_int @ n) @ zero_zero_int)) | ~spl0_1),
% 0.29/1.36 inference(superposition,[status(thm)],[f413,f444])).
% 0.29/1.36 thf(f444,plain,(
% 0.29/1.36 (zero_zero_int = (plus_plus_int @ (semiri1621563631at_int @ n) @ (number_number_of_int @ (bit1 @ zero_zero_int)))) | ~spl0_1),
% 0.29/1.36 inference(avatar_component_clause,[status(thm)],[f442])).
% 0.29/1.36 thf(f442,definition,(
% 0.29/1.36 spl0_1 <=> (zero_zero_int = (plus_plus_int @ (semiri1621563631at_int @ n) @ (number_number_of_int @ (bit1 @ zero_zero_int))))),
% 0.29/1.36 introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition])).
% 0.29/1.36 thf(f413,plain,(
% 0.29/1.36 ( ! [X1 : int] : (((ord_less_int @ X1 @ (plus_plus_int @ X1 @ (number_number_of_int @ (bit1 @ zero_zero_int)))) = $true)) )),
% 0.29/1.36 inference(equality_resolution,[status(thm)],[f381])).
% 0.29/1.36 thf(f381,plain,(
% 0.29/1.36 ( ! [X0 : int,X1 : int] : (((ord_less_int @ X1 @ (plus_plus_int @ X0 @ (number_number_of_int @ (bit1 @ zero_zero_int)))) = $true) | (X0 != X1)) )),
% 0.29/1.36 inference(definition_unfolding,[status(thm)],[f299,f352])).
% 0.29/1.36 thf(f352,plain,(
% 0.29/1.36 (one_one_int = (number_number_of_int @ (bit1 @ zero_zero_int)))),
% 0.29/1.36 inference(definition_unfolding,[status(thm)],[f278,f313])).
% 0.29/1.36 thf(f313,plain,(
% 0.29/1.36 (zero_zero_int = pls)),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f79])).
% 0.29/1.36 thf(f79,axiom,(
% 0.29/1.36 (zero_zero_int = pls)),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_78_Pls__def)).
% 0.29/1.36 thf(f278,plain,(
% 0.29/1.36 (one_one_int = (number_number_of_int @ (bit1 @ pls)))),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f18])).
% 0.29/1.36 thf(f18,axiom,(
% 0.29/1.36 (one_one_int = (number_number_of_int @ (bit1 @ pls)))),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_17_numeral__1__eq__1)).
% 0.29/1.36 thf(f299,plain,(
% 0.29/1.36 ( ! [X0 : int,X1 : int] : (($true = (ord_less_int @ X1 @ (plus_plus_int @ X0 @ one_one_int))) | (X0 != X1)) )),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f231])).
% 0.29/1.36 thf(f231,plain,(
% 0.29/1.36 ! [X0 : int,X1 : int] : (((X0 = X1) | ((ord_less_int @ X1 @ X0) = $true) | ($true != (ord_less_int @ X1 @ (plus_plus_int @ X0 @ one_one_int)))) & (($true = (ord_less_int @ X1 @ (plus_plus_int @ X0 @ one_one_int))) | ((X0 != X1) & ((ord_less_int @ X1 @ X0) != $true))))),
% 0.29/1.36 inference(rectify,[status(thm)],[f230])).
% 0.29/1.36 thf(f230,plain,(
% 0.29/1.36 ! [X1 : int,X0 : int] : (((X0 = X1) | ((ord_less_int @ X0 @ X1) = $true) | ($true != (ord_less_int @ X0 @ (plus_plus_int @ X1 @ one_one_int)))) & (($true = (ord_less_int @ X0 @ (plus_plus_int @ X1 @ one_one_int))) | ((X0 != X1) & ((ord_less_int @ X0 @ X1) != $true))))),
% 0.29/1.36 inference(flattening,[status(thm)],[f229])).
% 0.29/1.36 thf(f229,plain,(
% 0.29/1.36 ! [X1 : int,X0 : int] : ((((X0 = X1) | ((ord_less_int @ X0 @ X1) = $true)) | ($true != (ord_less_int @ X0 @ (plus_plus_int @ X1 @ one_one_int)))) & (($true = (ord_less_int @ X0 @ (plus_plus_int @ X1 @ one_one_int))) | ((X0 != X1) & ((ord_less_int @ X0 @ X1) != $true))))),
% 0.29/1.36 inference(nnf_transformation,[status(thm)],[f153])).
% 0.29/1.36 thf(f153,plain,(
% 0.29/1.36 ! [X1 : int,X0 : int] : (((X0 = X1) | ((ord_less_int @ X0 @ X1) = $true)) <=> ($true = (ord_less_int @ X0 @ (plus_plus_int @ X1 @ one_one_int))))),
% 0.29/1.36 inference(fool_elimination,[status(thm)],[f152])).
% 0.29/1.36 thf(f152,plain,(
% 0.29/1.36 ! [X0 : int,X1 : int] : (((X0 = X1) | (ord_less_int @ X0 @ X1)) <=> (ord_less_int @ X0 @ (plus_plus_int @ X1 @ one_one_int)))),
% 0.29/1.36 inference(rectify,[status(thm)],[f66])).
% 0.29/1.36 thf(f66,axiom,(
% 0.29/1.36 ! [X9 : int,X14 : int] : (((X9 = X14) | (ord_less_int @ X9 @ X14)) <=> (ord_less_int @ X9 @ (plus_plus_int @ X14 @ one_one_int)))),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_65_zless__add1__eq)).
% 0.29/1.36 thf(f457,plain,(
% 0.29/1.36 spl0_1),
% 0.29/1.36 inference(avatar_split_clause,[status(thm)],[f456,f442])).
% 0.29/1.36 thf(f456,plain,(
% 0.29/1.36 (zero_zero_int = (plus_plus_int @ (semiri1621563631at_int @ n) @ (number_number_of_int @ (bit1 @ zero_zero_int))))),
% 0.29/1.36 inference(subsumption_resolution,[status(thm)],[f429,f379])).
% 0.29/1.36 thf(f379,plain,(
% 0.29/1.36 ($true != (ord_less_int @ zero_zero_int @ zero_zero_int))),
% 0.29/1.36 inference(definition_unfolding,[status(thm)],[f296,f313,f313])).
% 0.29/1.36 thf(f296,plain,(
% 0.29/1.36 ((ord_less_int @ pls @ pls) != $true)),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f216])).
% 0.29/1.36 thf(f216,plain,(
% 0.29/1.36 ((ord_less_int @ pls @ pls) != $true)),
% 0.29/1.36 inference(flattening,[status(thm)],[f141])).
% 0.29/1.36 thf(f141,plain,(
% 0.29/1.36 ~((ord_less_int @ pls @ pls) = $true)),
% 0.29/1.36 inference(fool_elimination,[status(thm)],[f140])).
% 0.29/1.36 thf(f140,plain,(
% 0.29/1.36 ~(ord_less_int @ pls @ pls)),
% 0.29/1.36 inference(rectify,[status(thm)],[f37])).
% 0.29/1.36 thf(f37,axiom,(
% 0.29/1.36 ~(ord_less_int @ pls @ pls)),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_36_rel__simps_I2_J)).
% 0.29/1.36 thf(f429,plain,(
% 0.29/1.36 ($true = (ord_less_int @ zero_zero_int @ zero_zero_int)) | (zero_zero_int = (plus_plus_int @ (semiri1621563631at_int @ n) @ (number_number_of_int @ (bit1 @ zero_zero_int))))),
% 0.29/1.36 inference(superposition,[status(thm)],[f374,f425])).
% 0.29/1.36 thf(f425,plain,(
% 0.29/1.36 (zero_zero_int = (power_power_int @ (plus_plus_int @ (semiri1621563631at_int @ n) @ (number_number_of_int @ (bit1 @ zero_zero_int))) @ (number_number_of_nat @ (bit0 @ (bit1 @ zero_zero_int)))))),
% 0.29/1.36 inference(forward_demodulation,[status(thm)],[f396,f320])).
% 0.29/1.36 thf(f320,plain,(
% 0.29/1.36 ( ! [X0 : int,X1 : int] : (((plus_plus_int @ X0 @ X1) = (plus_plus_int @ X1 @ X0))) )),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f183])).
% 0.29/1.36 thf(f183,plain,(
% 0.29/1.36 ! [X0 : int,X1 : int] : ((plus_plus_int @ X0 @ X1) = (plus_plus_int @ X1 @ X0))),
% 0.29/1.36 inference(rectify,[status(thm)],[f53])).
% 0.29/1.36 thf(f53,axiom,(
% 0.29/1.36 ! [X14 : int,X9 : int] : ((plus_plus_int @ X14 @ X9) = (plus_plus_int @ X9 @ X14))),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_52_zadd__commute)).
% 0.29/1.36 thf(f396,plain,(
% 0.29/1.36 (zero_zero_int = (power_power_int @ (plus_plus_int @ (number_number_of_int @ (bit1 @ zero_zero_int)) @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ zero_zero_int)))))),
% 0.29/1.36 inference(definition_unfolding,[status(thm)],[f325,f352,f313])).
% 0.29/1.36 thf(f325,plain,(
% 0.29/1.36 (zero_zero_int = (power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f176])).
% 0.29/1.36 thf(f176,plain,(
% 0.29/1.36 (zero_zero_int = (power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))),
% 0.29/1.36 inference(flattening,[status(thm)],[f108])).
% 0.29/1.36 thf(f108,negated_conjecture,(
% 0.29/1.36 ~(zero_zero_int != (power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))),
% 0.29/1.36 inference(negated_conjecture,[status(cth)],[f107])).
% 0.29/1.36 thf(f107,conjecture,(
% 0.29/1.36 (zero_zero_int != (power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',conj_0)).
% 0.29/1.36 thf(f374,plain,(
% 0.29/1.36 ( ! [X0 : int] : (((ord_less_int @ zero_zero_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ zero_zero_int))))) = $true) | (zero_zero_int = X0)) )),
% 0.29/1.36 inference(definition_unfolding,[status(thm)],[f290,f313])).
% 0.29/1.36 thf(f290,plain,(
% 0.29/1.36 ( ! [X0 : int] : (($true = (ord_less_int @ zero_zero_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | (zero_zero_int = X0)) )),
% 0.29/1.36 inference(cnf_transformation,[status(thm)],[f225])).
% 0.29/1.36 thf(f225,plain,(
% 0.29/1.36 ! [X0 : int] : ((($true = (ord_less_int @ zero_zero_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | (zero_zero_int = X0)) & ((zero_zero_int != X0) | ($true != (ord_less_int @ zero_zero_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))))),
% 0.29/1.36 inference(nnf_transformation,[status(thm)],[f169])).
% 0.29/1.36 thf(f169,plain,(
% 0.29/1.36 ! [X0 : int] : (($true = (ord_less_int @ zero_zero_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) <=> (zero_zero_int != X0))),
% 0.29/1.36 inference(fool_elimination,[status(thm)],[f168])).
% 0.29/1.36 thf(f168,plain,(
% 0.29/1.36 ! [X0 : int] : ((ord_less_int @ zero_zero_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) <=> (zero_zero_int != X0))),
% 0.29/1.36 inference(rectify,[status(thm)],[f104])).
% 0.29/1.36 thf(f104,axiom,(
% 0.29/1.36 ! [X45 : int] : ((ord_less_int @ zero_zero_int @ (power_power_int @ X45 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) <=> (zero_zero_int != X45))),
% 0.29/1.36 file('/export/starexec/sandbox2/tmp/tmp.zX9bJfbZiD/DTF2THF_846.p',fact_103_zero__less__power2)).
% 0.29/1.36 % SZS output end Proof for DTF2THF_846
% 0.29/1.36 % (983)------------------------------
% 0.29/1.36 % (983)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.29/1.36 % (983)Termination reason: Refutation
% 0.29/1.36
% 0.29/1.36 % (983)Memory used [KB]: 5884
% 0.29/1.36 % (983)Time elapsed: 0.023 s
% 0.29/1.36 % (983)Instructions burned: 34 (million)
% 0.29/1.36 % (983)------------------------------
% 0.29/1.36 % (983)------------------------------
% 0.29/1.36 % (977)Success in time 0.032 s
%------------------------------------------------------------------------------