%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP128^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 Sep 30 08:10:48 AM UTC 2026
% Result : Theorem 1.55s 0.50s
% Output : Refutation 1.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 3
% Syntax : Number of formulae : 29 ( 29 unt; 0 typ; 0 def)
% Number of atoms : 85 ( 38 equ; 0 cnn)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 217 ( 9 ~; 0 |; 0 &; 192 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 2 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 10 ( 10 >; 0 *; 0 +; 0 <<)
% Number of symbols : 682 ( 678 usr; 6 con; 0-7 aty)
% ( 16 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 35 ( 25 ^; 10 !; 0 ?; 35 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
multiset_b: $tType ).
thf(type_def_6,type,
multiset_a: $tType ).
thf(type_def_7,type,
fset_b: $tType ).
thf(type_def_8,type,
fset_a: $tType ).
thf(type_def_9,type,
set_d: $tType ).
thf(type_def_10,type,
set_c: $tType ).
thf(type_def_11,type,
set_b: $tType ).
thf(type_def_12,type,
set_a: $tType ).
thf(type_def_13,type,
d: $tType ).
thf(type_def_14,type,
c: $tType ).
thf(type_def_15,type,
b: $tType ).
thf(type_def_16,type,
a: $tType ).
thf(type_def_17,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
bNF_re19414301_d_d_o: ( ( ( c > c ) > ( c > c ) > $o ) > ( ( d > d ) > ( d > d ) > $o ) > $o ) > ( ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( b > d > d ) > ( b > d > d ) > $o ) > $o ) > ( ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > ( a > c > c ) > $o ) > ( ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_1,type,
bNF_re674980784_d_d_o: ( ( ( c > c ) > ( c > c ) > $o ) > ( ( d > d ) > ( d > d ) > $o ) > $o ) > ( ( ( a > c > c ) > $o ) > ( ( b > d > d ) > $o ) > $o ) > ( ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > $o ) > ( ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_2,type,
bNF_re1867846365_a_a_o: ( ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > $o ) > ( ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ) > ( ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_3,type,
bNF_re708047067_a_b_o: ( ( ( c > c ) > ( c > c ) > $o ) > ( a > b > $o ) > $o ) > ( ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ) > ( ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_4,type,
bNF_re145798749_a_a_o: ( ( ( c > c ) > ( d > d ) > $o ) > ( a > a > $o ) > $o ) > ( ( ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ) > ( ( ( c > c ) > ( d > d ) > $o ) > ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_5,type,
bNF_re1133483099_a_b_o: ( ( ( c > c ) > ( d > d ) > $o ) > ( a > b > $o ) > $o ) > ( ( ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ) > ( ( ( c > c ) > ( d > d ) > $o ) > ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_6,type,
bNF_re141854397_b_d_d: ( ( ( c > c ) > c > c ) > ( ( d > d ) > d > d ) > $o ) > ( ( ( a > c > c ) > a > c > c ) > ( ( b > d > d ) > b > d > d ) > $o ) > ( ( ( c > c ) > c > c ) > ( a > c > c ) > a > c > c ) > ( ( ( d > d ) > d > d ) > ( b > d > d ) > b > d > d ) > $o ).
thf(func_def_7,type,
bNF_re35019871_b_d_d: ( ( ( c > c ) > a ) > ( ( d > d ) > b ) > $o ) > ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( c > c ) > a ) > a > c > c ) > ( ( ( d > d ) > b ) > b > d > d ) > $o ).
thf(func_def_8,type,
bNF_re1177671453_a_a_a: ( ( ( c > c ) > a ) > ( a > a ) > $o ) > ( ( ( c > c ) > a ) > ( a > a ) > $o ) > ( ( ( c > c ) > a ) > ( c > c ) > a ) > ( ( a > a ) > a > a ) > $o ).
thf(func_def_9,type,
bNF_re1238578079_d_d_d: ( ( ( c > c ) > c ) > ( ( d > d ) > d ) > $o ) > ( ( ( a > c > c ) > c > c ) > ( ( b > d > d ) > d > d ) > $o ) > ( ( ( c > c ) > c ) > ( a > c > c ) > c > c ) > ( ( ( d > d ) > d ) > ( b > d > d ) > d > d ) > $o ).
thf(func_def_10,type,
bNF_re1209333166_c_b_d: ( ( ( c > c ) > c ) > ( ( d > d ) > d ) > $o ) > ( ( a > c ) > ( b > d ) > $o ) > ( ( ( c > c ) > c ) > a > c ) > ( ( ( d > d ) > d ) > b > d ) > $o ).
thf(func_def_11,type,
bNF_re323253981_b_b_b: ( ( ( d > d ) > b ) > ( b > b ) > $o ) > ( ( ( d > d ) > b ) > ( b > b ) > $o ) > ( ( ( d > d ) > b ) > ( d > d ) > b ) > ( ( b > b ) > b > b ) > $o ).
thf(func_def_12,type,
bNF_re1403739741_a_a_o: ( ( a > a > $o ) > ( a > a > $o ) > $o ) > ( ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_13,type,
bNF_re1165460699_a_b_o: ( ( a > a > $o ) > ( a > b > $o ) > $o ) > ( ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > ( ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_14,type,
bNF_re1310167325_a_a_o: ( ( a > a > $o ) > ( b > a > $o ) > $o ) > ( ( ( a > a ) > ( a > a ) > $o ) > ( ( a > b ) > ( a > a ) > $o ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > ( ( b > a > $o ) > ( a > b ) > ( a > a ) > $o ) > $o ).
thf(func_def_15,type,
bNF_re2129955100_d_d_o: ( ( a > a > $o ) > ( b > b > $o ) > $o ) > ( ( ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > $o ) > ( ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > $o ) > $o ) > ( ( a > a > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > $o ) > ( ( b > b > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_16,type,
bNF_re1071888283_a_b_o: ( ( a > a > $o ) > ( b > b > $o ) > $o ) > ( ( ( a > a ) > ( a > a ) > $o ) > ( ( a > b ) > ( a > b ) > $o ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > ( ( b > b > $o ) > ( a > b ) > ( a > b ) > $o ) > $o ).
thf(func_def_17,type,
bNF_re231976415_a_a_o: ( ( a > b > $o ) > ( a > a > $o ) > $o ) > ( ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ) > ( ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ) > ( ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_18,type,
bNF_re2141181021_a_b_o: ( ( a > b > $o ) > ( a > b > $o ) > $o ) > ( ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ) > ( ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ) > ( ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_19,type,
bNF_re880840541_a_c_c: ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( ( a > a ) > a > c > c ) > ( ( a > a ) > a > c > c ) > $o ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > $o ).
thf(func_def_20,type,
bNF_re1311853791_b_c_c: ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( ( a > a ) > a > c > c ) > ( ( b > a ) > b > c > c ) > $o ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > ( ( a > c > c ) > ( b > a ) > b > c > c ) > $o ).
thf(func_def_21,type,
bNF_re978949211_a_c_c: ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( ( b > a ) > b > c > c ) > ( ( a > a ) > a > c > c ) > $o ) > ( ( a > c > c ) > ( b > a ) > b > c > c ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > $o ).
thf(func_def_22,type,
bNF_re1409962461_b_c_c: ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( ( b > a ) > b > c > c ) > ( ( b > a ) > b > c > c ) > $o ) > ( ( a > c > c ) > ( b > a ) > b > c > c ) > ( ( a > c > c ) > ( b > a ) > b > c > c ) > $o ).
thf(func_def_23,type,
bNF_re27458217_c_c_c: ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( ( a > c > c ) > c > c ) > ( ( a > c > c ) > c > c ) > $o ).
thf(func_def_24,type,
bNF_re1955249705_c_d_d: ( ( a > c > c ) > ( a > d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( ( a > c > c ) > c > c ) > ( ( a > d > d ) > d > d ) > $o ).
thf(func_def_25,type,
bNF_re1684125987_a_a_o: ( ( a > c > c ) > ( a > a ) > $o ) > ( ( ( a > c > c ) > $o ) > ( ( a > a ) > $o ) > $o ) > ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_26,type,
bNF_re364411746_a_b_o: ( ( a > c > c ) > ( a > a ) > $o ) > ( ( ( a > c > c ) > $o ) > ( ( a > b ) > $o ) > $o ) > ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_27,type,
bNF_re1652452067_a_a_o: ( ( a > c > c ) > ( a > a ) > $o ) > ( ( ( a > d > d ) > $o ) > ( ( a > a ) > $o ) > $o ) > ( ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_28,type,
bNF_re332737826_a_b_o: ( ( a > c > c ) > ( a > a ) > $o ) > ( ( ( a > d > d ) > $o ) > ( ( a > b ) > $o ) > $o ) > ( ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_29,type,
bNF_re2074539676_a_o_o: ( ( a > c > c ) > ( a > a ) > $o ) > ( $o > $o > $o ) > ( ( a > c > c ) > $o ) > ( ( a > a ) > $o ) > $o ).
thf(func_def_30,type,
bNF_re1256092317_b_o_o: ( ( a > c > c ) > ( a > b ) > $o ) > ( $o > $o > $o ) > ( ( a > c > c ) > $o ) > ( ( a > b ) > $o ) > $o ).
thf(func_def_31,type,
bNF_re387831090_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( ( c > c ) > a ) > a > c > c ) > ( ( ( d > d ) > b ) > b > d > d ) > $o ) > ( ( a > c > c ) > ( ( c > c ) > a ) > a > c > c ) > ( ( b > d > d ) > ( ( d > d ) > b ) > b > d > d ) > $o ).
thf(func_def_32,type,
bNF_re364486559_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( a > c > c ) > ( ( c > c ) > a ) > a > c > c ) > ( ( b > d > d ) > ( ( d > d ) > b ) > b > d > d ) > $o ) > ( ( a > c > c ) > ( a > c > c ) > ( ( c > c ) > a ) > a > c > c ) > ( ( b > d > d ) > ( b > d > d ) > ( ( d > d ) > b ) > b > d > d ) > $o ).
thf(func_def_33,type,
bNF_re1855937521_d_d_o: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( a > c > c ) > $o ) > ( ( b > d > d ) > $o ) > $o ) > ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( b > d > d ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_34,type,
bNF_re631104669_a_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( a > a ) > a > c > c ) > ( ( a > b ) > a > d > d ) > $o ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > ( ( b > d > d ) > ( a > b ) > a > d > d ) > $o ).
thf(func_def_35,type,
bNF_re1062117919_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( a > a ) > a > c > c ) > ( ( b > b ) > b > d > d ) > $o ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > $o ).
thf(func_def_36,type,
bNF_re1160226589_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( b > a ) > b > c > c ) > ( ( b > b ) > b > d > d ) > $o ) > ( ( a > c > c ) > ( b > a ) > b > c > c ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > $o ).
thf(func_def_37,type,
bNF_re2120361759_d_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( c > a ) > c > c > c ) > ( ( d > b ) > d > d > d ) > $o ) > ( ( a > c > c ) > ( c > a ) > c > c > c ) > ( ( b > d > d ) > ( d > b ) > d > d > d ) > $o ).
thf(func_def_38,type,
bNF_re727696351_d_b_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( ( c > c ) > ( ( c > c ) > c ) > a > c ) > ( ( d > d ) > ( ( d > d ) > d ) > b > d ) > $o ) > ( ( a > c > c ) > ( c > c ) > ( ( c > c ) > c ) > a > c ) > ( ( b > d > d ) > ( d > d ) > ( ( d > d ) > d ) > b > d ) > $o ).
thf(func_def_39,type,
bNF_re1424479610_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( a > ( c > c ) > a > c > c ) > ( b > ( d > d ) > b > d > d ) > $o ) > ( ( a > c > c ) > a > ( c > c ) > a > c > c ) > ( ( b > d > d ) > b > ( d > d ) > b > d > d ) > $o ).
thf(func_def_40,type,
bNF_re692482399_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( a > c > c ) > a > c > c ) > ( ( b > d > d ) > b > d > d ) > $o ).
thf(func_def_41,type,
bNF_re84044842_c_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( ( a > c > c ) > c > c ) > ( ( b > d > d ) > d > d ) > $o ).
thf(func_def_42,type,
bNF_re1501709470_d_o_o: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( $o > $o > $o ) > ( ( a > c > c ) > $o ) > ( ( b > d > d ) > $o ) > $o ).
thf(func_def_43,type,
bNF_re1620723804_a_o_o: ( ( a > d > d ) > ( a > a ) > $o ) > ( $o > $o > $o ) > ( ( a > d > d ) > $o ) > ( ( a > a ) > $o ) > $o ).
thf(func_def_44,type,
bNF_re802276445_b_o_o: ( ( a > d > d ) > ( a > b ) > $o ) > ( $o > $o > $o ) > ( ( a > d > d ) > $o ) > ( ( a > b ) > $o ) > $o ).
thf(func_def_45,type,
bNF_re1503602041_a_a_a: ( ( a > a ) > ( a > a ) > $o ) > ( ( ( ( c > c ) > a ) > ( c > c ) > a ) > ( ( a > a ) > a > a ) > $o ) > ( ( a > a ) > ( ( c > c ) > a ) > ( c > c ) > a ) > ( ( a > a ) > ( a > a ) > a > a ) > $o ).
thf(func_def_46,type,
bNF_re1258259453_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 ) > $o ).
thf(func_def_47,type,
bNF_re1900831913_a_a_o: ( ( a > a ) > ( a > a ) > $o ) > ( ( ( a > a ) > $o ) > ( ( a > a ) > $o ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_48,type,
bNF_re581117672_a_b_o: ( ( a > a ) > ( a > a ) > $o ) > ( ( ( a > a ) > $o ) > ( ( a > b ) > $o ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_49,type,
bNF_re984549674_a_a_o: ( ( a > a ) > ( a > a ) > $o ) > ( ( ( a > b ) > $o ) > ( ( a > a ) > $o ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > $o ).
thf(func_def_50,type,
bNF_re1812319081_a_b_o: ( ( a > a ) > ( a > a ) > $o ) > ( ( ( a > b ) > $o ) > ( ( a > b ) > $o ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > $o ).
thf(func_def_51,type,
bNF_re1691224489_a_c_c: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > a ) > a > c > c ) > ( ( a > a ) > a > c > c ) > $o ).
thf(func_def_52,type,
bNF_re1690311157_a_a_a: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > a > a ) > ( ( a > a ) > a > a ) > $o ).
thf(func_def_53,type,
bNF_re1698572662_a_a_b: ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > a > a ) > ( ( a > a ) > a > b ) > $o ).
thf(func_def_54,type,
bNF_re134330537_a_o_o: ( ( a > a ) > ( a > a ) > $o ) > ( $o > $o > $o ) > ( ( a > a ) > $o ) > ( ( a > a ) > $o ) > $o ).
thf(func_def_55,type,
bNF_re571457705_a_a_a: ( ( a > a ) > ( a > a ) > $o ) > ( a > a > $o ) > ( ( a > a ) > a ) > ( ( a > a ) > a ) > $o ).
thf(func_def_56,type,
bNF_re1514436479_a_a_b: ( ( a > a ) > ( a > b ) > $o ) > ( ( ( a > a ) > a > a ) > ( ( a > a ) > a > b ) > $o ) > ( ( a > a ) > ( a > a ) > a > a ) > ( ( a > b ) > ( a > a ) > a > b ) > $o ).
thf(func_def_57,type,
bNF_re390230442_a_a_o: ( ( a > a ) > ( a > b ) > $o ) > ( ( ( a > a ) > $o ) > ( ( a > a ) > $o ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( ( a > b ) > ( a > a ) > $o ) > $o ).
thf(func_def_58,type,
bNF_re1217999849_a_b_o: ( ( a > a ) > ( a > b ) > $o ) > ( ( ( a > a ) > $o ) > ( ( a > b ) > $o ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( ( a > b ) > ( a > b ) > $o ) > $o ).
thf(func_def_59,type,
bNF_re1787520874_a_d_d: ( ( a > a ) > ( a > b ) > $o ) > ( ( a > c > c ) > ( a > d > d ) > $o ) > ( ( a > a ) > a > c > c ) > ( ( a > b ) > a > d > d ) > $o ).
thf(func_def_60,type,
bNF_re857382262_a_a_a: ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( ( a > a ) > a > a ) > ( ( a > b ) > a > a ) > $o ).
thf(func_def_61,type,
bNF_re865643767_a_a_b: ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > ( a > b ) > $o ) > ( ( a > a ) > a > a ) > ( ( a > b ) > a > b ) > $o ).
thf(func_def_62,type,
bNF_re1463366826_b_o_o: ( ( a > a ) > ( a > b ) > $o ) > ( $o > $o > $o ) > ( ( a > a ) > $o ) > ( ( a > b ) > $o ) > $o ).
thf(func_def_63,type,
bNF_re473406379_b_a_b: ( ( a > a ) > ( a > b ) > $o ) > ( a > b > $o ) > ( ( a > a ) > a ) > ( ( a > b ) > b ) > $o ).
thf(func_def_64,type,
bNF_re539937469_b_a_a: ( ( a > a ) > ( b > a ) > $o ) > ( ( ( a > a ) > a > a ) > ( ( a > b ) > a > a ) > $o ) > ( ( a > a ) > ( a > a ) > a > a ) > ( ( b > a ) > ( a > b ) > a > a ) > $o ).
thf(func_def_65,type,
bNF_re1665173865_b_c_c: ( ( a > a ) > ( b > a ) > $o ) > ( ( a > c > c ) > ( b > c > c ) > $o ) > ( ( a > a ) > a > c > c ) > ( ( b > a ) > b > c > c ) > $o ).
thf(func_def_66,type,
bNF_re932551557_b_d_d: ( ( a > a ) > ( b > b ) > $o ) > ( ( ( ( c > c ) > c > c ) > ( a > c > c ) > a > c > c ) > ( ( ( d > d ) > d > d ) > ( b > d > d ) > b > d > d ) > $o ) > ( ( a > a ) > ( ( c > c ) > c > c ) > ( a > c > c ) > a > c > c ) > ( ( b > b ) > ( ( d > d ) > d > d ) > ( b > d > d ) > b > d > d ) > $o ).
thf(func_def_67,type,
bNF_re796114495_b_a_b: ( ( a > a ) > ( b > b ) > $o ) > ( ( ( a > a ) > a > a ) > ( ( a > b ) > a > b ) > $o ) > ( ( a > a ) > ( a > a ) > a > a ) > ( ( b > b ) > ( a > b ) > a > b ) > $o ).
thf(func_def_68,type,
bNF_re835672381_b_b_b: ( ( a > a ) > ( b > b ) > $o ) > ( ( ( a > a ) > a > a ) > ( ( b > b ) > b > b ) > $o ) > ( ( a > a ) > ( a > a ) > a > a ) > ( ( b > b ) > ( b > b ) > b > b ) > $o ).
thf(func_def_69,type,
bNF_re774352699_b_b_b: ( ( a > a ) > ( b > b ) > $o ) > ( ( ( b > a ) > b > a ) > ( ( b > b ) > b > b ) > $o ) > ( ( a > a ) > ( b > a ) > b > a ) > ( ( b > b ) > ( b > b ) > b > b ) > $o ).
thf(func_def_70,type,
bNF_re1761470250_b_d_d: ( ( a > a ) > ( b > b ) > $o ) > ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( a > a ) > a > c > c ) > ( ( b > b ) > b > d > d ) > $o ).
thf(func_def_71,type,
bNF_re1307884917_a_b_b: ( ( a > a ) > ( b > b ) > $o ) > ( ( a > a ) > ( b > b ) > $o ) > ( ( a > a ) > a > a ) > ( ( b > b ) > b > b ) > $o ).
thf(func_def_72,type,
bNF_re2087760490_b_a_b: ( ( a > a ) > ( b > b ) > $o ) > ( a > b > $o ) > ( ( a > a ) > a ) > ( ( b > b ) > b ) > $o ).
thf(func_def_73,type,
bNF_re1906994858_a_o_o: ( ( a > b ) > ( a > a ) > $o ) > ( $o > $o > $o ) > ( ( a > b ) > $o ) > ( ( a > a ) > $o ) > $o ).
thf(func_def_74,type,
bNF_re1088547499_b_o_o: ( ( a > b ) > ( a > b ) > $o ) > ( $o > $o > $o ) > ( ( a > b ) > $o ) > ( ( a > b ) > $o ) > $o ).
thf(func_def_75,type,
bNF_re1606289753_b_d_d: ( ( a > c ) > ( b > d ) > $o ) > ( ( ( c > c > c ) > ( c > c ) > a > c > c ) > ( ( d > d > d ) > ( d > d ) > b > d > d ) > $o ) > ( ( a > c ) > ( c > c > c ) > ( c > c ) > a > c > c ) > ( ( b > d ) > ( d > d > d ) > ( d > d ) > b > d > d ) > $o ).
thf(func_def_76,type,
bNF_re561231771_a_c_c: ( ( b > d > d ) > ( a > c > c ) > $o ) > ( ( ( b > b ) > b > d > d ) > ( ( a > a ) > a > c > c ) > $o ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > $o ).
thf(func_def_77,type,
bNF_re742509149_b_d_d: ( ( b > d > d ) > ( b > d > d ) > $o ) > ( ( ( b > b ) > b > d > d ) > ( ( b > b ) > b > d > d ) > $o ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > $o ).
thf(func_def_78,type,
bNF_re1591514407_a_c_c: ( ( b > a ) > ( a > a ) > $o ) > ( ( b > c > c ) > ( a > c > c ) > $o ) > ( ( b > a ) > b > c > c ) > ( ( a > a ) > a > c > c ) > $o ).
thf(func_def_79,type,
bNF_re1565463783_b_c_c: ( ( b > a ) > ( b > a ) > $o ) > ( ( b > c > c ) > ( b > c > c ) > $o ) > ( ( b > a ) > b > c > c ) > ( ( b > a ) > b > c > c ) > $o ).
thf(func_def_80,type,
bNF_re1661760168_b_d_d: ( ( b > a ) > ( b > b ) > $o ) > ( ( b > c > c ) > ( b > d > d ) > $o ) > ( ( b > a ) > b > c > c ) > ( ( b > b ) > b > d > d ) > $o ).
thf(func_def_81,type,
bNF_re668686835_a_b_b: ( ( b > a ) > ( b > b ) > $o ) > ( ( b > a ) > ( b > b ) > $o ) > ( ( b > a ) > b > a ) > ( ( b > b ) > b > b ) > $o ).
thf(func_def_82,type,
bNF_re1794062813_d_d_b: ( ( b > b ) > ( ( d > d ) > b ) > $o ) > ( ( b > b ) > ( ( d > d ) > b ) > $o ) > ( ( b > b ) > b > b ) > ( ( ( d > d ) > b ) > ( d > d ) > b ) > $o ).
thf(func_def_83,type,
bNF_re1645058365_a_a_a: ( ( b > b ) > ( a > a ) > $o ) > ( ( ( b > b ) > b > b ) > ( ( a > a ) > a > a ) > $o ) > ( ( b > b ) > ( b > b ) > b > b ) > ( ( a > a ) > ( a > a ) > a > a ) > $o ).
thf(func_def_84,type,
bNF_re1342462312_a_c_c: ( ( b > b ) > ( a > a ) > $o ) > ( ( b > d > d ) > ( a > c > c ) > $o ) > ( ( b > b ) > b > d > d ) > ( ( a > a ) > a > c > c ) > $o ).
thf(func_def_85,type,
bNF_re310361461_b_a_a: ( ( b > b ) > ( a > a ) > $o ) > ( ( b > b ) > ( a > a ) > $o ) > ( ( b > b ) > b > b ) > ( ( a > a ) > a > a ) > $o ).
thf(func_def_86,type,
bNF_re1138812345_b_b_b: ( ( b > b ) > ( b > b ) > $o ) > ( ( ( ( d > d ) > b ) > ( d > d ) > b ) > ( ( b > b ) > b > b ) > $o ) > ( ( b > b ) > ( ( d > d ) > b ) > ( d > d ) > b ) > ( ( b > b ) > ( b > b ) > b > b ) > $o ).
thf(func_def_87,type,
bNF_re961930425_d_d_b: ( ( b > b ) > ( b > b ) > $o ) > ( ( ( b > b ) > b > b ) > ( ( ( d > d ) > b ) > ( d > d ) > b ) > $o ) > ( ( b > b ) > ( b > b ) > b > b ) > ( ( b > b ) > ( ( d > d ) > b ) > ( d > d ) > b ) > $o ).
thf(func_def_88,type,
bNF_re1222471293_b_b_b: ( ( b > b ) > ( b > b ) > $o ) > ( ( ( b > b ) > b > b ) > ( ( b > b ) > b > b ) > $o ) > ( ( b > b ) > ( b > b ) > b > b ) > ( ( b > b ) > ( b > b ) > b > b ) > $o ).
thf(func_def_89,type,
bNF_re1412708073_b_d_d: ( ( b > b ) > ( b > b ) > $o ) > ( ( b > d > d ) > ( b > d > d ) > $o ) > ( ( b > b ) > b > d > d ) > ( ( b > b ) > b > d > d ) > $o ).
thf(func_def_90,type,
bNF_re2075418869_b_b_b: ( ( b > b ) > ( b > b ) > $o ) > ( ( b > b ) > ( b > b ) > $o ) > ( ( b > b ) > b > b ) > ( ( b > b ) > b > b ) > $o ).
thf(func_def_91,type,
bNF_re921674337_d_d_o: ( ( c > c > $o ) > ( d > d > $o ) > $o ) > ( ( ( c > c > $o ) > ( c > c ) > $o ) > ( ( d > d > $o ) > ( d > d ) > $o ) > $o ) > ( ( c > c > $o ) > ( c > c > $o ) > ( c > c ) > $o ) > ( ( d > d > $o ) > ( d > d > $o ) > ( d > d ) > $o ) > $o ).
thf(func_def_92,type,
bNF_re764708765_d_d_o: ( ( c > c > $o ) > ( d > d > $o ) > $o ) > ( ( ( c > c ) > ( c > c ) > $o ) > ( ( d > d ) > ( d > d ) > $o ) > $o ) > ( ( c > c > $o ) > ( c > c ) > ( c > c ) > $o ) > ( ( d > d > $o ) > ( d > d ) > ( d > d ) > $o ) > $o ).
thf(func_def_93,type,
bNF_re27482973_d_d_o: ( ( c > c > $o ) > ( d > d > $o ) > $o ) > ( ( ( c > c ) > $o ) > ( ( d > d ) > $o ) > $o ) > ( ( c > c > $o ) > ( c > c ) > $o ) > ( ( d > d > $o ) > ( d > d ) > $o ) > $o ).
thf(func_def_94,type,
bNF_re1507718559_b_d_d: ( ( c > c > c ) > ( d > d > d ) > $o ) > ( ( ( c > c ) > a > c > c ) > ( ( d > d ) > b > d > d ) > $o ) > ( ( c > c > c ) > ( c > c ) > a > c > c ) > ( ( d > d > d ) > ( d > d ) > b > d > d ) > $o ).
thf(func_def_95,type,
bNF_re1164948833_d_d_d: ( ( c > a ) > ( d > b ) > $o ) > ( ( ( ( c > c ) > c ) > ( a > c > c ) > c > c ) > ( ( ( d > d ) > d ) > ( b > d > d ) > d > d ) > $o ) > ( ( c > a ) > ( ( c > c ) > c ) > ( a > c > c ) > c > c ) > ( ( d > b ) > ( ( d > d ) > d ) > ( b > d > d ) > d > d ) > $o ).
thf(func_def_96,type,
bNF_re1509948838_d_d_d: ( ( c > a ) > ( d > b ) > $o ) > ( ( c > c > c ) > ( d > d > d ) > $o ) > ( ( c > a ) > c > c > c ) > ( ( d > b ) > d > d > d ) > $o ).
thf(func_def_97,type,
bNF_re335372010_d_b_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( ( ( c > c ) > c ) > a > c ) > ( ( ( d > d ) > d ) > b > d ) > $o ) > ( ( c > c ) > ( ( c > c ) > c ) > a > c ) > ( ( d > d ) > ( ( d > d ) > d ) > b > d ) > $o ).
thf(func_def_98,type,
bNF_re1709888353_d_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( ( a > c > c ) > ( c > a ) > c > c > c ) > ( ( b > d > d ) > ( d > b ) > d > d > d ) > $o ) > ( ( c > c ) > ( a > c > c ) > ( c > a ) > c > c > c ) > ( ( d > d ) > ( b > d > d ) > ( d > b ) > d > d > d ) > $o ).
thf(func_def_99,type,
bNF_re888371717_d_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( ( c > c ) > ( c > c ) > c > c ) > ( ( d > d ) > ( d > d ) > d > d ) > $o ) > ( ( c > c ) > ( c > c ) > ( c > c ) > c > c ) > ( ( d > d ) > ( d > d ) > ( d > d ) > d > d ) > $o ).
thf(func_def_100,type,
bNF_re764096061_d_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( ( c > c ) > c > c ) > ( ( d > d ) > d > d ) > $o ) > ( ( c > c ) > ( c > c ) > c > c ) > ( ( d > d ) > ( d > d ) > d > d ) > $o ).
thf(func_def_101,type,
bNF_re781155241_d_d_o: ( ( c > c ) > ( d > d ) > $o ) > ( ( ( c > c ) > $o ) > ( ( d > d ) > $o ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( ( d > d ) > ( d > d ) > $o ) > $o ).
thf(func_def_102,type,
bNF_re1145286186_b_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( c > c ) > a > c > c ) > ( ( d > d ) > b > d > d ) > $o ).
thf(func_def_103,type,
bNF_re1941803873_d_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c > c > c ) > ( d > d > d > d ) > $o ) > ( ( c > c ) > c > c > c > c ) > ( ( d > d ) > d > d > d > d ) > $o ).
thf(func_def_104,type,
bNF_re2078100341_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > c > c ) > ( ( d > d ) > d > d ) > $o ).
thf(func_def_105,type,
bNF_re857878889_d_o_o: ( ( c > c ) > ( d > d ) > $o ) > ( $o > $o > $o ) > ( ( c > c ) > $o ) > ( ( d > d ) > $o ) > $o ).
thf(func_def_106,type,
bNF_re1795127658_d_a_b: ( ( c > c ) > ( d > d ) > $o ) > ( a > b > $o ) > ( ( c > c ) > a ) > ( ( d > d ) > b ) > $o ).
thf(func_def_107,type,
bNF_re1303182826_d_c_d: ( ( c > c ) > ( d > d ) > $o ) > ( c > d > $o ) > ( ( c > c ) > c ) > ( ( d > d ) > d ) > $o ).
thf(func_def_108,type,
bNF_re1450278895_o_a_o: ( ( c > c ) > a > $o ) > ( ( ( c > c ) > $o ) > ( a > $o ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > $o ).
thf(func_def_109,type,
bNF_re2038641070_o_b_o: ( ( c > c ) > a > $o ) > ( ( ( c > c ) > $o ) > ( b > $o ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > b > $o ) > $o ).
thf(func_def_110,type,
bNF_re1306877487_o_a_o: ( ( c > c ) > a > $o ) > ( ( ( d > d ) > $o ) > ( a > $o ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > a > $o ) > $o ).
thf(func_def_111,type,
bNF_re1895239662_o_b_o: ( ( c > c ) > a > $o ) > ( ( ( d > d ) > $o ) > ( b > $o ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > b > $o ) > $o ).
thf(func_def_112,type,
bNF_re883196986_a_o_o: ( ( c > c ) > a > $o ) > ( $o > $o > $o ) > ( ( c > c ) > $o ) > ( a > $o ) > $o ).
thf(func_def_113,type,
bNF_re1424579386_a_a_a: ( ( c > c ) > a > $o ) > ( a > a > $o ) > ( ( c > c ) > a ) > ( a > a ) > $o ).
thf(func_def_114,type,
bNF_re90976443_b_o_o: ( ( c > c ) > b > $o ) > ( $o > $o > $o ) > ( ( c > c ) > $o ) > ( b > $o ) > $o ).
thf(func_def_115,type,
bNF_re991543930_a_o_o: ( ( d > d ) > a > $o ) > ( $o > $o > $o ) > ( ( d > d ) > $o ) > ( a > $o ) > $o ).
thf(func_def_116,type,
bNF_re199323387_b_o_o: ( ( d > d ) > b > $o ) > ( $o > $o > $o ) > ( ( d > d ) > $o ) > ( b > $o ) > $o ).
thf(func_def_117,type,
bNF_re1703323451_b_b_b: ( ( d > d ) > b > $o ) > ( b > b > $o ) > ( ( d > d ) > b ) > ( b > b ) > $o ).
thf(func_def_118,type,
bNF_re1705765981_a_a_a: ( $o > $o > $o ) > ( ( a > a > a ) > ( a > a > a ) > $o ) > ( $o > a > a > a ) > ( $o > a > a > a ) > $o ).
thf(func_def_119,type,
bNF_re588060702_b_b_b: ( $o > $o > $o ) > ( ( a > a > a ) > ( b > b > b ) > $o ) > ( $o > a > a > a ) > ( $o > b > b > b ) > $o ).
thf(func_def_120,type,
bNF_re647211934_d_d_d: ( $o > $o > $o ) > ( ( c > c > c ) > ( d > d > d ) > $o ) > ( $o > c > c > c ) > ( $o > d > d > d ) > $o ).
thf(func_def_121,type,
bNF_re1482032989_c_c_c: ( a > a > $o ) > ( ( ( a > c > c ) > c > c ) > ( ( a > c > c ) > c > c ) > $o ) > ( a > ( a > c > c ) > c > c ) > ( a > ( a > c > c ) > c > c ) > $o ).
thf(func_def_122,type,
bNF_re1391160029_d_d_d: ( a > a > $o ) > ( ( ( a > c > c ) > c > c ) > ( ( a > d > d ) > d > d ) > $o ) > ( a > ( a > c > c ) > c > c ) > ( a > ( a > d > d ) > d > d ) > $o ).
thf(func_def_123,type,
bNF_re865741149_a_a_a: ( a > a > $o ) > ( ( ( a > a ) > a ) > ( ( a > a ) > a ) > $o ) > ( a > ( a > a ) > a ) > ( a > ( a > a ) > a ) > $o ).
thf(func_def_124,type,
bNF_re1093913501_a_b_b: ( a > a > $o ) > ( ( ( a > a ) > a ) > ( ( a > b ) > b ) > $o ) > ( a > ( a > a ) > a ) > ( a > ( a > b ) > b ) > $o ).
thf(func_def_125,type,
bNF_re1690123229_o_a_o: ( a > a > $o ) > ( ( a > $o ) > ( a > $o ) > $o ) > ( a > a > $o ) > ( a > a > $o ) > $o ).
thf(func_def_126,type,
bNF_re131001756_o_b_o: ( a > a > $o ) > ( ( a > $o ) > ( b > $o ) > $o ) > ( a > a > $o ) > ( a > b > $o ) > $o ).
thf(func_def_127,type,
bNF_re911029929_a_a_a: ( a > a > $o ) > ( ( a > a ) > ( a > a ) > $o ) > ( a > a > a ) > ( a > a > a ) > $o ).
thf(func_def_128,type,
bNF_re1809376028_o_a_o: ( a > a > $o ) > ( ( b > $o ) > ( a > $o ) > $o ) > ( a > b > $o ) > ( a > a > $o ) > $o ).
thf(func_def_129,type,
bNF_re250254555_o_b_o: ( a > a > $o ) > ( ( b > $o ) > ( b > $o ) > $o ) > ( a > b > $o ) > ( a > b > $o ) > $o ).
thf(func_def_130,type,
bNF_re1143700905_c_c_c: ( a > a > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > ( a > c > c ) > $o ).
thf(func_def_131,type,
bNF_re1979731817_c_d_d: ( a > a > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > c > c ) > ( a > d > d ) > $o ).
thf(func_def_132,type,
bNF_re950444090_c_c_a: ( a > a > $o ) > ( ( c > c ) > a > $o ) > ( a > c > c ) > ( a > a ) > $o ).
thf(func_def_133,type,
bNF_re950444091_c_c_b: ( a > a > $o ) > ( ( c > c ) > b > $o ) > ( a > c > c ) > ( a > b ) > $o ).
thf(func_def_134,type,
bNF_re2038021754_d_d_a: ( a > a > $o ) > ( ( d > d ) > a > $o ) > ( a > d > d ) > ( a > a ) > $o ).
thf(func_def_135,type,
bNF_re2038021755_d_d_b: ( a > a > $o ) > ( ( d > d ) > b > $o ) > ( a > d > d ) > ( a > b ) > $o ).
thf(func_def_136,type,
bNF_rel_fun_a_a_o_o: ( a > a > $o ) > ( $o > $o > $o ) > ( a > $o ) > ( a > $o ) > $o ).
thf(func_def_137,type,
bNF_rel_fun_a_a_a_a: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ).
thf(func_def_138,type,
bNF_rel_fun_a_a_a_b: ( a > a > $o ) > ( a > b > $o ) > ( a > a ) > ( a > b ) > $o ).
thf(func_def_139,type,
bNF_rel_fun_a_a_b_a: ( a > a > $o ) > ( b > a > $o ) > ( a > b ) > ( a > a ) > $o ).
thf(func_def_140,type,
bNF_rel_fun_a_a_b_b: ( a > a > $o ) > ( b > b > $o ) > ( a > b ) > ( a > b ) > $o ).
thf(func_def_141,type,
bNF_re1327926367_d_d_d: ( a > b > $o ) > ( ( ( a > c > c ) > c > c ) > ( ( b > d > d ) > d > d ) > $o ) > ( a > ( a > c > c ) > c > c ) > ( b > ( b > d > d ) > d > d ) > $o ).
thf(func_def_142,type,
bNF_re1730737055_b_b_b: ( a > b > $o ) > ( ( ( a > a ) > a ) > ( ( b > b ) > b ) > $o ) > ( a > ( a > a ) > a ) > ( b > ( b > b ) > b ) > $o ).
thf(func_def_143,type,
bNF_re1573878111_b_d_d: ( a > b > $o ) > ( ( ( c > c ) > a > c > c ) > ( ( d > d ) > b > d > d ) > $o ) > ( a > ( c > c ) > a > c > c ) > ( b > ( d > d ) > b > d > d ) > $o ).
thf(func_def_144,type,
bNF_re1977372894_o_a_o: ( a > b > $o ) > ( ( a > $o ) > ( a > $o ) > $o ) > ( a > a > $o ) > ( b > a > $o ) > $o ).
thf(func_def_145,type,
bNF_re418251421_o_b_o: ( a > b > $o ) > ( ( a > $o ) > ( b > $o ) > $o ) > ( a > a > $o ) > ( b > b > $o ) > $o ).
thf(func_def_146,type,
bNF_re569932906_a_b_b: ( a > b > $o ) > ( ( a > a ) > ( b > b ) > $o ) > ( a > a > a ) > ( b > b > b ) > $o ).
thf(func_def_147,type,
bNF_re2114056618_c_c_c: ( a > b > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > ( b > c > c ) > $o ).
thf(func_def_148,type,
bNF_re802603882_c_d_d: ( a > b > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > c > c ) > ( b > d > d ) > $o ).
thf(func_def_149,type,
bNF_rel_fun_a_b_o_o: ( a > b > $o ) > ( $o > $o > $o ) > ( a > $o ) > ( b > $o ) > $o ).
thf(func_def_150,type,
bNF_rel_fun_a_b_a_a: ( a > b > $o ) > ( a > a > $o ) > ( a > a ) > ( b > a ) > $o ).
thf(func_def_151,type,
bNF_rel_fun_a_b_a_b: ( a > b > $o ) > ( a > b > $o ) > ( a > a ) > ( b > b ) > $o ).
thf(func_def_152,type,
bNF_rel_fun_a_b_c_d: ( a > b > $o ) > ( c > d > $o ) > ( a > c ) > ( b > d ) > $o ).
thf(func_def_153,type,
bNF_re1573506119_d_b_b: ( b > ( d > d ) > $o ) > ( b > b > $o ) > ( b > b ) > ( ( d > d ) > b ) > $o ).
thf(func_def_154,type,
bNF_re758172648_c_c_c: ( b > a > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( b > c > c ) > ( a > c > c ) > $o ).
thf(func_def_155,type,
bNF_re38477224_d_c_c: ( b > a > $o ) > ( ( d > d ) > ( c > c ) > $o ) > ( b > d > d ) > ( a > c > c ) > $o ).
thf(func_def_156,type,
bNF_rel_fun_b_a_o_o: ( b > a > $o ) > ( $o > $o > $o ) > ( b > $o ) > ( a > $o ) > $o ).
thf(func_def_157,type,
bNF_rel_fun_b_a_a_a: ( b > a > $o ) > ( a > a > $o ) > ( b > a ) > ( a > a ) > $o ).
thf(func_def_158,type,
bNF_rel_fun_b_a_b_a: ( b > a > $o ) > ( b > a > $o ) > ( b > b ) > ( a > a ) > $o ).
thf(func_def_159,type,
bNF_re1728528361_c_c_c: ( b > b > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( b > c > c ) > ( b > c > c ) > $o ).
thf(func_def_160,type,
bNF_re417075625_c_d_d: ( b > b > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( b > c > c ) > ( b > d > d ) > $o ).
thf(func_def_161,type,
bNF_re1844863849_d_d_d: ( b > b > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > ( b > d > d ) > $o ).
thf(func_def_162,type,
bNF_rel_fun_b_b_o_o: ( b > b > $o ) > ( $o > $o > $o ) > ( b > $o ) > ( b > $o ) > $o ).
thf(func_def_163,type,
bNF_rel_fun_b_b_a_a: ( b > b > $o ) > ( a > a > $o ) > ( b > a ) > ( b > a ) > $o ).
thf(func_def_164,type,
bNF_rel_fun_b_b_a_b: ( b > b > $o ) > ( a > b > $o ) > ( b > a ) > ( b > b ) > $o ).
thf(func_def_165,type,
bNF_rel_fun_b_b_b_b: ( b > b > $o ) > ( b > b > $o ) > ( b > b ) > ( b > b ) > $o ).
thf(func_def_166,type,
bNF_rel_fun_c_c_c_c: ( c > c > $o ) > ( c > c > $o ) > ( c > c ) > ( c > c ) > $o ).
thf(func_def_167,type,
bNF_re1313098655_d_d_d: ( c > d > $o ) > ( ( ( c > c ) > c ) > ( ( d > d ) > d ) > $o ) > ( c > ( c > c ) > c ) > ( d > ( d > d ) > d ) > $o ).
thf(func_def_168,type,
bNF_re822780063_d_d_d: ( c > d > $o ) > ( ( c > c > c ) > ( d > d > d ) > $o ) > ( c > c > c > c ) > ( d > d > d > d ) > $o ).
thf(func_def_169,type,
bNF_re391428377_o_d_o: ( c > d > $o ) > ( ( c > $o ) > ( d > $o ) > $o ) > ( c > c > $o ) > ( d > d > $o ) > $o ).
thf(func_def_170,type,
bNF_re1972258794_c_d_d: ( c > d > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( c > c > c ) > ( d > d > d ) > $o ).
thf(func_def_171,type,
bNF_rel_fun_c_d_o_o: ( c > d > $o ) > ( $o > $o > $o ) > ( c > $o ) > ( d > $o ) > $o ).
thf(func_def_172,type,
bNF_rel_fun_c_d_a_b: ( c > d > $o ) > ( a > b > $o ) > ( c > a ) > ( d > b ) > $o ).
thf(func_def_173,type,
bNF_rel_fun_c_d_c_d: ( c > d > $o ) > ( c > d > $o ) > ( c > c ) > ( d > d ) > $o ).
thf(func_def_174,type,
bNF_rel_fun_d_d_d_d: ( d > d > $o ) > ( d > d > $o ) > ( d > d ) > ( d > d ) > $o ).
thf(func_def_175,type,
comple1702356924_a_c_c: ( a > a > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > $o ).
thf(func_def_176,type,
comple61207421_b_d_d: ( b > b > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > $o ).
thf(func_def_177,type,
comple787379047ne_c_c: ( c > c > $o ) > ( c > c > $o ) > ( c > c ) > $o ).
thf(func_def_178,type,
comple1615148455ne_d_d: ( d > d > $o ) > ( d > d > $o ) > ( d > d ) > $o ).
thf(func_def_179,type,
ffold_a_c: ( a > c > c ) > c > fset_a > c ).
thf(func_def_180,type,
ffold_b_d: ( b > d > d ) > d > fset_b > d ).
thf(func_def_181,type,
finite746615251te_a_c: ( a > c > c ) > $o ).
thf(func_def_182,type,
finite1574384658te_b_c: ( b > c > c ) > $o ).
thf(func_def_183,type,
finite1574384659te_b_d: ( b > d > d ) > $o ).
thf(func_def_184,type,
finite40241358em_a_c: ( a > c > c ) > $o ).
thf(func_def_185,type,
finite868010765em_b_c: ( b > c > c ) > $o ).
thf(func_def_186,type,
finite868010766em_b_d: ( b > d > d ) > $o ).
thf(func_def_187,type,
finite19304177ms_a_c: ( a > c > c ) > $o ).
thf(func_def_188,type,
finite847073585ms_b_d: ( b > d > d ) > $o ).
thf(func_def_189,type,
finite1511629766ph_a_a: ( a > a > a ) > a > set_a > a > $o ).
thf(func_def_190,type,
finite1511629767ph_a_b: ( a > b > b ) > b > set_a > b > $o ).
thf(func_def_191,type,
finite1511629768ph_a_c: ( a > c > c ) > c > set_a > c > $o ).
thf(func_def_192,type,
finite1511629769ph_a_d: ( a > d > d ) > d > set_a > d > $o ).
thf(func_def_193,type,
finite191915525ph_b_a: ( b > a > a ) > a > set_b > a > $o ).
thf(func_def_194,type,
finite191915528ph_b_d: ( b > d > d ) > d > set_b > d > $o ).
thf(func_def_195,type,
finite1019684932ph_c_a: ( c > a > a ) > a > set_c > a > $o ).
thf(func_def_196,type,
finite1019684933ph_c_b: ( c > b > b ) > b > set_c > b > $o ).
thf(func_def_197,type,
finite1019684934ph_c_c: ( c > c > c ) > c > set_c > c > $o ).
thf(func_def_198,type,
finite1019684935ph_c_d: ( c > d > d ) > d > set_c > d > $o ).
thf(func_def_199,type,
comp_a_a_a_c_c_c_c_a: ( ( a > a ) > a > c > c ) > ( ( ( c > c ) > a ) > a > a ) > ( ( c > c ) > a ) > a > c > c ).
thf(func_def_200,type,
comp_a_b_a_d_d_c_c_b: ( ( a > b ) > a > d > d ) > ( ( ( c > c ) > b ) > a > b ) > ( ( c > c ) > b ) > a > d > d ).
thf(func_def_201,type,
comp_b_a_b_c_c_d_d_a: ( ( b > a ) > b > c > c ) > ( ( ( d > d ) > a ) > b > a ) > ( ( d > d ) > a ) > b > c > c ).
thf(func_def_202,type,
comp_b_b_b_d_d_d_d_b: ( ( b > b ) > b > d > d ) > ( ( ( d > d ) > b ) > b > b ) > ( ( d > d ) > b ) > b > d > d ).
thf(func_def_203,type,
comp_c_c_c_c_a: ( ( c > c ) > c > c ) > ( a > c > c ) > a > c > c ).
thf(func_def_204,type,
comp_c_c_a_c_c: ( ( c > c ) > a ) > ( ( c > c ) > c > c ) > ( c > c ) > a ).
thf(func_def_205,type,
comp_c_c_a_a: ( ( c > c ) > a ) > ( a > c > c ) > a > a ).
thf(func_def_206,type,
comp_c_c_b_a: ( ( c > c ) > b ) > ( a > c > c ) > a > b ).
thf(func_def_207,type,
comp_c_c_b_b: ( ( c > c ) > b ) > ( b > c > c ) > b > b ).
thf(func_def_208,type,
comp_d_d_d_d_b: ( ( d > d ) > d > d ) > ( b > d > d ) > b > d > d ).
thf(func_def_209,type,
comp_d_d_b_b: ( ( d > d ) > b ) > ( b > d > d ) > b > b ).
thf(func_def_210,type,
comp_a_c_c_a: ( a > c > c ) > ( a > a ) > a > c > c ).
thf(func_def_211,type,
comp_a_c_c_b: ( a > c > c ) > ( b > a ) > b > c > c ).
thf(func_def_212,type,
comp_a_a_c_c: ( a > a ) > ( ( c > c ) > a ) > ( c > c ) > a ).
thf(func_def_213,type,
comp_a_a_a: ( a > a ) > ( a > a ) > a > a ).
thf(func_def_214,type,
comp_a_a_b: ( a > a ) > ( b > a ) > b > a ).
thf(func_def_215,type,
comp_a_b_a: ( a > b ) > ( a > a ) > a > b ).
thf(func_def_216,type,
comp_a_b_b: ( a > b ) > ( b > a ) > b > b ).
thf(func_def_217,type,
comp_b_c_c_a: ( b > c > c ) > ( a > b ) > a > c > c ).
thf(func_def_218,type,
comp_b_c_c_b: ( b > c > c ) > ( b > b ) > b > c > c ).
thf(func_def_219,type,
comp_b_d_d_a: ( b > d > d ) > ( a > b ) > a > d > d ).
thf(func_def_220,type,
comp_b_d_d_b: ( b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_221,type,
comp_b_a_a: ( b > a ) > ( a > b ) > a > a ).
thf(func_def_222,type,
comp_b_a_b: ( b > a ) > ( b > b ) > b > a ).
thf(func_def_223,type,
comp_b_b_d_d: ( b > b ) > ( ( d > d ) > b ) > ( d > d ) > b ).
thf(func_def_224,type,
comp_b_b_a: ( b > b ) > ( a > b ) > a > b ).
thf(func_def_225,type,
comp_b_b_b: ( b > b ) > ( b > b ) > b > b ).
thf(func_def_226,type,
comp_c_c_c: ( c > c ) > ( c > c ) > c > c ).
thf(func_def_227,type,
comp_d_d_d: ( d > d ) > ( d > d ) > d > d ).
thf(func_def_228,type,
fun_upd_a_c_c: ( a > c > c ) > a > ( c > c ) > a > c > c ).
thf(func_def_229,type,
fun_upd_b_d_d: ( b > d > d ) > b > ( d > d ) > b > d > d ).
thf(func_def_230,type,
fun_upd_c_c: ( c > c ) > c > c > c > c ).
thf(func_def_231,type,
fun_upd_d_d: ( d > d ) > d > d > d > d ).
thf(func_def_232,type,
map_fu676564502_a_c_c: ( ( a > c > c ) > a > c > c ) > ( ( ( a > a ) > a > c > c ) > ( a > a ) > a > c > c ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > ( a > c > c ) > ( a > a ) > a > c > c ).
thf(func_def_233,type,
map_fu232832790_a_c_c: ( ( a > c > c ) > b > d > d ) > ( ( ( b > b ) > b > d > d ) > ( a > a ) > a > c > c ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > ( a > c > c ) > ( a > a ) > a > c > c ).
thf(func_def_234,type,
map_fu961723106_a_c_c: ( ( a > a ) > a > a ) > ( ( a > c > c ) > a > c > c ) > ( ( a > a ) > a > c > c ) > ( a > a ) > a > c > c ).
thf(func_def_235,type,
map_fu75729569_a_c_c: ( ( a > a ) > b > b ) > ( ( b > d > d ) > a > c > c ) > ( ( b > b ) > b > d > d ) > ( a > a ) > a > c > c ).
thf(func_def_236,type,
map_fu981964822_b_d_d: ( ( b > d > d ) > a > c > c ) > ( ( ( a > a ) > a > c > c ) > ( b > b ) > b > d > d ) > ( ( a > c > c ) > ( a > a ) > a > c > c ) > ( b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_237,type,
map_fu538233110_b_d_d: ( ( b > d > d ) > b > d > d ) > ( ( ( b > b ) > b > d > d ) > ( b > b ) > b > d > d ) > ( ( b > d > d ) > ( b > b ) > b > d > d ) > ( b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_238,type,
map_fu1569200227_b_d_d: ( ( b > b ) > a > a ) > ( ( a > c > c ) > b > d > d ) > ( ( a > a ) > a > c > c ) > ( b > b ) > b > d > d ).
thf(func_def_239,type,
map_fu683206690_b_d_d: ( ( b > b ) > b > b ) > ( ( b > d > d ) > b > d > d ) > ( ( b > b ) > b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_240,type,
map_fun_a_c_c_a_c_c: ( a > c > c ) > ( a > c > c ) > ( ( c > c ) > a ) > a > c > c ).
thf(func_def_241,type,
map_fun_a_c_c_a_a: ( a > c > c ) > ( a > a ) > ( ( c > c ) > a ) > a > a ).
thf(func_def_242,type,
map_fun_a_c_c_b_d_d: ( a > c > c ) > ( b > d > d ) > ( ( c > c ) > b ) > a > d > d ).
thf(func_def_243,type,
map_fun_a_c_c_b_b: ( a > c > c ) > ( b > b ) > ( ( c > c ) > b ) > a > b ).
thf(func_def_244,type,
map_fun_a_c_c_c_c: ( a > c > c ) > ( c > c ) > ( ( c > c ) > c ) > a > c ).
thf(func_def_245,type,
map_fun_a_a_c_c_c_c: ( a > a ) > ( ( c > c ) > c > c ) > ( a > c > c ) > a > c > c ).
thf(func_def_246,type,
map_fun_a_a_a_c_c: ( a > a ) > ( a > c > c ) > ( a > a ) > a > c > c ).
thf(func_def_247,type,
map_fun_a_a_a_a: ( a > a ) > ( a > a ) > ( a > a ) > a > a ).
thf(func_def_248,type,
map_fun_a_a_b_d_d: ( a > a ) > ( b > d > d ) > ( a > b ) > a > d > d ).
thf(func_def_249,type,
map_fun_a_b_d_d_c_c: ( a > b ) > ( ( d > d ) > c > c ) > ( b > d > d ) > a > c > c ).
thf(func_def_250,type,
map_fun_a_b_b_a: ( a > b ) > ( b > a ) > ( b > b ) > a > a ).
thf(func_def_251,type,
map_fun_a_c_c_c_c2: ( a > c ) > ( c > c > c ) > ( c > c ) > a > c > c ).
thf(func_def_252,type,
map_fun_b_d_d_a_c_c: ( b > d > d ) > ( a > c > c ) > ( ( d > d ) > a ) > b > c > c ).
thf(func_def_253,type,
map_fun_b_d_d_a_a: ( b > d > d ) > ( a > a ) > ( ( d > d ) > a ) > b > a ).
thf(func_def_254,type,
map_fun_b_d_d_b_d_d: ( b > d > d ) > ( b > d > d ) > ( ( d > d ) > b ) > b > d > d ).
thf(func_def_255,type,
map_fun_b_d_d_b_b: ( b > d > d ) > ( b > b ) > ( ( d > d ) > b ) > b > b ).
thf(func_def_256,type,
map_fun_b_d_d_d_d: ( b > d > d ) > ( d > d ) > ( ( d > d ) > d ) > b > d ).
thf(func_def_257,type,
map_fun_b_a_c_c_d_d: ( b > a ) > ( ( c > c ) > d > d ) > ( a > c > c ) > b > d > d ).
thf(func_def_258,type,
map_fun_b_a_a_b: ( b > a ) > ( a > b ) > ( a > a ) > b > b ).
thf(func_def_259,type,
map_fun_b_b_d_d_d_d: ( b > b ) > ( ( d > d ) > d > d ) > ( b > d > d ) > b > d > d ).
thf(func_def_260,type,
map_fun_b_b_a_c_c: ( b > b ) > ( a > c > c ) > ( b > a ) > b > c > c ).
thf(func_def_261,type,
map_fun_b_b_b_d_d: ( b > b ) > ( b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_262,type,
map_fun_b_b_b_b: ( b > b ) > ( b > b ) > ( b > b ) > b > b ).
thf(func_def_263,type,
map_fun_b_d_d_d_d2: ( b > d ) > ( d > d > d ) > ( d > d ) > b > d > d ).
thf(func_def_264,type,
map_fun_c_a_c_c_c: ( c > a ) > ( ( c > c ) > c ) > ( a > c > c ) > c > c ).
thf(func_def_265,type,
map_fun_c_c_a_c_c: ( c > c ) > ( a > c > c ) > ( c > a ) > c > c > c ).
thf(func_def_266,type,
map_fun_c_c_c_c: ( c > c ) > ( c > c ) > ( c > c ) > c > c ).
thf(func_def_267,type,
map_fun_d_b_d_d_d: ( d > b ) > ( ( d > d ) > d ) > ( b > d > d ) > d > d ).
thf(func_def_268,type,
map_fun_d_d_b_d_d: ( d > d ) > ( b > d > d ) > ( d > b ) > d > d > d ).
thf(func_def_269,type,
map_fun_d_d_d_d: ( d > d ) > ( d > d ) > ( d > d ) > d > d ).
thf(func_def_270,type,
plus_plus_multiset_a: multiset_a > multiset_a > multiset_a ).
thf(func_def_271,type,
plus_plus_multiset_b: multiset_b > multiset_b > multiset_b ).
thf(func_def_272,type,
if_a: $o > a > a > a ).
thf(func_def_273,type,
if_b: $o > b > b > b ).
thf(func_def_274,type,
if_c: $o > c > c > c ).
thf(func_def_275,type,
if_d: $o > d > d > d ).
thf(func_def_276,type,
fold_mset_a_c: ( a > c > c ) > c > multiset_a > c ).
thf(func_def_277,type,
fold_mset_b_d: ( b > d > d ) > d > multiset_b > d ).
thf(func_def_278,type,
ord_le469275661_d_d_o: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_279,type,
ord_le1338099484_d_d_o: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_280,type,
ord_less_eq_a_b_o: ( a > b > $o ) > ( a > b > $o ) > $o ).
thf(func_def_281,type,
ord_less_eq_c_d_o: ( c > d > $o ) > ( c > d > $o ) > $o ).
thf(func_def_282,type,
partia186872226_c_c_a: ( ( c > c ) > ( c > c ) > $o ) > ( a > c > c ) > ( a > c > c ) > $o ).
thf(func_def_283,type,
partia1709452835_d_d_b: ( ( d > d ) > ( d > d ) > $o ) > ( b > d > d ) > ( b > d > d ) > $o ).
thf(func_def_284,type,
partia1494029680_c_c_c: ( c > c > $o ) > ( c > c ) > ( c > c ) > $o ).
thf(func_def_285,type,
partia1041982257_d_d_d: ( d > d > $o ) > ( d > d ) > ( d > d ) > $o ).
thf(func_def_286,type,
quotient3_c_c_c_c: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > c > c ) > ( ( c > c ) > c > c ) > $o ).
thf(func_def_287,type,
quotient3_c_c_d_d: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > d > d ) > ( ( d > d ) > c > c ) > $o ).
thf(func_def_288,type,
quotient3_c_c_a: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > a ) > ( a > c > c ) > $o ).
thf(func_def_289,type,
quotient3_d_d_c_c: ( ( d > d ) > ( d > d ) > $o ) > ( ( d > d ) > c > c ) > ( ( c > c ) > d > d ) > $o ).
thf(func_def_290,type,
quotient3_d_d_d_d: ( ( d > d ) > ( d > d ) > $o ) > ( ( d > d ) > d > d ) > ( ( d > d ) > d > d ) > $o ).
thf(func_def_291,type,
quotient3_d_d_b: ( ( d > d ) > ( d > d ) > $o ) > ( ( d > d ) > b ) > ( b > d > d ) > $o ).
thf(func_def_292,type,
quotient3_a_c_c: ( a > a > $o ) > ( a > c > c ) > ( ( c > c ) > a ) > $o ).
thf(func_def_293,type,
quotient3_a_a: ( a > a > $o ) > ( a > a ) > ( a > a ) > $o ).
thf(func_def_294,type,
quotient3_a_b: ( a > a > $o ) > ( a > b ) > ( b > a ) > $o ).
thf(func_def_295,type,
quotient3_b_d_d: ( b > b > $o ) > ( b > d > d ) > ( ( d > d ) > b ) > $o ).
thf(func_def_296,type,
quotient3_b_a: ( b > b > $o ) > ( b > a ) > ( a > b ) > $o ).
thf(func_def_297,type,
quotient3_b_b: ( b > b > $o ) > ( b > b ) > ( b > b ) > $o ).
thf(func_def_298,type,
relcom1813708708_b_d_d: ( ( a > c > c ) > ( a > c > c ) > $o ) > ( ( a > c > c ) > ( b > d > d ) > $o ) > ( a > c > c ) > ( b > d > d ) > $o ).
thf(func_def_299,type,
relcom1887247779_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > ( ( b > d > d ) > ( b > d > d ) > $o ) > ( a > c > c ) > ( b > d > d ) > $o ).
thf(func_def_300,type,
relcompp_c_c_c_c_c_c: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > ( c > c ) > ( c > c ) > $o ).
thf(func_def_301,type,
relcompp_c_c_c_c_d_d: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( c > c ) > ( d > d ) > $o ).
thf(func_def_302,type,
relcompp_c_c_d_d_d_d: ( ( c > c ) > ( d > d ) > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( c > c ) > ( d > d ) > $o ).
thf(func_def_303,type,
relcompp_d_d_d_d_d_d: ( ( d > d ) > ( d > d ) > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( d > d ) > ( d > d ) > $o ).
thf(func_def_304,type,
relcompp_a_a_a: ( a > a > $o ) > ( a > a > $o ) > a > a > $o ).
thf(func_def_305,type,
relcompp_a_a_b: ( a > a > $o ) > ( a > b > $o ) > a > b > $o ).
thf(func_def_306,type,
relcompp_a_b_b: ( a > b > $o ) > ( b > b > $o ) > a > b > $o ).
thf(func_def_307,type,
relcompp_b_b_b: ( b > b > $o ) > ( b > b > $o ) > b > b > $o ).
thf(func_def_308,type,
relcompp_c_c_d: ( c > c > $o ) > ( c > d > $o ) > c > d > $o ).
thf(func_def_309,type,
relcompp_c_d_d: ( c > d > $o ) > ( d > d > $o ) > c > d > $o ).
thf(func_def_310,type,
collect_a: ( a > $o ) > set_a ).
thf(func_def_311,type,
collect_b: ( b > $o ) > set_b ).
thf(func_def_312,type,
collect_c: ( c > $o ) > set_c ).
thf(func_def_313,type,
collect_d: ( d > $o ) > set_d ).
thf(func_def_314,type,
bi_total_a_c_c_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_315,type,
bi_total_c_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_316,type,
bi_total_a_b: ( a > b > $o ) > $o ).
thf(func_def_317,type,
bi_total_c_d: ( c > d > $o ) > $o ).
thf(func_def_318,type,
bi_uni844770768_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_319,type,
bi_unique_c_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_320,type,
bi_unique_a_b: ( a > b > $o ) > $o ).
thf(func_def_321,type,
bi_unique_c_d: ( c > d > $o ) > $o ).
thf(func_def_322,type,
left_t1993719015_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_323,type,
left_total_c_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_324,type,
left_total_a_b: ( a > b > $o ) > $o ).
thf(func_def_325,type,
left_total_b_b: ( b > b > $o ) > $o ).
thf(func_def_326,type,
left_total_c_d: ( c > d > $o ) > $o ).
thf(func_def_327,type,
left_total_d_d: ( d > d > $o ) > $o ).
thf(func_def_328,type,
left_u1654071760_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_329,type,
left_unique_c_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_330,type,
left_unique_d_d_d_d: ( ( d > d ) > ( d > d ) > $o ) > $o ).
thf(func_def_331,type,
left_unique_a_a: ( a > a > $o ) > $o ).
thf(func_def_332,type,
left_unique_a_b: ( a > b > $o ) > $o ).
thf(func_def_333,type,
left_unique_c_c: ( c > c > $o ) > $o ).
thf(func_def_334,type,
left_unique_c_d: ( c > d > $o ) > $o ).
thf(func_def_335,type,
left_unique_d_d: ( d > d > $o ) > $o ).
thf(func_def_336,type,
rev_implies: $o > $o > $o ).
thf(func_def_337,type,
right_386984928_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_338,type,
right_total_c_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_339,type,
right_total_d_d_d_d: ( ( d > d ) > ( d > d ) > $o ) > $o ).
thf(func_def_340,type,
right_total_a_a: ( a > a > $o ) > $o ).
thf(func_def_341,type,
right_total_a_b: ( a > b > $o ) > $o ).
thf(func_def_342,type,
right_total_c_c: ( c > c > $o ) > $o ).
thf(func_def_343,type,
right_total_c_d: ( c > d > $o ) > $o ).
thf(func_def_344,type,
right_total_d_d: ( d > d > $o ) > $o ).
thf(func_def_345,type,
right_2142487_b_d_d: ( ( a > c > c ) > ( b > d > d ) > $o ) > $o ).
thf(func_def_346,type,
right_unique_c_c_d_d: ( ( c > c ) > ( d > d ) > $o ) > $o ).
thf(func_def_347,type,
right_unique_a_b: ( a > b > $o ) > $o ).
thf(func_def_348,type,
right_unique_b_b: ( b > b > $o ) > $o ).
thf(func_def_349,type,
right_unique_c_d: ( c > d > $o ) > $o ).
thf(func_def_350,type,
right_unique_d_d: ( d > d > $o ) > $o ).
thf(func_def_351,type,
member_a: a > set_a > $o ).
thf(func_def_352,type,
member_b: b > set_b > $o ).
thf(func_def_353,type,
member_c: c > set_c > $o ).
thf(func_def_354,type,
member_d: d > set_d > $o ).
thf(func_def_355,type,
a2: a > b > $o ).
thf(func_def_356,type,
b2: c > d > $o ).
thf(func_def_357,type,
f1: a > c > c ).
thf(func_def_358,type,
f2: b > d > d ).
thf(func_def_362,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_363,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_364,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_365,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_366,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_367,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_368,type,
vIMP: $o > $o > $o ).
thf(func_def_369,type,
vAND: $o > $o > $o ).
thf(func_def_370,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_371,type,
sP0: set_b > set_d > ( b > d > d ) > ( b > d > d ) > $o ).
thf(func_def_372,type,
sP1: set_a > set_c > ( a > c > c ) > ( a > c > c ) > $o ).
thf(func_def_373,type,
sP2: set_a > set_a > ( a > a > a ) > ( a > a > a ) > $o ).
thf(func_def_374,type,
sP3: set_a > set_b > ( a > b > b ) > ( a > b > b ) > $o ).
thf(func_def_375,type,
sP4: set_a > set_d > ( a > d > d ) > ( a > d > d ) > $o ).
thf(func_def_376,type,
sP5: set_c > set_a > ( c > a > a ) > ( c > a > a ) > $o ).
thf(func_def_377,type,
sP6: set_c > set_c > ( c > c > c ) > ( c > c > c ) > $o ).
thf(func_def_378,type,
sP7: set_c > set_b > ( c > b > b ) > ( c > b > b ) > $o ).
thf(func_def_379,type,
sP8: set_c > set_d > ( c > d > d ) > ( c > d > d ) > $o ).
thf(func_def_380,type,
sP9: set_b > set_a > ( b > a > a ) > ( b > a > a ) > $o ).
thf(func_def_381,type,
sP10: set_b > set_d > ( b > d > d ) > ( b > d > d ) > $o ).
thf(func_def_382,type,
sP11: set_a > set_c > ( a > c > c ) > ( a > c > c ) > $o ).
thf(func_def_383,type,
sP12: set_a > set_a > ( a > a > a ) > ( a > a > a ) > $o ).
thf(func_def_384,type,
sP13: set_a > set_b > ( a > b > b ) > ( a > b > b ) > $o ).
thf(func_def_385,type,
sP14: set_a > set_d > ( a > d > d ) > ( a > d > d ) > $o ).
thf(func_def_386,type,
sP15: set_c > set_a > ( c > a > a ) > ( c > a > a ) > $o ).
thf(func_def_387,type,
sP16: set_c > set_c > ( c > c > c ) > ( c > c > c ) > $o ).
thf(func_def_388,type,
sP17: set_c > set_b > ( c > b > b ) > ( c > b > b ) > $o ).
thf(func_def_389,type,
sP18: set_c > set_d > ( c > d > d ) > ( c > d > d ) > $o ).
thf(func_def_390,type,
sP19: set_b > set_a > ( b > a > a ) > ( b > a > a ) > $o ).
thf(func_def_391,type,
sK20: ( c > c ) > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_392,type,
sK21: ( c > c ) > ( a > c > c ) > ( a > c > c ) > c ).
thf(func_def_393,type,
sK22: ( d > d ) > ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_394,type,
sK23: ( d > d ) > ( b > d > d ) > ( b > d > d ) > d ).
thf(func_def_395,type,
sK24: ( a > c > c ) > a ).
thf(func_def_396,type,
sK25: ( a > c > c ) > a ).
thf(func_def_397,type,
sK26: ( b > d > d ) > b ).
thf(func_def_398,type,
sK27: ( b > d > d ) > b ).
thf(func_def_399,type,
sK28: set_b > set_d > ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_400,type,
sK29: set_b > set_d > ( b > d > d ) > ( b > d > d ) > d ).
thf(func_def_401,type,
sK30: ( b > d > d ) > set_d > set_b > b ).
thf(func_def_402,type,
sK31: ( b > d > d ) > set_d > set_b > d ).
thf(func_def_403,type,
sK32: set_a > set_c > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_404,type,
sK33: set_a > set_c > ( a > c > c ) > ( a > c > c ) > c ).
thf(func_def_405,type,
sK34: ( a > c > c ) > set_c > set_a > a ).
thf(func_def_406,type,
sK35: ( a > c > c ) > set_c > set_a > c ).
thf(func_def_407,type,
sK36: set_a > set_a > ( a > a > a ) > ( a > a > a ) > a ).
thf(func_def_408,type,
sK37: set_a > set_a > ( a > a > a ) > ( a > a > a ) > a ).
thf(func_def_409,type,
sK38: ( a > a > a ) > set_a > set_a > a ).
thf(func_def_410,type,
sK39: ( a > a > a ) > set_a > set_a > a ).
thf(func_def_411,type,
sK40: set_a > set_b > ( a > b > b ) > ( a > b > b ) > a ).
thf(func_def_412,type,
sK41: set_a > set_b > ( a > b > b ) > ( a > b > b ) > b ).
thf(func_def_413,type,
sK42: ( a > b > b ) > set_b > set_a > a ).
thf(func_def_414,type,
sK43: ( a > b > b ) > set_b > set_a > b ).
thf(func_def_415,type,
sK44: set_a > set_d > ( a > d > d ) > ( a > d > d ) > a ).
thf(func_def_416,type,
sK45: set_a > set_d > ( a > d > d ) > ( a > d > d ) > d ).
thf(func_def_417,type,
sK46: ( a > d > d ) > set_d > set_a > a ).
thf(func_def_418,type,
sK47: ( a > d > d ) > set_d > set_a > d ).
thf(func_def_419,type,
sK48: set_c > set_a > ( c > a > a ) > ( c > a > a ) > c ).
thf(func_def_420,type,
sK49: set_c > set_a > ( c > a > a ) > ( c > a > a ) > a ).
thf(func_def_421,type,
sK50: ( c > a > a ) > set_a > set_c > c ).
thf(func_def_422,type,
sK51: ( c > a > a ) > set_a > set_c > a ).
thf(func_def_423,type,
sK52: set_c > set_c > ( c > c > c ) > ( c > c > c ) > c ).
thf(func_def_424,type,
sK53: set_c > set_c > ( c > c > c ) > ( c > c > c ) > c ).
thf(func_def_425,type,
sK54: ( c > c > c ) > set_c > set_c > c ).
thf(func_def_426,type,
sK55: ( c > c > c ) > set_c > set_c > c ).
thf(func_def_427,type,
sK56: set_c > set_b > ( c > b > b ) > ( c > b > b ) > c ).
thf(func_def_428,type,
sK57: set_c > set_b > ( c > b > b ) > ( c > b > b ) > b ).
thf(func_def_429,type,
sK58: ( c > b > b ) > set_b > set_c > c ).
thf(func_def_430,type,
sK59: ( c > b > b ) > set_b > set_c > b ).
thf(func_def_431,type,
sK60: set_c > set_d > ( c > d > d ) > ( c > d > d ) > c ).
thf(func_def_432,type,
sK61: set_c > set_d > ( c > d > d ) > ( c > d > d ) > d ).
thf(func_def_433,type,
sK62: ( c > d > d ) > set_d > set_c > c ).
thf(func_def_434,type,
sK63: ( c > d > d ) > set_d > set_c > d ).
thf(func_def_435,type,
sK64: set_b > set_a > ( b > a > a ) > ( b > a > a ) > b ).
thf(func_def_436,type,
sK65: set_b > set_a > ( b > a > a ) > ( b > a > a ) > a ).
thf(func_def_437,type,
sK66: ( b > a > a ) > set_a > set_b > b ).
thf(func_def_438,type,
sK67: ( b > a > a ) > set_a > set_b > a ).
thf(func_def_439,type,
sK68: set_b > set_d > ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_440,type,
sK69: set_b > set_d > ( b > d > d ) > ( b > d > d ) > d ).
thf(func_def_441,type,
sK70: set_d > set_b > ( b > d > d ) > b ).
thf(func_def_442,type,
sK71: set_d > set_b > ( b > d > d ) > d ).
thf(func_def_443,type,
sK72: set_a > set_c > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_444,type,
sK73: set_a > set_c > ( a > c > c ) > ( a > c > c ) > c ).
thf(func_def_445,type,
sK74: set_c > set_a > ( a > c > c ) > a ).
thf(func_def_446,type,
sK75: set_c > set_a > ( a > c > c ) > c ).
thf(func_def_447,type,
sK76: set_a > set_a > ( a > a > a ) > ( a > a > a ) > a ).
thf(func_def_448,type,
sK77: set_a > set_a > ( a > a > a ) > ( a > a > a ) > a ).
thf(func_def_449,type,
sK78: set_a > set_a > ( a > a > a ) > a ).
thf(func_def_450,type,
sK79: set_a > set_a > ( a > a > a ) > a ).
thf(func_def_451,type,
sK80: set_a > set_b > ( a > b > b ) > ( a > b > b ) > a ).
thf(func_def_452,type,
sK81: set_a > set_b > ( a > b > b ) > ( a > b > b ) > b ).
thf(func_def_453,type,
sK82: set_b > set_a > ( a > b > b ) > a ).
thf(func_def_454,type,
sK83: set_b > set_a > ( a > b > b ) > b ).
thf(func_def_455,type,
sK84: set_a > set_d > ( a > d > d ) > ( a > d > d ) > a ).
thf(func_def_456,type,
sK85: set_a > set_d > ( a > d > d ) > ( a > d > d ) > d ).
thf(func_def_457,type,
sK86: set_d > set_a > ( a > d > d ) > a ).
thf(func_def_458,type,
sK87: set_d > set_a > ( a > d > d ) > d ).
thf(func_def_459,type,
sK88: set_c > set_a > ( c > a > a ) > ( c > a > a ) > c ).
thf(func_def_460,type,
sK89: set_c > set_a > ( c > a > a ) > ( c > a > a ) > a ).
thf(func_def_461,type,
sK90: set_a > set_c > ( c > a > a ) > c ).
thf(func_def_462,type,
sK91: set_a > set_c > ( c > a > a ) > a ).
thf(func_def_463,type,
sK92: set_c > set_c > ( c > c > c ) > ( c > c > c ) > c ).
thf(func_def_464,type,
sK93: set_c > set_c > ( c > c > c ) > ( c > c > c ) > c ).
thf(func_def_465,type,
sK94: set_c > set_c > ( c > c > c ) > c ).
thf(func_def_466,type,
sK95: set_c > set_c > ( c > c > c ) > c ).
thf(func_def_467,type,
sK96: set_c > set_b > ( c > b > b ) > ( c > b > b ) > c ).
thf(func_def_468,type,
sK97: set_c > set_b > ( c > b > b ) > ( c > b > b ) > b ).
thf(func_def_469,type,
sK98: set_b > set_c > ( c > b > b ) > c ).
thf(func_def_470,type,
sK99: set_b > set_c > ( c > b > b ) > b ).
thf(func_def_471,type,
sK100: set_c > set_d > ( c > d > d ) > ( c > d > d ) > c ).
thf(func_def_472,type,
sK101: set_c > set_d > ( c > d > d ) > ( c > d > d ) > d ).
thf(func_def_473,type,
sK102: set_d > set_c > ( c > d > d ) > c ).
thf(func_def_474,type,
sK103: set_d > set_c > ( c > d > d ) > d ).
thf(func_def_475,type,
sK104: set_b > set_a > ( b > a > a ) > ( b > a > a ) > b ).
thf(func_def_476,type,
sK105: set_b > set_a > ( b > a > a ) > ( b > a > a ) > a ).
thf(func_def_477,type,
sK106: set_a > set_b > ( b > a > a ) > b ).
thf(func_def_478,type,
sK107: set_a > set_b > ( b > a > a ) > a ).
thf(func_def_479,type,
sK108: ( b > b ) > ( a > a ) > ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_480,type,
sK109: ( b > b ) > ( a > a ) > ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_481,type,
sK110: ( a > d > d ) > ( a > c > c ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > a > $o ) > a ).
thf(func_def_482,type,
sK111: ( a > d > d ) > ( a > c > c ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > a > $o ) > a ).
thf(func_def_483,type,
sK112: ( a > c > c ) > ( a > c > c ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > a ).
thf(func_def_484,type,
sK113: ( a > c > c ) > ( a > c > c ) > ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > a ).
thf(func_def_485,type,
sK114: ( a > b ) > ( a > a ) > ( a > b > $o ) > ( a > a > $o ) > a ).
thf(func_def_486,type,
sK115: ( a > b ) > ( a > a ) > ( a > b > $o ) > ( a > a > $o ) > a ).
thf(func_def_487,type,
sK116: ( a > a ) > ( a > a ) > ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_488,type,
sK117: ( a > a ) > ( a > a ) > ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_489,type,
sK118: ( b > d > d ) > ( a > c > c ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > b > $o ) > a ).
thf(func_def_490,type,
sK119: ( b > d > d ) > ( a > c > c ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > b > $o ) > b ).
thf(func_def_491,type,
sK120: ( d > d ) > ( c > c ) > ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_492,type,
sK121: ( d > d ) > ( c > c ) > ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_493,type,
sK122: ( b > d > d ) > b ).
thf(func_def_494,type,
sK123: ( a > c > c ) > a ).
thf(func_def_495,type,
sK124: ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_496,type,
sK125: ( a > a > $o ) > a ).
thf(func_def_497,type,
sK126: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_498,type,
sK127: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_499,type,
sK128: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_500,type,
sK129: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_501,type,
sK130: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_502,type,
sK131: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_503,type,
sK132: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_504,type,
sK133: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_505,type,
sK134: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_506,type,
sK135: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_507,type,
sK136: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_508,type,
sK137: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_509,type,
sK138: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_510,type,
sK139: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_511,type,
sK140: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_512,type,
sK141: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_513,type,
sK142: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_514,type,
sK143: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_515,type,
sK144: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_516,type,
sK145: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_517,type,
sK146: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_518,type,
sK147: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_519,type,
sK148: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_520,type,
sK149: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_521,type,
sK150: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_522,type,
sK151: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_523,type,
sK152: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_524,type,
sK153: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_525,type,
sK154: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_526,type,
sK155: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_527,type,
sK156: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_528,type,
sK157: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_529,type,
sK158: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_530,type,
sK159: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_531,type,
sK160: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_532,type,
sK161: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_533,type,
sK162: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_534,type,
sK163: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_535,type,
sK164: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_536,type,
sK165: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_537,type,
sK166: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_538,type,
sK167: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_539,type,
sK168: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_540,type,
sK169: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_541,type,
sK170: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_542,type,
sK171: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_543,type,
sK172: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_544,type,
sK173: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_545,type,
sK174: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_546,type,
sK175: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_547,type,
sK176: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_548,type,
sK177: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_549,type,
sK178: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_550,type,
sK179: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_551,type,
sK180: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_552,type,
sK181: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_553,type,
sK182: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( b > d > d ) > b ).
thf(func_def_554,type,
sK183: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( b > d > d ) > b ).
thf(func_def_555,type,
sK184: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( ( d > d ) > b ) > ( ( d > d ) > ( d > d ) > $o ) > d > d ).
thf(func_def_556,type,
sK185: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( ( d > d ) > b ) > ( ( d > d ) > ( d > d ) > $o ) > d > d ).
thf(func_def_557,type,
sK186: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( a > c > c ) > a ).
thf(func_def_558,type,
sK187: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( a > c > c ) > a ).
thf(func_def_559,type,
sK188: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( ( c > c ) > a ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_560,type,
sK189: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( ( c > c ) > a ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_561,type,
sK190: ( b > b > $o ) > ( b > b > $o ) > ( b > b ) > b ).
thf(func_def_562,type,
sK191: ( b > b > $o ) > ( b > b > $o ) > ( b > b ) > b ).
thf(func_def_563,type,
sK192: ( b > b > $o ) > ( b > b > $o ) > ( b > b ) > ( b > b > $o ) > b ).
thf(func_def_564,type,
sK193: ( b > b > $o ) > ( b > b > $o ) > ( b > b ) > ( b > b > $o ) > b ).
thf(func_def_565,type,
sK194: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > a ).
thf(func_def_566,type,
sK195: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > a ).
thf(func_def_567,type,
sK196: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > ( a > a > $o ) > a ).
thf(func_def_568,type,
sK197: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > ( a > a > $o ) > a ).
thf(func_def_569,type,
vNOT: $o > $o ).
thf(func_def_570,type,
sK198: a ).
thf(func_def_571,type,
sK199: a ).
thf(func_def_572,type,
sK200: ( b > d > d ) > b ).
thf(func_def_573,type,
sK201: ( b > d > d ) > b ).
thf(func_def_574,type,
sK202: ( a > c > c ) > a ).
thf(func_def_575,type,
sK203: ( a > c > c ) > a ).
thf(func_def_576,type,
sK204: ( a > c > c ) > ( a > a ) > a ).
thf(func_def_577,type,
sK205: ( a > c > c ) > ( a > a ) > a > c > c ).
thf(func_def_578,type,
sK206: ( a > c > c ) > ( a > a ) > a ).
thf(func_def_579,type,
sK207: ( b > d > d ) > ( b > b ) > b ).
thf(func_def_580,type,
sK208: ( b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_581,type,
sK209: ( b > d > d ) > ( b > b ) > b ).
thf(func_def_582,type,
sK210: ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_583,type,
sK211: ( a > c > c ) > ( a > c > c ) > a > a ).
thf(func_def_584,type,
sK212: ( a > c > c ) > ( a > c > c ) > a > a ).
thf(func_def_585,type,
sK213: ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_586,type,
sK214: ( b > d > d ) > ( b > d > d ) > b > b ).
thf(func_def_587,type,
sK215: ( b > d > d ) > ( b > d > d ) > b > b ).
thf(func_def_588,type,
sK216: ( a > c > c ) > a ).
thf(func_def_589,type,
sK217: ( a > c > c ) > a ).
thf(func_def_590,type,
sK218: ( a > c > c ) > a ).
thf(func_def_591,type,
sK219: ( b > d > d ) > b ).
thf(func_def_592,type,
sK220: ( b > d > d ) > b ).
thf(func_def_593,type,
sK221: ( b > d > d ) > b ).
thf(func_def_594,type,
sK222: ( b > d > d ) > b ).
thf(func_def_595,type,
sK223: ( b > d > d ) > b ).
thf(func_def_596,type,
sK224: ( b > d > d ) > b ).
thf(func_def_597,type,
sK225: ( b > d > d ) > b ).
thf(func_def_598,type,
sK226: ( b > d > d ) > b ).
thf(func_def_599,type,
sK227: ( b > d > d ) > b ).
thf(func_def_600,type,
sK228: ( a > c > c ) > a ).
thf(func_def_601,type,
sK229: ( a > c > c ) > a ).
thf(func_def_602,type,
sK230: ( a > c > c ) > a ).
thf(func_def_603,type,
sK231: ( a > c > c ) > a ).
thf(func_def_604,type,
sK232: ( a > c > c ) > a ).
thf(func_def_605,type,
sK233: ( a > c > c ) > a ).
thf(func_def_606,type,
sK234: ( c > d > $o ) > ( c > d > $o ) > ( a > c > c ) > ( a > b > $o ) > ( b > d > d ) > b ).
thf(func_def_607,type,
sK235: ( c > d > $o ) > ( a > c > c ) > ( a > b > $o ) > ( b > d > d ) > ( c > d > $o ) > a ).
thf(func_def_608,type,
sK236: ( c > c > $o ) > ( a > c > c ) > ( a > a > $o ) > ( a > c > c ) > ( c > c > $o ) > a ).
thf(func_def_609,type,
sK237: ( c > c > $o ) > ( a > c > c ) > ( a > a > $o ) > ( a > c > c ) > ( c > c > $o ) > a ).
thf(func_def_610,type,
sK238: ( c > d > $o ) > ( a > c > c ) > ( a > a > $o ) > ( a > d > d ) > ( c > d > $o ) > a ).
thf(func_def_611,type,
sK239: ( c > d > $o ) > ( a > c > c ) > ( a > a > $o ) > ( a > d > d ) > ( c > d > $o ) > a ).
thf(func_def_612,type,
sK240: ( a > c > c ) > a ).
thf(func_def_613,type,
sK241: ( a > c > c ) > a ).
thf(func_def_614,type,
sK242: ( a > c > c ) > a ).
thf(func_def_615,type,
sK243: ( a > c > c ) > a ).
thf(func_def_616,type,
sK244: ( a > c > c ) > a ).
thf(func_def_617,type,
sK245: ( a > c > c ) > a ).
thf(func_def_618,type,
sK246: ( b > d > d ) > b ).
thf(func_def_619,type,
sK247: ( b > d > d ) > b ).
thf(func_def_620,type,
sK248: ( b > d > d ) > b ).
thf(func_def_621,type,
sK249: ( b > d > d ) > b ).
thf(func_def_622,type,
sK250: ( b > d > d ) > b ).
thf(func_def_623,type,
sK251: ( b > d > d ) > b ).
thf(func_def_624,type,
sK252: ( a > c > c ) > a ).
thf(func_def_625,type,
sK253: ( a > c > c ) > a ).
thf(func_def_626,type,
sK254: ( a > c > c ) > a ).
thf(func_def_627,type,
sK255: ( a > c > c ) > a ).
thf(func_def_628,type,
sK256: ( a > c > c ) > a ).
thf(func_def_629,type,
sK257: ( a > c > c ) > a ).
thf(func_def_630,type,
sK258: ( b > d > d ) > b ).
thf(func_def_631,type,
sK259: ( b > d > d ) > b ).
thf(func_def_632,type,
sK260: ( b > d > d ) > b ).
thf(func_def_633,type,
sK261: ( a > c > c ) > a ).
thf(func_def_634,type,
sK262: ( a > c > c ) > a ).
thf(func_def_635,type,
sK263: ( a > c > c ) > a ).
thf(func_def_636,type,
sK264: ( b > d > d ) > b ).
thf(func_def_637,type,
sK265: ( b > d > d ) > b ).
thf(func_def_638,type,
sK266: ( b > d > d ) > b ).
thf(func_def_639,type,
sK267: ( b > d > d ) > b ).
thf(func_def_640,type,
sK268: ( b > d > d ) > b ).
thf(func_def_641,type,
sK269: ( a > c > c ) > a ).
thf(func_def_642,type,
sK270: ( a > c > c ) > a ).
thf(func_def_643,type,
sK271: ( b > d > d ) > b ).
thf(func_def_644,type,
sK272: ( b > d > d ) > b ).
thf(func_def_645,type,
sK273: ( a > c > c ) > a ).
thf(func_def_646,type,
sK274: ( a > c > c ) > a ).
thf(func_def_647,type,
sK275: ( a > c > c ) > a ).
thf(func_def_648,type,
sK276: ( a > c > c ) > a ).
thf(func_def_649,type,
sK277: ( b > d > d ) > b ).
thf(func_def_650,type,
sK278: ( b > d > d ) > b ).
thf(func_def_651,type,
sK279: ( a > c > c ) > a ).
thf(func_def_652,type,
sK280: ( a > c > c ) > a ).
thf(func_def_653,type,
sK281: ( b > d > d ) > b ).
thf(func_def_654,type,
sK282: ( b > d > d ) > b ).
thf(func_def_655,type,
sK283: ( a > c > c ) > a ).
thf(func_def_656,type,
sK284: ( a > c > c ) > a ).
thf(func_def_657,type,
sK285: ( b > d > d ) > b ).
thf(func_def_658,type,
sK286: ( b > d > d ) > b ).
thf(func_def_659,type,
sK287: ( b > d > d ) > b ).
thf(func_def_660,type,
sK288: ( a > c > c ) > a ).
thf(func_def_661,type,
sK289: ( a > c > c ) > a ).
thf(func_def_662,type,
sK290: ( a > c > c ) > a ).
thf(func_def_663,type,
sK291: ( b > d > d ) > b ).
thf(func_def_664,type,
sK292: ( b > d > d ) > b ).
thf(func_def_665,type,
sK293: ( a > c > c ) > a ).
thf(func_def_666,type,
sK294: ( a > c > c ) > a ).
thf(func_def_667,type,
sK295: ( b > d > d ) > b ).
thf(func_def_668,type,
sK296: ( b > d > d ) > b ).
thf(func_def_669,type,
sK297: ( b > d > d ) > b ).
thf(func_def_670,type,
sK298: ( b > d > d ) > b ).
thf(func_def_671,type,
sK299: ( a > c > c ) > a ).
thf(func_def_672,type,
sK300: ( a > c > c ) > a ).
thf(func_def_673,type,
sK301: ( a > c > c ) > a ).
thf(func_def_674,type,
sK302: ( a > c > c ) > a ).
thf(func_def_675,type,
sK303: ( b > d > d ) > b ).
thf(func_def_676,type,
sK304: ( b > d > d ) > b ).
thf(func_def_677,type,
sK305: ( a > c > c ) > a ).
thf(func_def_678,type,
sK306: ( a > c > c ) > a ).
thf(func_def_679,type,
sK307: c ).
thf(f1,axiom,
finite746615251te_a_c @ f1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_assms_I2_J) ).
thf(f19,axiom,
( finite746615251te_a_c
= ( ^ [X0: a > c > c] :
! [X1: a,X2: a] :
( ( comp_c_c_c @ ( X0 @ X1 ) @ ( X0 @ X2 ) )
= ( comp_c_c_c @ ( X0 @ X2 ) @ ( X0 @ X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_comp__fun__commute__def) ).
thf(f364,conjecture,
finite746615251te_a_c @ f1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(f365,negated_conjecture,
~ ( finite746615251te_a_c @ f1 ),
inference(negated_conjecture,[status(cth)],[f364]) ).
thf(f366,plain,
finite746615251te_a_c @ f1,
inference(rectify,[],[f1]) ).
thf(f367,plain,
( ( finite746615251te_a_c @ f1 )
= $true ),
inference(fool_elimination,[],[f366]) ).
thf(f402,plain,
( finite746615251te_a_c
= ( ^ [Y0: a > c > c] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( comp_c_c_c @ ( Y0 @ Y2 ) @ ( Y0 @ Y1 ) )
= ( comp_c_c_c @ ( Y0 @ Y1 ) @ ( Y0 @ Y2 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f19]) ).
thf(f849,plain,
~ ( finite746615251te_a_c @ f1 ),
inference(rectify,[],[f365]) ).
thf(f850,plain,
( ( finite746615251te_a_c @ f1 )
!= $true ),
inference(fool_elimination,[],[f849]) ).
thf(f851,plain,
( ( finite746615251te_a_c @ f1 )
!= $true ),
inference(flattening,[],[f850]) ).
thf(f1353,plain,
( ( finite746615251te_a_c @ f1 )
= $true ),
inference(cnf_transformation,[],[f367]) ).
thf(f1371,plain,
( finite746615251te_a_c
= ( ^ [Y0: a > c > c] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( comp_c_c_c @ ( Y0 @ Y2 ) @ ( Y0 @ Y1 ) )
= ( comp_c_c_c @ ( Y0 @ Y1 ) @ ( Y0 @ Y2 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f402]) ).
thf(f1923,plain,
( ( finite746615251te_a_c @ f1 )
!= $true ),
inference(cnf_transformation,[],[f851]) ).
thf(f1930,plain,
( $true
= ( ^ [Y0: a > c > c] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( comp_c_c_c @ ( Y0 @ Y2 ) @ ( Y0 @ Y1 ) )
= ( comp_c_c_c @ ( Y0 @ Y1 ) @ ( Y0 @ Y2 ) ) ) ) )
@ f1 ) ),
inference(definition_unfolding,[],[f1353,f1371]) ).
thf(f2158,plain,
( $true
!= ( ^ [Y0: a > c > c] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( comp_c_c_c @ ( Y0 @ Y2 ) @ ( Y0 @ Y1 ) )
= ( comp_c_c_c @ ( Y0 @ Y1 ) @ ( Y0 @ Y2 ) ) ) ) )
@ f1 ) ),
inference(definition_unfolding,[],[f1923,f1371]) ).
thf(f2206,plain,
( $true
!= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( comp_c_c_c @ ( f1 @ Y1 ) @ ( f1 @ Y0 ) )
= ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ Y1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f2158]) ).
thf(f2207,plain,
( $false
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( comp_c_c_c @ ( f1 @ Y1 ) @ ( f1 @ Y0 ) )
= ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ Y1 ) ) ) )
@ sK198 ) ),
inference(sigma_proxy_clausification,[],[f2206]) ).
thf(f2208,plain,
( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ sK198 ) )
= ( comp_c_c_c @ ( f1 @ sK198 ) @ ( f1 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f2207]) ).
thf(f2209,plain,
( $false
= ( ^ [Y0: a] :
( ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ sK198 ) )
= ( comp_c_c_c @ ( f1 @ sK198 ) @ ( f1 @ Y0 ) ) )
@ sK199 ) ),
inference(sigma_proxy_clausification,[],[f2208]) ).
thf(f2210,plain,
( $false
= ( ( comp_c_c_c @ ( f1 @ sK199 ) @ ( f1 @ sK198 ) )
= ( comp_c_c_c @ ( f1 @ sK198 ) @ ( f1 @ sK199 ) ) ) ),
inference(beta-eta_normalization,[],[f2209]) ).
thf(f2211,plain,
( ( comp_c_c_c @ ( f1 @ sK199 ) @ ( f1 @ sK198 ) )
!= ( comp_c_c_c @ ( f1 @ sK198 ) @ ( f1 @ sK199 ) ) ),
inference(equality_proxy_clausification,[],[f2210]) ).
thf(f2838,plain,
( $true
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( comp_c_c_c @ ( f1 @ Y1 ) @ ( f1 @ Y0 ) )
= ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ Y1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1930]) ).
thf(f2839,plain,
! [X1: a] :
( $true
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( comp_c_c_c @ ( f1 @ Y1 ) @ ( f1 @ Y0 ) )
= ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ Y1 ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f2838]) ).
thf(f2840,plain,
! [X1: a] :
( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ X1 ) )
= ( comp_c_c_c @ ( f1 @ X1 ) @ ( f1 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f2839]) ).
thf(f2841,plain,
! [X2: a,X1: a] :
( $true
= ( ^ [Y0: a] :
( ( comp_c_c_c @ ( f1 @ Y0 ) @ ( f1 @ X1 ) )
= ( comp_c_c_c @ ( f1 @ X1 ) @ ( f1 @ Y0 ) ) )
@ X2 ) ),
inference(pi_proxy_clausification,[],[f2840]) ).
thf(f2842,plain,
! [X2: a,X1: a] :
( $true
= ( ( comp_c_c_c @ ( f1 @ X2 ) @ ( f1 @ X1 ) )
= ( comp_c_c_c @ ( f1 @ X1 ) @ ( f1 @ X2 ) ) ) ),
inference(beta-eta_normalization,[],[f2841]) ).
thf(f2843,plain,
! [X2: a,X1: a] :
( ( comp_c_c_c @ ( f1 @ X2 ) @ ( f1 @ X1 ) )
= ( comp_c_c_c @ ( f1 @ X1 ) @ ( f1 @ X2 ) ) ),
inference(equality_proxy_clausification,[],[f2842]) ).
thf(f2854,plain,
( ( comp_c_c_c @ ( f1 @ sK198 ) @ ( f1 @ sK199 ) )
!= ( comp_c_c_c @ ( f1 @ sK198 ) @ ( f1 @ sK199 ) ) ),
inference(constrained_superposition,[],[f2211,f2843]) ).
thf(f2855,plain,
$false,
inference(trivial_inequality_removal,[],[f2854]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP128^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n016.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 20:02:35 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.55/0.50 % (833834)Will run a generic schedule for satisfiability detection.
% 1.55/0.50 % (833844)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=622735804:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.55/0.50 % (833840)% WARNING: option uhcvi not known.
% 1.55/0.50 % (833840)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3763177730:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.55/0.50 % (833841)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=241663363:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.55/0.50 % (833843)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3900928241:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.55/0.50 % (833839)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2442039550_2999 on theBenchmark for (2999ds/0Mi)
% 1.55/0.50 % (833842)dis+10_1_sil=32000:sp=arity:random_seed=2784157469:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.55/0.50 % (833845)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4146125871:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.55/0.50 % (833844)Instruction limit reached!
% 1.55/0.50 % (833844)------------------------------
% 1.55/0.50 % (833844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833844)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833844)Termination reason: Instruction limit
% 1.55/0.50 % (833844)Termination phase: Preprocessing 3
% 1.55/0.50 % (833844)Time elapsed: 0.029 s
% 1.55/0.50 % (833844)Peak memory usage: 12 MB
% 1.55/0.50 % (833844)Instructions burned: 134 (million)
% 1.55/0.50 % (833853)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2539971128:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.55/0.50 % (833842)Instruction limit reached!
% 1.55/0.50 % (833842)------------------------------
% 1.55/0.50 % (833842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833842)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833842)Termination reason: Instruction limit
% 1.55/0.50 % (833842)Termination phase: Property scanning
% 1.55/0.50 % (833842)Time elapsed: 0.041 s
% 1.55/0.50 % (833842)Peak memory usage: 11 MB
% 1.55/0.50 % (833842)Instructions burned: 103 (million)
% 1.55/0.50 % (833843)Instruction limit reached!
% 1.55/0.50 % (833843)------------------------------
% 1.55/0.50 % (833843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833843)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833843)Termination reason: Instruction limit
% 1.55/0.50 % (833843)Termination phase: Unused predicate definition removal
% 1.55/0.50 % (833843)Time elapsed: 0.047 s
% 1.55/0.50 % (833843)Peak memory usage: 11 MB
% 1.55/0.50 % (833843)Instructions burned: 121 (million)
% 1.55/0.50 % (833840)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.55/0.50 % (833856)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3807418979:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.55/0.50 % (833855)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2083001310:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.55/0.50 % Exception at run slice level
% 1.55/0.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.55/0.50 % (833859)ott-21_1_sil=16000:fs=off:random_seed=3298176198:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.55/0.50 % (833840)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.55/0.50 % (833856)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.55/0.50 % (833845)Instruction limit reached!
% 1.55/0.50 % (833845)------------------------------
% 1.55/0.50 % (833845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833845)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833845)Termination reason: Instruction limit
% 1.55/0.50 % (833845)Termination phase: Property scanning
% 1.55/0.50 % (833845)Time elapsed: 0.118 s
% 1.55/0.50 % (833845)Peak memory usage: 12 MB
% 1.55/0.50 % (833845)Instructions burned: 159 (million)
% 1.55/0.50 % Exception at run slice level
% 1.55/0.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.55/0.50 % (833859)Instruction limit reached!
% 1.55/0.50 % (833859)------------------------------
% 1.55/0.50 % (833859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833859)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833859)Termination reason: Instruction limit
% 1.55/0.50 % (833859)Termination phase: Property scanning
% 1.55/0.50 % (833859)Time elapsed: 0.041 s
% 1.55/0.50 % (833859)Peak memory usage: 12 MB
% 1.55/0.50 % (833859)Instructions burned: 181 (million)
% 1.55/0.50 % (833855)Instruction limit reached!
% 1.55/0.50 % (833855)------------------------------
% 1.55/0.50 % (833855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833855)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833855)Termination reason: Instruction limit
% 1.55/0.50 % (833855)Termination phase: Preprocessing 3
% 1.55/0.50 % (833855)Time elapsed: 0.071 s
% 1.55/0.50 % (833855)Peak memory usage: 12 MB
% 1.55/0.50 % (833855)Instructions burned: 131 (million)
% 1.55/0.50 % (833861)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2221695088:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.55/0.50 % (833863)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=787301759:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.55/0.50 % (833862)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=976955646:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.55/0.50 % (833864)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3168741979:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.55/0.50 % (833856)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.55/0.50 % (833856) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-833834-833856"...
% 1.55/0.50 % (833856)...printing done.
% 1.55/0.50 % (833856)Refutation found. Thanks to Tanya!
% 1.55/0.50 % SZS status Theorem for theBenchmark
% 1.55/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 1.55/0.50 % (833856)------------------------------
% 1.55/0.50 % (833856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.50 % (833856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.50 % (833856)CaDiCaL version: 2.1.3
% 1.55/0.50 % (833856)Termination reason: Refutation
% 1.55/0.50 % (833856)Time elapsed: 0.150 s
% 1.55/0.50 % (833856)Peak memory usage: 15 MB
% 1.55/0.50 % (833856)Instructions burned: 359 (million)
% 1.55/0.50 % (833834)Success in time 0.274 s
% 1.55/0.50 % Vampire exiting
%------------------------------------------------------------------------------