%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SEU667^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:46:10 AM UTC 2026
% Result : Theorem 167.87s 33.98s
% Output : CNFRefutation 167.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 21 unt; 0 typ; 3 def)
% Number of atoms : 124 ( 39 equ; 0 cnn)
% Maximal formula atoms : 2 ( 5 avg)
% Number of connectives : 491 ( 121 ~; 27 |; 27 &; 313 @)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 32 ( 32 >; 0 *; 0 +; 0 <<)
% Number of symbols : 280 ( 277 usr; 5 con; 0-9 aty)
% Number of variables : 111 ( 30 ^; 63 !; 18 ?; 111 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_breln,type,
breln: $i > $i > $i > $o ).
thf(tp_cartprod,type,
cartprod: $i > $i > $i ).
thf(tp_dpsetconstr,type,
dpsetconstr: $i > $i > ( $i > $i > $o ) > $i ).
thf(tp_dpsetconstrSub,type,
dpsetconstrSub: $o ).
thf(tp_dsetconstr,type,
dsetconstr: $i > ( $i > $o ) > $i ).
thf(tp_in,type,
in: $i > $i > $o ).
thf(tp_kpair,type,
kpair: $i > $i > $i ).
thf(tp_sK100_E,type,
sK100_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK101_E,type,
sK101_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK102_E,type,
sK102_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK103_E,type,
sK103_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK104_E,type,
sK104_E: $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 ).
thf(tp_sK106_E,type,
sK106_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 > $o ) > $i ).
thf(tp_sK107_E,type,
sK107_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 > $o ) > $i ).
thf(tp_sK108_E,type,
sK108_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK109_E,type,
sK109_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK10_E,type,
sK10_E: ( $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 ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK111_E,type,
sK111_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > $i > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK112_E,type,
sK112_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK113_E,type,
sK113_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK114_E,type,
sK114_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK115_E,type,
sK115_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK116_E,type,
sK116_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK117_E,type,
sK117_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK118_E,type,
sK118_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK119_E,type,
sK119_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK11_E,type,
sK11_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK120_E,type,
sK120_E: $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 ).
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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK124_E,type,
sK124_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK125_E,type,
sK125_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $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 > $o ) > $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 > $o ) > $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 ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK12_E,type,
sK12_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK130_E,type,
sK130_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK131_E,type,
sK131_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK132_E,type,
sK132_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK133_E,type,
sK133_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK134_E,type,
sK134_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK135_E,type,
sK135_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK136_E,type,
sK136_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > $i ).
thf(tp_sK137_E,type,
sK137_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > $i ).
thf(tp_sK138_E,type,
sK138_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 > $o ) > $i ).
thf(tp_sK139_E,type,
sK139_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 > $o ) > $i ).
thf(tp_sK13_E,type,
sK13_E: ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK140_E,type,
sK140_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK141_E,type,
sK141_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK142_E,type,
sK142_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK143_E,type,
sK143_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > $i > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK144_E,type,
sK144_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK145_E,type,
sK145_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK146_E,type,
sK146_E: $i > ( $i > $i > $o ) > $i > $i ).
thf(tp_sK147_E,type,
sK147_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK148_E,type,
sK148_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK149_E,type,
sK149_E: $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 > $o ) > $i ).
thf(tp_sK150_E,type,
sK150_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > $i ).
thf(tp_sK151_E,type,
sK151_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 > $o ) > $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 > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK153_E,type,
sK153_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK154_E,type,
sK154_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK155_E,type,
sK155_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $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 ).
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 > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK159_E,type,
sK159_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK15_E,type,
sK15_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK160_E,type,
sK160_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK162_E,type,
sK162_E: ( $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 > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 > $i > $i > $i > $o ) > $i ).
thf(tp_sK165_E,type,
sK165_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK166_E,type,
sK166_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK167_E,type,
sK167_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $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 ).
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 > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK16_E,type,
sK16_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $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 > $o ) > $i ).
thf(tp_sK171_E,type,
sK171_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK172_E,type,
sK172_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK174_E,type,
sK174_E: ( $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 > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK177_E,type,
sK177_E: $i > ( $i > $i > $o ) > $i > $i ).
thf(tp_sK178_E,type,
sK178_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK179_E,type,
sK179_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK17_E,type,
sK17_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK180_E,type,
sK180_E: $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 ).
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 > $i > $i > $i > $i > $i > $o ) > $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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK184_E,type,
sK184_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK185_E,type,
sK185_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK187_E,type,
sK187_E: ( $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 > $o ) > $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 > $o ) > $i ).
thf(tp_sK18_E,type,
sK18_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK190_E,type,
sK190_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK191_E,type,
sK191_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK193_E,type,
sK193_E: ( $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 > $o ) > $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 > $o ) > $i ).
thf(tp_sK196_E,type,
sK196_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK197_E,type,
sK197_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK199_E,type,
sK199_E: ( $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 > $o ) > $i ).
thf(tp_sK1_SY0,type,
sK1_SY0: $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 > $o ) > $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 > $o ) > $i ).
thf(tp_sK202_E,type,
sK202_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK203_E,type,
sK203_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK204_E,type,
sK204_E: $i > $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 > $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 ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK207_E,type,
sK207_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 > $o ) > $i ).
thf(tp_sK208_E,type,
sK208_E: $i > ( $i > $i > $o ) > $i > $i ).
thf(tp_sK209_E,type,
sK209_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK20_E,type,
sK20_E: ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK210_E,type,
sK210_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK211_E,type,
sK211_E: $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 ).
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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK214_E,type,
sK214_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 > $o ) > $i ).
thf(tp_sK215_E,type,
sK215_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK216_E,type,
sK216_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK217_E,type,
sK217_E: $i > $i > ( $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 > $i > $i ) > ( $i > $i > $i ) > $i > $i > $i ).
thf(tp_sK219_E,type,
sK219_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 > $o ) > $i ).
thf(tp_sK21_E,type,
sK21_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $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 > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK221_E,type,
sK221_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK222_E,type,
sK222_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK224_E,type,
sK224_E: ( $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 > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK227_E,type,
sK227_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK228_E,type,
sK228_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK229_E,type,
sK229_E: $i > $i > ( $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 > $i > $o ) > $i ).
thf(tp_sK230_E,type,
sK230_E: ( $i > $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 > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK232_E,type,
sK232_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 > $o ) > $i ).
thf(tp_sK233_E,type,
sK233_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK234_E,type,
sK234_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK236_E,type,
sK236_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > $i > $i ).
thf(tp_sK237_E,type,
sK237_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 > $o ) > $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 > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK239_E,type,
sK239_E: $i > ( $i > $i > $o ) > $i > $i ).
thf(tp_sK23_E,type,
sK23_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK240_E,type,
sK240_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK241_E,type,
sK241_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK242_E,type,
sK242_E: $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 ).
thf(tp_sK244_E,type,
sK244_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 > $o ) > $i ).
thf(tp_sK245_E,type,
sK245_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 > $o ) > $i ).
thf(tp_sK246_E,type,
sK246_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK247_E,type,
sK247_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK248_E,type,
sK248_E: $i > $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 > $i > $i ).
thf(tp_sK24_E,type,
sK24_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $i > $i > $o ) > $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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK252_E,type,
sK252_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK253_E,type,
sK253_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK255_E,type,
sK255_E: ( $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 > $o ) > $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 > $o ) > $i ).
thf(tp_sK258_E,type,
sK258_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK259_E,type,
sK259_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK25_E,type,
sK25_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK260_E,type,
sK260_E: $i > $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 > $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 ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK263_E,type,
sK263_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 > $o ) > $i ).
thf(tp_sK264_E,type,
sK264_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK265_E,type,
sK265_E: $i > $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ).
thf(tp_sK267_E,type,
sK267_E: ( $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 > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK269_E,type,
sK269_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 > $o ) > $i ).
thf(tp_sK26_E,type,
sK26_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK27_E,type,
sK27_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > $i ).
thf(tp_sK28_E,type,
sK28_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > $i ).
thf(tp_sK29_E,type,
sK29_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK2_SY57,type,
sK2_SY57: $i ).
thf(tp_sK30_E,type,
sK30_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK31_E,type,
sK31_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK32_E,type,
sK32_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK33_E,type,
sK33_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK34_E,type,
sK34_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK35_E,type,
sK35_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK36_E,type,
sK36_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK37_E,type,
sK37_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK38_E,type,
sK38_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK39_E,type,
sK39_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK3_SY62,type,
sK3_SY62: $i > $i > $o ).
thf(tp_sK40_E,type,
sK40_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK41_E,type,
sK41_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK42_E,type,
sK42_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK43_E,type,
sK43_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK44_E,type,
sK44_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK45_E,type,
sK45_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK46_E,type,
sK46_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK47_E,type,
sK47_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK48_E,type,
sK48_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK49_E,type,
sK49_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK4_E,type,
sK4_E: ( $i > $i > $o ) > $i ).
thf(tp_sK50_E,type,
sK50_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK51_E,type,
sK51_E: ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK52_E,type,
sK52_E: ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK53_E,type,
sK53_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK54_E,type,
sK54_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK55_E,type,
sK55_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK56_E,type,
sK56_E: ( $i > $i > $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK57_E,type,
sK57_E: ( $i > $i > $o ) > $i > $i > $i ).
thf(tp_sK58_E,type,
sK58_E: ( $i > $i > $o ) > $i > $i > $i ).
thf(tp_sK59_E,type,
sK59_E: ( $i > $i > $o ) > $i > $i ).
thf(tp_sK5_E,type,
sK5_E: ( $i > $i > $o ) > $i ).
thf(tp_sK60_E,type,
sK60_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK61_E,type,
sK61_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK62_E,type,
sK62_E: $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 ).
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 > $o ) > $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 > $o ) > $i ).
thf(tp_sK66_E,type,
sK66_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK67_E,type,
sK67_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK68_E,type,
sK68_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK69_E,type,
sK69_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK6_E,type,
sK6_E: ( $i > $i > $o ) > $i ).
thf(tp_sK70_E,type,
sK70_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK71_E,type,
sK71_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK72_E,type,
sK72_E: ( $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 ).
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 > $o ) > $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 > $o ) > $i ).
thf(tp_sK76_E,type,
sK76_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK77_E,type,
sK77_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK78_E,type,
sK78_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK79_E,type,
sK79_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK7_E,type,
sK7_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK80_E,type,
sK80_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK81_E,type,
sK81_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK82_E,type,
sK82_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK83_E,type,
sK83_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK84_E,type,
sK84_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK85_E,type,
sK85_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK86_E,type,
sK86_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK87_E,type,
sK87_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK88_E,type,
sK88_E: $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 ).
thf(tp_sK8_E,type,
sK8_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $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 ) > ( $i > $i > $i > $i > $i > $i > $o ) > $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 > $i ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK92_E,type,
sK92_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK93_E,type,
sK93_E: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK94_E,type,
sK94_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK95_E,type,
sK95_E: ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > ( $i > $i > $i ) > $i > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK96_E,type,
sK96_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK97_E,type,
sK97_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 > $o ) > ( $i > $i > $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK98_E,type,
sK98_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK99_E,type,
sK99_E: $i > ( $i > $i > $i ) > ( $i > $i > $i > $i > $o ) > $i ).
thf(tp_sK9_E,type,
sK9_E: ( $i > $i > $i ) > ( $i > $i > $i > $i > $i ) > $i ).
thf(tp_subset,type,
subset: $i > $i > $o ).
thf(breln,definition,
( breln
= ( ^ [A: $i,B: $i,C: $i] : ( subset @ C @ ( cartprod @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',breln) ).
thf(dpsetconstr,definition,
( dpsetconstr
= ( ^ [A: $i,B: $i,Xphi: $i > $i > $o] :
( dsetconstr @ ( cartprod @ A @ B )
@ ^ [Xu: $i] :
? [Xx: $i] :
( ( in @ Xx @ A )
& ? [Xy: $i] :
( ( in @ Xy @ B )
& ( Xphi @ Xx @ Xy )
& ( Xu
= ( kpair @ Xx @ Xy ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dpsetconstr) ).
thf(dpsetconstrSub,definition,
( dpsetconstrSub
= ( ! [A: $i,B: $i,Xphi: $i > $i > $o] :
( subset
@ ( dpsetconstr @ A @ B
@ ^ [Xx: $i,Xy: $i] : ( Xphi @ Xx @ Xy ) )
@ ( cartprod @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dpsetconstrSub) ).
thf(1,conjecture,
( dpsetconstrSub
=> ! [A: $i,B: $i,Xphi: $i > $i > $o] :
( breln @ A @ B
@ ( dpsetconstr @ A @ B
@ ^ [Xx: $i,Xy: $i] : ( Xphi @ Xx @ Xy ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',setOfPairsIsBReln) ).
thf(2,negated_conjecture,
( ( dpsetconstrSub
=> ! [A: $i,B: $i,Xphi: $i > $i > $o] :
( breln @ A @ B
@ ( dpsetconstr @ A @ B
@ ^ [Xx: $i,Xy: $i] : ( Xphi @ Xx @ Xy ) ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[1]) ).
thf(3,plain,
( ( ! [SY21: $i,SY22: $i,SY23: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SY21 @ SY22 )
@ ^ [SY35: $i] :
? [SY36: $i] :
( ( in @ SY36 @ SY21 )
& ? [SY37: $i] :
( ( in @ SY37 @ SY22 )
& ( SY23 @ SY36 @ SY37 )
& ( SY35
= ( kpair @ SY36 @ SY37 ) ) ) ) )
@ ( cartprod @ SY21 @ SY22 ) )
=> ! [SY0: $i,SY1: $i,SY2: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SY0 @ SY1 )
@ ^ [SY17: $i] :
? [SY18: $i] :
( ( in @ SY18 @ SY0 )
& ? [SY19: $i] :
( ( in @ SY19 @ SY1 )
& ( SY2 @ SY18 @ SY19 )
& ( SY17
= ( kpair @ SY18 @ SY19 ) ) ) ) )
@ ( cartprod @ SY0 @ SY1 ) ) )
= $false ),
inference(unfold_def,[status(thm)],[2,breln,dpsetconstr,dpsetconstrSub]) ).
thf(4,plain,
( ( ! [SY21: $i,SY22: $i,SY23: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SY21 @ SY22 )
@ ^ [SY35: $i] :
? [SY36: $i] :
( ( in @ SY36 @ SY21 )
& ? [SY37: $i] :
( ( in @ SY37 @ SY22 )
& ( SY23 @ SY36 @ SY37 )
& ( SY35
= ( kpair @ SY36 @ SY37 ) ) ) ) )
@ ( cartprod @ SY21 @ SY22 ) ) )
= $true ),
inference(standard_cnf,[status(thm)],[3]) ).
thf(5,plain,
( ( ! [SY0: $i,SY1: $i,SY2: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SY0 @ SY1 )
@ ^ [SY17: $i] :
? [SY18: $i] :
( ( in @ SY18 @ SY0 )
& ? [SY19: $i] :
( ( in @ SY19 @ SY1 )
& ( SY2 @ SY18 @ SY19 )
& ( SY17
= ( kpair @ SY18 @ SY19 ) ) ) ) )
@ ( cartprod @ SY0 @ SY1 ) ) )
= $false ),
inference(standard_cnf,[status(thm)],[3]) ).
thf(6,plain,
( ( ~ ! [SY0: $i,SY1: $i,SY2: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SY0 @ SY1 )
@ ^ [SY17: $i] :
? [SY18: $i] :
( ( in @ SY18 @ SY0 )
& ? [SY19: $i] :
( ( in @ SY19 @ SY1 )
& ( SY2 @ SY18 @ SY19 )
& ( SY17
= ( kpair @ SY18 @ SY19 ) ) ) ) )
@ ( cartprod @ SY0 @ SY1 ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[5]) ).
thf(7,plain,
( ( ~ ( subset
@ ( dsetconstr @ ( cartprod @ sK1_SY0 @ sK2_SY57 )
@ ^ [SY66: $i] :
? [SY67: $i] :
( ( in @ SY67 @ sK1_SY0 )
& ? [SY68: $i] :
( ( in @ SY68 @ sK2_SY57 )
& ( sK3_SY62 @ SY67 @ SY68 )
& ( SY66
= ( kpair @ SY67 @ SY68 ) ) ) ) )
@ ( cartprod @ sK1_SY0 @ sK2_SY57 ) ) )
= $true ),
inference(extcnf_combined,[status(esa)],[6]) ).
thf(8,plain,
( ( ! [SY21: $i,SY22: $i,SY23: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SY21 @ SY22 )
@ ^ [SY35: $i] :
? [SY36: $i] :
( ( in @ SY36 @ SY21 )
& ? [SY37: $i] :
( ( in @ SY37 @ SY22 )
& ( SY23 @ SY36 @ SY37 )
& ( SY35
= ( kpair @ SY36 @ SY37 ) ) ) ) )
@ ( cartprod @ SY21 @ SY22 ) ) )
= $true ),
inference(copy,[status(thm)],[4]) ).
thf(9,plain,
( ( ~ ( subset
@ ( dsetconstr @ ( cartprod @ sK1_SY0 @ sK2_SY57 )
@ ^ [SY66: $i] :
? [SY67: $i] :
( ( in @ SY67 @ sK1_SY0 )
& ? [SY68: $i] :
( ( in @ SY68 @ sK2_SY57 )
& ( sK3_SY62 @ SY67 @ SY68 )
& ( SY66
= ( kpair @ SY67 @ SY68 ) ) ) ) )
@ ( cartprod @ sK1_SY0 @ sK2_SY57 ) ) )
= $true ),
inference(copy,[status(thm)],[7]) ).
thf(10,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SX0 @ SX1 )
@ ^ [SX3: $i] :
~ ! [SX4: $i] :
~ ~ ( ~ ( in @ SX4 @ SX0 )
| ~ ~ ! [SX5: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX5 @ SX1 )
| ~ ( SX2 @ SX4 @ SX5 ) )
| ( SX3
!= ( kpair @ SX4 @ SX5 ) ) ) ) )
@ ( cartprod @ SX0 @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[8,breln,dpsetconstr,dpsetconstrSub]) ).
thf(11,plain,
( ( ~ ( subset
@ ( dsetconstr @ ( cartprod @ sK1_SY0 @ sK2_SY57 )
@ ^ [SX0: $i] :
~ ! [SX1: $i] :
~ ~ ( ~ ( in @ SX1 @ sK1_SY0 )
| ~ ~ ! [SX2: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX2 @ sK2_SY57 )
| ~ ( sK3_SY62 @ SX1 @ SX2 ) )
| ( SX0
!= ( kpair @ SX1 @ SX2 ) ) ) ) )
@ ( cartprod @ sK1_SY0 @ sK2_SY57 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[9,breln,dpsetconstr,dpsetconstrSub]) ).
thf(12,plain,
! [SV1: $i] :
( ( ! [SY69: $i,SY70: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SV1 @ SY69 )
@ ^ [SY71: $i] :
~ ! [SY72: $i] :
~ ~ ( ~ ( in @ SY72 @ SV1 )
| ~ ~ ! [SX5: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX5 @ SY69 )
| ~ ( SY70 @ SY72 @ SX5 ) )
| ( SY71
!= ( kpair @ SY72 @ SX5 ) ) ) ) )
@ ( cartprod @ SV1 @ SY69 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[10]) ).
thf(13,plain,
( ( subset
@ ( dsetconstr @ ( cartprod @ sK1_SY0 @ sK2_SY57 )
@ ^ [SX0: $i] :
~ ! [SX1: $i] :
~ ~ ( ~ ( in @ SX1 @ sK1_SY0 )
| ~ ~ ! [SX2: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX2 @ sK2_SY57 )
| ~ ( sK3_SY62 @ SX1 @ SX2 ) )
| ( SX0
!= ( kpair @ SX1 @ SX2 ) ) ) ) )
@ ( cartprod @ sK1_SY0 @ sK2_SY57 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[11]) ).
thf(14,plain,
! [SV2: $i,SV1: $i] :
( ( ! [SY74: $i > $i > $o] :
( subset
@ ( dsetconstr @ ( cartprod @ SV1 @ SV2 )
@ ^ [SY75: $i] :
~ ! [SY76: $i] :
~ ~ ( ~ ( in @ SY76 @ SV1 )
| ~ ~ ! [SY77: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SY77 @ SV2 )
| ~ ( SY74 @ SY76 @ SY77 ) )
| ( SY75
!= ( kpair @ SY76 @ SY77 ) ) ) ) )
@ ( cartprod @ SV1 @ SV2 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[12]) ).
thf(15,plain,
! [SV3: $i > $i > $o,SV2: $i,SV1: $i] :
( ( subset
@ ( dsetconstr @ ( cartprod @ SV1 @ SV2 )
@ ^ [SY78: $i] :
~ ! [SY79: $i] :
~ ~ ( ~ ( in @ SY79 @ SV1 )
| ~ ~ ! [SY80: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SY80 @ SV2 )
| ~ ( SV3 @ SY79 @ SY80 ) )
| ( SY78
!= ( kpair @ SY79 @ SY80 ) ) ) ) )
@ ( cartprod @ SV1 @ SV2 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[14]) ).
thf(16,plain,
! [SV4: $i > $i > $o,SV5: $i,SV6: $i] :
( ( subset
@ ( dsetconstr @ ( cartprod @ SV6 @ SV5 )
@ ^ [SX0: $i] :
~ ! [SX1: $i] :
~ ~ ( ~ ( in @ SX1 @ SV6 )
| ~ ~ ! [SX2: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX2 @ SV5 )
| ~ ( SV4 @ SX1 @ SX2 ) )
| ( SX0
!= ( kpair @ SX1 @ SX2 ) ) ) ) )
@ ( cartprod @ SV6 @ SV5 ) )
= $true ),
inference(rename,[status(thm)],[15]) ).
thf(17,plain,
! [SV4: $i > $i > $o,SV5: $i,SV6: $i] :
( ( ( subset
@ ( dsetconstr @ ( cartprod @ SV6 @ SV5 )
@ ^ [SX0: $i] :
~ ! [SX1: $i] :
~ ~ ( ~ ( in @ SX1 @ SV6 )
| ~ ~ ! [SX2: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX2 @ SV5 )
| ~ ( SV4 @ SX1 @ SX2 ) )
| ( SX0
!= ( kpair @ SX1 @ SX2 ) ) ) ) )
@ ( cartprod @ SV6 @ SV5 ) )
= ( subset
@ ( dsetconstr @ ( cartprod @ sK1_SY0 @ sK2_SY57 )
@ ^ [SX0: $i] :
~ ! [SX1: $i] :
~ ~ ( ~ ( in @ SX1 @ sK1_SY0 )
| ~ ~ ! [SX2: $i] :
~ ~ ( ~ ~ ( ~ ( in @ SX2 @ sK2_SY57 )
| ~ ( sK3_SY62 @ SX1 @ SX2 ) )
| ( SX0
!= ( kpair @ SX1 @ SX2 ) ) ) ) )
@ ( cartprod @ sK1_SY0 @ sK2_SY57 ) ) )
= $false ),
inference(res,[status(thm)],[16,13]) ).
thf(149,plain,
$false = $true,
inference(extuni,[status(esa)],[17:[bind(SV4,$thf( ^ [SX0: $i] : ^ [SX1: $i] : ( sK3_SY62 @ SX0 @ SX1 ) )),bind(SV5,$thf( sK2_SY57 )),bind(SV6,$thf( sK1_SY0 ))]]) ).
thf(150,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[149]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU667^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.18 % Computer : n008.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Oct 6 15:31:09 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 167.87/33.98
% 167.87/33.98 No.of.Axioms: 0
% 167.87/33.98
% 167.87/33.98 Length.of.Defs: 683
% 167.87/33.98
% 167.87/33.98 Contains.Choice.Funs: false
% 167.87/33.98 ..eprover: CPU time limit exceeded, terminating
% 167.87/33.98 .............................................................................................................
% 167.87/33.98
% 167.87/33.98 ********************************
% 167.87/33.98 * All subproblems solved! *
% 167.87/33.98 ********************************
% 167.87/33.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:15,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:149,loop_count:2,foatp_calls:1,translation:fof_full)
% 167.87/33.98
% 167.87/33.98 %**** Beginning of derivation protocol ****
% 167.87/33.98 % SZS output start CNFRefutation
% See solution above
% 167.87/33.98
% 167.87/33.98 %**** End of derivation protocol ****
% 167.87/33.98 %**** no. of clauses in derivation: 19 ****
% 167.87/33.98 %**** clause counter: 149 ****
% 167.87/33.98
% 167.87/33.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:15,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:149,loop_count:2,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------