LEO-II---2.3.1.THM-CRf.s

%------------------------------------------------------------------------------
% File     : LEO-II---2.3.1
% Problem  : SYO551^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Oct  7 11:08:42 AM UTC 2026

% Result   : Theorem 63.20s 12.87s
% Output   : CNFRefutation 63.20s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   13
%            Number of leaves      :    1
% Syntax   : Number of formulae    :   14 (  14 unt;   0 typ;   0 def)
%            Number of atoms       :   38 (  24 equ;   0 cnn)
%            Maximal formula atoms :    1 (   2 avg)
%            Number of connectives :   25 (   9   ~;   0   |;   0   &;  16   @)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    3 (   1 avg)
%            Number of types       :    1 (   0 usr)
%            Number of type conns  :   46 (  46   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :  410 ( 407 usr;  11 con; 0-9 aty)
%            Number of variables   :   22 (   0   ^;  17   !;   5   ?;  22   :)

% Comments : 
%------------------------------------------------------------------------------
thf(tp_sK100_E,type,
    sK100_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK101_E,type,
    sK101_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK102_E,type,
    sK102_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK103_E,type,
    sK103_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK104_E,type,
    sK104_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK105_E,type,
    sK105_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK106_E,type,
    sK106_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK107_E,type,
    sK107_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK108_E,type,
    sK108_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK109_E,type,
    sK109_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK10_E,type,
    sK10_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK110_E,type,
    sK110_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK111_E,type,
    sK111_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK112_E,type,
    sK112_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK113_E,type,
    sK113_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK114_E,type,
    sK114_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK115_E,type,
    sK115_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK116_E,type,
    sK116_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK117_E,type,
    sK117_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK118_E,type,
    sK118_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK119_E,type,
    sK119_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK11_E,type,
    sK11_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK120_E,type,
    sK120_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK121_E,type,
    sK121_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK122_E,type,
    sK122_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK123_E,type,
    sK123_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK124_E,type,
    sK124_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK125_E,type,
    sK125_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK126_E,type,
    sK126_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK127_E,type,
    sK127_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK128_E,type,
    sK128_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK129_E,type,
    sK129_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK12_E,type,
    sK12_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK130_E,type,
    sK130_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK131_E,type,
    sK131_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK132_E,type,
    sK132_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK133_E,type,
    sK133_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK134_E,type,
    sK134_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK135_E,type,
    sK135_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK136_E,type,
    sK136_E: $i > $i ).

thf(tp_sK137_E,type,
    sK137_E: $i ).

thf(tp_sK138_E,type,
    sK138_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK139_E,type,
    sK139_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK13_E,type,
    sK13_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK140_E,type,
    sK140_E: $i > $i ).

thf(tp_sK141_E,type,
    sK141_E: $i ).

thf(tp_sK142_E,type,
    sK142_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK143_E,type,
    sK143_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK144_E,type,
    sK144_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK145_E,type,
    sK145_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK146_E,type,
    sK146_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK147_E,type,
    sK147_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK148_E,type,
    sK148_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK149_E,type,
    sK149_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK14_E,type,
    sK14_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK150_E,type,
    sK150_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK151_E,type,
    sK151_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK152_E,type,
    sK152_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK153_E,type,
    sK153_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK154_E,type,
    sK154_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK155_E,type,
    sK155_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK156_E,type,
    sK156_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK157_E,type,
    sK157_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK158_E,type,
    sK158_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK159_E,type,
    sK159_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK15_E,type,
    sK15_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK160_E,type,
    sK160_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK161_E,type,
    sK161_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK162_E,type,
    sK162_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK163_E,type,
    sK163_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK164_E,type,
    sK164_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK165_E,type,
    sK165_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK166_E,type,
    sK166_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK167_E,type,
    sK167_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK168_E,type,
    sK168_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK169_E,type,
    sK169_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK16_E,type,
    sK16_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK170_E,type,
    sK170_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK171_E,type,
    sK171_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK172_E,type,
    sK172_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK173_E,type,
    sK173_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK174_E,type,
    sK174_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK175_E,type,
    sK175_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK176_E,type,
    sK176_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK177_E,type,
    sK177_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK178_E,type,
    sK178_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK179_E,type,
    sK179_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK17_E,type,
    sK17_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK180_E,type,
    sK180_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK181_E,type,
    sK181_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK182_E,type,
    sK182_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK183_E,type,
    sK183_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK184_E,type,
    sK184_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK185_E,type,
    sK185_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK186_E,type,
    sK186_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK187_E,type,
    sK187_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK188_E,type,
    sK188_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK189_E,type,
    sK189_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK18_E,type,
    sK18_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK190_E,type,
    sK190_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK191_E,type,
    sK191_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK192_E,type,
    sK192_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK193_E,type,
    sK193_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK194_E,type,
    sK194_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK195_E,type,
    sK195_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK196_E,type,
    sK196_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK197_E,type,
    sK197_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK198_E,type,
    sK198_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK199_E,type,
    sK199_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK19_E,type,
    sK19_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK1_SY2,type,
    sK1_SY2: ( ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK200_E,type,
    sK200_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK201_E,type,
    sK201_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK202_E,type,
    sK202_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK203_E,type,
    sK203_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK204_E,type,
    sK204_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK205_E,type,
    sK205_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK206_E,type,
    sK206_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK207_E,type,
    sK207_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK208_E,type,
    sK208_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK209_E,type,
    sK209_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK20_E,type,
    sK20_E: $i > $i ).

thf(tp_sK210_E,type,
    sK210_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK211_E,type,
    sK211_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK212_E,type,
    sK212_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK213_E,type,
    sK213_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK214_E,type,
    sK214_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK215_E,type,
    sK215_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK216_E,type,
    sK216_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK217_E,type,
    sK217_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK218_E,type,
    sK218_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK219_E,type,
    sK219_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK21_E,type,
    sK21_E: $i ).

thf(tp_sK220_E,type,
    sK220_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK221_E,type,
    sK221_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK222_E,type,
    sK222_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK223_E,type,
    sK223_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK224_E,type,
    sK224_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK225_E,type,
    sK225_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK226_E,type,
    sK226_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK227_E,type,
    sK227_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK228_E,type,
    sK228_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK229_E,type,
    sK229_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK22_E,type,
    sK22_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK230_E,type,
    sK230_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK231_E,type,
    sK231_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK232_E,type,
    sK232_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK233_E,type,
    sK233_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK234_E,type,
    sK234_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK235_E,type,
    sK235_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK236_E,type,
    sK236_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK237_E,type,
    sK237_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK238_E,type,
    sK238_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK239_E,type,
    sK239_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK23_E,type,
    sK23_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK240_E,type,
    sK240_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK241_E,type,
    sK241_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK242_E,type,
    sK242_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK243_E,type,
    sK243_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK244_E,type,
    sK244_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK245_E,type,
    sK245_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK246_E,type,
    sK246_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK247_E,type,
    sK247_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK248_E,type,
    sK248_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK249_E,type,
    sK249_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK24_E,type,
    sK24_E: $i > $i ).

thf(tp_sK250_E,type,
    sK250_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK251_E,type,
    sK251_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK252_E,type,
    sK252_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK253_E,type,
    sK253_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK254_E,type,
    sK254_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK255_E,type,
    sK255_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK256_E,type,
    sK256_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK257_E,type,
    sK257_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK258_E,type,
    sK258_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK259_E,type,
    sK259_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK25_E,type,
    sK25_E: $i ).

thf(tp_sK260_E,type,
    sK260_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK261_E,type,
    sK261_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK262_E,type,
    sK262_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK263_E,type,
    sK263_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK264_E,type,
    sK264_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK265_E,type,
    sK265_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK266_E,type,
    sK266_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK267_E,type,
    sK267_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK268_E,type,
    sK268_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK269_E,type,
    sK269_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK26_E,type,
    sK26_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK270_E,type,
    sK270_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK271_E,type,
    sK271_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK272_E,type,
    sK272_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK273_E,type,
    sK273_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK274_E,type,
    sK274_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK275_E,type,
    sK275_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK276_E,type,
    sK276_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK277_E,type,
    sK277_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK278_E,type,
    sK278_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK279_E,type,
    sK279_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK27_E,type,
    sK27_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK280_E,type,
    sK280_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK281_E,type,
    sK281_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK282_E,type,
    sK282_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK283_E,type,
    sK283_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK284_E,type,
    sK284_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK285_E,type,
    sK285_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK286_E,type,
    sK286_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK287_E,type,
    sK287_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK288_E,type,
    sK288_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK289_E,type,
    sK289_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK28_E,type,
    sK28_E: $i > $i ).

thf(tp_sK290_E,type,
    sK290_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK291_E,type,
    sK291_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK292_E,type,
    sK292_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK293_E,type,
    sK293_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK294_E,type,
    sK294_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK295_E,type,
    sK295_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK296_E,type,
    sK296_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK297_E,type,
    sK297_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK298_E,type,
    sK298_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK299_E,type,
    sK299_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK29_E,type,
    sK29_E: $i ).

thf(tp_sK2_SV2,type,
    sK2_SV2: ( ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK300_E,type,
    sK300_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK301_E,type,
    sK301_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK302_E,type,
    sK302_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK303_E,type,
    sK303_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK304_E,type,
    sK304_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK305_E,type,
    sK305_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK306_E,type,
    sK306_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK307_E,type,
    sK307_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK308_E,type,
    sK308_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK309_E,type,
    sK309_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK30_E,type,
    sK30_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK310_E,type,
    sK310_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK311_E,type,
    sK311_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK312_E,type,
    sK312_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK313_E,type,
    sK313_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK314_E,type,
    sK314_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK315_E,type,
    sK315_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK316_E,type,
    sK316_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK317_E,type,
    sK317_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK318_E,type,
    sK318_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK319_E,type,
    sK319_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK31_E,type,
    sK31_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK320_E,type,
    sK320_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK321_E,type,
    sK321_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK322_E,type,
    sK322_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK323_E,type,
    sK323_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK324_E,type,
    sK324_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK325_E,type,
    sK325_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK326_E,type,
    sK326_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK327_E,type,
    sK327_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK328_E,type,
    sK328_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK329_E,type,
    sK329_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK32_E,type,
    sK32_E: $i > $i ).

thf(tp_sK330_E,type,
    sK330_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK331_E,type,
    sK331_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK332_E,type,
    sK332_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK333_E,type,
    sK333_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK334_E,type,
    sK334_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK335_E,type,
    sK335_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK336_E,type,
    sK336_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK337_E,type,
    sK337_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK338_E,type,
    sK338_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK339_E,type,
    sK339_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK33_E,type,
    sK33_E: $i ).

thf(tp_sK340_E,type,
    sK340_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK341_E,type,
    sK341_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK342_E,type,
    sK342_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK343_E,type,
    sK343_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK344_E,type,
    sK344_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK345_E,type,
    sK345_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK346_E,type,
    sK346_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK347_E,type,
    sK347_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK348_E,type,
    sK348_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK349_E,type,
    sK349_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK34_E,type,
    sK34_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK350_E,type,
    sK350_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK351_E,type,
    sK351_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK352_E,type,
    sK352_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK353_E,type,
    sK353_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK354_E,type,
    sK354_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK355_E,type,
    sK355_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK356_E,type,
    sK356_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK357_E,type,
    sK357_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK358_E,type,
    sK358_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK359_E,type,
    sK359_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK35_E,type,
    sK35_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK360_E,type,
    sK360_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK361_E,type,
    sK361_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK362_E,type,
    sK362_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK363_E,type,
    sK363_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK364_E,type,
    sK364_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK365_E,type,
    sK365_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK366_E,type,
    sK366_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK367_E,type,
    sK367_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK368_E,type,
    sK368_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK369_E,type,
    sK369_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK36_E,type,
    sK36_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK370_E,type,
    sK370_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK371_E,type,
    sK371_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK372_E,type,
    sK372_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK373_E,type,
    sK373_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK374_E,type,
    sK374_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK375_E,type,
    sK375_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK376_E,type,
    sK376_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK377_E,type,
    sK377_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK378_E,type,
    sK378_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK379_E,type,
    sK379_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK37_E,type,
    sK37_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK380_E,type,
    sK380_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK381_E,type,
    sK381_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK382_E,type,
    sK382_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK383_E,type,
    sK383_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK384_E,type,
    sK384_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK385_E,type,
    sK385_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK386_E,type,
    sK386_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK387_E,type,
    sK387_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK388_E,type,
    sK388_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK389_E,type,
    sK389_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK38_E,type,
    sK38_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK390_E,type,
    sK390_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK391_E,type,
    sK391_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK392_E,type,
    sK392_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK393_E,type,
    sK393_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK394_E,type,
    sK394_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK395_E,type,
    sK395_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK396_E,type,
    sK396_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK397_E,type,
    sK397_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK398_E,type,
    sK398_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK399_E,type,
    sK399_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK39_E,type,
    sK39_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK3_E,type,
    sK3_E: ( ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK400_E,type,
    sK400_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK401_E,type,
    sK401_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK402_E,type,
    sK402_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK403_E,type,
    sK403_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK404_E,type,
    sK404_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK405_E,type,
    sK405_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK406_E,type,
    sK406_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK407_E,type,
    sK407_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK40_E,type,
    sK40_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK41_E,type,
    sK41_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK42_E,type,
    sK42_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK43_E,type,
    sK43_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK44_E,type,
    sK44_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK45_E,type,
    sK45_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK46_E,type,
    sK46_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK47_E,type,
    sK47_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK48_E,type,
    sK48_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK49_E,type,
    sK49_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK4_E,type,
    sK4_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK50_E,type,
    sK50_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK51_E,type,
    sK51_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK52_E,type,
    sK52_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK53_E,type,
    sK53_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK54_E,type,
    sK54_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK55_E,type,
    sK55_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK56_E,type,
    sK56_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK57_E,type,
    sK57_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK58_E,type,
    sK58_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK59_E,type,
    sK59_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK5_E,type,
    sK5_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK60_E,type,
    sK60_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK61_E,type,
    sK61_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK62_E,type,
    sK62_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK63_E,type,
    sK63_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK64_E,type,
    sK64_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK65_E,type,
    sK65_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK66_E,type,
    sK66_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK67_E,type,
    sK67_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK68_E,type,
    sK68_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK69_E,type,
    sK69_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK6_E,type,
    sK6_E: $i > $i ).

thf(tp_sK70_E,type,
    sK70_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK71_E,type,
    sK71_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK72_E,type,
    sK72_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK73_E,type,
    sK73_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK74_E,type,
    sK74_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK75_E,type,
    sK75_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK76_E,type,
    sK76_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK77_E,type,
    sK77_E: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK78_E,type,
    sK78_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK79_E,type,
    sK79_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK7_E,type,
    sK7_E: $i ).

thf(tp_sK80_E,type,
    sK80_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK81_E,type,
    sK81_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK82_E,type,
    sK82_E: $i > $i ).

thf(tp_sK83_E,type,
    sK83_E: $i ).

thf(tp_sK84_E,type,
    sK84_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK85_E,type,
    sK85_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK86_E,type,
    sK86_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK87_E,type,
    sK87_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK88_E,type,
    sK88_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK89_E,type,
    sK89_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK8_E,type,
    sK8_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK90_E,type,
    sK90_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK91_E,type,
    sK91_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK92_E,type,
    sK92_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK93_E,type,
    sK93_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK94_E,type,
    sK94_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK95_E,type,
    sK95_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK96_E,type,
    sK96_E: $i > $i ).

thf(tp_sK97_E,type,
    sK97_E: $i ).

thf(tp_sK98_E,type,
    sK98_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i > $i ).

thf(tp_sK99_E,type,
    sK99_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(tp_sK9_E,type,
    sK9_E: ( ( $i > $i ) > $i > ( $i > $i ) > $i > ( $i > $i ) > $i > $i ) > $i ).

thf(1,conjecture,
    ? [F: ( $i > $i ) > $i > $i] :
    ! [X: $i > $i] :
      ( ( F @ X )
      = X ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',claim) ).

thf(2,negated_conjecture,
    ( ( ? [F: ( $i > $i ) > $i > $i] :
        ! [X: $i > $i] :
          ( ( F @ X )
          = X ) )
    = $false ),
    inference(negate_conjecture,[status(cth)],[1]) ).

thf(3,plain,
    ( ( ? [F: ( $i > $i ) > $i > $i] :
        ! [X: $i > $i] :
          ( ( F @ X )
          = X ) )
    = $false ),
    inference(unfold_def,[status(thm)],[2]) ).

thf(4,plain,
    ( ( ~ ? [F: ( $i > $i ) > $i > $i] :
          ! [X: $i > $i] :
            ( ( F @ X )
            = X ) )
    = $true ),
    inference(polarity_switch,[status(thm)],[3]) ).

thf(5,plain,
    ( ( ~ ? [F: ( $i > $i ) > $i > $i] :
          ! [X: $i > $i] :
            ( ( F @ X )
            = X ) )
    = $true ),
    inference(copy,[status(thm)],[4]) ).

thf(6,plain,
    ( ( ~ ~ ! [SX0: ( $i > $i ) > $i > $i] :
              ~ ! [SX1: $i > $i] :
                  ( ( SX0 @ SX1 )
                  = SX1 ) )
    = $true ),
    inference(unfold_def,[status(thm)],[5]) ).

thf(7,plain,
    ( ( ~ ! [SX0: ( $i > $i ) > $i > $i] :
            ~ ! [SX1: $i > $i] :
                ( ( SX0 @ SX1 )
                = SX1 ) )
    = $false ),
    inference(extcnf_not_pos,[status(thm)],[6]) ).

thf(8,plain,
    ( ( ! [SX0: ( $i > $i ) > $i > $i] :
          ~ ! [SX1: $i > $i] :
              ( ( SX0 @ SX1 )
              = SX1 ) )
    = $true ),
    inference(extcnf_not_neg,[status(thm)],[7]) ).

thf(9,plain,
    ! [SV1: ( $i > $i ) > $i > $i] :
      ( ( ~ ! [SY2: $i > $i] :
              ( ( SV1 @ SY2 )
              = SY2 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8]) ).

thf(10,plain,
    ! [SV1: ( $i > $i ) > $i > $i] :
      ( ( ! [SY2: $i > $i] :
            ( ( SV1 @ SY2 )
            = SY2 ) )
      = $false ),
    inference(extcnf_not_pos,[status(thm)],[9]) ).

thf(11,plain,
    ! [SV1: ( $i > $i ) > $i > $i] :
      ( ( ( SV1 @ ( sK1_SY2 @ SV1 ) )
        = ( sK1_SY2 @ SV1 ) )
      = $false ),
    inference(extcnf_forall_neg,[status(esa)],[10]) ).

thf(13,plain,
    ! [SV1: ( $i > $i ) > $i > $i] :
      ( ( ( SV1 @ ( sK1_SY2 @ SV1 ) )
        = ( sK1_SY2 @ SV1 ) )
      = $false ),
    inference(extcnf_equal_neg,[status(thm)],[11]) ).

thf(342,plain,
    $false = $true,
    inference(extuni,[status(esa)],[13:[bind(SV1,$thf( ^ [SX0: $i > $i] : ^ [SX1: $i] : ( SX0 @ SX1 ) ))]]) ).

thf(343,plain,
    $false,
    inference(solved_all_splits,[solved_all_splits(join,[])],[342]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SYO551^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04  % Command  : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.15  % Computer : n010.cluster.edu
% 0.10/0.15  % Model    : x86_64 x86_64
% 0.10/0.15  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.15  % Memory   : 8046.5625MB
% 0.10/0.15  % OS       : Linux 6.8.0-71-generic
% 0.10/0.15  % CPULimit : 300
% 0.10/0.15  % WCLimit  : 300
% 0.10/0.15  % DateTime : Tue Oct  6 17:42:25 UTC 2026
% 0.10/0.16  % CPUTime  : 
% 0.10/0.16  Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 63.20/12.87  
% 63.20/12.87   No.of.Axioms: 0
% 63.20/12.87  
% 63.20/12.87   Length.of.Defs: 0
% 63.20/12.87  
% 63.20/12.87   Contains.Choice.Funs: false
% 63.20/12.87  ..................................................................................................................................
% 63.20/12.87  
% 63.20/12.87  ********************************
% 63.20/12.87  *   All subproblems solved!    *
% 63.20/12.87  ********************************
% 63.20/12.87  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:0,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:342,loop_count:0,foatp_calls:1,translation:fof_full)
% 63.20/12.87  
% 63.20/12.87  %**** Beginning of derivation protocol ****
% 63.20/12.87  % SZS output start CNFRefutation
% See solution above
% 63.20/12.87  
% 63.20/12.87  %**** End of derivation protocol ****
% 63.20/12.87  %**** no. of clauses in derivation: 14 ****
% 63.20/12.87  %**** clause counter: 342 ****
% 63.20/12.87  
% 63.20/12.87  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:0,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:342,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------