%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : NUM926^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 : n018.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:09 AM UTC 2026
% Result : Theorem 2.08s 1.47s
% Output : Refutation 2.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 7
% Syntax : Number of formulae : 35 ( 12 unt; 0 typ; 0 def)
% Number of atoms : 129 ( 66 equ; 0 cnn)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 537 ( 29 ~; 22 |; 9 &; 468 @)
% ( 3 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 30 ( 27 usr; 13 con; 0-2 aty)
% Number of variables : 42 ( 0 ^; 18 !; 24 ?; 42 :)
% 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,
times_times_int: int > int > int ).
thf(func_def_7,type,
times_times_nat: nat > nat > nat ).
thf(func_def_8,type,
zprime: int > $o ).
thf(func_def_9,type,
bit0: int > int ).
thf(func_def_10,type,
bit1: int > int ).
thf(func_def_11,type,
pls: int ).
thf(func_def_12,type,
number_number_of_int: int > int ).
thf(func_def_13,type,
number_number_of_nat: int > nat ).
thf(func_def_14,type,
ord_less_int: int > int > $o ).
thf(func_def_15,type,
ord_less_nat: nat > nat > $o ).
thf(func_def_16,type,
ord_less_eq_int: int > int > $o ).
thf(func_def_17,type,
ord_less_eq_nat: nat > nat > $o ).
thf(func_def_18,type,
power_power_int: int > nat > int ).
thf(func_def_19,type,
power_power_nat: nat > nat > nat ).
thf(func_def_20,type,
twoSqu1013291560sum2sq: int > $o ).
thf(func_def_21,type,
m: int ).
thf(func_def_22,type,
s: int ).
thf(func_def_23,type,
t: int ).
thf(func_def_27,type,
sK0: int ).
thf(func_def_28,type,
sK1: int ).
thf(func_def_29,type,
sK2: int ).
thf(func_def_30,type,
sK3: int ).
thf(func_def_31,type,
sK4: int ).
thf(f625,plain,
$false,
inference(subsumption_resolution,[status(thm)],[f624,f591]) ).
thf(f591,plain,
one_one_int != t,
inference(subsumption_resolution,[status(thm)],[f389,f477]) ).
thf(f477,plain,
! [X0: int,X1: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
!= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(cnf_transformation,[status(thm)],[f297]) ).
thf(f297,plain,
! [X0: int,X1: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
!= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(ennf_transformation,[status(thm)],[f125]) ).
thf(f125,negated_conjecture,
~ ? [X0: int,X1: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(negated_conjecture,[status(cth)],[f124]) ).
thf(f124,conjecture,
? [X0: int,X1: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',conj_0) ).
thf(f389,plain,
( ( one_one_int != t )
| ( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ sK1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sK0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
thf(f316,plain,
( ( one_one_int != t )
| ( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ sK1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sK0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f314,f315]) ).
thf(f315,plain,
( ? [X0: int,X1: int] :
( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
=> ( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ sK1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sK0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f314,plain,
( ( one_one_int != t )
| ? [X0: int,X1: int] :
( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(rectify,[status(thm)],[f307]) ).
thf(f307,plain,
( ( one_one_int != t )
| ? [X1: int,X0: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(ennf_transformation,[status(thm)],[f2]) ).
thf(f2,axiom,
( ( one_one_int = t )
=> ? [X1: int,X0: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
thf(f624,plain,
one_one_int = t,
inference(subsumption_resolution,[status(thm)],[f623,f401]) ).
thf(f401,plain,
( ( ord_less_eq_int @ one_one_int @ t )
= $true ),
inference(cnf_transformation,[status(thm)],[f176]) ).
thf(f176,plain,
( ( ord_less_eq_int @ one_one_int @ t )
= $true ),
inference(fool_elimination,[status(thm)],[f175]) ).
thf(f175,plain,
ord_less_eq_int @ one_one_int @ t,
inference(rectify,[status(thm)],[f1]) ).
thf(f1,axiom,
ord_less_eq_int @ one_one_int @ t,
file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_0_tpos) ).
thf(f623,plain,
( ( ( ord_less_eq_int @ one_one_int @ t )
!= $true )
| ( one_one_int = t ) ),
inference(trivial_inequality_removal,[status(thm)],[f621]) ).
thf(f621,plain,
( ( ( ord_less_eq_int @ one_one_int @ t )
!= $true )
| ( one_one_int = t )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f590,f469]) ).
thf(f469,plain,
! [X0: int,X1: int] :
( ( ( ord_less_int @ X1 @ X0 )
= $true )
| ( X0 = X1 )
| ( ( ord_less_eq_int @ X1 @ X0 )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f355]) ).
thf(f355,plain,
! [X0: int,X1: int] :
( ( ( ( ord_less_int @ X1 @ X0 )
= $true )
| ( ( ord_less_eq_int @ X1 @ X0 )
!= $true )
| ( X0 = X1 ) )
& ( ( ( ( ord_less_eq_int @ X1 @ X0 )
= $true )
& ( X0 != X1 ) )
| ( ( ord_less_int @ X1 @ X0 )
!= $true ) ) ),
inference(rectify,[status(thm)],[f354]) ).
thf(f354,plain,
! [X1: int,X0: int] :
( ( ( ( ord_less_int @ X0 @ X1 )
= $true )
| ( ( ord_less_eq_int @ X0 @ X1 )
!= $true )
| ( X0 = X1 ) )
& ( ( ( ( ord_less_eq_int @ X0 @ X1 )
= $true )
& ( X0 != X1 ) )
| ( ( ord_less_int @ X0 @ X1 )
!= $true ) ) ),
inference(flattening,[status(thm)],[f353]) ).
thf(f353,plain,
! [X1: int,X0: int] :
( ( ( ( ord_less_int @ X0 @ X1 )
= $true )
| ( ( ord_less_eq_int @ X0 @ X1 )
!= $true )
| ( X0 = X1 ) )
& ( ( ( ( ord_less_eq_int @ X0 @ X1 )
= $true )
& ( X0 != X1 ) )
| ( ( ord_less_int @ X0 @ X1 )
!= $true ) ) ),
inference(nnf_transformation,[status(thm)],[f154]) ).
thf(f154,plain,
! [X1: int,X0: int] :
( ( ( ord_less_int @ X0 @ X1 )
= $true )
<=> ( ( ( ord_less_eq_int @ X0 @ X1 )
= $true )
& ( X0 != X1 ) ) ),
inference(fool_elimination,[status(thm)],[f153]) ).
thf(f153,plain,
! [X0: int,X1: int] :
( ( ord_less_int @ X0 @ X1 )
<=> ( ( ord_less_eq_int @ X0 @ X1 )
& ( X0 != X1 ) ) ),
inference(rectify,[status(thm)],[f29]) ).
thf(f29,axiom,
! [X15: int,X14: int] :
( ( ord_less_int @ X15 @ X14 )
<=> ( ( ord_less_eq_int @ X15 @ X14 )
& ( X14 != X15 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_28_zless__le) ).
thf(f590,plain,
( ( ord_less_int @ one_one_int @ t )
!= $true ),
inference(subsumption_resolution,[status(thm)],[f508,f477]) ).
thf(f508,plain,
( ( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ sK3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sK4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
| ( ( ord_less_int @ one_one_int @ t )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
thf(f376,plain,
( ( ( ord_less_int @ one_one_int @ t )
!= $true )
| ( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ sK3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sK4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK3,sK4])],[f374,f375]) ).
thf(f375,plain,
( ? [X0: int,X1: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) )
=> ( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ sK3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sK4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f374,plain,
( ( ( ord_less_int @ one_one_int @ t )
!= $true )
| ? [X0: int,X1: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(rectify,[status(thm)],[f306]) ).
thf(f306,plain,
( ( ( ord_less_int @ one_one_int @ t )
!= $true )
| ? [X1: int,X0: int] :
( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(ennf_transformation,[status(thm)],[f180]) ).
thf(f180,plain,
( ( ( ord_less_int @ one_one_int @ t )
= $true )
=> ? [X1: int,X0: int] :
( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f179]) ).
thf(f179,plain,
( ( ord_less_int @ one_one_int @ t )
=> ? [X0: int,X1: int] :
( ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int )
= ( plus_plus_int @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
( ( ord_less_int @ one_one_int @ t )
=> ? [X1: int,X0: int] :
( ( plus_plus_int @ ( power_power_int @ X0 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ X1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM926^1 : TPTP v9.2.1. Released v5.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.33 % Computer : n018.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue Feb 24 11:17:31 EST 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.29/0.46 ---- Original DTF file ---
% 0.29/0.46 thf(spec,logic,$$dhol).
% 0.29/0.46 %------------------------------------------------------------------------------
% 0.29/0.46 % File : NUM926^1 : TPTP v9.2.1. Released v5.3.0.
% 0.29/0.46 % Domain : Number Theory
% 0.29/0.46 % Problem : Sum of two squares line 258, 100 axioms selected
% 0.29/0.46 % Version : Especial.
% 0.29/0.46 % English :
% 0.29/0.46
% 0.29/0.46 % Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day
% 0.29/0.46 % : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe
% 0.29/0.46 % Source : [Bla11]
% 0.29/0.46 % Names : s2s_100_thf_l258 [Bla11]
% 0.29/0.46
% 0.29/0.46 % Status : Theorem
% 0.29/0.46 % Rating : 0.22 v9.1.0, 0.25 v9.0.0, 0.20 v8.2.0, 0.23 v8.1.0, 0.18 v7.5.0, 0.14 v7.4.0, 0.44 v7.2.0, 0.38 v7.1.0, 0.50 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.60 v5.3.0
% 0.29/0.46 % Syntax : Number of formulae : 148 ( 76 unt; 24 typ; 0 def)
% 0.29/0.46 % Number of atoms : 183 ( 87 equ; 0 cnn)
% 0.29/0.46 % Maximal formula atoms : 7 ( 1 avg)
% 0.29/0.46 % Number of connectives : 1077 ( 8 ~; 3 |; 3 &;1010 @)
% 0.29/0.46 % ( 36 <=>; 17 =>; 0 <=; 0 <~>)
% 0.29/0.46 % Maximal formula depth : 12 ( 5 avg)
% 0.29/0.46 % Number of types : 3 ( 2 usr)
% 0.29/0.46 % Number of type conns : 26 ( 26 >; 0 *; 0 +; 0 <<)
% 0.29/0.46 % Number of symbols : 23 ( 22 usr; 6 con; 0-2 aty)
% 0.29/0.46 % Number of variables : 244 ( 0 ^; 238 !; 6 ?; 244 :)
% 0.29/0.46 % SPC : TH0_THM_EQU_NAR
% 0.29/0.46
% 0.29/0.46 % Comments : This file was generated by Isabelle (most likely Sledgehammer)
% 0.29/0.46 % 2011-08-09 19:14:34
% 0.29/0.46 %------------------------------------------------------------------------------
% 0.29/0.46 %----Should-be-implicit typings (2)
% 0.29/0.46 thf(ty_ty_tc__Int__Oint,type,
% 0.29/0.46 int: $tType ).
% 0.29/0.46
% 0.29/0.46 thf(ty_ty_tc__Nat__Onat,type,
% 0.29/0.46 nat: $tType ).
% 0.29/0.46
% 0.29/0.46 %----Explicit typings (22)
% 0.29/0.46 thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,
% 0.29/0.46 one_one_int: int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,
% 0.29/0.46 one_one_nat: nat ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,
% 0.29/0.46 plus_plus_int: int > int > int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,
% 0.29/0.46 plus_plus_nat: nat > nat > nat ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Int__Oint,type,
% 0.29/0.46 times_times_int: int > int > int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Nat__Onat,type,
% 0.29/0.46 times_times_nat: nat > nat > nat ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_IntPrimes_Ozprime,type,
% 0.29/0.46 zprime: int > $o ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Int_OBit0,type,
% 0.29/0.46 bit0: int > int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Int_OBit1,type,
% 0.29/0.46 bit1: int > int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Int_OPls,type,
% 0.29/0.46 pls: int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,
% 0.29/0.46 number_number_of_int: int > int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,
% 0.29/0.46 number_number_of_nat: int > nat ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,
% 0.29/0.46 ord_less_int: int > int > $o ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,
% 0.29/0.46 ord_less_nat: nat > nat > $o ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Int__Oint,type,
% 0.29/0.46 ord_less_eq_int: int > int > $o ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Nat__Onat,type,
% 0.29/0.46 ord_less_eq_nat: nat > nat > $o ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,
% 0.29/0.46 power_power_int: int > nat > int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,
% 0.29/0.46 power_power_nat: nat > nat > nat ).
% 0.29/0.46
% 0.29/0.46 thf(sy_c_TwoSquares__Mirabelle__fqdbopfjxb_Ois__sum2sq,type,
% 0.29/0.46 twoSqu1013291560sum2sq: int > $o ).
% 0.29/0.46
% 0.29/0.46 thf(sy_v_m,type,
% 0.29/0.46 m: int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_v_s____,type,
% 0.29/0.46 s: int ).
% 0.29/0.46
% 0.29/0.46 thf(sy_v_t____,type,
% 0.29/0.46 t: int ).
% 0.29/0.46
% 0.29/0.46 %----Relevant facts (123)
% 0.29/0.46 thf(fact_0_tpos,axiom,
% 0.29/0.46 ord_less_eq_int @ one_one_int @ t ).
% 0.29/0.46
% 0.29/0.46 thf(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
% 0.29/0.46 ( ( t = one_one_int )
% 0.29/0.46 => ? [X: int,Y: int] :
% 0.29/0.46 ( ( 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/0.46 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
% 0.29/0.46 ( ( ord_less_int @ one_one_int @ t )
% 0.29/0.46 => ? [X: int,Y: int] :
% 0.29/0.46 ( ( 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/0.46 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_3_t__l__p,axiom,
% 0.29/0.46 ord_less_int @ t @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_4_p,axiom,
% 0.29/0.46 zprime @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_5_t,axiom,
% 0.29/0.46 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 0.29/0.46 = ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_6_qf1pt,axiom,
% 0.29/0.46 twoSqu1013291560sum2sq @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_7_zadd__power2,axiom,
% 0.29/0.46 ! [A_8: int,B_4: int] :
% 0.29/0.46 ( ( power_power_int @ ( plus_plus_int @ A_8 @ B_4 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( plus_plus_int @ ( plus_plus_int @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) @ A_8 ) @ B_4 ) ) @ ( power_power_int @ B_4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_8_zadd__power3,axiom,
% 0.29/0.46 ! [A_8: int,B_4: int] :
% 0.29/0.46 ( ( power_power_int @ ( plus_plus_int @ A_8 @ B_4 ) @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( plus_plus_int @ ( plus_plus_int @ ( plus_plus_int @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit1 @ ( bit1 @ pls ) ) ) @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ B_4 ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit1 @ ( bit1 @ pls ) ) ) @ A_8 ) @ ( power_power_int @ B_4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) @ ( power_power_int @ B_4 @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_9_power2__sum,axiom,
% 0.29/0.46 ! [X_11: nat,Y_5: nat] :
% 0.29/0.46 ( ( power_power_nat @ ( plus_plus_nat @ X_11 @ Y_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( plus_plus_nat @ ( plus_plus_nat @ ( power_power_nat @ X_11 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_nat @ Y_5 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_nat @ ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ X_11 ) @ Y_5 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_10_power2__sum,axiom,
% 0.29/0.46 ! [X_11: int,Y_5: int] :
% 0.29/0.46 ( ( power_power_int @ ( plus_plus_int @ X_11 @ Y_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( plus_plus_int @ ( plus_plus_int @ ( power_power_int @ X_11 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_5 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) @ X_11 ) @ Y_5 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_11_power2__eq__square__number__of,axiom,
% 0.29/0.46 ! [W_5: int] :
% 0.29/0.46 ( ( power_power_int @ ( number_number_of_int @ W_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( times_times_int @ ( number_number_of_int @ W_5 ) @ ( number_number_of_int @ W_5 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_12_power2__eq__square__number__of,axiom,
% 0.29/0.46 ! [W_5: int] :
% 0.29/0.46 ( ( power_power_nat @ ( number_number_of_nat @ W_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( times_times_nat @ ( number_number_of_nat @ W_5 ) @ ( number_number_of_nat @ W_5 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_13_cube__square,axiom,
% 0.29/0.46 ! [A_8: int] :
% 0.29/0.46 ( ( times_times_int @ A_8 @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.29/0.46 = ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_14_one__power2,axiom,
% 0.29/0.46 ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = one_one_nat ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_15_one__power2,axiom,
% 0.29/0.46 ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = one_one_int ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_16_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
% 0.29/0.46 ! [X_10: int] :
% 0.29/0.46 ( ( times_times_int @ X_10 @ X_10 )
% 0.29/0.46 = ( power_power_int @ X_10 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_17_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
% 0.29/0.46 ! [X_10: nat] :
% 0.29/0.46 ( ( times_times_nat @ X_10 @ X_10 )
% 0.29/0.46 = ( power_power_nat @ X_10 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_18_power2__eq__square,axiom,
% 0.29/0.46 ! [A_7: int] :
% 0.29/0.46 ( ( power_power_int @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( times_times_int @ A_7 @ A_7 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_19_power2__eq__square,axiom,
% 0.29/0.46 ! [A_7: nat] :
% 0.29/0.46 ( ( power_power_nat @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( times_times_nat @ A_7 @ A_7 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_20_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
% 0.29/0.46 ! [X_9: int,N: nat] :
% 0.29/0.46 ( ( power_power_int @ X_9 @ ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ N ) )
% 0.29/0.46 = ( times_times_int @ ( power_power_int @ X_9 @ N ) @ ( power_power_int @ X_9 @ N ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_21_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
% 0.29/0.46 ! [X_9: nat,N: nat] :
% 0.29/0.46 ( ( power_power_nat @ X_9 @ ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ N ) )
% 0.29/0.46 = ( times_times_nat @ ( power_power_nat @ X_9 @ N ) @ ( power_power_nat @ X_9 @ N ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_22_add__special_I2_J,axiom,
% 0.29/0.46 ! [W_4: int] :
% 0.29/0.46 ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_4 ) )
% 0.29/0.46 = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_4 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_23_add__special_I3_J,axiom,
% 0.29/0.46 ! [V_3: int] :
% 0.29/0.46 ( ( plus_plus_int @ ( number_number_of_int @ V_3 ) @ one_one_int )
% 0.29/0.46 = ( number_number_of_int @ ( plus_plus_int @ V_3 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_24_one__add__one__is__two,axiom,
% 0.29/0.46 ( ( plus_plus_int @ one_one_int @ one_one_int )
% 0.29/0.46 = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_25__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_,axiom,
% 0.29/0.46 ~ ! [T: int] :
% 0.29/0.46 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 0.29/0.46 != ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ T ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_26_zle__refl,axiom,
% 0.29/0.46 ! [W: int] : ( ord_less_eq_int @ W @ W ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_27_zle__linear,axiom,
% 0.29/0.46 ! [Z: int,W: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ Z @ W )
% 0.29/0.46 | ( ord_less_eq_int @ W @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_28_zless__le,axiom,
% 0.29/0.46 ! [Z: int,W: int] :
% 0.29/0.46 ( ( ord_less_int @ Z @ W )
% 0.29/0.46 <=> ( ( ord_less_eq_int @ Z @ W )
% 0.29/0.46 & ( Z != W ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_29_zless__linear,axiom,
% 0.29/0.46 ! [X_1: int,Y_1: int] :
% 0.29/0.46 ( ( ord_less_int @ X_1 @ Y_1 )
% 0.29/0.46 | ( X_1 = Y_1 )
% 0.29/0.46 | ( ord_less_int @ Y_1 @ X_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_30_zle__trans,axiom,
% 0.29/0.46 ! [K: int,I: int,J: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ I @ J )
% 0.29/0.46 => ( ( ord_less_eq_int @ J @ K )
% 0.29/0.46 => ( ord_less_eq_int @ I @ K ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_31_zle__antisym,axiom,
% 0.29/0.46 ! [Z: int,W: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ Z @ W )
% 0.29/0.46 => ( ( ord_less_eq_int @ W @ Z )
% 0.29/0.46 => ( Z = W ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_32_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
% 0.29/0.46 ! [X_8: int,P_1: nat,Q_1: nat] :
% 0.29/0.46 ( ( power_power_int @ ( power_power_int @ X_8 @ P_1 ) @ Q_1 )
% 0.29/0.46 = ( power_power_int @ X_8 @ ( times_times_nat @ P_1 @ Q_1 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
% 0.29/0.46 ! [X_8: nat,P_1: nat,Q_1: nat] :
% 0.29/0.46 ( ( power_power_nat @ ( power_power_nat @ X_8 @ P_1 ) @ Q_1 )
% 0.29/0.46 = ( power_power_nat @ X_8 @ ( times_times_nat @ P_1 @ Q_1 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_34_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
% 0.29/0.46 ! [X_7: int] :
% 0.29/0.46 ( ( power_power_int @ X_7 @ one_one_nat )
% 0.29/0.46 = X_7 ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_35_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
% 0.29/0.46 ! [X_7: nat] :
% 0.29/0.46 ( ( power_power_nat @ X_7 @ one_one_nat )
% 0.29/0.46 = X_7 ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_36_zpower__zpower,axiom,
% 0.29/0.46 ! [X_1: int,Y_1: nat,Z: nat] :
% 0.29/0.46 ( ( power_power_int @ ( power_power_int @ X_1 @ Y_1 ) @ Z )
% 0.29/0.46 = ( power_power_int @ X_1 @ ( times_times_nat @ Y_1 @ Z ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_37_le__number__of__eq__not__less,axiom,
% 0.29/0.46 ! [V_2: int,W_3: int] :
% 0.29/0.46 ( ( ord_less_eq_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ W_3 ) )
% 0.29/0.46 <=> ~ ( ord_less_nat @ ( number_number_of_nat @ W_3 ) @ ( number_number_of_nat @ V_2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_38_le__number__of__eq__not__less,axiom,
% 0.29/0.46 ! [V_2: int,W_3: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( number_number_of_int @ V_2 ) @ ( number_number_of_int @ W_3 ) )
% 0.29/0.46 <=> ~ ( ord_less_int @ ( number_number_of_int @ W_3 ) @ ( number_number_of_int @ V_2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_39_less__number__of,axiom,
% 0.29/0.46 ! [X_6: int,Y_4: int] :
% 0.29/0.46 ( ( ord_less_int @ ( number_number_of_int @ X_6 ) @ ( number_number_of_int @ Y_4 ) )
% 0.29/0.46 <=> ( ord_less_int @ X_6 @ Y_4 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_40_le__number__of,axiom,
% 0.29/0.46 ! [X_5: int,Y_3: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( number_number_of_int @ X_5 ) @ ( number_number_of_int @ Y_3 ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ X_5 @ Y_3 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_41_zadd__zless__mono,axiom,
% 0.29/0.46 ! [Z_1: int,Z: int,W_2: int,W: int] :
% 0.29/0.46 ( ( ord_less_int @ W_2 @ W )
% 0.29/0.46 => ( ( ord_less_eq_int @ Z_1 @ Z )
% 0.29/0.46 => ( ord_less_int @ ( plus_plus_int @ W_2 @ Z_1 ) @ ( plus_plus_int @ W @ Z ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_42_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
% 0.29/0.46 ! [X_4: int,P: nat,Q: nat] :
% 0.29/0.46 ( ( times_times_int @ ( power_power_int @ X_4 @ P ) @ ( power_power_int @ X_4 @ Q ) )
% 0.29/0.46 = ( power_power_int @ X_4 @ ( plus_plus_nat @ P @ Q ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_43_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
% 0.29/0.46 ! [X_4: nat,P: nat,Q: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( power_power_nat @ X_4 @ P ) @ ( power_power_nat @ X_4 @ Q ) )
% 0.29/0.46 = ( power_power_nat @ X_4 @ ( plus_plus_nat @ P @ Q ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_44_zpower__zadd__distrib,axiom,
% 0.29/0.46 ! [X_1: int,Y_1: nat,Z: nat] :
% 0.29/0.46 ( ( power_power_int @ X_1 @ ( plus_plus_nat @ Y_1 @ Z ) )
% 0.29/0.46 = ( times_times_int @ ( power_power_int @ X_1 @ Y_1 ) @ ( power_power_int @ X_1 @ Z ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_45_nat__mult__2,axiom,
% 0.29/0.46 ! [Z: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ Z )
% 0.29/0.46 = ( plus_plus_nat @ Z @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_46_nat__mult__2__right,axiom,
% 0.29/0.46 ! [Z: nat] :
% 0.29/0.46 ( ( times_times_nat @ Z @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.29/0.46 = ( plus_plus_nat @ Z @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_47_nat__1__add__1,axiom,
% 0.29/0.46 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 0.29/0.46 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_48_less__int__code_I16_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_49_rel__simps_I17_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 0.29/0.46 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_50_less__eq__int__code_I16_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_51_rel__simps_I34_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_52_rel__simps_I2_J,axiom,
% 0.29/0.46 ~ ( ord_less_int @ pls @ pls ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_53_less__int__code_I13_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_54_rel__simps_I14_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.29/0.46 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_55_rel__simps_I19_J,axiom,
% 0.29/0.46 ord_less_eq_int @ pls @ pls ).
% 0.29/0.46
% 0.29/0.46 thf(fact_56_less__eq__int__code_I13_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_57_rel__simps_I31_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_58_less__number__of__int__code,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 0.29/0.46 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_59_less__eq__number__of__int__code,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_60_zadd__strict__right__mono,axiom,
% 0.29/0.46 ! [K: int,I: int,J: int] :
% 0.29/0.46 ( ( ord_less_int @ I @ J )
% 0.29/0.46 => ( ord_less_int @ ( plus_plus_int @ I @ K ) @ ( plus_plus_int @ J @ K ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_61_zadd__left__mono,axiom,
% 0.29/0.46 ! [K: int,I: int,J: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ I @ J )
% 0.29/0.46 => ( ord_less_eq_int @ ( plus_plus_int @ K @ I ) @ ( plus_plus_int @ K @ J ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_62_add__nat__number__of,axiom,
% 0.29/0.46 ! [V_1: int,V: int] :
% 0.29/0.46 ( ( ( ord_less_int @ V @ pls )
% 0.29/0.46 => ( ( plus_plus_nat @ ( number_number_of_nat @ V ) @ ( number_number_of_nat @ V_1 ) )
% 0.29/0.46 = ( number_number_of_nat @ V_1 ) ) )
% 0.29/0.46 & ( ~ ( ord_less_int @ V @ pls )
% 0.29/0.46 => ( ( ( ord_less_int @ V_1 @ pls )
% 0.29/0.46 => ( ( plus_plus_nat @ ( number_number_of_nat @ V ) @ ( number_number_of_nat @ V_1 ) )
% 0.29/0.46 = ( number_number_of_nat @ V ) ) )
% 0.29/0.46 & ( ~ ( ord_less_int @ V_1 @ pls )
% 0.29/0.46 => ( ( plus_plus_nat @ ( number_number_of_nat @ V ) @ ( number_number_of_nat @ V_1 ) )
% 0.29/0.46 = ( number_number_of_nat @ ( plus_plus_int @ V @ V_1 ) ) ) ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_63_nat__numeral__1__eq__1,axiom,
% 0.29/0.46 ( ( number_number_of_nat @ ( bit1 @ pls ) )
% 0.29/0.46 = one_one_nat ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_64_Numeral1__eq1__nat,axiom,
% 0.29/0.46 ( one_one_nat
% 0.29/0.46 = ( number_number_of_nat @ ( bit1 @ pls ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_65_rel__simps_I29_J,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit1 @ K ) @ pls )
% 0.29/0.46 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_66_rel__simps_I5_J,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( ord_less_int @ pls @ ( bit1 @ K ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_67_less__eq__int__code_I15_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_68_rel__simps_I33_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.29/0.46 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_69_less__int__code_I14_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_70_rel__simps_I15_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_71_zless__imp__add1__zle,axiom,
% 0.29/0.46 ! [W: int,Z: int] :
% 0.29/0.46 ( ( ord_less_int @ W @ Z )
% 0.29/0.46 => ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_72_add1__zle__eq,axiom,
% 0.29/0.46 ! [W: int,Z: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z )
% 0.29/0.46 <=> ( ord_less_int @ W @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_73_zle__add1__eq__le,axiom,
% 0.29/0.46 ! [W: int,Z: int] :
% 0.29/0.46 ( ( ord_less_int @ W @ ( plus_plus_int @ Z @ one_one_int ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ W @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_74_zprime__2,axiom,
% 0.29/0.46 zprime @ ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_75_is__mult__sum2sq,axiom,
% 0.29/0.46 ! [Y_1: int,X_1: int] :
% 0.29/0.46 ( ( twoSqu1013291560sum2sq @ X_1 )
% 0.29/0.46 => ( ( twoSqu1013291560sum2sq @ Y_1 )
% 0.29/0.46 => ( twoSqu1013291560sum2sq @ ( times_times_int @ X_1 @ Y_1 ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
% 0.29/0.46 ! [Lx_6: int,Ly_4: int,Rx_6: int,Ry_4: int] :
% 0.29/0.46 ( ( times_times_int @ ( times_times_int @ Lx_6 @ Ly_4 ) @ ( times_times_int @ Rx_6 @ Ry_4 ) )
% 0.29/0.46 = ( times_times_int @ ( times_times_int @ Lx_6 @ Rx_6 ) @ ( times_times_int @ Ly_4 @ Ry_4 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
% 0.29/0.46 ! [Lx_6: nat,Ly_4: nat,Rx_6: nat,Ry_4: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( times_times_nat @ Lx_6 @ Ly_4 ) @ ( times_times_nat @ Rx_6 @ Ry_4 ) )
% 0.29/0.46 = ( times_times_nat @ ( times_times_nat @ Lx_6 @ Rx_6 ) @ ( times_times_nat @ Ly_4 @ Ry_4 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
% 0.29/0.46 ! [Lx_5: int,Ly_3: int,Rx_5: int,Ry_3: int] :
% 0.29/0.46 ( ( times_times_int @ ( times_times_int @ Lx_5 @ Ly_3 ) @ ( times_times_int @ Rx_5 @ Ry_3 ) )
% 0.29/0.46 = ( times_times_int @ Rx_5 @ ( times_times_int @ ( times_times_int @ Lx_5 @ Ly_3 ) @ Ry_3 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
% 0.29/0.46 ! [Lx_5: nat,Ly_3: nat,Rx_5: nat,Ry_3: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( times_times_nat @ Lx_5 @ Ly_3 ) @ ( times_times_nat @ Rx_5 @ Ry_3 ) )
% 0.29/0.46 = ( times_times_nat @ Rx_5 @ ( times_times_nat @ ( times_times_nat @ Lx_5 @ Ly_3 ) @ Ry_3 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_80_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
% 0.29/0.46 ! [Lx_4: int,Ly_2: int,Rx_4: int,Ry_2: int] :
% 0.29/0.46 ( ( times_times_int @ ( times_times_int @ Lx_4 @ Ly_2 ) @ ( times_times_int @ Rx_4 @ Ry_2 ) )
% 0.29/0.46 = ( times_times_int @ Lx_4 @ ( times_times_int @ Ly_2 @ ( times_times_int @ Rx_4 @ Ry_2 ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_81_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
% 0.29/0.46 ! [Lx_4: nat,Ly_2: nat,Rx_4: nat,Ry_2: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( times_times_nat @ Lx_4 @ Ly_2 ) @ ( times_times_nat @ Rx_4 @ Ry_2 ) )
% 0.29/0.46 = ( times_times_nat @ Lx_4 @ ( times_times_nat @ Ly_2 @ ( times_times_nat @ Rx_4 @ Ry_2 ) ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_82_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
% 0.29/0.46 ! [Lx_3: int,Ly_1: int,Rx_3: int] :
% 0.29/0.46 ( ( times_times_int @ ( times_times_int @ Lx_3 @ Ly_1 ) @ Rx_3 )
% 0.29/0.46 = ( times_times_int @ ( times_times_int @ Lx_3 @ Rx_3 ) @ Ly_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_83_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
% 0.29/0.46 ! [Lx_3: nat,Ly_1: nat,Rx_3: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( times_times_nat @ Lx_3 @ Ly_1 ) @ Rx_3 )
% 0.29/0.46 = ( times_times_nat @ ( times_times_nat @ Lx_3 @ Rx_3 ) @ Ly_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
% 0.29/0.46 ! [Lx_2: int,Ly: int,Rx_2: int] :
% 0.29/0.46 ( ( times_times_int @ ( times_times_int @ Lx_2 @ Ly ) @ Rx_2 )
% 0.29/0.46 = ( times_times_int @ Lx_2 @ ( times_times_int @ Ly @ Rx_2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
% 0.29/0.46 ! [Lx_2: nat,Ly: nat,Rx_2: nat] :
% 0.29/0.46 ( ( times_times_nat @ ( times_times_nat @ Lx_2 @ Ly ) @ Rx_2 )
% 0.29/0.46 = ( times_times_nat @ Lx_2 @ ( times_times_nat @ Ly @ Rx_2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_86_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
% 0.29/0.46 ! [Lx_1: int,Rx_1: int,Ry_1: int] :
% 0.29/0.46 ( ( times_times_int @ Lx_1 @ ( times_times_int @ Rx_1 @ Ry_1 ) )
% 0.29/0.46 = ( times_times_int @ ( times_times_int @ Lx_1 @ Rx_1 ) @ Ry_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
% 0.29/0.46 ! [Lx_1: nat,Rx_1: nat,Ry_1: nat] :
% 0.29/0.46 ( ( times_times_nat @ Lx_1 @ ( times_times_nat @ Rx_1 @ Ry_1 ) )
% 0.29/0.46 = ( times_times_nat @ ( times_times_nat @ Lx_1 @ Rx_1 ) @ Ry_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_88_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
% 0.29/0.46 ! [Lx: int,Rx: int,Ry: int] :
% 0.29/0.46 ( ( times_times_int @ Lx @ ( times_times_int @ Rx @ Ry ) )
% 0.29/0.46 = ( times_times_int @ Rx @ ( times_times_int @ Lx @ Ry ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_89_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
% 0.29/0.46 ! [Lx: nat,Rx: nat,Ry: nat] :
% 0.29/0.46 ( ( times_times_nat @ Lx @ ( times_times_nat @ Rx @ Ry ) )
% 0.29/0.46 = ( times_times_nat @ Rx @ ( times_times_nat @ Lx @ Ry ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
% 0.29/0.46 ! [A_6: int,B_3: int] :
% 0.29/0.46 ( ( times_times_int @ A_6 @ B_3 )
% 0.29/0.46 = ( times_times_int @ B_3 @ A_6 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
% 0.29/0.46 ! [A_6: nat,B_3: nat] :
% 0.29/0.46 ( ( times_times_nat @ A_6 @ B_3 )
% 0.29/0.46 = ( times_times_nat @ B_3 @ A_6 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_92_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
% 0.29/0.46 ! [A_5: int,B_2: int,C_5: int,D_2: int] :
% 0.29/0.46 ( ( plus_plus_int @ ( plus_plus_int @ A_5 @ B_2 ) @ ( plus_plus_int @ C_5 @ D_2 ) )
% 0.29/0.46 = ( plus_plus_int @ ( plus_plus_int @ A_5 @ C_5 ) @ ( plus_plus_int @ B_2 @ D_2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_93_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
% 0.29/0.46 ! [A_5: nat,B_2: nat,C_5: nat,D_2: nat] :
% 0.29/0.46 ( ( plus_plus_nat @ ( plus_plus_nat @ A_5 @ B_2 ) @ ( plus_plus_nat @ C_5 @ D_2 ) )
% 0.29/0.46 = ( plus_plus_nat @ ( plus_plus_nat @ A_5 @ C_5 ) @ ( plus_plus_nat @ B_2 @ D_2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_94_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
% 0.29/0.46 ! [A_4: int,B_1: int,C_4: int] :
% 0.29/0.46 ( ( plus_plus_int @ ( plus_plus_int @ A_4 @ B_1 ) @ C_4 )
% 0.29/0.46 = ( plus_plus_int @ ( plus_plus_int @ A_4 @ C_4 ) @ B_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_95_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
% 0.29/0.46 ! [A_4: nat,B_1: nat,C_4: nat] :
% 0.29/0.46 ( ( plus_plus_nat @ ( plus_plus_nat @ A_4 @ B_1 ) @ C_4 )
% 0.29/0.46 = ( plus_plus_nat @ ( plus_plus_nat @ A_4 @ C_4 ) @ B_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
% 0.29/0.46 ! [A_3: int,B: int,C_3: int] :
% 0.29/0.46 ( ( plus_plus_int @ ( plus_plus_int @ A_3 @ B ) @ C_3 )
% 0.29/0.46 = ( plus_plus_int @ A_3 @ ( plus_plus_int @ B @ C_3 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
% 0.29/0.46 ! [A_3: nat,B: nat,C_3: nat] :
% 0.29/0.46 ( ( plus_plus_nat @ ( plus_plus_nat @ A_3 @ B ) @ C_3 )
% 0.29/0.46 = ( plus_plus_nat @ A_3 @ ( plus_plus_nat @ B @ C_3 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_98_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
% 0.29/0.46 ! [A_2: int,C_2: int,D_1: int] :
% 0.29/0.46 ( ( plus_plus_int @ A_2 @ ( plus_plus_int @ C_2 @ D_1 ) )
% 0.29/0.46 = ( plus_plus_int @ ( plus_plus_int @ A_2 @ C_2 ) @ D_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
% 0.29/0.46 ! [A_2: nat,C_2: nat,D_1: nat] :
% 0.29/0.46 ( ( plus_plus_nat @ A_2 @ ( plus_plus_nat @ C_2 @ D_1 ) )
% 0.29/0.46 = ( plus_plus_nat @ ( plus_plus_nat @ A_2 @ C_2 ) @ D_1 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_100_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
% 0.29/0.46 ! [A_1: int,C_1: int,D: int] :
% 0.29/0.46 ( ( plus_plus_int @ A_1 @ ( plus_plus_int @ C_1 @ D ) )
% 0.29/0.46 = ( plus_plus_int @ C_1 @ ( plus_plus_int @ A_1 @ D ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_101_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
% 0.29/0.46 ! [A_1: nat,C_1: nat,D: nat] :
% 0.29/0.46 ( ( plus_plus_nat @ A_1 @ ( plus_plus_nat @ C_1 @ D ) )
% 0.29/0.46 = ( plus_plus_nat @ C_1 @ ( plus_plus_nat @ A_1 @ D ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
% 0.29/0.46 ! [A: int,C: int] :
% 0.29/0.46 ( ( plus_plus_int @ A @ C )
% 0.29/0.46 = ( plus_plus_int @ C @ A ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
% 0.29/0.46 ! [A: nat,C: nat] :
% 0.29/0.46 ( ( plus_plus_nat @ A @ C )
% 0.29/0.46 = ( plus_plus_nat @ C @ A ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_104_eq__number__of,axiom,
% 0.29/0.46 ! [X_3: int,Y_2: int] :
% 0.29/0.46 ( ( ( number_number_of_int @ X_3 )
% 0.29/0.46 = ( number_number_of_int @ Y_2 ) )
% 0.29/0.46 <=> ( X_3 = Y_2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_105_number__of__reorient,axiom,
% 0.29/0.46 ! [W_1: int,X_2: nat] :
% 0.29/0.46 ( ( ( number_number_of_nat @ W_1 )
% 0.29/0.46 = X_2 )
% 0.29/0.46 <=> ( X_2
% 0.29/0.46 = ( number_number_of_nat @ W_1 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_106_number__of__reorient,axiom,
% 0.29/0.46 ! [W_1: int,X_2: int] :
% 0.29/0.46 ( ( ( number_number_of_int @ W_1 )
% 0.29/0.46 = X_2 )
% 0.29/0.46 <=> ( X_2
% 0.29/0.46 = ( number_number_of_int @ W_1 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_107_rel__simps_I51_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ( bit1 @ K )
% 0.29/0.46 = ( bit1 @ L ) )
% 0.29/0.46 <=> ( K = L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_108_rel__simps_I48_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ( bit0 @ K )
% 0.29/0.46 = ( bit0 @ L ) )
% 0.29/0.46 <=> ( K = L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_109_zmult__assoc,axiom,
% 0.29/0.46 ! [Z1: int,Z2: int,Z3: int] :
% 0.29/0.46 ( ( times_times_int @ ( times_times_int @ Z1 @ Z2 ) @ Z3 )
% 0.29/0.46 = ( times_times_int @ Z1 @ ( times_times_int @ Z2 @ Z3 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_110_zmult__commute,axiom,
% 0.29/0.46 ! [Z: int,W: int] :
% 0.29/0.46 ( ( times_times_int @ Z @ W )
% 0.29/0.46 = ( times_times_int @ W @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_111_number__of__is__id,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( number_number_of_int @ K )
% 0.29/0.46 = K ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_112_zadd__assoc,axiom,
% 0.29/0.46 ! [Z1: int,Z2: int,Z3: int] :
% 0.29/0.46 ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 )
% 0.29/0.46 = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_113_zadd__left__commute,axiom,
% 0.29/0.46 ! [X_1: int,Y_1: int,Z: int] :
% 0.29/0.46 ( ( plus_plus_int @ X_1 @ ( plus_plus_int @ Y_1 @ Z ) )
% 0.29/0.46 = ( plus_plus_int @ Y_1 @ ( plus_plus_int @ X_1 @ Z ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_114_zadd__commute,axiom,
% 0.29/0.46 ! [Z: int,W: int] :
% 0.29/0.46 ( ( plus_plus_int @ Z @ W )
% 0.29/0.46 = ( plus_plus_int @ W @ Z ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_115_rel__simps_I12_J,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit1 @ K ) @ pls )
% 0.29/0.46 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_116_less__int__code_I15_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_117_rel__simps_I16_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.29/0.46 <=> ( ord_less_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_118_rel__simps_I10_J,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( ord_less_int @ ( bit0 @ K ) @ pls )
% 0.29/0.46 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_119_rel__simps_I4_J,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( ord_less_int @ pls @ ( bit0 @ K ) )
% 0.29/0.46 <=> ( ord_less_int @ pls @ K ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_120_rel__simps_I22_J,axiom,
% 0.29/0.46 ! [K: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ pls @ ( bit1 @ K ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_121_less__eq__int__code_I14_J,axiom,
% 0.29/0.46 ! [K1: int,K2: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(fact_122_rel__simps_I32_J,axiom,
% 0.29/0.46 ! [K: int,L: int] :
% 0.29/0.46 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 0.29/0.46 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.29/0.46
% 0.29/0.46 %----Conjectures (1)
% 0.29/0.46 thf(conj_0,conjecture,
% 0.29/0.46 ? [X: int,Y: int] :
% 0.29/0.46 ( ( 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/0.46 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ).
% 0.29/0.46
% 0.29/0.46 %------------------------------------------------------------------------------
% 0.29/0.46 ------------------------
% 1.88/1.37 ---- Embedded in THF ---
% 1.88/1.38 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.88/1.38 %%% Generated on Tue Feb 24 11:17:32 EST 2026
% 1.88/1.38 %%% using '$$dhol' embedding, version 1.3.0.
% 1.88/1.38 %%% Logic specification used:
% 1.88/1.38 %%% thf(spec, logic, $$dhol).
% 1.88/1.38
% 1.88/1.38 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2DTF24772.p
% See solution above
% 1.88/1.38 ------------------------
% 2.08/1.40 ---- Cleaned THF ---
% 2.08/1.40 thf(ty_ty_tc__Int__Oint,type,
% 2.08/1.40 int: $tType ).
% 2.08/1.40
% 2.08/1.40 thf(ty_ty_tc__Nat__Onat,type,
% 2.08/1.40 nat: $tType ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,
% 2.08/1.40 one_one_int: int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,
% 2.08/1.40 one_one_nat: nat ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,
% 2.08/1.40 plus_plus_int: int > int > int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,
% 2.08/1.40 plus_plus_nat: nat > nat > nat ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Int__Oint,type,
% 2.08/1.40 times_times_int: int > int > int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Nat__Onat,type,
% 2.08/1.40 times_times_nat: nat > nat > nat ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_IntPrimes_Ozprime,type,
% 2.08/1.40 zprime: int > $o ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Int_OBit0,type,
% 2.08/1.40 bit0: int > int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Int_OBit1,type,
% 2.08/1.40 bit1: int > int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Int_OPls,type,
% 2.08/1.40 pls: int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,
% 2.08/1.40 number_number_of_int: int > int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,
% 2.08/1.40 number_number_of_nat: int > nat ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,
% 2.08/1.40 ord_less_int: int > int > $o ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,
% 2.08/1.40 ord_less_nat: nat > nat > $o ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Int__Oint,type,
% 2.08/1.40 ord_less_eq_int: int > int > $o ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Nat__Onat,type,
% 2.08/1.40 ord_less_eq_nat: nat > nat > $o ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,
% 2.08/1.40 power_power_int: int > nat > int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,
% 2.08/1.40 power_power_nat: nat > nat > nat ).
% 2.08/1.40
% 2.08/1.40 thf(sy_c_TwoSquares__Mirabelle__fqdbopfjxb_Ois__sum2sq,type,
% 2.08/1.40 twoSqu1013291560sum2sq: int > $o ).
% 2.08/1.40
% 2.08/1.40 thf(sy_v_m,type,
% 2.08/1.40 m: int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_v_s____,type,
% 2.08/1.40 s: int ).
% 2.08/1.40
% 2.08/1.40 thf(sy_v_t____,type,
% 2.08/1.40 t: int ).
% 2.08/1.40
% 2.08/1.40 thf(fact_0_tpos,axiom,
% 2.08/1.40 ord_less_eq_int @ one_one_int @ t ).
% 2.08/1.40
% 2.08/1.40 thf(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
% 2.08/1.40 ( ( t = one_one_int )
% 2.08/1.40 => ? [X: int,Y: int] :
% 2.08/1.40 ( ( 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 ) ) ) ) )
% 2.08/1.40 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
% 2.08/1.40 ( ( ord_less_int @ one_one_int @ t )
% 2.08/1.40 => ? [X: int,Y: int] :
% 2.08/1.40 ( ( 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 ) ) ) ) )
% 2.08/1.40 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_3_t__l__p,axiom,
% 2.08/1.40 ord_less_int @ t @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_4_p,axiom,
% 2.08/1.40 zprime @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_5_t,axiom,
% 2.08/1.40 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 2.08/1.40 = ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_6_qf1pt,axiom,
% 2.08/1.40 twoSqu1013291560sum2sq @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_7_zadd__power2,axiom,
% 2.08/1.40 ! [A_8: int,B_4: int] :
% 2.08/1.40 ( ( power_power_int @ ( plus_plus_int @ A_8 @ B_4 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( plus_plus_int @ ( plus_plus_int @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) @ A_8 ) @ B_4 ) ) @ ( power_power_int @ B_4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_8_zadd__power3,axiom,
% 2.08/1.40 ! [A_8: int,B_4: int] :
% 2.08/1.40 ( ( power_power_int @ ( plus_plus_int @ A_8 @ B_4 ) @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( plus_plus_int @ ( plus_plus_int @ ( plus_plus_int @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit1 @ ( bit1 @ pls ) ) ) @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ B_4 ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit1 @ ( bit1 @ pls ) ) ) @ A_8 ) @ ( power_power_int @ B_4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) @ ( power_power_int @ B_4 @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_9_power2__sum,axiom,
% 2.08/1.40 ! [X_11: nat,Y_5: nat] :
% 2.08/1.40 ( ( power_power_nat @ ( plus_plus_nat @ X_11 @ Y_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( plus_plus_nat @ ( plus_plus_nat @ ( power_power_nat @ X_11 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_nat @ Y_5 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_nat @ ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ X_11 ) @ Y_5 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_10_power2__sum,axiom,
% 2.08/1.40 ! [X_11: int,Y_5: int] :
% 2.08/1.40 ( ( power_power_int @ ( plus_plus_int @ X_11 @ Y_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( plus_plus_int @ ( plus_plus_int @ ( power_power_int @ X_11 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_5 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) @ X_11 ) @ Y_5 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_11_power2__eq__square__number__of,axiom,
% 2.08/1.40 ! [W_5: int] :
% 2.08/1.40 ( ( power_power_int @ ( number_number_of_int @ W_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( times_times_int @ ( number_number_of_int @ W_5 ) @ ( number_number_of_int @ W_5 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_12_power2__eq__square__number__of,axiom,
% 2.08/1.40 ! [W_5: int] :
% 2.08/1.40 ( ( power_power_nat @ ( number_number_of_nat @ W_5 ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( times_times_nat @ ( number_number_of_nat @ W_5 ) @ ( number_number_of_nat @ W_5 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_13_cube__square,axiom,
% 2.08/1.40 ! [A_8: int] :
% 2.08/1.40 ( ( times_times_int @ A_8 @ ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 2.08/1.40 = ( power_power_int @ A_8 @ ( number_number_of_nat @ ( bit1 @ ( bit1 @ pls ) ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_14_one__power2,axiom,
% 2.08/1.40 ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = one_one_nat ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_15_one__power2,axiom,
% 2.08/1.40 ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = one_one_int ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_16_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
% 2.08/1.40 ! [X_10: int] :
% 2.08/1.40 ( ( times_times_int @ X_10 @ X_10 )
% 2.08/1.40 = ( power_power_int @ X_10 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_17_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
% 2.08/1.40 ! [X_10: nat] :
% 2.08/1.40 ( ( times_times_nat @ X_10 @ X_10 )
% 2.08/1.40 = ( power_power_nat @ X_10 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_18_power2__eq__square,axiom,
% 2.08/1.40 ! [A_7: int] :
% 2.08/1.40 ( ( power_power_int @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( times_times_int @ A_7 @ A_7 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_19_power2__eq__square,axiom,
% 2.08/1.40 ! [A_7: nat] :
% 2.08/1.40 ( ( power_power_nat @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( times_times_nat @ A_7 @ A_7 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_20_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
% 2.08/1.40 ! [X_9: int,N: nat] :
% 2.08/1.40 ( ( power_power_int @ X_9 @ ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ N ) )
% 2.08/1.40 = ( times_times_int @ ( power_power_int @ X_9 @ N ) @ ( power_power_int @ X_9 @ N ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_21_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
% 2.08/1.40 ! [X_9: nat,N: nat] :
% 2.08/1.40 ( ( power_power_nat @ X_9 @ ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ N ) )
% 2.08/1.40 = ( times_times_nat @ ( power_power_nat @ X_9 @ N ) @ ( power_power_nat @ X_9 @ N ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_22_add__special_I2_J,axiom,
% 2.08/1.40 ! [W_4: int] :
% 2.08/1.40 ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_4 ) )
% 2.08/1.40 = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_4 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_23_add__special_I3_J,axiom,
% 2.08/1.40 ! [V_3: int] :
% 2.08/1.40 ( ( plus_plus_int @ ( number_number_of_int @ V_3 ) @ one_one_int )
% 2.08/1.40 = ( number_number_of_int @ ( plus_plus_int @ V_3 @ ( bit1 @ pls ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_24_one__add__one__is__two,axiom,
% 2.08/1.40 ( ( plus_plus_int @ one_one_int @ one_one_int )
% 2.08/1.40 = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_25__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_,axiom,
% 2.08/1.40 ~ ! [T: int] :
% 2.08/1.40 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 2.08/1.40 != ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ T ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_26_zle__refl,axiom,
% 2.08/1.40 ! [W: int] : ( ord_less_eq_int @ W @ W ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_27_zle__linear,axiom,
% 2.08/1.40 ! [Z: int,W: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ Z @ W )
% 2.08/1.40 | ( ord_less_eq_int @ W @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_28_zless__le,axiom,
% 2.08/1.40 ! [Z: int,W: int] :
% 2.08/1.40 ( ( ord_less_int @ Z @ W )
% 2.08/1.40 <=> ( ( ord_less_eq_int @ Z @ W )
% 2.08/1.40 & ( Z != W ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_29_zless__linear,axiom,
% 2.08/1.40 ! [X_1: int,Y_1: int] :
% 2.08/1.40 ( ( ord_less_int @ X_1 @ Y_1 )
% 2.08/1.40 | ( X_1 = Y_1 )
% 2.08/1.40 | ( ord_less_int @ Y_1 @ X_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_30_zle__trans,axiom,
% 2.08/1.40 ! [K: int,I: int,J: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ I @ J )
% 2.08/1.40 => ( ( ord_less_eq_int @ J @ K )
% 2.08/1.40 => ( ord_less_eq_int @ I @ K ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_31_zle__antisym,axiom,
% 2.08/1.40 ! [Z: int,W: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ Z @ W )
% 2.08/1.40 => ( ( ord_less_eq_int @ W @ Z )
% 2.08/1.40 => ( Z = W ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_32_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
% 2.08/1.40 ! [X_8: int,P_1: nat,Q_1: nat] :
% 2.08/1.40 ( ( power_power_int @ ( power_power_int @ X_8 @ P_1 ) @ Q_1 )
% 2.08/1.40 = ( power_power_int @ X_8 @ ( times_times_nat @ P_1 @ Q_1 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
% 2.08/1.40 ! [X_8: nat,P_1: nat,Q_1: nat] :
% 2.08/1.40 ( ( power_power_nat @ ( power_power_nat @ X_8 @ P_1 ) @ Q_1 )
% 2.08/1.40 = ( power_power_nat @ X_8 @ ( times_times_nat @ P_1 @ Q_1 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_34_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
% 2.08/1.40 ! [X_7: int] :
% 2.08/1.40 ( ( power_power_int @ X_7 @ one_one_nat )
% 2.08/1.40 = X_7 ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_35_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
% 2.08/1.40 ! [X_7: nat] :
% 2.08/1.40 ( ( power_power_nat @ X_7 @ one_one_nat )
% 2.08/1.40 = X_7 ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_36_zpower__zpower,axiom,
% 2.08/1.40 ! [X_1: int,Y_1: nat,Z: nat] :
% 2.08/1.40 ( ( power_power_int @ ( power_power_int @ X_1 @ Y_1 ) @ Z )
% 2.08/1.40 = ( power_power_int @ X_1 @ ( times_times_nat @ Y_1 @ Z ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_37_le__number__of__eq__not__less,axiom,
% 2.08/1.40 ! [V_2: int,W_3: int] :
% 2.08/1.40 ( ( ord_less_eq_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ W_3 ) )
% 2.08/1.40 <=> ~ ( ord_less_nat @ ( number_number_of_nat @ W_3 ) @ ( number_number_of_nat @ V_2 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_38_le__number__of__eq__not__less,axiom,
% 2.08/1.40 ! [V_2: int,W_3: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( number_number_of_int @ V_2 ) @ ( number_number_of_int @ W_3 ) )
% 2.08/1.40 <=> ~ ( ord_less_int @ ( number_number_of_int @ W_3 ) @ ( number_number_of_int @ V_2 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_39_less__number__of,axiom,
% 2.08/1.40 ! [X_6: int,Y_4: int] :
% 2.08/1.40 ( ( ord_less_int @ ( number_number_of_int @ X_6 ) @ ( number_number_of_int @ Y_4 ) )
% 2.08/1.40 <=> ( ord_less_int @ X_6 @ Y_4 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_40_le__number__of,axiom,
% 2.08/1.40 ! [X_5: int,Y_3: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( number_number_of_int @ X_5 ) @ ( number_number_of_int @ Y_3 ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ X_5 @ Y_3 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_41_zadd__zless__mono,axiom,
% 2.08/1.40 ! [Z_1: int,Z: int,W_2: int,W: int] :
% 2.08/1.40 ( ( ord_less_int @ W_2 @ W )
% 2.08/1.40 => ( ( ord_less_eq_int @ Z_1 @ Z )
% 2.08/1.40 => ( ord_less_int @ ( plus_plus_int @ W_2 @ Z_1 ) @ ( plus_plus_int @ W @ Z ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_42_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
% 2.08/1.40 ! [X_4: int,P: nat,Q: nat] :
% 2.08/1.40 ( ( times_times_int @ ( power_power_int @ X_4 @ P ) @ ( power_power_int @ X_4 @ Q ) )
% 2.08/1.40 = ( power_power_int @ X_4 @ ( plus_plus_nat @ P @ Q ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_43_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
% 2.08/1.40 ! [X_4: nat,P: nat,Q: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( power_power_nat @ X_4 @ P ) @ ( power_power_nat @ X_4 @ Q ) )
% 2.08/1.40 = ( power_power_nat @ X_4 @ ( plus_plus_nat @ P @ Q ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_44_zpower__zadd__distrib,axiom,
% 2.08/1.40 ! [X_1: int,Y_1: nat,Z: nat] :
% 2.08/1.40 ( ( power_power_int @ X_1 @ ( plus_plus_nat @ Y_1 @ Z ) )
% 2.08/1.40 = ( times_times_int @ ( power_power_int @ X_1 @ Y_1 ) @ ( power_power_int @ X_1 @ Z ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_45_nat__mult__2,axiom,
% 2.08/1.40 ! [Z: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) @ Z )
% 2.08/1.40 = ( plus_plus_nat @ Z @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_46_nat__mult__2__right,axiom,
% 2.08/1.40 ! [Z: nat] :
% 2.08/1.40 ( ( times_times_nat @ Z @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 2.08/1.40 = ( plus_plus_nat @ Z @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_47_nat__1__add__1,axiom,
% 2.08/1.40 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 2.08/1.40 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_48_less__int__code_I16_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_49_rel__simps_I17_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 2.08/1.40 <=> ( ord_less_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_50_less__eq__int__code_I16_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_51_rel__simps_I34_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_52_rel__simps_I2_J,axiom,
% 2.08/1.40 ~ ( ord_less_int @ pls @ pls ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_53_less__int__code_I13_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_54_rel__simps_I14_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 2.08/1.40 <=> ( ord_less_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_55_rel__simps_I19_J,axiom,
% 2.08/1.40 ord_less_eq_int @ pls @ pls ).
% 2.08/1.40
% 2.08/1.40 thf(fact_56_less__eq__int__code_I13_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_57_rel__simps_I31_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_58_less__number__of__int__code,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 2.08/1.40 <=> ( ord_less_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_59_less__eq__number__of__int__code,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_60_zadd__strict__right__mono,axiom,
% 2.08/1.40 ! [K: int,I: int,J: int] :
% 2.08/1.40 ( ( ord_less_int @ I @ J )
% 2.08/1.40 => ( ord_less_int @ ( plus_plus_int @ I @ K ) @ ( plus_plus_int @ J @ K ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_61_zadd__left__mono,axiom,
% 2.08/1.40 ! [K: int,I: int,J: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ I @ J )
% 2.08/1.40 => ( ord_less_eq_int @ ( plus_plus_int @ K @ I ) @ ( plus_plus_int @ K @ J ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_62_add__nat__number__of,axiom,
% 2.08/1.40 ! [V_1: int,V: int] :
% 2.08/1.40 ( ( ( ord_less_int @ V @ pls )
% 2.08/1.40 => ( ( plus_plus_nat @ ( number_number_of_nat @ V ) @ ( number_number_of_nat @ V_1 ) )
% 2.08/1.40 = ( number_number_of_nat @ V_1 ) ) )
% 2.08/1.40 & ( ~ ( ord_less_int @ V @ pls )
% 2.08/1.40 => ( ( ( ord_less_int @ V_1 @ pls )
% 2.08/1.40 => ( ( plus_plus_nat @ ( number_number_of_nat @ V ) @ ( number_number_of_nat @ V_1 ) )
% 2.08/1.40 = ( number_number_of_nat @ V ) ) )
% 2.08/1.40 & ( ~ ( ord_less_int @ V_1 @ pls )
% 2.08/1.40 => ( ( plus_plus_nat @ ( number_number_of_nat @ V ) @ ( number_number_of_nat @ V_1 ) )
% 2.08/1.40 = ( number_number_of_nat @ ( plus_plus_int @ V @ V_1 ) ) ) ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_63_nat__numeral__1__eq__1,axiom,
% 2.08/1.40 ( ( number_number_of_nat @ ( bit1 @ pls ) )
% 2.08/1.40 = one_one_nat ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_64_Numeral1__eq1__nat,axiom,
% 2.08/1.40 ( one_one_nat
% 2.08/1.40 = ( number_number_of_nat @ ( bit1 @ pls ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_65_rel__simps_I29_J,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit1 @ K ) @ pls )
% 2.08/1.40 <=> ( ord_less_int @ K @ pls ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_66_rel__simps_I5_J,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( ord_less_int @ pls @ ( bit1 @ K ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_67_less__eq__int__code_I15_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_68_rel__simps_I33_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 2.08/1.40 <=> ( ord_less_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_69_less__int__code_I14_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_70_rel__simps_I15_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_71_zless__imp__add1__zle,axiom,
% 2.08/1.40 ! [W: int,Z: int] :
% 2.08/1.40 ( ( ord_less_int @ W @ Z )
% 2.08/1.40 => ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_72_add1__zle__eq,axiom,
% 2.08/1.40 ! [W: int,Z: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z )
% 2.08/1.40 <=> ( ord_less_int @ W @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_73_zle__add1__eq__le,axiom,
% 2.08/1.40 ! [W: int,Z: int] :
% 2.08/1.40 ( ( ord_less_int @ W @ ( plus_plus_int @ Z @ one_one_int ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ W @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_74_zprime__2,axiom,
% 2.08/1.40 zprime @ ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_75_is__mult__sum2sq,axiom,
% 2.08/1.40 ! [Y_1: int,X_1: int] :
% 2.08/1.40 ( ( twoSqu1013291560sum2sq @ X_1 )
% 2.08/1.40 => ( ( twoSqu1013291560sum2sq @ Y_1 )
% 2.08/1.40 => ( twoSqu1013291560sum2sq @ ( times_times_int @ X_1 @ Y_1 ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
% 2.08/1.40 ! [Lx_6: int,Ly_4: int,Rx_6: int,Ry_4: int] :
% 2.08/1.40 ( ( times_times_int @ ( times_times_int @ Lx_6 @ Ly_4 ) @ ( times_times_int @ Rx_6 @ Ry_4 ) )
% 2.08/1.40 = ( times_times_int @ ( times_times_int @ Lx_6 @ Rx_6 ) @ ( times_times_int @ Ly_4 @ Ry_4 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
% 2.08/1.40 ! [Lx_6: nat,Ly_4: nat,Rx_6: nat,Ry_4: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( times_times_nat @ Lx_6 @ Ly_4 ) @ ( times_times_nat @ Rx_6 @ Ry_4 ) )
% 2.08/1.40 = ( times_times_nat @ ( times_times_nat @ Lx_6 @ Rx_6 ) @ ( times_times_nat @ Ly_4 @ Ry_4 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
% 2.08/1.40 ! [Lx_5: int,Ly_3: int,Rx_5: int,Ry_3: int] :
% 2.08/1.40 ( ( times_times_int @ ( times_times_int @ Lx_5 @ Ly_3 ) @ ( times_times_int @ Rx_5 @ Ry_3 ) )
% 2.08/1.40 = ( times_times_int @ Rx_5 @ ( times_times_int @ ( times_times_int @ Lx_5 @ Ly_3 ) @ Ry_3 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
% 2.08/1.40 ! [Lx_5: nat,Ly_3: nat,Rx_5: nat,Ry_3: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( times_times_nat @ Lx_5 @ Ly_3 ) @ ( times_times_nat @ Rx_5 @ Ry_3 ) )
% 2.08/1.40 = ( times_times_nat @ Rx_5 @ ( times_times_nat @ ( times_times_nat @ Lx_5 @ Ly_3 ) @ Ry_3 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_80_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
% 2.08/1.40 ! [Lx_4: int,Ly_2: int,Rx_4: int,Ry_2: int] :
% 2.08/1.40 ( ( times_times_int @ ( times_times_int @ Lx_4 @ Ly_2 ) @ ( times_times_int @ Rx_4 @ Ry_2 ) )
% 2.08/1.40 = ( times_times_int @ Lx_4 @ ( times_times_int @ Ly_2 @ ( times_times_int @ Rx_4 @ Ry_2 ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_81_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
% 2.08/1.40 ! [Lx_4: nat,Ly_2: nat,Rx_4: nat,Ry_2: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( times_times_nat @ Lx_4 @ Ly_2 ) @ ( times_times_nat @ Rx_4 @ Ry_2 ) )
% 2.08/1.40 = ( times_times_nat @ Lx_4 @ ( times_times_nat @ Ly_2 @ ( times_times_nat @ Rx_4 @ Ry_2 ) ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_82_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
% 2.08/1.40 ! [Lx_3: int,Ly_1: int,Rx_3: int] :
% 2.08/1.40 ( ( times_times_int @ ( times_times_int @ Lx_3 @ Ly_1 ) @ Rx_3 )
% 2.08/1.40 = ( times_times_int @ ( times_times_int @ Lx_3 @ Rx_3 ) @ Ly_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_83_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
% 2.08/1.40 ! [Lx_3: nat,Ly_1: nat,Rx_3: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( times_times_nat @ Lx_3 @ Ly_1 ) @ Rx_3 )
% 2.08/1.40 = ( times_times_nat @ ( times_times_nat @ Lx_3 @ Rx_3 ) @ Ly_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
% 2.08/1.40 ! [Lx_2: int,Ly: int,Rx_2: int] :
% 2.08/1.40 ( ( times_times_int @ ( times_times_int @ Lx_2 @ Ly ) @ Rx_2 )
% 2.08/1.40 = ( times_times_int @ Lx_2 @ ( times_times_int @ Ly @ Rx_2 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
% 2.08/1.40 ! [Lx_2: nat,Ly: nat,Rx_2: nat] :
% 2.08/1.40 ( ( times_times_nat @ ( times_times_nat @ Lx_2 @ Ly ) @ Rx_2 )
% 2.08/1.40 = ( times_times_nat @ Lx_2 @ ( times_times_nat @ Ly @ Rx_2 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_86_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
% 2.08/1.40 ! [Lx_1: int,Rx_1: int,Ry_1: int] :
% 2.08/1.40 ( ( times_times_int @ Lx_1 @ ( times_times_int @ Rx_1 @ Ry_1 ) )
% 2.08/1.40 = ( times_times_int @ ( times_times_int @ Lx_1 @ Rx_1 ) @ Ry_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
% 2.08/1.40 ! [Lx_1: nat,Rx_1: nat,Ry_1: nat] :
% 2.08/1.40 ( ( times_times_nat @ Lx_1 @ ( times_times_nat @ Rx_1 @ Ry_1 ) )
% 2.08/1.40 = ( times_times_nat @ ( times_times_nat @ Lx_1 @ Rx_1 ) @ Ry_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_88_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
% 2.08/1.40 ! [Lx: int,Rx: int,Ry: int] :
% 2.08/1.40 ( ( times_times_int @ Lx @ ( times_times_int @ Rx @ Ry ) )
% 2.08/1.40 = ( times_times_int @ Rx @ ( times_times_int @ Lx @ Ry ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_89_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
% 2.08/1.40 ! [Lx: nat,Rx: nat,Ry: nat] :
% 2.08/1.40 ( ( times_times_nat @ Lx @ ( times_times_nat @ Rx @ Ry ) )
% 2.08/1.40 = ( times_times_nat @ Rx @ ( times_times_nat @ Lx @ Ry ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
% 2.08/1.40 ! [A_6: int,B_3: int] :
% 2.08/1.40 ( ( times_times_int @ A_6 @ B_3 )
% 2.08/1.40 = ( times_times_int @ B_3 @ A_6 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
% 2.08/1.40 ! [A_6: nat,B_3: nat] :
% 2.08/1.40 ( ( times_times_nat @ A_6 @ B_3 )
% 2.08/1.40 = ( times_times_nat @ B_3 @ A_6 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_92_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
% 2.08/1.40 ! [A_5: int,B_2: int,C_5: int,D_2: int] :
% 2.08/1.40 ( ( plus_plus_int @ ( plus_plus_int @ A_5 @ B_2 ) @ ( plus_plus_int @ C_5 @ D_2 ) )
% 2.08/1.40 = ( plus_plus_int @ ( plus_plus_int @ A_5 @ C_5 ) @ ( plus_plus_int @ B_2 @ D_2 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_93_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
% 2.08/1.40 ! [A_5: nat,B_2: nat,C_5: nat,D_2: nat] :
% 2.08/1.40 ( ( plus_plus_nat @ ( plus_plus_nat @ A_5 @ B_2 ) @ ( plus_plus_nat @ C_5 @ D_2 ) )
% 2.08/1.40 = ( plus_plus_nat @ ( plus_plus_nat @ A_5 @ C_5 ) @ ( plus_plus_nat @ B_2 @ D_2 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_94_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
% 2.08/1.40 ! [A_4: int,B_1: int,C_4: int] :
% 2.08/1.40 ( ( plus_plus_int @ ( plus_plus_int @ A_4 @ B_1 ) @ C_4 )
% 2.08/1.40 = ( plus_plus_int @ ( plus_plus_int @ A_4 @ C_4 ) @ B_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_95_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
% 2.08/1.40 ! [A_4: nat,B_1: nat,C_4: nat] :
% 2.08/1.40 ( ( plus_plus_nat @ ( plus_plus_nat @ A_4 @ B_1 ) @ C_4 )
% 2.08/1.40 = ( plus_plus_nat @ ( plus_plus_nat @ A_4 @ C_4 ) @ B_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
% 2.08/1.40 ! [A_3: int,B: int,C_3: int] :
% 2.08/1.40 ( ( plus_plus_int @ ( plus_plus_int @ A_3 @ B ) @ C_3 )
% 2.08/1.40 = ( plus_plus_int @ A_3 @ ( plus_plus_int @ B @ C_3 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
% 2.08/1.40 ! [A_3: nat,B: nat,C_3: nat] :
% 2.08/1.40 ( ( plus_plus_nat @ ( plus_plus_nat @ A_3 @ B ) @ C_3 )
% 2.08/1.40 = ( plus_plus_nat @ A_3 @ ( plus_plus_nat @ B @ C_3 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_98_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
% 2.08/1.40 ! [A_2: int,C_2: int,D_1: int] :
% 2.08/1.40 ( ( plus_plus_int @ A_2 @ ( plus_plus_int @ C_2 @ D_1 ) )
% 2.08/1.40 = ( plus_plus_int @ ( plus_plus_int @ A_2 @ C_2 ) @ D_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
% 2.08/1.40 ! [A_2: nat,C_2: nat,D_1: nat] :
% 2.08/1.40 ( ( plus_plus_nat @ A_2 @ ( plus_plus_nat @ C_2 @ D_1 ) )
% 2.08/1.40 = ( plus_plus_nat @ ( plus_plus_nat @ A_2 @ C_2 ) @ D_1 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_100_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
% 2.08/1.40 ! [A_1: int,C_1: int,D: int] :
% 2.08/1.40 ( ( plus_plus_int @ A_1 @ ( plus_plus_int @ C_1 @ D ) )
% 2.08/1.40 = ( plus_plus_int @ C_1 @ ( plus_plus_int @ A_1 @ D ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_101_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
% 2.08/1.40 ! [A_1: nat,C_1: nat,D: nat] :
% 2.08/1.40 ( ( plus_plus_nat @ A_1 @ ( plus_plus_nat @ C_1 @ D ) )
% 2.08/1.40 = ( plus_plus_nat @ C_1 @ ( plus_plus_nat @ A_1 @ D ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
% 2.08/1.40 ! [A: int,C: int] :
% 2.08/1.40 ( ( plus_plus_int @ A @ C )
% 2.08/1.40 = ( plus_plus_int @ C @ A ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
% 2.08/1.40 ! [A: nat,C: nat] :
% 2.08/1.40 ( ( plus_plus_nat @ A @ C )
% 2.08/1.40 = ( plus_plus_nat @ C @ A ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_104_eq__number__of,axiom,
% 2.08/1.40 ! [X_3: int,Y_2: int] :
% 2.08/1.40 ( ( ( number_number_of_int @ X_3 )
% 2.08/1.40 = ( number_number_of_int @ Y_2 ) )
% 2.08/1.40 <=> ( X_3 = Y_2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_105_number__of__reorient,axiom,
% 2.08/1.40 ! [W_1: int,X_2: nat] :
% 2.08/1.40 ( ( ( number_number_of_nat @ W_1 )
% 2.08/1.40 = X_2 )
% 2.08/1.40 <=> ( X_2
% 2.08/1.40 = ( number_number_of_nat @ W_1 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_106_number__of__reorient,axiom,
% 2.08/1.40 ! [W_1: int,X_2: int] :
% 2.08/1.40 ( ( ( number_number_of_int @ W_1 )
% 2.08/1.40 = X_2 )
% 2.08/1.40 <=> ( X_2
% 2.08/1.40 = ( number_number_of_int @ W_1 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_107_rel__simps_I51_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ( bit1 @ K )
% 2.08/1.40 = ( bit1 @ L ) )
% 2.08/1.40 <=> ( K = L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_108_rel__simps_I48_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ( bit0 @ K )
% 2.08/1.40 = ( bit0 @ L ) )
% 2.08/1.40 <=> ( K = L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_109_zmult__assoc,axiom,
% 2.08/1.40 ! [Z1: int,Z2: int,Z3: int] :
% 2.08/1.40 ( ( times_times_int @ ( times_times_int @ Z1 @ Z2 ) @ Z3 )
% 2.08/1.40 = ( times_times_int @ Z1 @ ( times_times_int @ Z2 @ Z3 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_110_zmult__commute,axiom,
% 2.08/1.40 ! [Z: int,W: int] :
% 2.08/1.40 ( ( times_times_int @ Z @ W )
% 2.08/1.40 = ( times_times_int @ W @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_111_number__of__is__id,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( number_number_of_int @ K )
% 2.08/1.40 = K ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_112_zadd__assoc,axiom,
% 2.08/1.40 ! [Z1: int,Z2: int,Z3: int] :
% 2.08/1.40 ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 )
% 2.08/1.40 = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_113_zadd__left__commute,axiom,
% 2.08/1.40 ! [X_1: int,Y_1: int,Z: int] :
% 2.08/1.40 ( ( plus_plus_int @ X_1 @ ( plus_plus_int @ Y_1 @ Z ) )
% 2.08/1.40 = ( plus_plus_int @ Y_1 @ ( plus_plus_int @ X_1 @ Z ) ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_114_zadd__commute,axiom,
% 2.08/1.40 ! [Z: int,W: int] :
% 2.08/1.40 ( ( plus_plus_int @ Z @ W )
% 2.08/1.40 = ( plus_plus_int @ W @ Z ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_115_rel__simps_I12_J,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit1 @ K ) @ pls )
% 2.08/1.40 <=> ( ord_less_int @ K @ pls ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_116_less__int__code_I15_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_117_rel__simps_I16_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 2.08/1.40 <=> ( ord_less_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_118_rel__simps_I10_J,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( ord_less_int @ ( bit0 @ K ) @ pls )
% 2.08/1.40 <=> ( ord_less_int @ K @ pls ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_119_rel__simps_I4_J,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( ord_less_int @ pls @ ( bit0 @ K ) )
% 2.08/1.40 <=> ( ord_less_int @ pls @ K ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_120_rel__simps_I22_J,axiom,
% 2.08/1.40 ! [K: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ pls @ ( bit1 @ K ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_121_less__eq__int__code_I14_J,axiom,
% 2.08/1.40 ! [K1: int,K2: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(fact_122_rel__simps_I32_J,axiom,
% 2.08/1.40 ! [K: int,L: int] :
% 2.08/1.40 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 2.08/1.40 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 2.08/1.40
% 2.08/1.40 thf(conj_0,conjecture,
% 2.08/1.40 ? [X: int,Y: int] :
% 2.08/1.40 ( ( 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 ) ) ) ) )
% 2.08/1.40 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ).
% 2.08/1.40 ------------------------
% 2.08/1.42 % (25059)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_24772 for (2999ds/275Mi)
% 2.08/1.42 % (25058)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_24772 for (2999ds/2Mi)
% 2.08/1.42 % (25060)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_24772 for (2999ds/18Mi)
% 2.08/1.42 % (25058)Instruction limit reached!
% 2.08/1.42 % (25058)------------------------------
% 2.08/1.42 % (25058)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.42 % (25058)Termination reason: Unknown
% 2.08/1.42 % (25058)Termination phase: shuffling
% 2.08/1.42
% 2.08/1.42 % (25058)Memory used [KB]: 1151
% 2.08/1.42 % (25058)Time elapsed: 0.002 s
% 2.08/1.42 % (25058)Instructions burned: 3 (million)
% 2.08/1.42 % (25058)------------------------------
% 2.08/1.42 % (25058)------------------------------
% 2.08/1.43 % (25054)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_24772 for (2999ds/183Mi)
% 2.08/1.43 % (25055)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_24772 for (2999ds/4Mi)
% 2.08/1.43 % (25060)Instruction limit reached!
% 2.08/1.43 % (25060)------------------------------
% 2.08/1.43 % (25060)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.43 % (25060)Termination reason: Unknown
% 2.08/1.43 % (25060)Termination phase: Property scanning
% 2.08/1.43
% 2.08/1.43 % (25060)Memory used [KB]: 1407
% 2.08/1.43 % (25060)Time elapsed: 0.008 s
% 2.08/1.43 % (25060)Instructions burned: 21 (million)
% 2.08/1.43 % (25060)------------------------------
% 2.08/1.43 % (25060)------------------------------
% 2.08/1.43 % (25056)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_24772 for (2999ds/27Mi)
% 2.08/1.43 % (25057)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_24772 for (2999ds/2Mi)
% 2.08/1.43 % (25055)Instruction limit reached!
% 2.08/1.43 % (25055)------------------------------
% 2.08/1.43 % (25055)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.43 % (25055)Termination reason: Unknown
% 2.08/1.43 % (25055)Termination phase: shuffling
% 2.08/1.43
% 2.08/1.43 % (25055)Memory used [KB]: 1151
% 2.08/1.43 % (25055)Time elapsed: 0.004 s
% 2.08/1.43 % (25055)Instructions burned: 4 (million)
% 2.08/1.43 % (25055)------------------------------
% 2.08/1.43 % (25055)------------------------------
% 2.08/1.43 % (25057)Instruction limit reached!
% 2.08/1.43 % (25057)------------------------------
% 2.08/1.43 % (25057)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.43 % (25057)Termination reason: Unknown
% 2.08/1.43 % (25057)Termination phase: shuffling
% 2.08/1.43
% 2.08/1.43 % (25057)Memory used [KB]: 1151
% 2.08/1.43 % (25057)Time elapsed: 0.004 s
% 2.08/1.43 % (25057)Instructions burned: 3 (million)
% 2.08/1.43 % (25057)------------------------------
% 2.08/1.43 % (25057)------------------------------
% 2.08/1.43 % (25061)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_24772 for (2999ds/3Mi)
% 2.08/1.43 % (25061)Instruction limit reached!
% 2.08/1.43 % (25061)------------------------------
% 2.08/1.43 % (25061)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.43 % (25061)Termination reason: Unknown
% 2.08/1.43 % (25061)Termination phase: shuffling
% 2.08/1.43
% 2.08/1.43 % (25061)Memory used [KB]: 1151
% 2.08/1.43 % (25061)Time elapsed: 0.003 s
% 2.08/1.43 % (25061)Instructions burned: 4 (million)
% 2.08/1.43 % (25061)------------------------------
% 2.08/1.43 % (25061)------------------------------
% 2.08/1.44 % (25062)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_24772 for (2999ds/37Mi)
% 2.08/1.44 % (25056)Instruction limit reached!
% 2.08/1.44 % (25056)------------------------------
% 2.08/1.44 % (25056)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.44 % (25056)Termination reason: Unknown
% 2.08/1.44 % (25056)Termination phase: Saturation
% 2.08/1.44
% 2.08/1.44 % (25056)Memory used [KB]: 5884
% 2.08/1.44 % (25056)Time elapsed: 0.017 s
% 2.08/1.44 % (25056)Instructions burned: 28 (million)
% 2.08/1.44 % (25056)------------------------------
% 2.08/1.44 % (25056)------------------------------
% 2.08/1.44 % (25065)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_24772 for (2999ds/1041Mi)
% 2.08/1.45 % (25063)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_24772 for (2999ds/15Mi)
% 2.08/1.45 % (25064)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_24772 for (2999ds/3Mi)
% 2.08/1.45 % (25064)Instruction limit reached!
% 2.08/1.45 % (25064)------------------------------
% 2.08/1.45 % (25064)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.45 % (25064)Termination reason: Unknown
% 2.08/1.45 % (25064)Termination phase: shuffling
% 2.08/1.45
% 2.08/1.45 % (25064)Memory used [KB]: 1151
% 2.08/1.45 % (25064)Time elapsed: 0.004 s
% 2.08/1.45 % (25064)Instructions burned: 4 (million)
% 2.08/1.45 % (25064)------------------------------
% 2.08/1.45 % (25064)------------------------------
% 2.08/1.45 % (25062)Instruction limit reached!
% 2.08/1.45 % (25062)------------------------------
% 2.08/1.45 % (25062)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.45 % (25062)Termination reason: Unknown
% 2.08/1.45 % (25062)Termination phase: Property scanning
% 2.08/1.45
% 2.08/1.45 % (25062)Memory used [KB]: 1535
% 2.08/1.45 % (25062)Time elapsed: 0.012 s
% 2.08/1.45 % (25062)Instructions burned: 40 (million)
% 2.08/1.45 % (25062)------------------------------
% 2.08/1.45 % (25062)------------------------------
% 2.08/1.46 % (25063)Instruction limit reached!
% 2.08/1.46 % (25063)------------------------------
% 2.08/1.46 % (25063)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.46 % (25063)Termination reason: Unknown
% 2.08/1.46 % (25063)Termination phase: Property scanning
% 2.08/1.46
% 2.08/1.46 % (25063)Memory used [KB]: 1407
% 2.08/1.46 % (25063)Time elapsed: 0.010 s
% 2.08/1.46 % (25063)Instructions burned: 15 (million)
% 2.08/1.46 % (25063)------------------------------
% 2.08/1.46 % (25063)------------------------------
% 2.08/1.46 % (25068)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_24772 for (2999ds/3Mi)
% 2.08/1.46 % (25066)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_24772 for (2999ds/7Mi)
% 2.08/1.46 % (25068)Instruction limit reached!
% 2.08/1.46 % (25068)------------------------------
% 2.08/1.46 % (25068)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.46 % (25068)Termination reason: Unknown
% 2.08/1.46 % (25068)Termination phase: shuffling
% 2.08/1.46
% 2.08/1.46 % (25068)Memory used [KB]: 1151
% 2.08/1.46 % (25068)Time elapsed: 0.003 s
% 2.08/1.46 % (25068)Instructions burned: 4 (million)
% 2.08/1.46 % (25068)------------------------------
% 2.08/1.46 % (25068)------------------------------
% 2.08/1.46 % (25054)First to succeed.
% 2.08/1.46 % (25066)Instruction limit reached!
% 2.08/1.46 % (25066)------------------------------
% 2.08/1.46 % (25066)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.46 % (25066)Termination reason: Unknown
% 2.08/1.46 % (25066)Termination phase: Property scanning
% 2.08/1.46
% 2.08/1.46 % (25066)Memory used [KB]: 1151
% 2.08/1.46 % (25066)Time elapsed: 0.006 s
% 2.08/1.46 % (25066)Instructions burned: 7 (million)
% 2.08/1.46 % (25066)------------------------------
% 2.08/1.46 % (25066)------------------------------
% 2.08/1.47 % (25054)Refutation found. Thanks to Tanya!
% 2.08/1.47 % SZS status Theorem for DTF2THF_24772
% 2.08/1.47 % SZS output start Proof for DTF2THF_24772
% 2.08/1.47 thf(type_def_5, type, int: $tType).
% 2.08/1.47 thf(type_def_6, type, nat: $tType).
% 2.08/1.47 thf(func_def_0, type, int: $tType).
% 2.08/1.47 thf(func_def_1, type, nat: $tType).
% 2.08/1.47 thf(func_def_2, type, one_one_int: int).
% 2.08/1.47 thf(func_def_3, type, one_one_nat: nat).
% 2.08/1.47 thf(func_def_4, type, plus_plus_int: int > int > int).
% 2.08/1.47 thf(func_def_5, type, plus_plus_nat: nat > nat > nat).
% 2.08/1.47 thf(func_def_6, type, times_times_int: int > int > int).
% 2.08/1.47 thf(func_def_7, type, times_times_nat: nat > nat > nat).
% 2.08/1.47 thf(func_def_8, type, zprime: int > $o).
% 2.08/1.47 thf(func_def_9, type, bit0: int > int).
% 2.08/1.47 thf(func_def_10, type, bit1: int > int).
% 2.08/1.47 thf(func_def_11, type, pls: int).
% 2.08/1.47 thf(func_def_12, type, number_number_of_int: int > int).
% 2.08/1.47 thf(func_def_13, type, number_number_of_nat: int > nat).
% 2.08/1.47 thf(func_def_14, type, ord_less_int: int > int > $o).
% 2.08/1.47 thf(func_def_15, type, ord_less_nat: nat > nat > $o).
% 2.08/1.47 thf(func_def_16, type, ord_less_eq_int: int > int > $o).
% 2.08/1.47 thf(func_def_17, type, ord_less_eq_nat: nat > nat > $o).
% 2.08/1.47 thf(func_def_18, type, power_power_int: int > nat > int).
% 2.08/1.47 thf(func_def_19, type, power_power_nat: nat > nat > nat).
% 2.08/1.47 thf(func_def_20, type, twoSqu1013291560sum2sq: int > $o).
% 2.08/1.47 thf(func_def_21, type, m: int).
% 2.08/1.47 thf(func_def_22, type, s: int).
% 2.08/1.47 thf(func_def_23, type, t: int).
% 2.08/1.47 thf(func_def_27, type, sK0: int).
% 2.08/1.47 thf(func_def_28, type, sK1: int).
% 2.08/1.47 thf(func_def_29, type, sK2: int).
% 2.08/1.47 thf(func_def_30, type, sK3: int).
% 2.08/1.47 thf(func_def_31, type, sK4: int).
% 2.08/1.47 thf(f625,plain,(
% 2.08/1.47 $false),
% 2.08/1.47 inference(subsumption_resolution,[status(thm)],[f624,f591])).
% 2.08/1.47 thf(f591,plain,(
% 2.08/1.47 (one_one_int != t)),
% 2.08/1.47 inference(subsumption_resolution,[status(thm)],[f389,f477])).
% 2.08/1.47 thf(f477,plain,(
% 2.08/1.47 ( ! [X0 : int,X1 : int] : (((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) != (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))) )),
% 2.08/1.47 inference(cnf_transformation,[status(thm)],[f297])).
% 2.08/1.47 thf(f297,plain,(
% 2.08/1.47 ! [X0 : int,X1 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) != (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 inference(ennf_transformation,[status(thm)],[f125])).
% 2.08/1.47 thf(f125,negated_conjecture,(
% 2.08/1.47 ~? [X0 : int,X1 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 inference(negated_conjecture,[status(cth)],[f124])).
% 2.08/1.47 thf(f124,conjecture,(
% 2.08/1.47 ? [X0 : int,X1 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',conj_0)).
% 2.08/1.47 thf(f389,plain,(
% 2.08/1.47 (one_one_int != t) | ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ sK1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ sK0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(cnf_transformation,[status(thm)],[f316])).
% 2.08/1.47 thf(f316,plain,(
% 2.08/1.47 (one_one_int != t) | ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ sK1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ sK0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f314,f315])).
% 2.08/1.47 thf(f315,plain,(
% 2.08/1.47 ? [X0 : int,X1 : int] : ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) => ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ sK1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ sK0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 introduced(definition,[],[choice_axiom])).
% 2.08/1.47 thf(f314,plain,(
% 2.08/1.47 (one_one_int != t) | ? [X0 : int,X1 : int] : ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(rectify,[status(thm)],[f307])).
% 2.08/1.47 thf(f307,plain,(
% 2.08/1.47 (one_one_int != t) | ? [X1 : int,X0 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 inference(ennf_transformation,[status(thm)],[f2])).
% 2.08/1.47 thf(f2,axiom,(
% 2.08/1.47 (one_one_int = t) => ? [X1 : int,X0 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06)).
% 2.08/1.47 thf(f624,plain,(
% 2.08/1.47 (one_one_int = t)),
% 2.08/1.47 inference(subsumption_resolution,[status(thm)],[f623,f401])).
% 2.08/1.47 thf(f401,plain,(
% 2.08/1.47 ((ord_less_eq_int @ one_one_int @ t) = $true)),
% 2.08/1.47 inference(cnf_transformation,[status(thm)],[f176])).
% 2.08/1.47 thf(f176,plain,(
% 2.08/1.47 ((ord_less_eq_int @ one_one_int @ t) = $true)),
% 2.08/1.47 inference(fool_elimination,[status(thm)],[f175])).
% 2.08/1.47 thf(f175,plain,(
% 2.08/1.47 (ord_less_eq_int @ one_one_int @ t)),
% 2.08/1.47 inference(rectify,[status(thm)],[f1])).
% 2.08/1.47 thf(f1,axiom,(
% 2.08/1.47 (ord_less_eq_int @ one_one_int @ t)),
% 2.08/1.47 file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_0_tpos)).
% 2.08/1.47 thf(f623,plain,(
% 2.08/1.47 ((ord_less_eq_int @ one_one_int @ t) != $true) | (one_one_int = t)),
% 2.08/1.47 inference(trivial_inequality_removal,[status(thm)],[f621])).
% 2.08/1.47 thf(f621,plain,(
% 2.08/1.47 ((ord_less_eq_int @ one_one_int @ t) != $true) | (one_one_int = t) | ($true != $true)),
% 2.08/1.47 inference(superposition,[status(thm)],[f590,f469])).
% 2.08/1.47 thf(f469,plain,(
% 2.08/1.47 ( ! [X0 : int,X1 : int] : (((ord_less_int @ X1 @ X0) = $true) | (X0 = X1) | ((ord_less_eq_int @ X1 @ X0) != $true)) )),
% 2.08/1.47 inference(cnf_transformation,[status(thm)],[f355])).
% 2.08/1.47 thf(f355,plain,(
% 2.08/1.47 ! [X0 : int,X1 : int] : ((((ord_less_int @ X1 @ X0) = $true) | ((ord_less_eq_int @ X1 @ X0) != $true) | (X0 = X1)) & ((((ord_less_eq_int @ X1 @ X0) = $true) & (X0 != X1)) | ((ord_less_int @ X1 @ X0) != $true)))),
% 2.08/1.47 inference(rectify,[status(thm)],[f354])).
% 2.08/1.47 thf(f354,plain,(
% 2.08/1.47 ! [X1 : int,X0 : int] : ((((ord_less_int @ X0 @ X1) = $true) | ((ord_less_eq_int @ X0 @ X1) != $true) | (X0 = X1)) & ((((ord_less_eq_int @ X0 @ X1) = $true) & (X0 != X1)) | ((ord_less_int @ X0 @ X1) != $true)))),
% 2.08/1.47 inference(flattening,[status(thm)],[f353])).
% 2.08/1.47 thf(f353,plain,(
% 2.08/1.47 ! [X1 : int,X0 : int] : ((((ord_less_int @ X0 @ X1) = $true) | (((ord_less_eq_int @ X0 @ X1) != $true) | (X0 = X1))) & ((((ord_less_eq_int @ X0 @ X1) = $true) & (X0 != X1)) | ((ord_less_int @ X0 @ X1) != $true)))),
% 2.08/1.47 inference(nnf_transformation,[status(thm)],[f154])).
% 2.08/1.47 thf(f154,plain,(
% 2.08/1.47 ! [X1 : int,X0 : int] : (((ord_less_int @ X0 @ X1) = $true) <=> (((ord_less_eq_int @ X0 @ X1) = $true) & (X0 != X1)))),
% 2.08/1.47 inference(fool_elimination,[status(thm)],[f153])).
% 2.08/1.47 thf(f153,plain,(
% 2.08/1.47 ! [X0 : int,X1 : int] : ((ord_less_int @ X0 @ X1) <=> ((ord_less_eq_int @ X0 @ X1) & (X0 != X1)))),
% 2.08/1.47 inference(rectify,[status(thm)],[f29])).
% 2.08/1.47 thf(f29,axiom,(
% 2.08/1.47 ! [X15 : int,X14 : int] : ((ord_less_int @ X15 @ X14) <=> ((ord_less_eq_int @ X15 @ X14) & (X14 != X15)))),
% 2.08/1.47 file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_28_zless__le)).
% 2.08/1.47 thf(f590,plain,(
% 2.08/1.47 ((ord_less_int @ one_one_int @ t) != $true)),
% 2.08/1.47 inference(subsumption_resolution,[status(thm)],[f508,f477])).
% 2.08/1.47 thf(f508,plain,(
% 2.08/1.47 ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ sK3 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ sK4 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | ((ord_less_int @ one_one_int @ t) != $true)),
% 2.08/1.47 inference(cnf_transformation,[status(thm)],[f376])).
% 2.08/1.47 thf(f376,plain,(
% 2.08/1.47 ((ord_less_int @ one_one_int @ t) != $true) | ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ sK3 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ sK4 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(skolemisation,[status(esa),new_symbols(skolem,[sK3,sK4])],[f374,f375])).
% 2.08/1.47 thf(f375,plain,(
% 2.08/1.47 ? [X0 : int,X1 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int)) => ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ sK3 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ sK4 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 introduced(definition,[],[choice_axiom])).
% 2.08/1.47 thf(f374,plain,(
% 2.08/1.47 ((ord_less_int @ one_one_int @ t) != $true) | ? [X0 : int,X1 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 inference(rectify,[status(thm)],[f306])).
% 2.08/1.47 thf(f306,plain,(
% 2.08/1.47 ((ord_less_int @ one_one_int @ t) != $true) | ? [X1 : int,X0 : int] : ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(ennf_transformation,[status(thm)],[f180])).
% 2.08/1.47 thf(f180,plain,(
% 2.08/1.47 ((ord_less_int @ one_one_int @ t) = $true) => ? [X1 : int,X0 : int] : ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(fool_elimination,[status(thm)],[f179])).
% 2.08/1.47 thf(f179,plain,(
% 2.08/1.47 (ord_less_int @ one_one_int @ t) => ? [X0 : int,X1 : int] : ((plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) = (plus_plus_int @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 2.08/1.47 inference(rectify,[status(thm)],[f3])).
% 2.08/1.47 thf(f3,axiom,(
% 2.08/1.47 (ord_less_int @ one_one_int @ t) => ? [X1 : int,X0 : int] : ((plus_plus_int @ (power_power_int @ X0 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ (power_power_int @ X1 @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int))),
% 2.08/1.47 file('/export/starexec/sandbox2/tmp/tmp.DxmYewbZaj/DTF2THF_24772.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06)).
% 2.08/1.47 % SZS output end Proof for DTF2THF_24772
% 2.08/1.47 % (25054)------------------------------
% 2.08/1.47 % (25054)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.08/1.47 % (25054)Termination reason: Refutation
% 2.08/1.47
% 2.08/1.47 % (25054)Memory used [KB]: 6012
% 2.08/1.47 % (25054)Time elapsed: 0.040 s
% 2.08/1.47 % (25054)Instructions burned: 63 (million)
% 2.08/1.47 % (25054)------------------------------
% 2.08/1.47 % (25054)------------------------------
% 2.08/1.47 % (25053)Success in time 0.059 s
%------------------------------------------------------------------------------