%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SEU892^5 : TPTP v9.3.1. Released v4.0.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 : n014.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 10:49:11 AM UTC 2026
% Result : Theorem 30.90s 5.46s
% Output : CNFRefutation 30.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 1
% Syntax : Number of formulae : 30 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 169 ( 106 equ; 0 cnn)
% Maximal formula atoms : 5 ( 5 avg)
% Number of connectives : 657 ( 83 ~; 65 |; 10 &; 494 @)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 184 ( 184 >; 0 *; 0 +; 0 <<)
% Number of symbols : 334 ( 331 usr; 2 con; 0-6 aty)
% Number of variables : 203 ( 121 ^; 77 !; 5 ?; 203 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $tType ).
thf(tp_sK100_E,type,
sK100_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK101_E,type,
sK101_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK102_E,type,
sK102_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK103_E,type,
sK103_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK104_E,type,
sK104_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK105_E,type,
sK105_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK106_E,type,
sK106_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK107_E,type,
sK107_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK108_E,type,
sK108_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK109_E,type,
sK109_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK10_E,type,
sK10_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK110_E,type,
sK110_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK111_E,type,
sK111_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK112_E,type,
sK112_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK113_E,type,
sK113_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK114_E,type,
sK114_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK115_E,type,
sK115_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK116_E,type,
sK116_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK117_E,type,
sK117_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK118_E,type,
sK118_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK119_E,type,
sK119_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK11_E,type,
sK11_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK120_E,type,
sK120_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK121_E,type,
sK121_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK122_E,type,
sK122_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK123_E,type,
sK123_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK124_E,type,
sK124_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK125_E,type,
sK125_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK126_E,type,
sK126_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK127_E,type,
sK127_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK128_E,type,
sK128_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK129_E,type,
sK129_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK12_E,type,
sK12_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK130_E,type,
sK130_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK131_E,type,
sK131_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK132_E,type,
sK132_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK133_E,type,
sK133_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK134_E,type,
sK134_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK135_E,type,
sK135_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK136_E,type,
sK136_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK137_E,type,
sK137_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK138_E,type,
sK138_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK139_E,type,
sK139_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK13_E,type,
sK13_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK140_E,type,
sK140_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK141_E,type,
sK141_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK142_E,type,
sK142_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK143_E,type,
sK143_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK144_E,type,
sK144_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK145_E,type,
sK145_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK146_E,type,
sK146_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK147_E,type,
sK147_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK148_E,type,
sK148_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK149_E,type,
sK149_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK14_E,type,
sK14_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK150_E,type,
sK150_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK151_E,type,
sK151_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK152_E,type,
sK152_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK153_E,type,
sK153_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK154_E,type,
sK154_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK155_E,type,
sK155_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK156_E,type,
sK156_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK157_E,type,
sK157_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK158_E,type,
sK158_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK159_E,type,
sK159_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK15_E,type,
sK15_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK160_E,type,
sK160_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK161_E,type,
sK161_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK162_E,type,
sK162_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK163_E,type,
sK163_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK164_E,type,
sK164_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK165_E,type,
sK165_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK166_E,type,
sK166_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK167_E,type,
sK167_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK168_E,type,
sK168_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK169_E,type,
sK169_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK16_E,type,
sK16_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK170_E,type,
sK170_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK171_E,type,
sK171_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK172_E,type,
sK172_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK173_E,type,
sK173_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK174_E,type,
sK174_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK175_E,type,
sK175_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK176_E,type,
sK176_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK177_E,type,
sK177_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK178_E,type,
sK178_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK179_E,type,
sK179_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK17_E,type,
sK17_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK180_E,type,
sK180_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK181_E,type,
sK181_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK182_E,type,
sK182_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK183_E,type,
sK183_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK184_E,type,
sK184_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK185_E,type,
sK185_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK186_E,type,
sK186_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK187_E,type,
sK187_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK188_E,type,
sK188_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK189_E,type,
sK189_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK18_E,type,
sK18_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK190_E,type,
sK190_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK191_E,type,
sK191_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK192_E,type,
sK192_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK193_E,type,
sK193_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK194_E,type,
sK194_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK195_E,type,
sK195_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK196_E,type,
sK196_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK197_E,type,
sK197_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK198_E,type,
sK198_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK199_E,type,
sK199_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK19_E,type,
sK19_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK1_SY7,type,
sK1_SY7: ( ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK200_E,type,
sK200_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK201_E,type,
sK201_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK202_E,type,
sK202_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK203_E,type,
sK203_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK204_E,type,
sK204_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK205_E,type,
sK205_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK206_E,type,
sK206_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK207_E,type,
sK207_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK208_E,type,
sK208_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK209_E,type,
sK209_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK20_E,type,
sK20_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK210_E,type,
sK210_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK211_E,type,
sK211_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK212_E,type,
sK212_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK213_E,type,
sK213_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK214_E,type,
sK214_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK215_E,type,
sK215_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK216_E,type,
sK216_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK217_E,type,
sK217_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK218_E,type,
sK218_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK219_E,type,
sK219_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK21_E,type,
sK21_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK220_E,type,
sK220_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK221_E,type,
sK221_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK222_E,type,
sK222_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK223_E,type,
sK223_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK224_E,type,
sK224_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK225_E,type,
sK225_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK226_E,type,
sK226_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK227_E,type,
sK227_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK228_E,type,
sK228_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK229_E,type,
sK229_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK22_E,type,
sK22_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK230_E,type,
sK230_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK231_E,type,
sK231_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK232_E,type,
sK232_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK233_E,type,
sK233_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK234_E,type,
sK234_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK235_E,type,
sK235_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK236_E,type,
sK236_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK237_E,type,
sK237_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK238_E,type,
sK238_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK239_E,type,
sK239_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK23_E,type,
sK23_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK240_E,type,
sK240_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK241_E,type,
sK241_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK242_E,type,
sK242_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK243_E,type,
sK243_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK244_E,type,
sK244_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK245_E,type,
sK245_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK246_E,type,
sK246_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK247_E,type,
sK247_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK248_E,type,
sK248_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK249_E,type,
sK249_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK24_E,type,
sK24_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK250_E,type,
sK250_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK251_E,type,
sK251_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK252_E,type,
sK252_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK253_E,type,
sK253_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK254_E,type,
sK254_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK255_E,type,
sK255_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK256_E,type,
sK256_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK257_E,type,
sK257_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK258_E,type,
sK258_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK259_E,type,
sK259_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK25_E,type,
sK25_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK260_E,type,
sK260_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK261_E,type,
sK261_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK262_E,type,
sK262_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK263_E,type,
sK263_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK264_E,type,
sK264_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK265_E,type,
sK265_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK266_E,type,
sK266_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK267_E,type,
sK267_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK268_E,type,
sK268_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK269_E,type,
sK269_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK26_E,type,
sK26_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK270_E,type,
sK270_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK271_E,type,
sK271_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK272_E,type,
sK272_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK273_E,type,
sK273_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK274_E,type,
sK274_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK275_E,type,
sK275_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK276_E,type,
sK276_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK277_E,type,
sK277_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK278_E,type,
sK278_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK279_E,type,
sK279_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK27_E,type,
sK27_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK280_E,type,
sK280_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK281_E,type,
sK281_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK282_E,type,
sK282_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK283_E,type,
sK283_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK284_E,type,
sK284_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK285_E,type,
sK285_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK286_E,type,
sK286_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK287_E,type,
sK287_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK288_E,type,
sK288_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK289_E,type,
sK289_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK28_E,type,
sK28_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK290_E,type,
sK290_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK291_E,type,
sK291_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK292_E,type,
sK292_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK293_E,type,
sK293_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK294_E,type,
sK294_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK295_E,type,
sK295_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK296_E,type,
sK296_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK297_E,type,
sK297_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK298_E,type,
sK298_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK299_E,type,
sK299_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK29_E,type,
sK29_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK2_SY10,type,
sK2_SY10: ( ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK300_E,type,
sK300_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK301_E,type,
sK301_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK302_E,type,
sK302_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK303_E,type,
sK303_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK304_E,type,
sK304_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK305_E,type,
sK305_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK306_E,type,
sK306_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK307_E,type,
sK307_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK308_E,type,
sK308_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK309_E,type,
sK309_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK30_E,type,
sK30_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK310_E,type,
sK310_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK311_E,type,
sK311_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK312_E,type,
sK312_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK313_E,type,
sK313_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK314_E,type,
sK314_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK315_E,type,
sK315_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK316_E,type,
sK316_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK317_E,type,
sK317_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK318_E,type,
sK318_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK319_E,type,
sK319_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK31_E,type,
sK31_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK320_E,type,
sK320_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK321_E,type,
sK321_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK322_E,type,
sK322_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK323_E,type,
sK323_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK324_E,type,
sK324_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK325_E,type,
sK325_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK326_E,type,
sK326_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK327_E,type,
sK327_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK328_E,type,
sK328_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK329_E,type,
sK329_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK32_E,type,
sK32_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK330_E,type,
sK330_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK331_E,type,
sK331_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK33_E,type,
sK33_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK34_E,type,
sK34_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK35_E,type,
sK35_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK36_E,type,
sK36_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK37_E,type,
sK37_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK38_E,type,
sK38_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK39_E,type,
sK39_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > a ) > a > a ).
thf(tp_sK3_SY15,type,
sK3_SY15: ( ( a > a ) > ( a > a ) > $o ) > a ).
thf(tp_sK40_E,type,
sK40_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK41_E,type,
sK41_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK42_E,type,
sK42_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK43_E,type,
sK43_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK44_E,type,
sK44_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK45_E,type,
sK45_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK46_E,type,
sK46_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK47_E,type,
sK47_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK48_E,type,
sK48_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK49_E,type,
sK49_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK4_E,type,
sK4_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK50_E,type,
sK50_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK51_E,type,
sK51_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK52_E,type,
sK52_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK53_E,type,
sK53_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK54_E,type,
sK54_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK55_E,type,
sK55_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK56_E,type,
sK56_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK57_E,type,
sK57_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK58_E,type,
sK58_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK59_E,type,
sK59_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK5_E,type,
sK5_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK60_E,type,
sK60_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK61_E,type,
sK61_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK62_E,type,
sK62_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK63_E,type,
sK63_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK64_E,type,
sK64_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK65_E,type,
sK65_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK66_E,type,
sK66_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK67_E,type,
sK67_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK68_E,type,
sK68_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK69_E,type,
sK69_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK6_E,type,
sK6_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK70_E,type,
sK70_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK71_E,type,
sK71_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK72_E,type,
sK72_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK73_E,type,
sK73_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK74_E,type,
sK74_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK75_E,type,
sK75_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK76_E,type,
sK76_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK77_E,type,
sK77_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK78_E,type,
sK78_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK79_E,type,
sK79_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK7_E,type,
sK7_E: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK80_E,type,
sK80_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK81_E,type,
sK81_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK82_E,type,
sK82_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK83_E,type,
sK83_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK84_E,type,
sK84_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK85_E,type,
sK85_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK86_E,type,
sK86_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK87_E,type,
sK87_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK88_E,type,
sK88_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK89_E,type,
sK89_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK8_E,type,
sK8_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK90_E,type,
sK90_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK91_E,type,
sK91_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK92_E,type,
sK92_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK93_E,type,
sK93_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK94_E,type,
sK94_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK95_E,type,
sK95_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK96_E,type,
sK96_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK97_E,type,
sK97_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK98_E,type,
sK98_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK99_E,type,
sK99_E: ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(tp_sK9_E,type,
sK9_E: ( ( a > a ) > ( a > a ) > a ) > ( ( a > a ) > ( a > a ) > ( a > a ) > ( a > a ) > $o ) > a > a ).
thf(1,conjecture,
? [Xi: ( a > a ) > ( a > a ) > $o] :
( ! [Xg: a > a] :
( ( Xi @ Xg
@ ^ [Xx: a] : Xx )
& ( Xi @ Xg
@ ^ [Xx: a] : ( Xg @ ( Xg @ Xx ) ) ) )
& ! [Xf: a > a,Xy: a] :
( ( Xi
@ ^ [Xx: a] : Xy
@ Xf )
=> ( ( Xf @ Xy )
= Xy ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cX6104) ).
thf(2,negated_conjecture,
( ( ? [Xi: ( a > a ) > ( a > a ) > $o] :
( ! [Xg: a > a] :
( ( Xi @ Xg
@ ^ [Xx: a] : Xx )
& ( Xi @ Xg
@ ^ [Xx: a] : ( Xg @ ( Xg @ Xx ) ) ) )
& ! [Xf: a > a,Xy: a] :
( ( Xi
@ ^ [Xx: a] : Xy
@ Xf )
=> ( ( Xf @ Xy )
= Xy ) ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[1]) ).
thf(3,plain,
( ( ? [Xi: ( a > a ) > ( a > a ) > $o] :
( ! [Xg: a > a] :
( ( Xi @ Xg
@ ^ [Xx: a] : Xx )
& ( Xi @ Xg
@ ^ [Xx: a] : ( Xg @ ( Xg @ Xx ) ) ) )
& ! [Xf: a > a,Xy: a] :
( ( Xi
@ ^ [Xx: a] : Xy
@ Xf )
=> ( ( Xf @ Xy )
= Xy ) ) ) )
= $false ),
inference(unfold_def,[status(thm)],[2]) ).
thf(4,plain,
( ( ~ ? [Xi: ( a > a ) > ( a > a ) > $o] :
( ! [Xg: a > a] :
( ( Xi @ Xg
@ ^ [Xx: a] : Xx )
& ( Xi @ Xg
@ ^ [Xx: a] : ( Xg @ ( Xg @ Xx ) ) ) )
& ! [Xf: a > a,Xy: a] :
( ( Xi
@ ^ [Xx: a] : Xy
@ Xf )
=> ( ( Xf @ Xy )
= Xy ) ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[3]) ).
thf(5,plain,
( ( ~ ? [Xi: ( a > a ) > ( a > a ) > $o] :
( ! [Xg: a > a] :
( ( Xi @ Xg
@ ^ [Xx: a] : Xx )
& ( Xi @ Xg
@ ^ [Xx: a] : ( Xg @ ( Xg @ Xx ) ) ) )
& ! [Xf: a > a,Xy: a] :
( ( Xi
@ ^ [Xx: a] : Xy
@ Xf )
=> ( ( Xf @ Xy )
= Xy ) ) ) )
= $true ),
inference(copy,[status(thm)],[4]) ).
thf(6,plain,
( ( ~ ~ ! [SX0: ( a > a ) > ( a > a ) > $o] :
~ ~ ( ~ ! [SX1: a > a] :
~ ( ~ ( SX0 @ SX1
@ ^ [SX2: a] : SX2 )
| ~ ( SX0 @ SX1
@ ^ [SX2: a] : ( SX1 @ ( SX1 @ SX2 ) ) ) )
| ~ ! [SX1: a > a,SX2: a] :
( ~ ( SX0
@ ^ [SX3: a] : SX2
@ SX1 )
| ( ( SX1 @ SX2 )
= SX2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5]) ).
thf(7,plain,
( ( ~ ! [SX0: ( a > a ) > ( a > a ) > $o] :
~ ~ ( ~ ! [SX1: a > a] :
~ ( ~ ( SX0 @ SX1
@ ^ [SX2: a] : SX2 )
| ~ ( SX0 @ SX1
@ ^ [SX2: a] : ( SX1 @ ( SX1 @ SX2 ) ) ) )
| ~ ! [SX1: a > a,SX2: a] :
( ~ ( SX0
@ ^ [SX3: a] : SX2
@ SX1 )
| ( ( SX1 @ SX2 )
= SX2 ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[6]) ).
thf(8,plain,
( ( ! [SX0: ( a > a ) > ( a > a ) > $o] :
~ ~ ( ~ ! [SX1: a > a] :
~ ( ~ ( SX0 @ SX1
@ ^ [SX2: a] : SX2 )
| ~ ( SX0 @ SX1
@ ^ [SX2: a] : ( SX1 @ ( SX1 @ SX2 ) ) ) )
| ~ ! [SX1: a > a,SX2: a] :
( ~ ( SX0
@ ^ [SX3: a] : SX2
@ SX1 )
| ( ( SX1 @ SX2 )
= SX2 ) ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[7]) ).
thf(9,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ~ ~ ( ~ ! [SY7: a > a] :
~ ( ~ ( SV1 @ SY7
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ SY7
@ ^ [SX2: a] : ( SY7 @ ( SY7 @ SX2 ) ) ) )
| ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[8]) ).
thf(10,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ~ ( ~ ! [SY7: a > a] :
~ ( ~ ( SV1 @ SY7
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ SY7
@ ^ [SX2: a] : ( SY7 @ ( SY7 @ SX2 ) ) ) )
| ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[9]) ).
thf(11,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ~ ! [SY7: a > a] :
~ ( ~ ( SV1 @ SY7
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ SY7
@ ^ [SX2: a] : ( SY7 @ ( SY7 @ SX2 ) ) ) )
| ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[10]) ).
thf(12,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ~ ! [SY7: a > a] :
~ ( ~ ( SV1 @ SY7
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ SY7
@ ^ [SX2: a] : ( SY7 @ ( SY7 @ SX2 ) ) ) ) )
= $true )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[11]) ).
thf(13,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ! [SY7: a > a] :
~ ( ~ ( SV1 @ SY7
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ SY7
@ ^ [SX2: a] : ( SY7 @ ( SY7 @ SX2 ) ) ) ) )
= $false )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[12]) ).
thf(14,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ~ ( ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) ) ) )
= $false )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[13]) ).
thf(15,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
| ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) ) )
= $true )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[14]) ).
thf(16,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 ) )
= $true )
| ( ( ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) ) )
= $true )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[15]) ).
thf(17,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( ~ ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) ) )
= $true )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[16]) ).
thf(18,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( ~ ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[17]) ).
thf(19,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ! [SY10: a > a,SY11: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY11
@ SY10 )
| ( ( SY10 @ SY11 )
= SY11 ) ) )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[18]) ).
thf(20,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ! [SY15: a] :
( ~ ( SV1
@ ^ [SX3: a] : SY15
@ ( sK2_SY10 @ SV1 ) )
| ( ( sK2_SY10 @ SV1 @ SY15 )
= SY15 ) ) )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false ) ),
inference(extcnf_forall_neg,[status(esa)],[19]) ).
thf(21,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ~ ( SV1
@ ^ [SY17: a] : ( sK3_SY15 @ SV1 )
@ ( sK2_SY10 @ SV1 ) )
| ( ( sK2_SY10 @ SV1 @ ( sK3_SY15 @ SV1 ) )
= ( sK3_SY15 @ SV1 ) ) )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false ) ),
inference(extcnf_forall_neg,[status(esa)],[20]) ).
thf(22,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ~ ( SV1
@ ^ [SY17: a] : ( sK3_SY15 @ SV1 )
@ ( sK2_SY10 @ SV1 ) ) )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[21]) ).
thf(23,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( ( sK2_SY10 @ SV1 @ ( sK3_SY15 @ SV1 ) )
= ( sK3_SY15 @ SV1 ) )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[21]) ).
thf(24,plain,
! [SV1: ( a > a ) > ( a > a ) > $o] :
( ( ( SV1
@ ^ [SY17: a] : ( sK3_SY15 @ SV1 )
@ ( sK2_SY10 @ SV1 ) )
= $true )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SX2: a] : SX2 )
= $false )
| ( ( SV1 @ ( sK1_SY7 @ SV1 )
@ ^ [SY14: a] : ( sK1_SY7 @ SV1 @ ( sK1_SY7 @ SV1 @ SY14 ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[22]) ).
thf(25,plain,
! [SV2: ( a > a ) > ( a > a ) > $o] :
( ( ( ( sK2_SY10 @ SV2 @ ( sK3_SY15 @ SV2 ) )
= ( sK3_SY15 @ SV2 ) )
= $false )
| ( ( SV2 @ ( sK1_SY7 @ SV2 )
@ ^ [SX0: a] : SX0 )
= $false )
| ( ( SV2 @ ( sK1_SY7 @ SV2 )
@ ^ [SX0: a] : ( sK1_SY7 @ SV2 @ ( sK1_SY7 @ SV2 @ SX0 ) ) )
= $false ) ),
inference(rename,[status(thm)],[23]) ).
thf(26,plain,
! [SV3: ( a > a ) > ( a > a ) > $o] :
( ( ( SV3
@ ^ [SX0: a] : ( sK3_SY15 @ SV3 )
@ ( sK2_SY10 @ SV3 ) )
= $true )
| ( ( SV3 @ ( sK1_SY7 @ SV3 )
@ ^ [SX0: a] : SX0 )
= $false )
| ( ( SV3 @ ( sK1_SY7 @ SV3 )
@ ^ [SX0: a] : ( sK1_SY7 @ SV3 @ ( sK1_SY7 @ SV3 @ SX0 ) ) )
= $false ) ),
inference(rename,[status(thm)],[24]) ).
thf(33,plain,
! [SV3: ( a > a ) > ( a > a ) > $o,SV2: ( a > a ) > ( a > a ) > $o] :
( ( ( ( SV3
@ ^ [SX0: a] : ( sK3_SY15 @ SV3 )
@ ( sK2_SY10 @ SV3 ) )
= ( ( sK2_SY10 @ SV2 @ ( sK3_SY15 @ SV2 ) )
= ( sK3_SY15 @ SV2 ) ) )
= $false )
| ( ( SV3 @ ( sK1_SY7 @ SV3 )
@ ^ [SX0: a] : SX0 )
= $false )
| ( ( SV3 @ ( sK1_SY7 @ SV3 )
@ ^ [SX0: a] : ( sK1_SY7 @ SV3 @ ( sK1_SY7 @ SV3 @ SX0 ) ) )
= $false )
| ( ( SV2 @ ( sK1_SY7 @ SV2 )
@ ^ [SX0: a] : SX0 )
= $false )
| ( ( SV2 @ ( sK1_SY7 @ SV2 )
@ ^ [SX0: a] : ( sK1_SY7 @ SV2 @ ( sK1_SY7 @ SV2 @ SX0 ) ) )
= $false ) ),
inference(res,[status(thm)],[26,25]) ).
thf(217,plain,
! [SV105: ( a > a ) > ( a > a ) > a,SV536: ( a > a ) > ( a > a ) > a] :
( ( ( ( SV536
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] :
( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ ( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ SX0 ) ) )
= ( SV105
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] :
( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ ( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ SX0 ) ) ) )
= $false )
| ( ( ( SV536
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] : SX0 )
= ( SV105
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] : SX0 ) )
= $false )
| ( ( ( SV536
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] :
( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ ( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ SX0 ) ) )
= ( SV105
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] :
( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ ( sK1_SY7
@ ^ [SX1: a > a,SX2: a > a] :
( ( SX1 @ ( SX2 @ ( SV536 @ SX1 @ SX2 ) ) )
= ( SX2 @ ( SX1 @ ( SV105 @ SX1 @ SX2 ) ) ) )
@ SX0 ) ) ) )
= $false )
| ( ( ( SV536
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] : SX0 )
= ( SV105
@ ( sK1_SY7
@ ^ [SX0: a > a,SX1: a > a] :
( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) )
= ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )
@ ^ [SX0: a] : SX0 ) )
= $false ) ),
inference(extuni,[status(esa)],[33:[bind(SV2,$thf( ^ [SX0: a > a] : ^ [SX1: a > a] : ( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) ) = ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) )),bind(SV3,$thf( ^ [SX0: a > a] : ^ [SX1: a > a] : ( ( SX0 @ ( SX1 @ ( SV536 @ SX0 @ SX1 ) ) ) = ( SX1 @ ( SX0 @ ( SV105 @ SX0 @ SX1 ) ) ) ) ))]]) ).
thf(218,plain,
$false = $true,
inference(flexflex,[status(thm)],[217]) ).
thf(219,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[218]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU892^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % 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.08/0.20 % Computer : n014.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Oct 6 15:37:41 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.90/5.46
% 30.90/5.46 No.of.Axioms: 0
% 30.90/5.46
% 30.90/5.46 Length.of.Defs: 0
% 30.90/5.46
% 30.90/5.46 Contains.Choice.Funs: false
% 30.90/5.46 ............................................................
% 30.90/5.46
% 30.90/5.46 ********************************
% 30.90/5.46 * All subproblems solved! *
% 30.90/5.46 ********************************
% 30.90/5.46 % 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:218,loop_count:2,foatp_calls:1,translation:fof_full)
% 30.90/5.46
% 30.90/5.46 %**** Beginning of derivation protocol ****
% 30.90/5.46 % SZS output start CNFRefutation
% See solution above
% 30.90/5.47
% 30.90/5.47 %**** End of derivation protocol ****
% 30.90/5.47 %**** no. of clauses in derivation: 30 ****
% 30.90/5.47 %**** clause counter: 218 ****
% 30.90/5.47
% 30.90/5.47 % 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:218,loop_count:2,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------