%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : NUM924^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 : n017.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:03 AM UTC 2026
% Result : Theorem 2.03s 1.46s
% Output : Refutation 2.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 61 ( 61 unt; 0 typ; 0 def)
% Number of atoms : 151 ( 75 equ; 0 cnn)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 520 ( 6 ~; 0 |; 0 &; 498 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 25 usr; 11 con; 0-2 aty)
% ( 16 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 56 ( 22 ^; 34 !; 0 ?; 56 :)
% 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,
zero_zero_int: int ).
thf(func_def_9,type,
zero_zero_nat: nat ).
thf(func_def_10,type,
zprime: int > $o ).
thf(func_def_11,type,
bit0: int > int ).
thf(func_def_12,type,
bit1: int > int ).
thf(func_def_13,type,
pls: int ).
thf(func_def_14,type,
number_number_of_int: int > int ).
thf(func_def_15,type,
number_number_of_nat: int > nat ).
thf(func_def_16,type,
ord_less_int: int > int > $o ).
thf(func_def_17,type,
ord_less_nat: nat > nat > $o ).
thf(func_def_18,type,
ord_less_eq_int: int > int > $o ).
thf(func_def_19,type,
ord_less_eq_nat: nat > nat > $o ).
thf(func_def_20,type,
power_power_int: int > nat > int ).
thf(func_def_21,type,
power_power_nat: nat > nat > nat ).
thf(func_def_22,type,
twoSqu1013291560sum2sq: int > $o ).
thf(func_def_23,type,
m: int ).
thf(func_def_24,type,
s: int ).
thf(func_def_25,type,
t: int ).
thf(func_def_42,type,
ph1:
!>[X0: $tType] : X0 ).
thf(f913,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f912]) ).
thf(f912,plain,
$false = $true,
inference(forward_demodulation,[status(thm)],[f911,f738]) ).
thf(f738,plain,
( $false
= ( ord_less_int @ ( plus_plus_int @ one_one_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ pls ) ),
inference(backward_demodulation,[status(thm)],[f498,f735]) ).
thf(f735,plain,
! [X2: int,X1: int] :
( ( plus_plus_int @ X1 @ X2 )
= ( plus_plus_int @ X2 @ X1 ) ),
inference(equality_proxy_clausification,[status(thm)],[f707]) ).
thf(f707,plain,
! [X2: int,X1: int] :
( $true
= ( ( plus_plus_int @ X2 @ X1 )
= ( plus_plus_int @ X1 @ X2 ) ) ),
inference(beta_eta_normalization,[status(thm)],[f706]) ).
thf(f706,plain,
! [X2: int,X1: int] :
( $true
= ( ^ [Y0: int] :
( ( plus_plus_int @ Y0 @ X1 )
= ( plus_plus_int @ X1 @ Y0 ) )
@ X2 ) ),
inference(pi_clausification,[status(thm)],[f678]) ).
thf(f678,plain,
! [X1: int] :
( $true
= ( !! @ int
@ ^ [Y0: int] :
( ( plus_plus_int @ Y0 @ X1 )
= ( plus_plus_int @ X1 @ Y0 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f677]) ).
thf(f677,plain,
! [X1: int] :
( $true
= ( ^ [Y0: int] :
( !! @ int
@ ^ [Y1: int] :
( ( plus_plus_int @ Y1 @ Y0 )
= ( plus_plus_int @ Y0 @ Y1 ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f387]) ).
thf(f387,plain,
( $true
= ( !! @ int
@ ^ [Y0: int] :
( !! @ int
@ ^ [Y1: int] :
( ( plus_plus_int @ Y1 @ Y0 )
= ( plus_plus_int @ Y0 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
thf(f196,plain,
( $true
= ( !! @ int
@ ^ [Y0: int] :
( !! @ int
@ ^ [Y1: int] :
( ( plus_plus_int @ Y1 @ Y0 )
= ( plus_plus_int @ Y0 @ Y1 ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f195]) ).
thf(f195,plain,
! [X0: int,X1: int] :
( ( plus_plus_int @ X0 @ X1 )
= ( plus_plus_int @ X1 @ X0 ) ),
inference(rectify,[status(thm)],[f105]) ).
thf(f105,axiom,
! [X12: int,X14: int] :
( ( plus_plus_int @ X12 @ X14 )
= ( plus_plus_int @ X14 @ X12 ) ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_104_zadd__commute) ).
thf(f498,plain,
( $false
= ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ pls ) ),
inference(not_proxy_clausification,[status(thm)],[f468]) ).
thf(f468,plain,
( $true
= ( ~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ pls ) ) ),
inference(backward_demodulation,[status(thm)],[f425,f465]) ).
thf(f465,plain,
! [X1: int] :
( ( number_number_of_int @ X1 )
= X1 ),
inference(equality_proxy_clausification,[status(thm)],[f464]) ).
thf(f464,plain,
! [X1: int] :
( $true
= ( ( number_number_of_int @ X1 )
= X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f463]) ).
thf(f463,plain,
! [X1: int] :
( $true
= ( ^ [Y0: int] :
( ( number_number_of_int @ Y0 )
= Y0 )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f412]) ).
thf(f412,plain,
( ( !! @ int
@ ^ [Y0: int] :
( ( number_number_of_int @ Y0 )
= Y0 ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f153]) ).
thf(f153,plain,
( ( !! @ int
@ ^ [Y0: int] :
( ( number_number_of_int @ Y0 )
= Y0 ) )
= $true ),
inference(fool_elimination,[status(thm)],[f152]) ).
thf(f152,plain,
! [X0: int] :
( ( number_number_of_int @ X0 )
= X0 ),
inference(rectify,[status(thm)],[f25]) ).
thf(f25,axiom,
! [X13: int] :
( ( number_number_of_int @ X13 )
= X13 ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_24_number__of__is__id) ).
thf(f425,plain,
( $true
= ( ~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ ( number_number_of_int @ pls ) ) ) ),
inference(definition_unfolding,[status(thm)],[f349,f378]) ).
thf(f378,plain,
( zero_zero_int
= ( number_number_of_int @ pls ) ),
inference(cnf_transformation,[status(thm)],[f299]) ).
thf(f299,plain,
( zero_zero_int
= ( number_number_of_int @ pls ) ),
inference(fool_elimination,[status(thm)],[f106]) ).
thf(f106,axiom,
( zero_zero_int
= ( number_number_of_int @ pls ) ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_105_zero__is__num__zero) ).
thf(f349,plain,
( ( ~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f145]) ).
thf(f145,plain,
( ( ~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int ) )
= $true ),
inference(fool_elimination,[status(thm)],[f144]) ).
thf(f144,plain,
~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int ),
inference(rectify,[status(thm)],[f108]) ).
thf(f108,negated_conjecture,
~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int ),
inference(negated_conjecture,[status(cth)],[f107]) ).
thf(f107,conjecture,
ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int,
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',conj_0) ).
thf(f911,plain,
( $true
= ( ord_less_int @ ( plus_plus_int @ one_one_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ pls ) ),
inference(forward_demodulation,[status(thm)],[f906,f481]) ).
thf(f481,plain,
! [X1: int] :
( pls
= ( times_times_int @ pls @ X1 ) ),
inference(equality_proxy_clausification,[status(thm)],[f480]) ).
thf(f480,plain,
! [X1: int] :
( ( pls
= ( times_times_int @ pls @ X1 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f479]) ).
thf(f479,plain,
! [X1: int] :
( $true
= ( ^ [Y0: int] :
( pls
= ( times_times_int @ pls @ Y0 ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f380]) ).
thf(f380,plain,
( $true
= ( !! @ int
@ ^ [Y0: int] :
( pls
= ( times_times_int @ pls @ Y0 ) ) ) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
thf(f218,plain,
( $true
= ( !! @ int
@ ^ [Y0: int] :
( pls
= ( times_times_int @ pls @ Y0 ) ) ) ),
inference(fool_elimination,[status(thm)],[f217]) ).
thf(f217,plain,
! [X0: int] :
( pls
= ( times_times_int @ pls @ X0 ) ),
inference(rectify,[status(thm)],[f67]) ).
thf(f67,axiom,
! [X12: int] :
( pls
= ( times_times_int @ pls @ X12 ) ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_66_mult__Pls) ).
thf(f906,plain,
( ( ord_less_int @ ( plus_plus_int @ one_one_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_int @ pls @ ( plus_plus_int @ one_one_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) ) ) )
= $true ),
inference(backward_demodulation,[status(thm)],[f747,f895]) ).
thf(f895,plain,
! [X2: int,X1: int] :
( ( times_times_int @ X1 @ X2 )
= ( times_times_int @ X2 @ X1 ) ),
inference(equality_proxy_clausification,[status(thm)],[f894]) ).
thf(f894,plain,
! [X2: int,X1: int] :
( $true
= ( ( times_times_int @ X1 @ X2 )
= ( times_times_int @ X2 @ X1 ) ) ),
inference(beta_eta_normalization,[status(thm)],[f893]) ).
thf(f893,plain,
! [X2: int,X1: int] :
( $true
= ( ^ [Y0: int] :
( ( times_times_int @ X1 @ Y0 )
= ( times_times_int @ Y0 @ X1 ) )
@ X2 ) ),
inference(pi_clausification,[status(thm)],[f878]) ).
thf(f878,plain,
! [X1: int] :
( $true
= ( !! @ int
@ ^ [Y0: int] :
( ( times_times_int @ X1 @ Y0 )
= ( times_times_int @ Y0 @ X1 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f877]) ).
thf(f877,plain,
! [X1: int] :
( $true
= ( ^ [Y0: int] :
( !! @ int
@ ^ [Y1: int] :
( ( times_times_int @ Y0 @ Y1 )
= ( times_times_int @ Y1 @ Y0 ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f409]) ).
thf(f409,plain,
( $true
= ( !! @ int
@ ^ [Y0: int] :
( !! @ int
@ ^ [Y1: int] :
( ( times_times_int @ Y0 @ Y1 )
= ( times_times_int @ Y1 @ Y0 ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
thf(f178,plain,
( $true
= ( !! @ int
@ ^ [Y0: int] :
( !! @ int
@ ^ [Y1: int] :
( ( times_times_int @ Y0 @ Y1 )
= ( times_times_int @ Y1 @ Y0 ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f177]) ).
thf(f177,plain,
! [X0: int,X1: int] :
( ( times_times_int @ X1 @ X0 )
= ( times_times_int @ X0 @ X1 ) ),
inference(rectify,[status(thm)],[f26]) ).
thf(f26,axiom,
! [X12: int,X14: int] :
( ( times_times_int @ X14 @ X12 )
= ( times_times_int @ X12 @ X14 ) ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_25_zmult__commute) ).
thf(f747,plain,
( $true
= ( ord_less_int @ ( plus_plus_int @ one_one_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_int @ ( plus_plus_int @ one_one_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) ) @ pls ) ) ),
inference(forward_demodulation,[status(thm)],[f739,f735]) ).
thf(f739,plain,
( $true
= ( ord_less_int @ ( plus_plus_int @ one_one_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) @ pls ) ) ),
inference(backward_demodulation,[status(thm)],[f478,f735]) ).
thf(f478,plain,
( $true
= ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) @ pls ) ) ),
inference(forward_demodulation,[status(thm)],[f467,f465]) ).
thf(f467,plain,
( $true
= ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ pls ) ) ),
inference(backward_demodulation,[status(thm)],[f448,f465]) ).
thf(f448,plain,
( ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ ( number_number_of_int @ pls ) ) )
= $true ),
inference(backward_demodulation,[status(thm)],[f431,f351]) ).
thf(f351,plain,
( ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t )
= ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
thf(f172,plain,
( ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t )
= ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,axiom,
( ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t )
= ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_3_t) ).
thf(f431,plain,
( ( ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ ( number_number_of_int @ pls ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f376,f378]) ).
thf(f376,plain,
( ( ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ zero_zero_int ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f214]) ).
thf(f214,plain,
( ( ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ zero_zero_int ) )
= $true ),
inference(fool_elimination,[status(thm)],[f213]) ).
thf(f213,plain,
ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ zero_zero_int ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ zero_zero_int ),
file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM924^1 : TPTP v9.2.1. Released v5.3.0.
% 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.34 % Computer : n017.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue Feb 24 11:15:56 EST 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.20/0.47 ---- Original DTF file ---
% 0.20/0.47 thf(spec,logic,$$dhol).
% 0.20/0.47 %------------------------------------------------------------------------------
% 0.20/0.47 % File : NUM924^1 : TPTP v9.2.1. Released v5.3.0.
% 0.20/0.47 % Domain : Number Theory
% 0.20/0.47 % Problem : Sum of two squares line 102, 100 axioms selected
% 0.20/0.47 % Version : Especial.
% 0.20/0.47 % English :
% 0.20/0.47
% 0.20/0.47 % Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day
% 0.20/0.47 % : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe
% 0.20/0.47 % Source : [Bla11]
% 0.20/0.47 % Names : s2s_100_thf_l102 [Bla11]
% 0.20/0.47
% 0.20/0.47 % Status : ContradictoryAxioms
% 0.20/0.47 % Rating : 0.22 v9.1.0, 0.25 v9.0.0, 0.30 v8.2.0, 0.31 v8.1.0, 0.27 v7.5.0, 0.14 v7.4.0, 0.33 v7.2.0, 0.25 v7.1.0, 0.50 v7.0.0, 0.57 v6.4.0, 0.67 v6.3.0, 0.60 v6.2.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.60 v5.3.0
% 0.20/0.47 % Syntax : Number of formulae : 133 ( 50 unt; 26 typ; 0 def)
% 0.20/0.47 % Number of atoms : 184 ( 73 equ; 0 cnn)
% 0.20/0.47 % Maximal formula atoms : 7 ( 1 avg)
% 0.20/0.47 % Number of connectives : 814 ( 13 ~; 4 |; 7 &; 724 @)
% 0.20/0.47 % ( 43 <=>; 23 =>; 0 <=; 0 <~>)
% 0.20/0.47 % Maximal formula depth : 13 ( 5 avg)
% 0.20/0.47 % Number of types : 3 ( 2 usr)
% 0.20/0.47 % Number of type conns : 26 ( 26 >; 0 *; 0 +; 0 <<)
% 0.20/0.47 % Number of symbols : 25 ( 24 usr; 8 con; 0-2 aty)
% 0.20/0.47 % Number of variables : 160 ( 0 ^; 160 !; 0 ?; 160 :)
% 0.20/0.47 % SPC : TH0_THM_EQU_NAR
% 0.20/0.47
% 0.20/0.47 % Comments : This file was generated by Isabelle (most likely Sledgehammer)
% 0.20/0.47 % 2011-08-09 19:06:31
% 0.20/0.47 %------------------------------------------------------------------------------
% 0.20/0.47 %----Should-be-implicit typings (2)
% 0.20/0.47 thf(ty_ty_tc__Int__Oint,type,
% 0.20/0.47 int: $tType ).
% 0.20/0.47
% 0.20/0.47 thf(ty_ty_tc__Nat__Onat,type,
% 0.20/0.47 nat: $tType ).
% 0.20/0.47
% 0.20/0.47 %----Explicit typings (24)
% 0.20/0.47 thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,
% 0.20/0.47 one_one_int: int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,
% 0.20/0.47 one_one_nat: nat ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,
% 0.20/0.47 plus_plus_int: int > int > int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,
% 0.20/0.47 plus_plus_nat: nat > nat > nat ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Int__Oint,type,
% 0.20/0.47 times_times_int: int > int > int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Nat__Onat,type,
% 0.20/0.47 times_times_nat: nat > nat > nat ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Int__Oint,type,
% 0.20/0.47 zero_zero_int: int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Nat__Onat,type,
% 0.20/0.47 zero_zero_nat: nat ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_IntPrimes_Ozprime,type,
% 0.20/0.47 zprime: int > $o ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Int_OBit0,type,
% 0.20/0.47 bit0: int > int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Int_OBit1,type,
% 0.20/0.47 bit1: int > int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Int_OPls,type,
% 0.20/0.47 pls: int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,
% 0.20/0.47 number_number_of_int: int > int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,
% 0.20/0.47 number_number_of_nat: int > nat ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,
% 0.20/0.47 ord_less_int: int > int > $o ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,
% 0.20/0.47 ord_less_nat: nat > nat > $o ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Int__Oint,type,
% 0.20/0.47 ord_less_eq_int: int > int > $o ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Nat__Onat,type,
% 0.20/0.47 ord_less_eq_nat: nat > nat > $o ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,
% 0.20/0.47 power_power_int: int > nat > int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,
% 0.20/0.47 power_power_nat: nat > nat > nat ).
% 0.20/0.47
% 0.20/0.47 thf(sy_c_TwoSquares__Mirabelle__fqdbopfjxb_Ois__sum2sq,type,
% 0.20/0.47 twoSqu1013291560sum2sq: int > $o ).
% 0.20/0.47
% 0.20/0.47 thf(sy_v_m,type,
% 0.20/0.47 m: int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_v_s____,type,
% 0.20/0.47 s: int ).
% 0.20/0.47
% 0.20/0.47 thf(sy_v_t____,type,
% 0.20/0.47 t: int ).
% 0.20/0.47
% 0.20/0.47 %----Relevant facts (106)
% 0.20/0.47 thf(fact_0__096t_A_060_A0_096,axiom,
% 0.20/0.47 ord_less_int @ t @ zero_zero_int ).
% 0.20/0.47
% 0.20/0.47 thf(fact_1_calculation_I1_J,axiom,
% 0.20/0.47 ord_less_int @ t @ one_one_int ).
% 0.20/0.47
% 0.20/0.47 thf(fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096,axiom,
% 0.20/0.47 ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ zero_zero_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_3_t,axiom,
% 0.20/0.47 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 0.20/0.47 = ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_4_calculation_I2_J,axiom,
% 0.20/0.47 ( ( t = zero_zero_int )
% 0.20/0.47 => ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 0.20/0.47 = zero_zero_int ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_5__096_126_A1_A_060_061_At_096,axiom,
% 0.20/0.47 ~ ( ord_less_eq_int @ one_one_int @ t ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_6_p0,axiom,
% 0.20/0.47 ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_7_not__sum__power2__lt__zero,axiom,
% 0.20/0.47 ! [X: int,Y: int] :
% 0.20/0.47 ~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ X @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ zero_zero_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_8_sum__power2__gt__zero__iff,axiom,
% 0.20/0.47 ! [X_10: int,Y_9: int] :
% 0.20/0.47 ( ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( power_power_int @ X_10 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_9 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
% 0.20/0.47 <=> ( ( X_10 != zero_zero_int )
% 0.20/0.47 | ( Y_9 != zero_zero_int ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_9_sum__power2__eq__zero__iff,axiom,
% 0.20/0.47 ! [X_9: int,Y_8: int] :
% 0.20/0.47 ( ( ( plus_plus_int @ ( power_power_int @ X_9 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.20/0.47 = zero_zero_int )
% 0.20/0.47 <=> ( ( X_9 = zero_zero_int )
% 0.20/0.47 & ( Y_8 = zero_zero_int ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_10_power2__less__0,axiom,
% 0.20/0.47 ! [A_3: int] :
% 0.20/0.47 ~ ( ord_less_int @ ( power_power_int @ A_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ zero_zero_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_11_zero__less__power2,axiom,
% 0.20/0.47 ! [A_2: int] :
% 0.20/0.47 ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ A_2 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 0.20/0.47 <=> ( A_2 != zero_zero_int ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_12_one__power2,axiom,
% 0.20/0.47 ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.20/0.47 = one_one_nat ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_13_one__power2,axiom,
% 0.20/0.47 ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.20/0.47 = one_one_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_14_zero__power2,axiom,
% 0.20/0.47 ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.20/0.47 = zero_zero_nat ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_15_zero__power2,axiom,
% 0.20/0.47 ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.20/0.47 = zero_zero_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_16_zero__eq__power2,axiom,
% 0.20/0.47 ! [A_1: int] :
% 0.20/0.47 ( ( ( power_power_int @ A_1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 0.20/0.47 = zero_zero_int )
% 0.20/0.47 <=> ( A_1 = zero_zero_int ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_17_add__special_I2_J,axiom,
% 0.20/0.47 ! [W_7: int] :
% 0.20/0.47 ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_7 ) )
% 0.20/0.47 = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_7 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_18_add__special_I3_J,axiom,
% 0.20/0.47 ! [V_12: int] :
% 0.20/0.47 ( ( plus_plus_int @ ( number_number_of_int @ V_12 ) @ one_one_int )
% 0.20/0.47 = ( number_number_of_int @ ( plus_plus_int @ V_12 @ ( bit1 @ pls ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_19_t__l__p,axiom,
% 0.20/0.47 ord_less_int @ t @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_20__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.20/0.47 ~ ! [T: int] :
% 0.20/0.47 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 0.20/0.47 != ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ T ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_21_p,axiom,
% 0.20/0.47 zprime @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_22_qf1pt,axiom,
% 0.20/0.47 twoSqu1013291560sum2sq @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_23_zle__refl,axiom,
% 0.20/0.47 ! [W: int] : ( ord_less_eq_int @ W @ W ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_24_number__of__is__id,axiom,
% 0.20/0.47 ! [K: int] :
% 0.20/0.47 ( ( number_number_of_int @ K )
% 0.20/0.47 = K ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_25_zmult__commute,axiom,
% 0.20/0.47 ! [Z: int,W: int] :
% 0.20/0.47 ( ( times_times_int @ Z @ W )
% 0.20/0.47 = ( times_times_int @ W @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_26_zle__linear,axiom,
% 0.20/0.47 ! [Z: int,W: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ Z @ W )
% 0.20/0.47 | ( ord_less_eq_int @ W @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_27_times__numeral__code_I5_J,axiom,
% 0.20/0.47 ! [V_2: int,W: int] :
% 0.20/0.47 ( ( times_times_int @ ( number_number_of_int @ V_2 ) @ ( number_number_of_int @ W ) )
% 0.20/0.47 = ( number_number_of_int @ ( times_times_int @ V_2 @ W ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_28_less__eq__number__of__int__code,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_29_le__number__of,axiom,
% 0.20/0.47 ! [X_8: int,Y_7: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( number_number_of_int @ X_8 ) @ ( number_number_of_int @ Y_7 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ X_8 @ Y_7 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_30_zmult__assoc,axiom,
% 0.20/0.47 ! [Z1: int,Z2: int,Z3: int] :
% 0.20/0.47 ( ( times_times_int @ ( times_times_int @ Z1 @ Z2 ) @ Z3 )
% 0.20/0.47 = ( times_times_int @ Z1 @ ( times_times_int @ Z2 @ Z3 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_31_zle__trans,axiom,
% 0.20/0.47 ! [K: int,I: int,J: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ I @ J )
% 0.20/0.47 => ( ( ord_less_eq_int @ J @ K )
% 0.20/0.47 => ( ord_less_eq_int @ I @ K ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_32_zle__antisym,axiom,
% 0.20/0.47 ! [Z: int,W: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ Z @ W )
% 0.20/0.47 => ( ( ord_less_eq_int @ W @ Z )
% 0.20/0.47 => ( Z = W ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_33_zpower__zadd__distrib,axiom,
% 0.20/0.47 ! [X: int,Y: nat,Z: nat] :
% 0.20/0.47 ( ( power_power_int @ X @ ( plus_plus_nat @ Y @ Z ) )
% 0.20/0.47 = ( times_times_int @ ( power_power_int @ X @ Y ) @ ( power_power_int @ X @ Z ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_34_less__eq__int__code_I16_J,axiom,
% 0.20/0.47 ! [K1: int,K2: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_35_rel__simps_I34_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_36_rel__simps_I19_J,axiom,
% 0.20/0.47 ord_less_eq_int @ pls @ pls ).
% 0.20/0.47
% 0.20/0.47 thf(fact_37_less__eq__int__code_I13_J,axiom,
% 0.20/0.47 ! [K1: int,K2: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_38_rel__simps_I31_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_39_zless__le,axiom,
% 0.20/0.47 ! [Z: int,W: int] :
% 0.20/0.47 ( ( ord_less_int @ Z @ W )
% 0.20/0.47 <=> ( ( ord_less_eq_int @ Z @ W )
% 0.20/0.47 & ( Z != W ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_40_zadd__left__mono,axiom,
% 0.20/0.47 ! [K: int,I: int,J: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ I @ J )
% 0.20/0.47 => ( ord_less_eq_int @ ( plus_plus_int @ K @ I ) @ ( plus_plus_int @ K @ J ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_41_eq__number__of__0,axiom,
% 0.20/0.47 ! [V_2: int] :
% 0.20/0.47 ( ( ( number_number_of_nat @ V_2 )
% 0.20/0.47 = zero_zero_nat )
% 0.20/0.47 <=> ( ord_less_eq_int @ V_2 @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_42_eq__0__number__of,axiom,
% 0.20/0.47 ! [V_2: int] :
% 0.20/0.47 ( ( zero_zero_nat
% 0.20/0.47 = ( number_number_of_nat @ V_2 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ V_2 @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_43_semiring__mult__number__of,axiom,
% 0.20/0.47 ! [V_11: int,V_10: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ pls @ V_10 )
% 0.20/0.47 => ( ( ord_less_eq_int @ pls @ V_11 )
% 0.20/0.47 => ( ( times_times_nat @ ( number_number_of_nat @ V_10 ) @ ( number_number_of_nat @ V_11 ) )
% 0.20/0.47 = ( number_number_of_nat @ ( times_times_int @ V_10 @ V_11 ) ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_44_semiring__mult__number__of,axiom,
% 0.20/0.47 ! [V_11: int,V_10: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ pls @ V_10 )
% 0.20/0.47 => ( ( ord_less_eq_int @ pls @ V_11 )
% 0.20/0.47 => ( ( times_times_int @ ( number_number_of_int @ V_10 ) @ ( number_number_of_int @ V_11 ) )
% 0.20/0.47 = ( number_number_of_int @ ( times_times_int @ V_10 @ V_11 ) ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_45_mult__number__of__left,axiom,
% 0.20/0.47 ! [V_9: int,W_6: int,Z_2: int] :
% 0.20/0.47 ( ( times_times_int @ ( number_number_of_int @ V_9 ) @ ( times_times_int @ ( number_number_of_int @ W_6 ) @ Z_2 ) )
% 0.20/0.47 = ( times_times_int @ ( number_number_of_int @ ( times_times_int @ V_9 @ W_6 ) ) @ Z_2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_46_arith__simps_I32_J,axiom,
% 0.20/0.47 ! [V_8: int,W_5: int] :
% 0.20/0.47 ( ( times_times_int @ ( number_number_of_int @ V_8 ) @ ( number_number_of_int @ W_5 ) )
% 0.20/0.47 = ( number_number_of_int @ ( times_times_int @ V_8 @ W_5 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_47_number__of__mult,axiom,
% 0.20/0.47 ! [V_7: int,W_4: int] :
% 0.20/0.47 ( ( number_number_of_int @ ( times_times_int @ V_7 @ W_4 ) )
% 0.20/0.47 = ( times_times_int @ ( number_number_of_int @ V_7 ) @ ( number_number_of_int @ W_4 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_48_sum__squares__le__zero__iff,axiom,
% 0.20/0.47 ! [X_7: int,Y_6: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( plus_plus_int @ ( times_times_int @ X_7 @ X_7 ) @ ( times_times_int @ Y_6 @ Y_6 ) ) @ zero_zero_int )
% 0.20/0.47 <=> ( ( X_7 = zero_zero_int )
% 0.20/0.47 & ( Y_6 = zero_zero_int ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_49_sum__squares__ge__zero,axiom,
% 0.20/0.47 ! [X_6: int,Y_5: int] : ( ord_less_eq_int @ zero_zero_int @ ( plus_plus_int @ ( times_times_int @ X_6 @ X_6 ) @ ( times_times_int @ Y_5 @ Y_5 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_50_le__special_I3_J,axiom,
% 0.20/0.47 ! [X_5: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( number_number_of_int @ X_5 ) @ zero_zero_int )
% 0.20/0.47 <=> ( ord_less_eq_int @ X_5 @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_51_le__special_I1_J,axiom,
% 0.20/0.47 ! [Y_4: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ zero_zero_int @ ( number_number_of_int @ Y_4 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ pls @ Y_4 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_52_less__0__number__of,axiom,
% 0.20/0.47 ! [V_2: int] :
% 0.20/0.47 ( ( ord_less_nat @ zero_zero_nat @ ( number_number_of_nat @ V_2 ) )
% 0.20/0.47 <=> ( ord_less_int @ pls @ V_2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_53_le__number__of__eq__not__less,axiom,
% 0.20/0.47 ! [V_6: int,W_3: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( number_number_of_int @ V_6 ) @ ( number_number_of_int @ W_3 ) )
% 0.20/0.47 <=> ~ ( ord_less_int @ ( number_number_of_int @ W_3 ) @ ( number_number_of_int @ V_6 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_54_le__number__of__eq__not__less,axiom,
% 0.20/0.47 ! [V_6: int,W_3: int] :
% 0.20/0.47 ( ( ord_less_eq_nat @ ( number_number_of_nat @ V_6 ) @ ( number_number_of_nat @ W_3 ) )
% 0.20/0.47 <=> ~ ( ord_less_nat @ ( number_number_of_nat @ W_3 ) @ ( number_number_of_nat @ V_6 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_55_rel__simps_I22_J,axiom,
% 0.20/0.47 ! [K: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ pls @ ( bit1 @ K ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_56_less__eq__int__code_I14_J,axiom,
% 0.20/0.47 ! [K1: int,K2: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_57_rel__simps_I32_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_58_rel__simps_I27_J,axiom,
% 0.20/0.47 ! [K: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit0 @ K ) @ pls )
% 0.20/0.47 <=> ( ord_less_eq_int @ K @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_59_rel__simps_I21_J,axiom,
% 0.20/0.47 ! [K: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ pls @ ( bit0 @ K ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_60_zadd__zless__mono,axiom,
% 0.20/0.47 ! [Z_1: int,Z: int,W_2: int,W: int] :
% 0.20/0.47 ( ( ord_less_int @ W_2 @ W )
% 0.20/0.47 => ( ( ord_less_eq_int @ Z_1 @ Z )
% 0.20/0.47 => ( ord_less_int @ ( plus_plus_int @ W_2 @ Z_1 ) @ ( plus_plus_int @ W @ Z ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_61_nat__number__of__Pls,axiom,
% 0.20/0.47 ( ( number_number_of_nat @ pls )
% 0.20/0.47 = zero_zero_nat ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_62_semiring__norm_I113_J,axiom,
% 0.20/0.47 ( zero_zero_nat
% 0.20/0.47 = ( number_number_of_nat @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_63_le__special_I4_J,axiom,
% 0.20/0.47 ! [X_4: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( number_number_of_int @ X_4 ) @ one_one_int )
% 0.20/0.47 <=> ( ord_less_eq_int @ X_4 @ ( bit1 @ pls ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_64_le__special_I2_J,axiom,
% 0.20/0.47 ! [Y_3: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ one_one_int @ ( number_number_of_int @ Y_3 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ ( bit1 @ pls ) @ Y_3 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_65_nat__1__add__1,axiom,
% 0.20/0.47 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 0.20/0.47 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_66_mult__Pls,axiom,
% 0.20/0.47 ! [W: int] :
% 0.20/0.47 ( ( times_times_int @ pls @ W )
% 0.20/0.47 = pls ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_67_mult__Bit0,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( times_times_int @ ( bit0 @ K ) @ L )
% 0.20/0.47 = ( bit0 @ ( times_times_int @ K @ L ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_68_less__number__of__int__code,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 0.20/0.47 <=> ( ord_less_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_69_zmult__1__right,axiom,
% 0.20/0.47 ! [Z: int] :
% 0.20/0.47 ( ( times_times_int @ Z @ one_one_int )
% 0.20/0.47 = Z ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_70_zmult__1,axiom,
% 0.20/0.47 ! [Z: int] :
% 0.20/0.47 ( ( times_times_int @ one_one_int @ Z )
% 0.20/0.47 = Z ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_71_plus__numeral__code_I9_J,axiom,
% 0.20/0.47 ! [V_2: int,W: int] :
% 0.20/0.47 ( ( plus_plus_int @ ( number_number_of_int @ V_2 ) @ ( number_number_of_int @ W ) )
% 0.20/0.47 = ( number_number_of_int @ ( plus_plus_int @ V_2 @ W ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_72_zadd__zmult__distrib,axiom,
% 0.20/0.47 ! [Z1: int,Z2: int,W: int] :
% 0.20/0.47 ( ( times_times_int @ ( plus_plus_int @ Z1 @ Z2 ) @ W )
% 0.20/0.47 = ( plus_plus_int @ ( times_times_int @ Z1 @ W ) @ ( times_times_int @ Z2 @ W ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_73_zadd__zmult__distrib2,axiom,
% 0.20/0.47 ! [W: int,Z1: int,Z2: int] :
% 0.20/0.47 ( ( times_times_int @ W @ ( plus_plus_int @ Z1 @ Z2 ) )
% 0.20/0.47 = ( plus_plus_int @ ( times_times_int @ W @ Z1 ) @ ( times_times_int @ W @ Z2 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_74_rel__simps_I29_J,axiom,
% 0.20/0.47 ! [K: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit1 @ K ) @ pls )
% 0.20/0.47 <=> ( ord_less_int @ K @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_75_rel__simps_I5_J,axiom,
% 0.20/0.47 ! [K: int] :
% 0.20/0.47 ( ( ord_less_int @ pls @ ( bit1 @ K ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_76_less__eq__int__code_I15_J,axiom,
% 0.20/0.47 ! [K1: int,K2: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 0.20/0.47 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_77_rel__simps_I33_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 0.20/0.47 <=> ( ord_less_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_78_less__int__code_I14_J,axiom,
% 0.20/0.47 ! [K1: int,K2: int] :
% 0.20/0.47 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_79_rel__simps_I15_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_80_less__nat__number__of,axiom,
% 0.20/0.47 ! [V_2: int,V_3: int] :
% 0.20/0.47 ( ( ord_less_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 0.20/0.47 <=> ( ( ( ord_less_int @ V_2 @ V_3 )
% 0.20/0.47 => ( ord_less_int @ pls @ V_3 ) )
% 0.20/0.47 & ( ord_less_int @ V_2 @ V_3 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_81_int__one__le__iff__zero__less,axiom,
% 0.20/0.47 ! [Z: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ one_one_int @ Z )
% 0.20/0.47 <=> ( ord_less_int @ zero_zero_int @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_82_nat__numeral__1__eq__1,axiom,
% 0.20/0.47 ( ( number_number_of_nat @ ( bit1 @ pls ) )
% 0.20/0.47 = one_one_nat ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_83_Numeral1__eq1__nat,axiom,
% 0.20/0.47 ( one_one_nat
% 0.20/0.47 = ( number_number_of_nat @ ( bit1 @ pls ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_84_zless__imp__add1__zle,axiom,
% 0.20/0.47 ! [W: int,Z: int] :
% 0.20/0.47 ( ( ord_less_int @ W @ Z )
% 0.20/0.47 => ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_85_add1__zle__eq,axiom,
% 0.20/0.47 ! [W: int,Z: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z )
% 0.20/0.47 <=> ( ord_less_int @ W @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_86_zle__add1__eq__le,axiom,
% 0.20/0.47 ! [W: int,Z: int] :
% 0.20/0.47 ( ( ord_less_int @ W @ ( plus_plus_int @ Z @ one_one_int ) )
% 0.20/0.47 <=> ( ord_less_eq_int @ W @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_87_semiring__add__number__of,axiom,
% 0.20/0.47 ! [V_5: int,V_4: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ pls @ V_4 )
% 0.20/0.47 => ( ( ord_less_eq_int @ pls @ V_5 )
% 0.20/0.47 => ( ( plus_plus_int @ ( number_number_of_int @ V_4 ) @ ( number_number_of_int @ V_5 ) )
% 0.20/0.47 = ( number_number_of_int @ ( plus_plus_int @ V_4 @ V_5 ) ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_88_semiring__add__number__of,axiom,
% 0.20/0.47 ! [V_5: int,V_4: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ pls @ V_4 )
% 0.20/0.47 => ( ( ord_less_eq_int @ pls @ V_5 )
% 0.20/0.47 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_4 ) @ ( number_number_of_nat @ V_5 ) )
% 0.20/0.47 = ( number_number_of_nat @ ( plus_plus_int @ V_4 @ V_5 ) ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_89_add__nat__number__of,axiom,
% 0.20/0.47 ! [V_3: int,V_2: int] :
% 0.20/0.47 ( ( ( ord_less_int @ V_2 @ pls )
% 0.20/0.47 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 0.20/0.47 = ( number_number_of_nat @ V_3 ) ) )
% 0.20/0.47 & ( ~ ( ord_less_int @ V_2 @ pls )
% 0.20/0.47 => ( ( ( ord_less_int @ V_3 @ pls )
% 0.20/0.47 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 0.20/0.47 = ( number_number_of_nat @ V_2 ) ) )
% 0.20/0.47 & ( ~ ( ord_less_int @ V_3 @ pls )
% 0.20/0.47 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 0.20/0.47 = ( number_number_of_nat @ ( plus_plus_int @ V_2 @ V_3 ) ) ) ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_90_le__imp__0__less,axiom,
% 0.20/0.47 ! [Z: int] :
% 0.20/0.47 ( ( ord_less_eq_int @ zero_zero_int @ Z )
% 0.20/0.47 => ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ one_one_int @ Z ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_91_eq__number__of,axiom,
% 0.20/0.47 ! [X_3: int,Y_2: int] :
% 0.20/0.47 ( ( ( number_number_of_int @ X_3 )
% 0.20/0.47 = ( number_number_of_int @ Y_2 ) )
% 0.20/0.47 <=> ( X_3 = Y_2 ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_92_number__of__reorient,axiom,
% 0.20/0.47 ! [W_1: int,X_2: nat] :
% 0.20/0.47 ( ( ( number_number_of_nat @ W_1 )
% 0.20/0.47 = X_2 )
% 0.20/0.47 <=> ( X_2
% 0.20/0.47 = ( number_number_of_nat @ W_1 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_93_number__of__reorient,axiom,
% 0.20/0.47 ! [W_1: int,X_2: int] :
% 0.20/0.47 ( ( ( number_number_of_int @ W_1 )
% 0.20/0.47 = X_2 )
% 0.20/0.47 <=> ( X_2
% 0.20/0.47 = ( number_number_of_int @ W_1 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_94_rel__simps_I51_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ( bit1 @ K )
% 0.20/0.47 = ( bit1 @ L ) )
% 0.20/0.47 <=> ( K = L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_95_rel__simps_I48_J,axiom,
% 0.20/0.47 ! [K: int,L: int] :
% 0.20/0.47 ( ( ( bit0 @ K )
% 0.20/0.47 = ( bit0 @ L ) )
% 0.20/0.47 <=> ( K = L ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_96_zless__linear,axiom,
% 0.20/0.47 ! [X: int,Y: int] :
% 0.20/0.47 ( ( ord_less_int @ X @ Y )
% 0.20/0.47 | ( X = Y )
% 0.20/0.47 | ( ord_less_int @ Y @ X ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_97_sum__squares__eq__zero__iff,axiom,
% 0.20/0.47 ! [X_1: int,Y_1: int] :
% 0.20/0.47 ( ( ( plus_plus_int @ ( times_times_int @ X_1 @ X_1 ) @ ( times_times_int @ Y_1 @ Y_1 ) )
% 0.20/0.47 = zero_zero_int )
% 0.20/0.47 <=> ( ( X_1 = zero_zero_int )
% 0.20/0.47 & ( Y_1 = zero_zero_int ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_98_left__distrib__number__of,axiom,
% 0.20/0.47 ! [A: int,B_1: int,V_1: int] :
% 0.20/0.47 ( ( times_times_int @ ( plus_plus_int @ A @ B_1 ) @ ( number_number_of_int @ V_1 ) )
% 0.20/0.47 = ( plus_plus_int @ ( times_times_int @ A @ ( number_number_of_int @ V_1 ) ) @ ( times_times_int @ B_1 @ ( number_number_of_int @ V_1 ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_99_left__distrib__number__of,axiom,
% 0.20/0.47 ! [A: nat,B_1: nat,V_1: int] :
% 0.20/0.47 ( ( times_times_nat @ ( plus_plus_nat @ A @ B_1 ) @ ( number_number_of_nat @ V_1 ) )
% 0.20/0.47 = ( plus_plus_nat @ ( times_times_nat @ A @ ( number_number_of_nat @ V_1 ) ) @ ( times_times_nat @ B_1 @ ( number_number_of_nat @ V_1 ) ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_100_right__distrib__number__of,axiom,
% 0.20/0.47 ! [V: int,B: int,C: int] :
% 0.20/0.47 ( ( times_times_int @ ( number_number_of_int @ V ) @ ( plus_plus_int @ B @ C ) )
% 0.20/0.47 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ V ) @ B ) @ ( times_times_int @ ( number_number_of_int @ V ) @ C ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_101_right__distrib__number__of,axiom,
% 0.20/0.47 ! [V: int,B: nat,C: nat] :
% 0.20/0.47 ( ( times_times_nat @ ( number_number_of_nat @ V ) @ ( plus_plus_nat @ B @ C ) )
% 0.20/0.47 = ( plus_plus_nat @ ( times_times_nat @ ( number_number_of_nat @ V ) @ B ) @ ( times_times_nat @ ( number_number_of_nat @ V ) @ C ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_102_zadd__assoc,axiom,
% 0.20/0.47 ! [Z1: int,Z2: int,Z3: int] :
% 0.20/0.47 ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 )
% 0.20/0.47 = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_103_zadd__left__commute,axiom,
% 0.20/0.47 ! [X: int,Y: int,Z: int] :
% 0.20/0.47 ( ( plus_plus_int @ X @ ( plus_plus_int @ Y @ Z ) )
% 0.20/0.47 = ( plus_plus_int @ Y @ ( plus_plus_int @ X @ Z ) ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_104_zadd__commute,axiom,
% 0.20/0.47 ! [Z: int,W: int] :
% 0.20/0.47 ( ( plus_plus_int @ Z @ W )
% 0.20/0.47 = ( plus_plus_int @ W @ Z ) ) ).
% 0.20/0.47
% 0.20/0.47 thf(fact_105_zero__is__num__zero,axiom,
% 0.20/0.47 ( zero_zero_int
% 0.20/0.47 = ( number_number_of_int @ pls ) ) ).
% 0.20/0.47
% 0.20/0.47 %----Conjectures (1)
% 0.20/0.47 thf(conj_0,conjecture,
% 0.20/0.47 ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int ).
% 0.20/0.47
% 0.20/0.47 %------------------------------------------------------------------------------
% 0.20/0.47 ------------------------
% 1.88/1.35 ---- Embedded in THF ---
% 1.88/1.35 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.88/1.35 %%% Generated on Tue Feb 24 11:15:57 EST 2026
% 1.88/1.35 %%% using '$$dhol' embedding, version 1.3.0.
% 1.88/1.35 %%% Logic specification used:
% 1.88/1.35 %%% thf(spec, logic, $$dhol).
% 1.88/1.35
% 1.88/1.35 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2DTF30683.p
% See solution above
% 1.88/1.35 ------------------------
% 1.88/1.37 ---- Cleaned THF ---
% 1.88/1.37 thf(ty_ty_tc__Int__Oint,type,
% 1.88/1.37 int: $tType ).
% 1.88/1.37
% 1.88/1.37 thf(ty_ty_tc__Nat__Onat,type,
% 1.88/1.37 nat: $tType ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,
% 1.88/1.37 one_one_int: int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,
% 1.88/1.37 one_one_nat: nat ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,
% 1.88/1.37 plus_plus_int: int > int > int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,
% 1.88/1.37 plus_plus_nat: nat > nat > nat ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Int__Oint,type,
% 1.88/1.37 times_times_int: int > int > int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Otimes__class_Otimes_000tc__Nat__Onat,type,
% 1.88/1.37 times_times_nat: nat > nat > nat ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Int__Oint,type,
% 1.88/1.37 zero_zero_int: int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Groups_Ozero__class_Ozero_000tc__Nat__Onat,type,
% 1.88/1.37 zero_zero_nat: nat ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_IntPrimes_Ozprime,type,
% 1.88/1.37 zprime: int > $o ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Int_OBit0,type,
% 1.88/1.37 bit0: int > int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Int_OBit1,type,
% 1.88/1.37 bit1: int > int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Int_OPls,type,
% 1.88/1.37 pls: int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,
% 1.88/1.37 number_number_of_int: int > int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,
% 1.88/1.37 number_number_of_nat: int > nat ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,
% 1.88/1.37 ord_less_int: int > int > $o ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,
% 1.88/1.37 ord_less_nat: nat > nat > $o ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Int__Oint,type,
% 1.88/1.37 ord_less_eq_int: int > int > $o ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Nat__Onat,type,
% 1.88/1.37 ord_less_eq_nat: nat > nat > $o ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,
% 1.88/1.37 power_power_int: int > nat > int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,
% 1.88/1.37 power_power_nat: nat > nat > nat ).
% 1.88/1.37
% 1.88/1.37 thf(sy_c_TwoSquares__Mirabelle__fqdbopfjxb_Ois__sum2sq,type,
% 1.88/1.37 twoSqu1013291560sum2sq: int > $o ).
% 1.88/1.37
% 1.88/1.37 thf(sy_v_m,type,
% 1.88/1.37 m: int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_v_s____,type,
% 1.88/1.37 s: int ).
% 1.88/1.37
% 1.88/1.37 thf(sy_v_t____,type,
% 1.88/1.37 t: int ).
% 1.88/1.37
% 1.88/1.37 thf(fact_0__096t_A_060_A0_096,axiom,
% 1.88/1.37 ord_less_int @ t @ zero_zero_int ).
% 1.88/1.37
% 1.88/1.37 thf(fact_1_calculation_I1_J,axiom,
% 1.88/1.37 ord_less_int @ t @ one_one_int ).
% 1.88/1.37
% 1.88/1.37 thf(fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096,axiom,
% 1.88/1.37 ord_less_int @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ zero_zero_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_3_t,axiom,
% 1.88/1.37 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 1.88/1.37 = ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_4_calculation_I2_J,axiom,
% 1.88/1.37 ( ( t = zero_zero_int )
% 1.88/1.37 => ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 1.88/1.37 = zero_zero_int ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_5__096_126_A1_A_060_061_At_096,axiom,
% 1.88/1.37 ~ ( ord_less_eq_int @ one_one_int @ t ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_6_p0,axiom,
% 1.88/1.37 ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_7_not__sum__power2__lt__zero,axiom,
% 1.88/1.37 ! [X: int,Y: int] :
% 1.88/1.37 ~ ( ord_less_int @ ( plus_plus_int @ ( power_power_int @ X @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) @ zero_zero_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_8_sum__power2__gt__zero__iff,axiom,
% 1.88/1.37 ! [X_10: int,Y_9: int] :
% 1.88/1.37 ( ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( power_power_int @ X_10 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_9 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) )
% 1.88/1.37 <=> ( ( X_10 != zero_zero_int )
% 1.88/1.37 | ( Y_9 != zero_zero_int ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_9_sum__power2__eq__zero__iff,axiom,
% 1.88/1.37 ! [X_9: int,Y_8: int] :
% 1.88/1.37 ( ( ( plus_plus_int @ ( power_power_int @ X_9 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_8 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 1.88/1.37 = zero_zero_int )
% 1.88/1.37 <=> ( ( X_9 = zero_zero_int )
% 1.88/1.37 & ( Y_8 = zero_zero_int ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_10_power2__less__0,axiom,
% 1.88/1.37 ! [A_3: int] :
% 1.88/1.37 ~ ( ord_less_int @ ( power_power_int @ A_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ zero_zero_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_11_zero__less__power2,axiom,
% 1.88/1.37 ! [A_2: int] :
% 1.88/1.37 ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ A_2 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
% 1.88/1.37 <=> ( A_2 != zero_zero_int ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_12_one__power2,axiom,
% 1.88/1.37 ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 1.88/1.37 = one_one_nat ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_13_one__power2,axiom,
% 1.88/1.37 ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 1.88/1.37 = one_one_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_14_zero__power2,axiom,
% 1.88/1.37 ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 1.88/1.37 = zero_zero_nat ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_15_zero__power2,axiom,
% 1.88/1.37 ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 1.88/1.37 = zero_zero_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_16_zero__eq__power2,axiom,
% 1.88/1.37 ! [A_1: int] :
% 1.88/1.37 ( ( ( power_power_int @ A_1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
% 1.88/1.37 = zero_zero_int )
% 1.88/1.37 <=> ( A_1 = zero_zero_int ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_17_add__special_I2_J,axiom,
% 1.88/1.37 ! [W_7: int] :
% 1.88/1.37 ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_7 ) )
% 1.88/1.37 = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_7 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_18_add__special_I3_J,axiom,
% 1.88/1.37 ! [V_12: int] :
% 1.88/1.37 ( ( plus_plus_int @ ( number_number_of_int @ V_12 ) @ one_one_int )
% 1.88/1.37 = ( number_number_of_int @ ( plus_plus_int @ V_12 @ ( bit1 @ pls ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_19_t__l__p,axiom,
% 1.88/1.37 ord_less_int @ t @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_20__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,
% 1.88/1.37 ~ ! [T: int] :
% 1.88/1.37 ( ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int )
% 1.88/1.37 != ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ T ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_21_p,axiom,
% 1.88/1.37 zprime @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_22_qf1pt,axiom,
% 1.88/1.37 twoSqu1013291560sum2sq @ ( times_times_int @ ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) @ t ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_23_zle__refl,axiom,
% 1.88/1.37 ! [W: int] : ( ord_less_eq_int @ W @ W ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_24_number__of__is__id,axiom,
% 1.88/1.37 ! [K: int] :
% 1.88/1.37 ( ( number_number_of_int @ K )
% 1.88/1.37 = K ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_25_zmult__commute,axiom,
% 1.88/1.37 ! [Z: int,W: int] :
% 1.88/1.37 ( ( times_times_int @ Z @ W )
% 1.88/1.37 = ( times_times_int @ W @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_26_zle__linear,axiom,
% 1.88/1.37 ! [Z: int,W: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ Z @ W )
% 1.88/1.37 | ( ord_less_eq_int @ W @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_27_times__numeral__code_I5_J,axiom,
% 1.88/1.37 ! [V_2: int,W: int] :
% 1.88/1.37 ( ( times_times_int @ ( number_number_of_int @ V_2 ) @ ( number_number_of_int @ W ) )
% 1.88/1.37 = ( number_number_of_int @ ( times_times_int @ V_2 @ W ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_28_less__eq__number__of__int__code,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_29_le__number__of,axiom,
% 1.88/1.37 ! [X_8: int,Y_7: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( number_number_of_int @ X_8 ) @ ( number_number_of_int @ Y_7 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ X_8 @ Y_7 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_30_zmult__assoc,axiom,
% 1.88/1.37 ! [Z1: int,Z2: int,Z3: int] :
% 1.88/1.37 ( ( times_times_int @ ( times_times_int @ Z1 @ Z2 ) @ Z3 )
% 1.88/1.37 = ( times_times_int @ Z1 @ ( times_times_int @ Z2 @ Z3 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_31_zle__trans,axiom,
% 1.88/1.37 ! [K: int,I: int,J: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ I @ J )
% 1.88/1.37 => ( ( ord_less_eq_int @ J @ K )
% 1.88/1.37 => ( ord_less_eq_int @ I @ K ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_32_zle__antisym,axiom,
% 1.88/1.37 ! [Z: int,W: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ Z @ W )
% 1.88/1.37 => ( ( ord_less_eq_int @ W @ Z )
% 1.88/1.37 => ( Z = W ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_33_zpower__zadd__distrib,axiom,
% 1.88/1.37 ! [X: int,Y: nat,Z: nat] :
% 1.88/1.37 ( ( power_power_int @ X @ ( plus_plus_nat @ Y @ Z ) )
% 1.88/1.37 = ( times_times_int @ ( power_power_int @ X @ Y ) @ ( power_power_int @ X @ Z ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_34_less__eq__int__code_I16_J,axiom,
% 1.88/1.37 ! [K1: int,K2: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_35_rel__simps_I34_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit1 @ L ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_36_rel__simps_I19_J,axiom,
% 1.88/1.37 ord_less_eq_int @ pls @ pls ).
% 1.88/1.37
% 1.88/1.37 thf(fact_37_less__eq__int__code_I13_J,axiom,
% 1.88/1.37 ! [K1: int,K2: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_38_rel__simps_I31_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit0 @ L ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_39_zless__le,axiom,
% 1.88/1.37 ! [Z: int,W: int] :
% 1.88/1.37 ( ( ord_less_int @ Z @ W )
% 1.88/1.37 <=> ( ( ord_less_eq_int @ Z @ W )
% 1.88/1.37 & ( Z != W ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_40_zadd__left__mono,axiom,
% 1.88/1.37 ! [K: int,I: int,J: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ I @ J )
% 1.88/1.37 => ( ord_less_eq_int @ ( plus_plus_int @ K @ I ) @ ( plus_plus_int @ K @ J ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_41_eq__number__of__0,axiom,
% 1.88/1.37 ! [V_2: int] :
% 1.88/1.37 ( ( ( number_number_of_nat @ V_2 )
% 1.88/1.37 = zero_zero_nat )
% 1.88/1.37 <=> ( ord_less_eq_int @ V_2 @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_42_eq__0__number__of,axiom,
% 1.88/1.37 ! [V_2: int] :
% 1.88/1.37 ( ( zero_zero_nat
% 1.88/1.37 = ( number_number_of_nat @ V_2 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ V_2 @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_43_semiring__mult__number__of,axiom,
% 1.88/1.37 ! [V_11: int,V_10: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ pls @ V_10 )
% 1.88/1.37 => ( ( ord_less_eq_int @ pls @ V_11 )
% 1.88/1.37 => ( ( times_times_nat @ ( number_number_of_nat @ V_10 ) @ ( number_number_of_nat @ V_11 ) )
% 1.88/1.37 = ( number_number_of_nat @ ( times_times_int @ V_10 @ V_11 ) ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_44_semiring__mult__number__of,axiom,
% 1.88/1.37 ! [V_11: int,V_10: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ pls @ V_10 )
% 1.88/1.37 => ( ( ord_less_eq_int @ pls @ V_11 )
% 1.88/1.37 => ( ( times_times_int @ ( number_number_of_int @ V_10 ) @ ( number_number_of_int @ V_11 ) )
% 1.88/1.37 = ( number_number_of_int @ ( times_times_int @ V_10 @ V_11 ) ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_45_mult__number__of__left,axiom,
% 1.88/1.37 ! [V_9: int,W_6: int,Z_2: int] :
% 1.88/1.37 ( ( times_times_int @ ( number_number_of_int @ V_9 ) @ ( times_times_int @ ( number_number_of_int @ W_6 ) @ Z_2 ) )
% 1.88/1.37 = ( times_times_int @ ( number_number_of_int @ ( times_times_int @ V_9 @ W_6 ) ) @ Z_2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_46_arith__simps_I32_J,axiom,
% 1.88/1.37 ! [V_8: int,W_5: int] :
% 1.88/1.37 ( ( times_times_int @ ( number_number_of_int @ V_8 ) @ ( number_number_of_int @ W_5 ) )
% 1.88/1.37 = ( number_number_of_int @ ( times_times_int @ V_8 @ W_5 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_47_number__of__mult,axiom,
% 1.88/1.37 ! [V_7: int,W_4: int] :
% 1.88/1.37 ( ( number_number_of_int @ ( times_times_int @ V_7 @ W_4 ) )
% 1.88/1.37 = ( times_times_int @ ( number_number_of_int @ V_7 ) @ ( number_number_of_int @ W_4 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_48_sum__squares__le__zero__iff,axiom,
% 1.88/1.37 ! [X_7: int,Y_6: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( plus_plus_int @ ( times_times_int @ X_7 @ X_7 ) @ ( times_times_int @ Y_6 @ Y_6 ) ) @ zero_zero_int )
% 1.88/1.37 <=> ( ( X_7 = zero_zero_int )
% 1.88/1.37 & ( Y_6 = zero_zero_int ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_49_sum__squares__ge__zero,axiom,
% 1.88/1.37 ! [X_6: int,Y_5: int] : ( ord_less_eq_int @ zero_zero_int @ ( plus_plus_int @ ( times_times_int @ X_6 @ X_6 ) @ ( times_times_int @ Y_5 @ Y_5 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_50_le__special_I3_J,axiom,
% 1.88/1.37 ! [X_5: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( number_number_of_int @ X_5 ) @ zero_zero_int )
% 1.88/1.37 <=> ( ord_less_eq_int @ X_5 @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_51_le__special_I1_J,axiom,
% 1.88/1.37 ! [Y_4: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ zero_zero_int @ ( number_number_of_int @ Y_4 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ pls @ Y_4 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_52_less__0__number__of,axiom,
% 1.88/1.37 ! [V_2: int] :
% 1.88/1.37 ( ( ord_less_nat @ zero_zero_nat @ ( number_number_of_nat @ V_2 ) )
% 1.88/1.37 <=> ( ord_less_int @ pls @ V_2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_53_le__number__of__eq__not__less,axiom,
% 1.88/1.37 ! [V_6: int,W_3: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( number_number_of_int @ V_6 ) @ ( number_number_of_int @ W_3 ) )
% 1.88/1.37 <=> ~ ( ord_less_int @ ( number_number_of_int @ W_3 ) @ ( number_number_of_int @ V_6 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_54_le__number__of__eq__not__less,axiom,
% 1.88/1.37 ! [V_6: int,W_3: int] :
% 1.88/1.37 ( ( ord_less_eq_nat @ ( number_number_of_nat @ V_6 ) @ ( number_number_of_nat @ W_3 ) )
% 1.88/1.37 <=> ~ ( ord_less_nat @ ( number_number_of_nat @ W_3 ) @ ( number_number_of_nat @ V_6 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_55_rel__simps_I22_J,axiom,
% 1.88/1.37 ! [K: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ pls @ ( bit1 @ K ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_56_less__eq__int__code_I14_J,axiom,
% 1.88/1.37 ! [K1: int,K2: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_57_rel__simps_I32_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_58_rel__simps_I27_J,axiom,
% 1.88/1.37 ! [K: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit0 @ K ) @ pls )
% 1.88/1.37 <=> ( ord_less_eq_int @ K @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_59_rel__simps_I21_J,axiom,
% 1.88/1.37 ! [K: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ pls @ ( bit0 @ K ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_60_zadd__zless__mono,axiom,
% 1.88/1.37 ! [Z_1: int,Z: int,W_2: int,W: int] :
% 1.88/1.37 ( ( ord_less_int @ W_2 @ W )
% 1.88/1.37 => ( ( ord_less_eq_int @ Z_1 @ Z )
% 1.88/1.37 => ( ord_less_int @ ( plus_plus_int @ W_2 @ Z_1 ) @ ( plus_plus_int @ W @ Z ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_61_nat__number__of__Pls,axiom,
% 1.88/1.37 ( ( number_number_of_nat @ pls )
% 1.88/1.37 = zero_zero_nat ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_62_semiring__norm_I113_J,axiom,
% 1.88/1.37 ( zero_zero_nat
% 1.88/1.37 = ( number_number_of_nat @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_63_le__special_I4_J,axiom,
% 1.88/1.37 ! [X_4: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( number_number_of_int @ X_4 ) @ one_one_int )
% 1.88/1.37 <=> ( ord_less_eq_int @ X_4 @ ( bit1 @ pls ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_64_le__special_I2_J,axiom,
% 1.88/1.37 ! [Y_3: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ one_one_int @ ( number_number_of_int @ Y_3 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ ( bit1 @ pls ) @ Y_3 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_65_nat__1__add__1,axiom,
% 1.88/1.37 ( ( plus_plus_nat @ one_one_nat @ one_one_nat )
% 1.88/1.37 = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_66_mult__Pls,axiom,
% 1.88/1.37 ! [W: int] :
% 1.88/1.37 ( ( times_times_int @ pls @ W )
% 1.88/1.37 = pls ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_67_mult__Bit0,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( times_times_int @ ( bit0 @ K ) @ L )
% 1.88/1.37 = ( bit0 @ ( times_times_int @ K @ L ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_68_less__number__of__int__code,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) )
% 1.88/1.37 <=> ( ord_less_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_69_zmult__1__right,axiom,
% 1.88/1.37 ! [Z: int] :
% 1.88/1.37 ( ( times_times_int @ Z @ one_one_int )
% 1.88/1.37 = Z ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_70_zmult__1,axiom,
% 1.88/1.37 ! [Z: int] :
% 1.88/1.37 ( ( times_times_int @ one_one_int @ Z )
% 1.88/1.37 = Z ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_71_plus__numeral__code_I9_J,axiom,
% 1.88/1.37 ! [V_2: int,W: int] :
% 1.88/1.37 ( ( plus_plus_int @ ( number_number_of_int @ V_2 ) @ ( number_number_of_int @ W ) )
% 1.88/1.37 = ( number_number_of_int @ ( plus_plus_int @ V_2 @ W ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_72_zadd__zmult__distrib,axiom,
% 1.88/1.37 ! [Z1: int,Z2: int,W: int] :
% 1.88/1.37 ( ( times_times_int @ ( plus_plus_int @ Z1 @ Z2 ) @ W )
% 1.88/1.37 = ( plus_plus_int @ ( times_times_int @ Z1 @ W ) @ ( times_times_int @ Z2 @ W ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_73_zadd__zmult__distrib2,axiom,
% 1.88/1.37 ! [W: int,Z1: int,Z2: int] :
% 1.88/1.37 ( ( times_times_int @ W @ ( plus_plus_int @ Z1 @ Z2 ) )
% 1.88/1.37 = ( plus_plus_int @ ( times_times_int @ W @ Z1 ) @ ( times_times_int @ W @ Z2 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_74_rel__simps_I29_J,axiom,
% 1.88/1.37 ! [K: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit1 @ K ) @ pls )
% 1.88/1.37 <=> ( ord_less_int @ K @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_75_rel__simps_I5_J,axiom,
% 1.88/1.37 ! [K: int] :
% 1.88/1.37 ( ( ord_less_int @ pls @ ( bit1 @ K ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ pls @ K ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_76_less__eq__int__code_I15_J,axiom,
% 1.88/1.37 ! [K1: int,K2: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) )
% 1.88/1.37 <=> ( ord_less_int @ K1 @ K2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_77_rel__simps_I33_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( bit1 @ K ) @ ( bit0 @ L ) )
% 1.88/1.37 <=> ( ord_less_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_78_less__int__code_I14_J,axiom,
% 1.88/1.37 ! [K1: int,K2: int] :
% 1.88/1.37 ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit1 @ K2 ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K1 @ K2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_79_rel__simps_I15_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ord_less_int @ ( bit0 @ K ) @ ( bit1 @ L ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ K @ L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_80_less__nat__number__of,axiom,
% 1.88/1.37 ! [V_2: int,V_3: int] :
% 1.88/1.37 ( ( ord_less_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 1.88/1.37 <=> ( ( ( ord_less_int @ V_2 @ V_3 )
% 1.88/1.37 => ( ord_less_int @ pls @ V_3 ) )
% 1.88/1.37 & ( ord_less_int @ V_2 @ V_3 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_81_int__one__le__iff__zero__less,axiom,
% 1.88/1.37 ! [Z: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ one_one_int @ Z )
% 1.88/1.37 <=> ( ord_less_int @ zero_zero_int @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_82_nat__numeral__1__eq__1,axiom,
% 1.88/1.37 ( ( number_number_of_nat @ ( bit1 @ pls ) )
% 1.88/1.37 = one_one_nat ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_83_Numeral1__eq1__nat,axiom,
% 1.88/1.37 ( one_one_nat
% 1.88/1.37 = ( number_number_of_nat @ ( bit1 @ pls ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_84_zless__imp__add1__zle,axiom,
% 1.88/1.37 ! [W: int,Z: int] :
% 1.88/1.37 ( ( ord_less_int @ W @ Z )
% 1.88/1.37 => ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_85_add1__zle__eq,axiom,
% 1.88/1.37 ! [W: int,Z: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ ( plus_plus_int @ W @ one_one_int ) @ Z )
% 1.88/1.37 <=> ( ord_less_int @ W @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_86_zle__add1__eq__le,axiom,
% 1.88/1.37 ! [W: int,Z: int] :
% 1.88/1.37 ( ( ord_less_int @ W @ ( plus_plus_int @ Z @ one_one_int ) )
% 1.88/1.37 <=> ( ord_less_eq_int @ W @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_87_semiring__add__number__of,axiom,
% 1.88/1.37 ! [V_5: int,V_4: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ pls @ V_4 )
% 1.88/1.37 => ( ( ord_less_eq_int @ pls @ V_5 )
% 1.88/1.37 => ( ( plus_plus_int @ ( number_number_of_int @ V_4 ) @ ( number_number_of_int @ V_5 ) )
% 1.88/1.37 = ( number_number_of_int @ ( plus_plus_int @ V_4 @ V_5 ) ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_88_semiring__add__number__of,axiom,
% 1.88/1.37 ! [V_5: int,V_4: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ pls @ V_4 )
% 1.88/1.37 => ( ( ord_less_eq_int @ pls @ V_5 )
% 1.88/1.37 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_4 ) @ ( number_number_of_nat @ V_5 ) )
% 1.88/1.37 = ( number_number_of_nat @ ( plus_plus_int @ V_4 @ V_5 ) ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_89_add__nat__number__of,axiom,
% 1.88/1.37 ! [V_3: int,V_2: int] :
% 1.88/1.37 ( ( ( ord_less_int @ V_2 @ pls )
% 1.88/1.37 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 1.88/1.37 = ( number_number_of_nat @ V_3 ) ) )
% 1.88/1.37 & ( ~ ( ord_less_int @ V_2 @ pls )
% 1.88/1.37 => ( ( ( ord_less_int @ V_3 @ pls )
% 1.88/1.37 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 1.88/1.37 = ( number_number_of_nat @ V_2 ) ) )
% 1.88/1.37 & ( ~ ( ord_less_int @ V_3 @ pls )
% 1.88/1.37 => ( ( plus_plus_nat @ ( number_number_of_nat @ V_2 ) @ ( number_number_of_nat @ V_3 ) )
% 1.88/1.37 = ( number_number_of_nat @ ( plus_plus_int @ V_2 @ V_3 ) ) ) ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_90_le__imp__0__less,axiom,
% 1.88/1.37 ! [Z: int] :
% 1.88/1.37 ( ( ord_less_eq_int @ zero_zero_int @ Z )
% 1.88/1.37 => ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ one_one_int @ Z ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_91_eq__number__of,axiom,
% 1.88/1.37 ! [X_3: int,Y_2: int] :
% 1.88/1.37 ( ( ( number_number_of_int @ X_3 )
% 1.88/1.37 = ( number_number_of_int @ Y_2 ) )
% 1.88/1.37 <=> ( X_3 = Y_2 ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_92_number__of__reorient,axiom,
% 1.88/1.37 ! [W_1: int,X_2: nat] :
% 1.88/1.37 ( ( ( number_number_of_nat @ W_1 )
% 1.88/1.37 = X_2 )
% 1.88/1.37 <=> ( X_2
% 1.88/1.37 = ( number_number_of_nat @ W_1 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_93_number__of__reorient,axiom,
% 1.88/1.37 ! [W_1: int,X_2: int] :
% 1.88/1.37 ( ( ( number_number_of_int @ W_1 )
% 1.88/1.37 = X_2 )
% 1.88/1.37 <=> ( X_2
% 1.88/1.37 = ( number_number_of_int @ W_1 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_94_rel__simps_I51_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ( bit1 @ K )
% 1.88/1.37 = ( bit1 @ L ) )
% 1.88/1.37 <=> ( K = L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_95_rel__simps_I48_J,axiom,
% 1.88/1.37 ! [K: int,L: int] :
% 1.88/1.37 ( ( ( bit0 @ K )
% 1.88/1.37 = ( bit0 @ L ) )
% 1.88/1.37 <=> ( K = L ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_96_zless__linear,axiom,
% 1.88/1.37 ! [X: int,Y: int] :
% 1.88/1.37 ( ( ord_less_int @ X @ Y )
% 1.88/1.37 | ( X = Y )
% 1.88/1.37 | ( ord_less_int @ Y @ X ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_97_sum__squares__eq__zero__iff,axiom,
% 1.88/1.37 ! [X_1: int,Y_1: int] :
% 1.88/1.37 ( ( ( plus_plus_int @ ( times_times_int @ X_1 @ X_1 ) @ ( times_times_int @ Y_1 @ Y_1 ) )
% 1.88/1.37 = zero_zero_int )
% 1.88/1.37 <=> ( ( X_1 = zero_zero_int )
% 1.88/1.37 & ( Y_1 = zero_zero_int ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_98_left__distrib__number__of,axiom,
% 1.88/1.37 ! [A: int,B_1: int,V_1: int] :
% 1.88/1.37 ( ( times_times_int @ ( plus_plus_int @ A @ B_1 ) @ ( number_number_of_int @ V_1 ) )
% 1.88/1.37 = ( plus_plus_int @ ( times_times_int @ A @ ( number_number_of_int @ V_1 ) ) @ ( times_times_int @ B_1 @ ( number_number_of_int @ V_1 ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_99_left__distrib__number__of,axiom,
% 1.88/1.37 ! [A: nat,B_1: nat,V_1: int] :
% 1.88/1.37 ( ( times_times_nat @ ( plus_plus_nat @ A @ B_1 ) @ ( number_number_of_nat @ V_1 ) )
% 1.88/1.37 = ( plus_plus_nat @ ( times_times_nat @ A @ ( number_number_of_nat @ V_1 ) ) @ ( times_times_nat @ B_1 @ ( number_number_of_nat @ V_1 ) ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_100_right__distrib__number__of,axiom,
% 1.88/1.37 ! [V: int,B: int,C: int] :
% 1.88/1.37 ( ( times_times_int @ ( number_number_of_int @ V ) @ ( plus_plus_int @ B @ C ) )
% 1.88/1.37 = ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ V ) @ B ) @ ( times_times_int @ ( number_number_of_int @ V ) @ C ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_101_right__distrib__number__of,axiom,
% 1.88/1.37 ! [V: int,B: nat,C: nat] :
% 1.88/1.37 ( ( times_times_nat @ ( number_number_of_nat @ V ) @ ( plus_plus_nat @ B @ C ) )
% 1.88/1.37 = ( plus_plus_nat @ ( times_times_nat @ ( number_number_of_nat @ V ) @ B ) @ ( times_times_nat @ ( number_number_of_nat @ V ) @ C ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_102_zadd__assoc,axiom,
% 1.88/1.37 ! [Z1: int,Z2: int,Z3: int] :
% 1.88/1.37 ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 )
% 1.88/1.37 = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_103_zadd__left__commute,axiom,
% 1.88/1.37 ! [X: int,Y: int,Z: int] :
% 1.88/1.37 ( ( plus_plus_int @ X @ ( plus_plus_int @ Y @ Z ) )
% 1.88/1.37 = ( plus_plus_int @ Y @ ( plus_plus_int @ X @ Z ) ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_104_zadd__commute,axiom,
% 1.88/1.37 ! [Z: int,W: int] :
% 1.88/1.37 ( ( plus_plus_int @ Z @ W )
% 1.88/1.37 = ( plus_plus_int @ W @ Z ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(fact_105_zero__is__num__zero,axiom,
% 1.88/1.37 ( zero_zero_int
% 1.88/1.37 = ( number_number_of_int @ pls ) ) ).
% 1.88/1.37
% 1.88/1.37 thf(conj_0,conjecture,
% 1.88/1.37 ord_less_int @ ( plus_plus_int @ ( power_power_int @ s @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ one_one_int ) @ zero_zero_int ).
% 1.88/1.37 ------------------------
% 1.88/1.38 % (30800)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_30683 for (2999ds/4Mi)
% 1.88/1.38 % (30804)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_30683 for (2999ds/275Mi)
% 1.88/1.38 % (30805)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/18Mi)
% 1.88/1.38 % (30800)Instruction limit reached!
% 1.88/1.38 % (30800)------------------------------
% 1.88/1.38 % (30800)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.88/1.38 % (30800)Termination reason: Unknown
% 1.88/1.38 % (30800)Termination phase: shuffling
% 1.88/1.38
% 1.88/1.38 % (30800)Memory used [KB]: 1151
% 1.88/1.38 % (30800)Time elapsed: 0.003 s
% 1.88/1.38 % (30800)Instructions burned: 6 (million)
% 1.88/1.38 % (30800)------------------------------
% 1.88/1.38 % (30800)------------------------------
% 1.88/1.39 % (30805)Instruction limit reached!
% 1.88/1.39 % (30805)------------------------------
% 1.88/1.39 % (30805)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.88/1.39 % (30805)Termination reason: Unknown
% 1.88/1.39 % (30805)Termination phase: Function definition elimination
% 1.88/1.39
% 1.88/1.39 % (30805)Memory used [KB]: 1279
% 1.88/1.39 % (30805)Time elapsed: 0.006 s
% 1.88/1.39 % (30805)Instructions burned: 18 (million)
% 1.88/1.39 % (30805)------------------------------
% 1.88/1.39 % (30805)------------------------------
% 1.88/1.39 % (30799)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/183Mi)
% 1.88/1.39 % (30801)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_30683 for (2999ds/27Mi)
% 1.88/1.39 % (30803)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_30683 for (2999ds/2Mi)
% 1.88/1.39 % (30802)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/2Mi)
% 1.88/1.39 % (30803)Instruction limit reached!
% 1.88/1.39 % (30803)------------------------------
% 1.88/1.39 % (30803)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.88/1.39 % (30803)Termination reason: Unknown
% 1.88/1.39 % (30803)Termination phase: shuffling
% 1.88/1.39
% 1.88/1.39 % (30803)Memory used [KB]: 1151
% 1.88/1.39 % (30803)Time elapsed: 0.003 s
% 1.88/1.39 % (30803)Instructions burned: 2 (million)
% 1.88/1.39 % (30803)------------------------------
% 1.88/1.39 % (30803)------------------------------
% 1.88/1.39 % (30802)Instruction limit reached!
% 1.88/1.39 % (30802)------------------------------
% 1.88/1.39 % (30802)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.88/1.39 % (30802)Termination reason: Unknown
% 1.88/1.39 % (30802)Termination phase: shuffling
% 1.88/1.39
% 1.88/1.39 % (30802)Memory used [KB]: 1151
% 1.88/1.39 % (30802)Time elapsed: 0.004 s
% 1.88/1.39 % (30802)Instructions burned: 3 (million)
% 1.88/1.39 % (30802)------------------------------
% 1.88/1.39 % (30802)------------------------------
% 1.88/1.39 % (30806)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/3Mi)
% 1.88/1.40 % (30806)Instruction limit reached!
% 1.88/1.40 % (30806)------------------------------
% 1.88/1.40 % (30806)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.88/1.40 % (30806)Termination reason: Unknown
% 1.88/1.40 % (30806)Termination phase: shuffling
% 1.88/1.40
% 1.88/1.40 % (30806)Memory used [KB]: 1151
% 1.88/1.40 % (30806)Time elapsed: 0.003 s
% 1.88/1.40 % (30806)Instructions burned: 4 (million)
% 1.88/1.40 % (30806)------------------------------
% 1.88/1.40 % (30806)------------------------------
% 2.03/1.40 % (30807)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_30683 for (2999ds/37Mi)
% 2.03/1.40 % (30801)Instruction limit reached!
% 2.03/1.40 % (30801)------------------------------
% 2.03/1.40 % (30801)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.40 % (30801)Termination reason: Unknown
% 2.03/1.40 % (30801)Termination phase: Saturation
% 2.03/1.40
% 2.03/1.40 % (30801)Memory used [KB]: 5756
% 2.03/1.40 % (30801)Time elapsed: 0.017 s
% 2.03/1.41 % (30801)Instructions burned: 27 (million)
% 2.03/1.41 % (30801)------------------------------
% 2.03/1.41 % (30801)------------------------------
% 2.03/1.41 % (30810)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_30683 for (2999ds/1041Mi)
% 2.03/1.41 % (30807)Instruction limit reached!
% 2.03/1.41 % (30807)------------------------------
% 2.03/1.41 % (30807)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.41 % (30807)Termination reason: Unknown
% 2.03/1.41 % (30807)Termination phase: Saturation
% 2.03/1.41
% 2.03/1.41 % (30807)Memory used [KB]: 5884
% 2.03/1.41 % (30807)Time elapsed: 0.011 s
% 2.03/1.41 % (30807)Instructions burned: 40 (million)
% 2.03/1.41 % (30807)------------------------------
% 2.03/1.41 % (30807)------------------------------
% 2.03/1.41 % (30808)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_30683 for (2999ds/15Mi)
% 2.03/1.41 % (30809)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_30683 for (2999ds/3Mi)
% 2.03/1.41 % (30809)Instruction limit reached!
% 2.03/1.41 % (30809)------------------------------
% 2.03/1.41 % (30809)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.41 % (30809)Termination reason: Unknown
% 2.03/1.41 % (30809)Termination phase: shuffling
% 2.03/1.41
% 2.03/1.41 % (30809)Memory used [KB]: 1151
% 2.03/1.41 % (30809)Time elapsed: 0.004 s
% 2.03/1.41 % (30809)Instructions burned: 3 (million)
% 2.03/1.41 % (30809)------------------------------
% 2.03/1.41 % (30809)------------------------------
% 2.03/1.42 % (30808)Instruction limit reached!
% 2.03/1.42 % (30808)------------------------------
% 2.03/1.42 % (30808)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.42 % (30808)Termination reason: Unknown
% 2.03/1.42 % (30808)Termination phase: Property scanning
% 2.03/1.42
% 2.03/1.42 % (30808)Memory used [KB]: 1279
% 2.03/1.42 % (30808)Time elapsed: 0.010 s
% 2.03/1.42 % (30808)Instructions burned: 15 (million)
% 2.03/1.42 % (30808)------------------------------
% 2.03/1.42 % (30808)------------------------------
% 2.03/1.42 % (30812)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/16Mi)
% 2.03/1.42 % (30812)Instruction limit reached!
% 2.03/1.42 % (30812)------------------------------
% 2.03/1.42 % (30812)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.42 % (30812)Termination reason: Unknown
% 2.03/1.42 % (30812)Termination phase: Saturation
% 2.03/1.42
% 2.03/1.42 % (30812)Memory used [KB]: 1279
% 2.03/1.42 % (30812)Time elapsed: 0.006 s
% 2.03/1.42 % (30812)Instructions burned: 18 (million)
% 2.03/1.42 % (30812)------------------------------
% 2.03/1.42 % (30812)------------------------------
% 2.03/1.42 % (30811)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/7Mi)
% 2.03/1.43 % (30811)Instruction limit reached!
% 2.03/1.43 % (30811)------------------------------
% 2.03/1.43 % (30811)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.43 % (30811)Termination reason: Unknown
% 2.03/1.43 % (30811)Termination phase: Property scanning
% 2.03/1.43
% 2.03/1.43 % (30811)Memory used [KB]: 1151
% 2.03/1.43 % (30811)Time elapsed: 0.006 s
% 2.03/1.43 % (30811)Instructions burned: 7 (million)
% 2.03/1.43 % (30811)------------------------------
% 2.03/1.43 % (30811)------------------------------
% 2.03/1.43 % (30813)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_30683 for (2999ds/3Mi)
% 2.03/1.43 % (30813)Instruction limit reached!
% 2.03/1.43 % (30813)------------------------------
% 2.03/1.43 % (30813)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.43 % (30813)Termination reason: Unknown
% 2.03/1.43 % (30813)Termination phase: shuffling
% 2.03/1.43
% 2.03/1.43 % (30813)Memory used [KB]: 1151
% 2.03/1.43 % (30813)Time elapsed: 0.004 s
% 2.03/1.43 % (30813)Instructions burned: 3 (million)
% 2.03/1.43 % (30813)------------------------------
% 2.03/1.43 % (30813)------------------------------
% 2.03/1.43 % (30815)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/7Mi)
% 2.03/1.43 % (30815)Instruction limit reached!
% 2.03/1.43 % (30815)------------------------------
% 2.03/1.43 % (30815)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.43 % (30815)Termination reason: Unknown
% 2.03/1.43 % (30815)Termination phase: shuffling
% 2.03/1.43
% 2.03/1.43 % (30815)Memory used [KB]: 1151
% 2.03/1.43 % (30815)Time elapsed: 0.003 s
% 2.03/1.43 % (30815)Instructions burned: 7 (million)
% 2.03/1.43 % (30815)------------------------------
% 2.03/1.43 % (30815)------------------------------
% 2.03/1.43 % (30814)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/3Mi)
% 2.03/1.44 % (30814)Instruction limit reached!
% 2.03/1.44 % (30814)------------------------------
% 2.03/1.44 % (30814)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.44 % (30814)Termination reason: Unknown
% 2.03/1.44 % (30814)Termination phase: shuffling
% 2.03/1.44
% 2.03/1.44 % (30814)Memory used [KB]: 1151
% 2.03/1.44 % (30814)Time elapsed: 0.004 s
% 2.03/1.44 % (30814)Instructions burned: 4 (million)
% 2.03/1.44 % (30814)------------------------------
% 2.03/1.44 % (30814)------------------------------
% 2.03/1.44 % (30818)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/18Mi)
% 2.03/1.44 % (30816)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/3Mi)
% 2.03/1.45 % (30816)Instruction limit reached!
% 2.03/1.45 % (30816)------------------------------
% 2.03/1.45 % (30816)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.45 % (30816)Termination reason: Unknown
% 2.03/1.45 % (30816)Termination phase: shuffling
% 2.03/1.45
% 2.03/1.45 % (30816)Memory used [KB]: 1151
% 2.03/1.45 % (30816)Time elapsed: 0.004 s
% 2.03/1.45 % (30816)Instructions burned: 4 (million)
% 2.03/1.45 % (30816)------------------------------
% 2.03/1.45 % (30816)------------------------------
% 2.03/1.45 % (30818)Instruction limit reached!
% 2.03/1.45 % (30818)------------------------------
% 2.03/1.45 % (30818)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.45 % (30818)Termination reason: Unknown
% 2.03/1.45 % (30818)Termination phase: Property scanning
% 2.03/1.45
% 2.03/1.45 % (30818)Memory used [KB]: 1279
% 2.03/1.45 % (30818)Time elapsed: 0.006 s
% 2.03/1.45 % (30818)Instructions burned: 19 (million)
% 2.03/1.45 % (30818)------------------------------
% 2.03/1.45 % (30818)------------------------------
% 2.03/1.45 % (30817)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/4Mi)
% 2.03/1.45 % (30817)Instruction limit reached!
% 2.03/1.45 % (30817)------------------------------
% 2.03/1.45 % (30817)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.45 % (30817)Termination reason: Unknown
% 2.03/1.45 % (30817)Termination phase: shuffling
% 2.03/1.45
% 2.03/1.45 % (30817)Memory used [KB]: 1151
% 2.03/1.45 % (30817)Time elapsed: 0.004 s
% 2.03/1.45 % (30817)Instructions burned: 4 (million)
% 2.03/1.45 % (30817)------------------------------
% 2.03/1.45 % (30817)------------------------------
% 2.03/1.45 % (30819)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_30683 for (2999ds/710Mi)
% 2.03/1.45 % (30810)First to succeed.
% 2.03/1.46 % (30799)Instruction limit reached!
% 2.03/1.46 % (30799)------------------------------
% 2.03/1.46 % (30799)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.46 % (30799)Termination reason: Unknown
% 2.03/1.46 % (30799)Termination phase: Saturation
% 2.03/1.46
% 2.03/1.46 % (30799)Memory used [KB]: 6524
% 2.03/1.46 % (30799)Time elapsed: 0.069 s
% 2.03/1.46 % (30799)Instructions burned: 183 (million)
% 2.03/1.46 % (30799)------------------------------
% 2.03/1.46 % (30799)------------------------------
% 2.03/1.46 % (30810)Refutation found. Thanks to Tanya!
% 2.03/1.46 % SZS status Theorem for DTF2THF_30683
% 2.03/1.46 % SZS output start Proof for DTF2THF_30683
% 2.03/1.46 thf(type_def_5, type, int: $tType).
% 2.03/1.46 thf(type_def_6, type, nat: $tType).
% 2.03/1.46 thf(func_def_0, type, int: $tType).
% 2.03/1.46 thf(func_def_1, type, nat: $tType).
% 2.03/1.46 thf(func_def_2, type, one_one_int: int).
% 2.03/1.46 thf(func_def_3, type, one_one_nat: nat).
% 2.03/1.46 thf(func_def_4, type, plus_plus_int: int > int > int).
% 2.03/1.46 thf(func_def_5, type, plus_plus_nat: nat > nat > nat).
% 2.03/1.46 thf(func_def_6, type, times_times_int: int > int > int).
% 2.03/1.46 thf(func_def_7, type, times_times_nat: nat > nat > nat).
% 2.03/1.46 thf(func_def_8, type, zero_zero_int: int).
% 2.03/1.46 thf(func_def_9, type, zero_zero_nat: nat).
% 2.03/1.46 thf(func_def_10, type, zprime: int > $o).
% 2.03/1.46 thf(func_def_11, type, bit0: int > int).
% 2.03/1.46 thf(func_def_12, type, bit1: int > int).
% 2.03/1.46 thf(func_def_13, type, pls: int).
% 2.03/1.46 thf(func_def_14, type, number_number_of_int: int > int).
% 2.03/1.46 thf(func_def_15, type, number_number_of_nat: int > nat).
% 2.03/1.46 thf(func_def_16, type, ord_less_int: int > int > $o).
% 2.03/1.46 thf(func_def_17, type, ord_less_nat: nat > nat > $o).
% 2.03/1.46 thf(func_def_18, type, ord_less_eq_int: int > int > $o).
% 2.03/1.46 thf(func_def_19, type, ord_less_eq_nat: nat > nat > $o).
% 2.03/1.46 thf(func_def_20, type, power_power_int: int > nat > int).
% 2.03/1.46 thf(func_def_21, type, power_power_nat: nat > nat > nat).
% 2.03/1.46 thf(func_def_22, type, twoSqu1013291560sum2sq: int > $o).
% 2.03/1.46 thf(func_def_23, type, m: int).
% 2.03/1.46 thf(func_def_24, type, s: int).
% 2.03/1.46 thf(func_def_25, type, t: int).
% 2.03/1.46 thf(func_def_42, type, ph1: !>[X0: $tType]:(X0)).
% 2.03/1.46 thf(f913,plain,(
% 2.03/1.46 $false),
% 2.03/1.46 inference(trivial_inequality_removal,[status(thm)],[f912])).
% 2.03/1.46 thf(f912,plain,(
% 2.03/1.46 ($false = $true)),
% 2.03/1.46 inference(forward_demodulation,[status(thm)],[f911,f738])).
% 2.03/1.46 thf(f738,plain,(
% 2.03/1.46 ($false = (ord_less_int @ (plus_plus_int @ one_one_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ pls))),
% 2.03/1.46 inference(backward_demodulation,[status(thm)],[f498,f735])).
% 2.03/1.46 thf(f735,plain,(
% 2.03/1.46 ( ! [X2 : int,X1 : int] : (((plus_plus_int @ X1 @ X2) = (plus_plus_int @ X2 @ X1))) )),
% 2.03/1.46 inference(equality_proxy_clausification,[status(thm)],[f707])).
% 2.03/1.46 thf(f707,plain,(
% 2.03/1.46 ( ! [X2 : int,X1 : int] : (($true = ((plus_plus_int @ X2 @ X1) = (plus_plus_int @ X1 @ X2)))) )),
% 2.03/1.46 inference(beta_eta_normalization,[status(thm)],[f706])).
% 2.03/1.46 thf(f706,plain,(
% 2.03/1.46 ( ! [X2 : int,X1 : int] : (($true = ((^[Y0 : int]: ((plus_plus_int @ Y0 @ X1) = (plus_plus_int @ X1 @ Y0))) @ X2))) )),
% 2.03/1.46 inference(pi_clausification,[status(thm)],[f678])).
% 2.03/1.46 thf(f678,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = (!! @ int @ (^[Y0 : int]: ((plus_plus_int @ Y0 @ X1) = (plus_plus_int @ X1 @ Y0)))))) )),
% 2.03/1.46 inference(beta_eta_normalization,[status(thm)],[f677])).
% 2.03/1.46 thf(f677,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = ((^[Y0 : int]: (!! @ int @ (^[Y1 : int]: ((plus_plus_int @ Y1 @ Y0) = (plus_plus_int @ Y0 @ Y1))))) @ X1))) )),
% 2.03/1.46 inference(pi_clausification,[status(thm)],[f387])).
% 2.03/1.46 thf(f387,plain,(
% 2.03/1.46 ($true = (!! @ int @ (^[Y0 : int]: (!! @ int @ (^[Y1 : int]: ((plus_plus_int @ Y1 @ Y0) = (plus_plus_int @ Y0 @ Y1)))))))),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f196])).
% 2.03/1.46 thf(f196,plain,(
% 2.03/1.46 ($true = (!! @ int @ (^[Y0 : int]: (!! @ int @ (^[Y1 : int]: ((plus_plus_int @ Y1 @ Y0) = (plus_plus_int @ Y0 @ Y1)))))))),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f195])).
% 2.03/1.46 thf(f195,plain,(
% 2.03/1.46 ! [X0 : int,X1 : int] : ((plus_plus_int @ X0 @ X1) = (plus_plus_int @ X1 @ X0))),
% 2.03/1.46 inference(rectify,[status(thm)],[f105])).
% 2.03/1.46 thf(f105,axiom,(
% 2.03/1.46 ! [X12 : int,X14 : int] : ((plus_plus_int @ X12 @ X14) = (plus_plus_int @ X14 @ X12))),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_104_zadd__commute)).
% 2.03/1.46 thf(f498,plain,(
% 2.03/1.46 ($false = (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ pls))),
% 2.03/1.46 inference(not_proxy_clausification,[status(thm)],[f468])).
% 2.03/1.46 thf(f468,plain,(
% 2.03/1.46 ($true = (~ (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ pls)))),
% 2.03/1.46 inference(backward_demodulation,[status(thm)],[f425,f465])).
% 2.03/1.46 thf(f465,plain,(
% 2.03/1.46 ( ! [X1 : int] : (((number_number_of_int @ X1) = X1)) )),
% 2.03/1.46 inference(equality_proxy_clausification,[status(thm)],[f464])).
% 2.03/1.46 thf(f464,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = ((number_number_of_int @ X1) = X1))) )),
% 2.03/1.46 inference(beta_eta_normalization,[status(thm)],[f463])).
% 2.03/1.46 thf(f463,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = ((^[Y0 : int]: ((number_number_of_int @ Y0) = Y0)) @ X1))) )),
% 2.03/1.46 inference(pi_clausification,[status(thm)],[f412])).
% 2.03/1.46 thf(f412,plain,(
% 2.03/1.46 ((!! @ int @ (^[Y0 : int]: ((number_number_of_int @ Y0) = Y0))) = $true)),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f153])).
% 2.03/1.46 thf(f153,plain,(
% 2.03/1.46 ((!! @ int @ (^[Y0 : int]: ((number_number_of_int @ Y0) = Y0))) = $true)),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f152])).
% 2.03/1.46 thf(f152,plain,(
% 2.03/1.46 ! [X0 : int] : ((number_number_of_int @ X0) = X0)),
% 2.03/1.46 inference(rectify,[status(thm)],[f25])).
% 2.03/1.46 thf(f25,axiom,(
% 2.03/1.46 ! [X13 : int] : ((number_number_of_int @ X13) = X13)),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_24_number__of__is__id)).
% 2.03/1.46 thf(f425,plain,(
% 2.03/1.46 ($true = (~ (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ (number_number_of_int @ pls))))),
% 2.03/1.46 inference(definition_unfolding,[status(thm)],[f349,f378])).
% 2.03/1.46 thf(f378,plain,(
% 2.03/1.46 (zero_zero_int = (number_number_of_int @ pls))),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f299])).
% 2.03/1.46 thf(f299,plain,(
% 2.03/1.46 (zero_zero_int = (number_number_of_int @ pls))),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f106])).
% 2.03/1.46 thf(f106,axiom,(
% 2.03/1.46 (zero_zero_int = (number_number_of_int @ pls))),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_105_zero__is__num__zero)).
% 2.03/1.46 thf(f349,plain,(
% 2.03/1.46 ((~ (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ zero_zero_int)) = $true)),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f145])).
% 2.03/1.46 thf(f145,plain,(
% 2.03/1.46 ((~ (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ zero_zero_int)) = $true)),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f144])).
% 2.03/1.46 thf(f144,plain,(
% 2.03/1.46 ~(ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ zero_zero_int)),
% 2.03/1.46 inference(rectify,[status(thm)],[f108])).
% 2.03/1.46 thf(f108,negated_conjecture,(
% 2.03/1.46 ~(ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ zero_zero_int)),
% 2.03/1.46 inference(negated_conjecture,[status(cth)],[f107])).
% 2.03/1.46 thf(f107,conjecture,(
% 2.03/1.46 (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ zero_zero_int)),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',conj_0)).
% 2.03/1.46 thf(f911,plain,(
% 2.03/1.46 ($true = (ord_less_int @ (plus_plus_int @ one_one_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ pls))),
% 2.03/1.46 inference(forward_demodulation,[status(thm)],[f906,f481])).
% 2.03/1.46 thf(f481,plain,(
% 2.03/1.46 ( ! [X1 : int] : ((pls = (times_times_int @ pls @ X1))) )),
% 2.03/1.46 inference(equality_proxy_clausification,[status(thm)],[f480])).
% 2.03/1.46 thf(f480,plain,(
% 2.03/1.46 ( ! [X1 : int] : (((pls = (times_times_int @ pls @ X1)) = $true)) )),
% 2.03/1.46 inference(beta_eta_normalization,[status(thm)],[f479])).
% 2.03/1.46 thf(f479,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = ((^[Y0 : int]: (pls = (times_times_int @ pls @ Y0))) @ X1))) )),
% 2.03/1.46 inference(pi_clausification,[status(thm)],[f380])).
% 2.03/1.46 thf(f380,plain,(
% 2.03/1.46 ($true = (!! @ int @ (^[Y0 : int]: (pls = (times_times_int @ pls @ Y0)))))),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f218])).
% 2.03/1.46 thf(f218,plain,(
% 2.03/1.46 ($true = (!! @ int @ (^[Y0 : int]: (pls = (times_times_int @ pls @ Y0)))))),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f217])).
% 2.03/1.46 thf(f217,plain,(
% 2.03/1.46 ! [X0 : int] : (pls = (times_times_int @ pls @ X0))),
% 2.03/1.46 inference(rectify,[status(thm)],[f67])).
% 2.03/1.46 thf(f67,axiom,(
% 2.03/1.46 ! [X12 : int] : (pls = (times_times_int @ pls @ X12))),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_66_mult__Pls)).
% 2.03/1.46 thf(f906,plain,(
% 2.03/1.46 ((ord_less_int @ (plus_plus_int @ one_one_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ (times_times_int @ pls @ (plus_plus_int @ one_one_int @ (times_times_int @ (bit0 @ (bit0 @ (bit1 @ pls))) @ m)))) = $true)),
% 2.03/1.46 inference(backward_demodulation,[status(thm)],[f747,f895])).
% 2.03/1.46 thf(f895,plain,(
% 2.03/1.46 ( ! [X2 : int,X1 : int] : (((times_times_int @ X1 @ X2) = (times_times_int @ X2 @ X1))) )),
% 2.03/1.46 inference(equality_proxy_clausification,[status(thm)],[f894])).
% 2.03/1.46 thf(f894,plain,(
% 2.03/1.46 ( ! [X2 : int,X1 : int] : (($true = ((times_times_int @ X1 @ X2) = (times_times_int @ X2 @ X1)))) )),
% 2.03/1.46 inference(beta_eta_normalization,[status(thm)],[f893])).
% 2.03/1.46 thf(f893,plain,(
% 2.03/1.46 ( ! [X2 : int,X1 : int] : (($true = ((^[Y0 : int]: ((times_times_int @ X1 @ Y0) = (times_times_int @ Y0 @ X1))) @ X2))) )),
% 2.03/1.46 inference(pi_clausification,[status(thm)],[f878])).
% 2.03/1.46 thf(f878,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = (!! @ int @ (^[Y0 : int]: ((times_times_int @ X1 @ Y0) = (times_times_int @ Y0 @ X1)))))) )),
% 2.03/1.46 inference(beta_eta_normalization,[status(thm)],[f877])).
% 2.03/1.46 thf(f877,plain,(
% 2.03/1.46 ( ! [X1 : int] : (($true = ((^[Y0 : int]: (!! @ int @ (^[Y1 : int]: ((times_times_int @ Y0 @ Y1) = (times_times_int @ Y1 @ Y0))))) @ X1))) )),
% 2.03/1.46 inference(pi_clausification,[status(thm)],[f409])).
% 2.03/1.46 thf(f409,plain,(
% 2.03/1.46 ($true = (!! @ int @ (^[Y0 : int]: (!! @ int @ (^[Y1 : int]: ((times_times_int @ Y0 @ Y1) = (times_times_int @ Y1 @ Y0)))))))),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f178])).
% 2.03/1.46 thf(f178,plain,(
% 2.03/1.46 ($true = (!! @ int @ (^[Y0 : int]: (!! @ int @ (^[Y1 : int]: ((times_times_int @ Y0 @ Y1) = (times_times_int @ Y1 @ Y0)))))))),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f177])).
% 2.03/1.46 thf(f177,plain,(
% 2.03/1.46 ! [X0 : int,X1 : int] : ((times_times_int @ X1 @ X0) = (times_times_int @ X0 @ X1))),
% 2.03/1.46 inference(rectify,[status(thm)],[f26])).
% 2.03/1.46 thf(f26,axiom,(
% 2.03/1.46 ! [X12 : int,X14 : int] : ((times_times_int @ X14 @ X12) = (times_times_int @ X12 @ X14))),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_25_zmult__commute)).
% 2.03/1.46 thf(f747,plain,(
% 2.03/1.46 ($true = (ord_less_int @ (plus_plus_int @ one_one_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ (times_times_int @ (plus_plus_int @ one_one_int @ (times_times_int @ (bit0 @ (bit0 @ (bit1 @ pls))) @ m)) @ pls)))),
% 2.03/1.46 inference(forward_demodulation,[status(thm)],[f739,f735])).
% 2.03/1.46 thf(f739,plain,(
% 2.03/1.46 ($true = (ord_less_int @ (plus_plus_int @ one_one_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (bit0 @ (bit0 @ (bit1 @ pls))) @ m) @ one_one_int) @ pls)))),
% 2.03/1.46 inference(backward_demodulation,[status(thm)],[f478,f735])).
% 2.03/1.46 thf(f478,plain,(
% 2.03/1.46 ($true = (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (bit0 @ (bit0 @ (bit1 @ pls))) @ m) @ one_one_int) @ pls)))),
% 2.03/1.46 inference(forward_demodulation,[status(thm)],[f467,f465])).
% 2.03/1.46 thf(f467,plain,(
% 2.03/1.46 ($true = (ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ pls)))),
% 2.03/1.46 inference(backward_demodulation,[status(thm)],[f448,f465])).
% 2.03/1.46 thf(f448,plain,(
% 2.03/1.46 ((ord_less_int @ (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ (number_number_of_int @ pls))) = $true)),
% 2.03/1.46 inference(backward_demodulation,[status(thm)],[f431,f351])).
% 2.03/1.46 thf(f351,plain,(
% 2.03/1.46 ((times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) = (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int))),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f172])).
% 2.03/1.46 thf(f172,plain,(
% 2.03/1.46 ((times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) = (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int))),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f4])).
% 2.03/1.46 thf(f4,axiom,(
% 2.03/1.46 ((times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) = (plus_plus_int @ (power_power_int @ s @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) @ one_one_int))),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_3_t)).
% 2.03/1.46 thf(f431,plain,(
% 2.03/1.46 ((ord_less_int @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ (number_number_of_int @ pls))) = $true)),
% 2.03/1.46 inference(definition_unfolding,[status(thm)],[f376,f378])).
% 2.03/1.46 thf(f376,plain,(
% 2.03/1.46 ((ord_less_int @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ zero_zero_int)) = $true)),
% 2.03/1.46 inference(cnf_transformation,[status(thm)],[f214])).
% 2.03/1.46 thf(f214,plain,(
% 2.03/1.46 ((ord_less_int @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ zero_zero_int)) = $true)),
% 2.03/1.46 inference(fool_elimination,[status(thm)],[f213])).
% 2.03/1.46 thf(f213,plain,(
% 2.03/1.46 (ord_less_int @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ zero_zero_int))),
% 2.03/1.46 inference(rectify,[status(thm)],[f3])).
% 2.03/1.46 thf(f3,axiom,(
% 2.03/1.46 (ord_less_int @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ t) @ (times_times_int @ (plus_plus_int @ (times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls)))) @ m) @ one_one_int) @ zero_zero_int))),
% 2.03/1.46 file('/export/starexec/sandbox2/tmp/tmp.iTMIVAsqRB/DTF2THF_30683.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096)).
% 2.03/1.46 % SZS output end Proof for DTF2THF_30683
% 2.03/1.46 % (30810)------------------------------
% 2.03/1.46 % (30810)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.03/1.46 % (30810)Termination reason: Refutation
% 2.03/1.46
% 2.03/1.46 % (30810)Memory used [KB]: 6396
% 2.03/1.46 % (30810)Time elapsed: 0.051 s
% 2.03/1.46 % (30810)Instructions burned: 145 (million)
% 2.03/1.46 % (30810)------------------------------
% 2.03/1.46 % (30810)------------------------------
% 2.03/1.46 % (30798)Success in time 0.071 s
%------------------------------------------------------------------------------