%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n004.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:08:28 AM UTC 2026
% Result : Theorem 1.30s 0.62s
% Output : Refutation 1.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 3
% Syntax : Number of formulae : 17 ( 16 unt; 0 typ; 1 def)
% Number of atoms : 30 ( 6 equ; 0 cnn)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 19 ( 7 ~; 0 |; 0 &; 11 @)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 579 ( 576 usr; 3 con; 0-7 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?; 0 :)
% 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_360,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_361,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_362,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_363,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_366,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_367,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_368,type,
vAND: $o > $o > $o ).
thf(func_def_369,type,
vIMP: $o > $o > $o ).
thf(func_def_370,type,
sP0: set_c > set_d > ( c > d > d ) > ( c > d > d ) > $o ).
thf(func_def_371,type,
sP1: set_c > set_c > ( c > c > c ) > ( c > c > c ) > $o ).
thf(func_def_372,type,
sP2: set_a > ( a > a > a ) > set_a > $o ).
thf(func_def_373,type,
sP3: set_a > ( a > d > d ) > set_d > $o ).
thf(func_def_374,type,
sP4: set_a > set_c > ( a > c > c ) > ( a > c > c ) > $o ).
thf(func_def_375,type,
sP5: set_a > ( a > b > b ) > set_b > $o ).
thf(func_def_376,type,
sP6: set_b > ( b > d > d ) > set_d > $o ).
thf(func_def_377,type,
sP7: set_c > ( c > a > a ) > ( c > a > a ) > set_a > $o ).
thf(func_def_378,type,
sP8: set_a > ( b > a > a ) > ( b > a > a ) > set_b > $o ).
thf(func_def_379,type,
sP9: ( c > b > b ) > set_b > set_c > $o ).
thf(func_def_380,type,
sK10: ( a > a ) > ( a > c > c ) > a > c > c ).
thf(func_def_381,type,
sK11: ( a > a ) > ( a > c > c ) > a ).
thf(func_def_382,type,
sK12: ( a > a ) > ( a > c > c ) > a ).
thf(func_def_383,type,
sK13: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_384,type,
sK14: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_385,type,
sK15: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_386,type,
sK16: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_387,type,
sK17: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > ( a > a > $o ) > a ).
thf(func_def_388,type,
sK18: ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > ( a > a > $o ) > a ).
thf(func_def_389,type,
sK19: ( a > a ) > ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_390,type,
sK20: ( a > a ) > ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_391,type,
sK21: ( a > a > a ) > ( a > a > a ) > set_a > set_a > a ).
thf(func_def_392,type,
sK22: ( a > a > a ) > ( a > a > a ) > set_a > set_a > a ).
thf(func_def_393,type,
sK23: ( a > a > a ) > set_a > set_a > a ).
thf(func_def_394,type,
sK24: ( a > a > a ) > set_a > set_a > a ).
thf(func_def_395,type,
sK25: ( a > a > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > d > d ) > ( a > c > c ) > a ).
thf(func_def_396,type,
sK26: ( a > a > $o ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > d > d ) > ( a > c > c ) > a ).
thf(func_def_397,type,
sK27: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_398,type,
sK28: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_399,type,
sK29: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_400,type,
sK30: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_401,type,
sK31: ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_402,type,
sK32: ( b > d > d ) > b ).
thf(func_def_403,type,
sK33: ( c > c ) > ( c > d > $o ) > ( c > d > $o ) > ( d > d ) > d ).
thf(func_def_404,type,
sK34: ( c > c ) > ( c > d > $o ) > ( c > d > $o ) > ( d > d ) > c ).
thf(func_def_405,type,
sK35: ( b > d > d ) > ( b > b ) > b > d > d ).
thf(func_def_406,type,
sK36: ( b > d > d ) > ( b > b ) > b ).
thf(func_def_407,type,
sK37: ( b > d > d ) > ( b > b ) > b ).
thf(func_def_408,type,
sK38: ( a > c > c ) > ( c > c ) > ( a > c > c ) > c ).
thf(func_def_409,type,
sK39: ( a > c > c ) > ( c > c ) > ( a > c > c ) > a ).
thf(func_def_410,type,
sK40: set_a > set_c > ( a > c > c ) > a ).
thf(func_def_411,type,
sK41: set_a > set_c > ( a > c > c ) > c ).
thf(func_def_412,type,
sK42: set_a > set_c > ( a > c > c ) > ( a > c > c ) > c ).
thf(func_def_413,type,
sK43: set_a > set_c > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_414,type,
sK44: ( c > c > $o ) > ( c > c > $o ) > ( a > a > $o ) > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_415,type,
sK45: ( c > c > $o ) > ( c > c > $o ) > ( a > a > $o ) > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_416,type,
sK46: set_c > set_d > ( c > d > d ) > ( c > d > d ) > c ).
thf(func_def_417,type,
sK47: set_c > set_d > ( c > d > d ) > ( c > d > d ) > d ).
thf(func_def_418,type,
sK48: ( c > d > d ) > set_d > set_c > d ).
thf(func_def_419,type,
sK49: ( c > d > d ) > set_d > set_c > c ).
thf(func_def_420,type,
sK50: set_c > set_b > ( c > b > b ) > ( c > b > b ) > b ).
thf(func_def_421,type,
sK51: set_c > set_b > ( c > b > b ) > ( c > b > b ) > c ).
thf(func_def_422,type,
sK52: set_c > set_b > ( c > b > b ) > b ).
thf(func_def_423,type,
sK53: set_c > set_b > ( c > b > b ) > c ).
thf(func_def_424,type,
sK54: ( c > d > d ) > set_d > set_c > ( c > d > d ) > d ).
thf(func_def_425,type,
sK55: ( c > d > d ) > set_d > set_c > ( c > d > d ) > c ).
thf(func_def_426,type,
sK56: set_d > set_c > ( c > d > d ) > d ).
thf(func_def_427,type,
sK57: set_d > set_c > ( c > d > d ) > c ).
thf(func_def_428,type,
sK58: ( b > b ) > ( a > b > $o ) > ( a > b > $o ) > ( a > a ) > a ).
thf(func_def_429,type,
sK59: ( b > b ) > ( a > b > $o ) > ( a > b > $o ) > ( a > a ) > b ).
thf(func_def_430,type,
sK60: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_431,type,
sK61: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_432,type,
sK62: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_433,type,
sK63: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_434,type,
sK64: b > ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_435,type,
sK65: ( b > d > d ) > ( b > d > d ) > b > b ).
thf(func_def_436,type,
sK66: ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_437,type,
sK67: ( b > d > d ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > c > c ) > ( a > b > $o ) > a ).
thf(func_def_438,type,
sK68: ( b > d > d ) > ( ( c > c ) > ( d > d ) > $o ) > ( a > c > c ) > ( a > b > $o ) > b ).
thf(func_def_439,type,
sK69: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_440,type,
sK70: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_441,type,
sK71: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_442,type,
sK72: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_443,type,
sK73: set_c > set_c > ( c > c > c ) > ( c > c > c ) > c ).
thf(func_def_444,type,
sK74: set_c > set_c > ( c > c > c ) > ( c > c > c ) > c ).
thf(func_def_445,type,
sK75: set_c > ( c > c > c ) > set_c > c ).
thf(func_def_446,type,
sK76: set_c > ( c > c > c ) > set_c > c ).
thf(func_def_447,type,
sK77: ( a > b > b ) > set_a > set_b > ( a > b > b ) > b ).
thf(func_def_448,type,
sK78: ( a > b > b ) > set_a > set_b > ( a > b > b ) > a ).
thf(func_def_449,type,
sK79: set_a > set_b > ( a > b > b ) > a ).
thf(func_def_450,type,
sK80: set_a > set_b > ( a > b > b ) > b ).
thf(func_def_451,type,
sK81: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_452,type,
sK82: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_453,type,
sK83: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_454,type,
sK84: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_455,type,
sK85: ( a > b > $o ) > ( b > d > d ) > ( c > d > $o ) > ( a > c > c ) > ( c > d > $o ) > b ).
thf(func_def_456,type,
sK86: ( a > b > $o ) > ( b > d > d ) > ( c > d > $o ) > ( a > c > c ) > ( c > d > $o ) > a ).
thf(func_def_457,type,
sK87: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( b > d > d ) > b ).
thf(func_def_458,type,
sK88: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( b > d > d ) > b ).
thf(func_def_459,type,
sK89: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( ( d > d ) > b ) > d > d ).
thf(func_def_460,type,
sK90: ( ( d > d ) > ( d > d ) > $o ) > ( b > b > $o ) > ( ( d > d ) > ( d > d ) > $o ) > ( ( d > d ) > b ) > d > d ).
thf(func_def_461,type,
sK91: ( c > d > $o ) > ( a > a > $o ) > ( a > c > c ) > ( a > d > d ) > ( c > d > $o ) > a ).
thf(func_def_462,type,
sK92: ( c > d > $o ) > ( a > a > $o ) > ( a > c > c ) > ( a > d > d ) > ( c > d > $o ) > a ).
thf(func_def_463,type,
sK93: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_464,type,
sK94: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_465,type,
sK95: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_466,type,
sK96: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_467,type,
sK97: ( b > a > a ) > set_a > set_b > a ).
thf(func_def_468,type,
sK98: ( b > a > a ) > set_a > set_b > b ).
thf(func_def_469,type,
sK99: ( b > a > a ) > set_a > ( b > a > a ) > set_b > a ).
thf(func_def_470,type,
sK100: ( b > a > a ) > set_a > ( b > a > a ) > set_b > b ).
thf(func_def_471,type,
sK101: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_472,type,
sK102: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_473,type,
sK103: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_474,type,
sK104: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_475,type,
sK105: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_476,type,
sK106: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_477,type,
sK107: ( c > d > $o ) > ( c > d > $o ) > d ).
thf(func_def_478,type,
sK108: ( c > d > $o ) > ( c > d > $o ) > c ).
thf(func_def_479,type,
sK109: set_a > ( a > a > a ) > set_a > a ).
thf(func_def_480,type,
sK110: set_a > ( a > a > a ) > set_a > a ).
thf(func_def_481,type,
sK111: set_a > ( a > a > a ) > set_a > ( a > a > a ) > a ).
thf(func_def_482,type,
sK112: set_a > ( a > a > a ) > set_a > ( a > a > a ) > a ).
thf(func_def_483,type,
sK113: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_484,type,
sK114: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_485,type,
sK115: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_486,type,
sK116: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_487,type,
sK117: ( a > a > $o ) > a ).
thf(func_def_488,type,
sK118: ( b > d > d ) > ( b > d > d ) > ( d > d ) > d ).
thf(func_def_489,type,
sK119: ( b > d > d ) > ( b > d > d ) > ( d > d ) > b ).
thf(func_def_490,type,
sK120: set_a > ( a > d > d ) > set_d > a ).
thf(func_def_491,type,
sK121: set_a > ( a > d > d ) > set_d > d ).
thf(func_def_492,type,
sK122: ( a > d > d ) > set_d > ( a > d > d ) > set_a > d ).
thf(func_def_493,type,
sK123: ( a > d > d ) > set_d > ( a > d > d ) > set_a > a ).
thf(func_def_494,type,
sK124: ( c > a > a ) > ( c > a > a ) > set_a > set_c > a ).
thf(func_def_495,type,
sK125: ( c > a > a ) > ( c > a > a ) > set_a > set_c > c ).
thf(func_def_496,type,
sK126: ( c > a > a ) > set_a > set_c > a ).
thf(func_def_497,type,
sK127: ( c > a > a ) > set_a > set_c > c ).
thf(func_def_498,type,
sK128: set_a > set_c > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_499,type,
sK129: set_a > set_c > ( a > c > c ) > ( a > c > c ) > c ).
thf(func_def_500,type,
sK130: set_a > set_c > ( a > c > c ) > c ).
thf(func_def_501,type,
sK131: set_a > set_c > ( a > c > c ) > a ).
thf(func_def_502,type,
sK132: set_a > ( a > d > d ) > set_d > a ).
thf(func_def_503,type,
sK133: set_a > ( a > d > d ) > set_d > d ).
thf(func_def_504,type,
sK134: set_a > ( a > d > d ) > ( a > d > d ) > set_d > d ).
thf(func_def_505,type,
sK135: set_a > ( a > d > d ) > ( a > d > d ) > set_d > a ).
thf(func_def_506,type,
sK136: ( a > b > $o ) > ( a > b ) > ( a > a ) > ( a > a > $o ) > a ).
thf(func_def_507,type,
sK137: ( a > b > $o ) > ( a > b ) > ( a > a ) > ( a > a > $o ) > a ).
thf(func_def_508,type,
sK138: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_509,type,
sK139: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_510,type,
sK140: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_511,type,
sK141: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_512,type,
sK142: ( b > b ) > ( b > b > $o ) > ( b > b > $o ) > ( b > b > $o ) > b ).
thf(func_def_513,type,
sK143: ( b > b ) > ( b > b > $o ) > ( b > b > $o ) > ( b > b > $o ) > b ).
thf(func_def_514,type,
sK144: ( b > b > $o ) > ( b > b ) > ( b > b > $o ) > b ).
thf(func_def_515,type,
sK145: ( b > b > $o ) > ( b > b ) > ( b > b > $o ) > b ).
thf(func_def_516,type,
sK146: set_a > ( a > b > b ) > set_b > b ).
thf(func_def_517,type,
sK147: set_a > ( a > b > b ) > set_b > a ).
thf(func_def_518,type,
sK148: set_b > ( a > b > b ) > set_a > ( a > b > b ) > b ).
thf(func_def_519,type,
sK149: set_b > ( a > b > b ) > set_a > ( a > b > b ) > a ).
thf(func_def_520,type,
sK150: set_d > ( b > d > d ) > set_b > b ).
thf(func_def_521,type,
sK151: set_d > ( b > d > d ) > set_b > d ).
thf(func_def_522,type,
sK152: set_d > ( b > d > d ) > set_b > ( b > d > d ) > b ).
thf(func_def_523,type,
sK153: set_d > ( b > d > d ) > set_b > ( b > d > d ) > d ).
thf(func_def_524,type,
sK154: ( a > c > c ) > a ).
thf(func_def_525,type,
sK155: ( a > a ) > ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > a ).
thf(func_def_526,type,
sK156: ( a > a ) > ( a > a > $o ) > ( a > a > $o ) > ( a > a ) > a ).
thf(func_def_527,type,
sK157: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_528,type,
sK158: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_529,type,
sK159: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_530,type,
sK160: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_531,type,
sK161: set_b > ( b > d > d ) > set_d > d ).
thf(func_def_532,type,
sK162: set_b > ( b > d > d ) > set_d > b ).
thf(func_def_533,type,
sK163: set_d > set_b > ( b > d > d ) > ( b > d > d ) > b ).
thf(func_def_534,type,
sK164: set_d > set_b > ( b > d > d ) > ( b > d > d ) > d ).
thf(func_def_535,type,
sK165: ( a > b > $o ) > ( a > b > $o ) > a ).
thf(func_def_536,type,
sK166: ( a > b > $o ) > ( a > b > $o ) > b ).
thf(func_def_537,type,
sK167: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > c > c ).
thf(func_def_538,type,
sK168: ( ( c > c ) > ( d > d ) > $o ) > ( ( c > c ) > ( d > d ) > $o ) > d > d ).
thf(func_def_539,type,
sK169: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_540,type,
sK170: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_541,type,
sK171: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_542,type,
sK172: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_543,type,
sK173: set_c > ( c > a > a ) > ( c > a > a ) > set_a > c ).
thf(func_def_544,type,
sK174: set_c > ( c > a > a ) > ( c > a > a ) > set_a > a ).
thf(func_def_545,type,
sK175: set_a > set_c > ( c > a > a ) > c ).
thf(func_def_546,type,
sK176: set_a > set_c > ( c > a > a ) > a ).
thf(func_def_547,type,
sK177: set_a > ( b > a > a ) > ( b > a > a ) > set_b > a ).
thf(func_def_548,type,
sK178: set_a > ( b > a > a ) > ( b > a > a ) > set_b > b ).
thf(func_def_549,type,
sK179: set_b > ( b > a > a ) > set_a > a ).
thf(func_def_550,type,
sK180: set_b > ( b > a > a ) > set_a > b ).
thf(func_def_551,type,
sK181: ( a > c > c ) > a ).
thf(func_def_552,type,
sK182: ( a > c > c ) > a ).
thf(func_def_553,type,
sK183: ( c > b > b ) > set_b > set_c > b ).
thf(func_def_554,type,
sK184: ( c > b > b ) > set_b > set_c > c ).
thf(func_def_555,type,
sK185: ( c > b > b ) > set_b > set_c > ( c > b > b ) > b ).
thf(func_def_556,type,
sK186: ( c > b > b ) > set_b > set_c > ( c > b > b ) > c ).
thf(func_def_557,type,
sK187: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_558,type,
sK188: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_559,type,
sK189: ( b > d > d ) > b ).
thf(func_def_560,type,
sK190: ( b > d > d ) > b ).
thf(func_def_561,type,
sK191: ( a > a > $o ) > ( a > c > c ) > ( ( c > c ) > ( c > c ) > $o ) > a ).
thf(func_def_562,type,
sK192: ( a > a > $o ) > ( a > c > c ) > ( ( c > c ) > ( c > c ) > $o ) > a ).
thf(func_def_563,type,
sK193: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( ( c > c ) > a ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_564,type,
sK194: ( ( c > c ) > ( c > c ) > $o ) > ( a > a > $o ) > ( ( c > c ) > a ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_565,type,
sK195: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_566,type,
sK196: ( ( c > c ) > ( c > c ) > $o ) > ( ( c > c ) > ( c > c ) > $o ) > c > c ).
thf(func_def_567,type,
sK197: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_568,type,
sK198: ( a > a > $o ) > ( a > a > $o ) > a ).
thf(func_def_569,type,
sK199: ( c > c > c ) > set_c > set_c > ( c > c > c ) > c ).
thf(func_def_570,type,
sK200: ( c > c > c ) > set_c > set_c > ( c > c > c ) > c ).
thf(func_def_571,type,
sK201: ( c > c > c ) > set_c > set_c > c ).
thf(func_def_572,type,
sK202: ( c > c > c ) > set_c > set_c > c ).
thf(func_def_573,type,
sK203: ( a > c > c ) > ( a > c > c ) > a > a ).
thf(func_def_574,type,
sK204: ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_575,type,
sK205: a > ( a > c > c ) > ( a > c > c ) > a ).
thf(func_def_576,type,
vNOT: $o > $o ).
thf(f1,axiom,
finite746615251te_a_c @ f1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_assms_I2_J) ).
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(f464,plain,
finite746615251te_a_c @ f1,
inference(rectify,[],[f1]) ).
thf(f465,plain,
( ( finite746615251te_a_c @ f1 )
= $true ),
inference(fool_elimination,[],[f464]) ).
thf(f656,plain,
~ ( finite746615251te_a_c @ f1 ),
inference(rectify,[],[f365]) ).
thf(f657,plain,
( ( finite746615251te_a_c @ f1 )
!= $true ),
inference(fool_elimination,[],[f656]) ).
thf(f911,plain,
( ( finite746615251te_a_c @ f1 )
!= $true ),
inference(flattening,[],[f657]) ).
thf(f1766,plain,
( ( finite746615251te_a_c @ f1 )
!= $true ),
inference(cnf_transformation,[],[f911]) ).
thf(f2230,plain,
( ( finite746615251te_a_c @ f1 )
= $true ),
inference(cnf_transformation,[],[f465]) ).
thf(f2454,definition,
( spl206_15
<=> ( ( finite746615251te_a_c @ f1 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl206_15])],[avatar_definition]) ).
thf(f2457,plain,
~ spl206_15,
inference(avatar_split_clause,[],[f1766,f2454]) ).
thf(f2473,plain,
spl206_15,
inference(avatar_split_clause,[],[f2230,f2454]) ).
cnf(s18,plain,
~ spl206_15,
inference(sat_conversion,[],[f2457]) ).
cnf(s22,plain,
spl206_15,
inference(sat_conversion,[],[f2473]) ).
cnf(s30,plain,
$false,
inference(rat,[],[s18,s22]) ).
thf(f2489,plain,
$false,
inference(avatar_sat_refutation,[],[s30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP128^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n004.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 19:57:37 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.33/0.37 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.58/0.53 % (1765823)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.58/0.53 % (1765833)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=664692401:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.58/0.53 % (1765834)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.58/0.53 % (1765834)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.58/0.53 % (1765828)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4195209423:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.58/0.53 % (1765829)lrs+10_16_si=on:nwc=1.5:random_seed=1678822398:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.58/0.53 % (1765831)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=570731183:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.58/0.53 % (1765832)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1712005463:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.58/0.53 % (1765834)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2079349478:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.58/0.53 % (1765830)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4166701776:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.58/0.53 % (1765830)Instruction limit reached!
% 0.58/0.53 % (1765830)------------------------------
% 0.58/0.53 % (1765830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.53 % (1765830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.53 % (1765830)CaDiCaL version: 2.1.3
% 0.58/0.53 % (1765830)Termination reason: Instruction limit
% 0.58/0.53 % (1765830)Termination phase: shuffling
% 0.58/0.53 % (1765830)Time elapsed: 0.002 s
% 0.58/0.53 % (1765830)Peak memory usage: 10 MB
% 0.58/0.53 % (1765830)Instructions burned: 4 (million)
% 0.58/0.53 % (1765829)Instruction limit reached!
% 0.58/0.53 % (1765829)------------------------------
% 0.58/0.53 % (1765829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.53 % (1765829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.53 % (1765829)CaDiCaL version: 2.1.3
% 0.58/0.53 % (1765829)Termination reason: Instruction limit
% 0.58/0.53 % (1765829)Termination phase: shuffling
% 0.58/0.53 % (1765829)Time elapsed: 0.009 s
% 0.58/0.53 % (1765829)Peak memory usage: 11 MB
% 0.58/0.53 % (1765829)Instructions burned: 20 (million)
% 0.58/0.53 % (1765833)Instruction limit reached!
% 0.58/0.53 % (1765833)------------------------------
% 0.58/0.53 % (1765833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.53 % (1765833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.53 % (1765833)CaDiCaL version: 2.1.3
% 0.58/0.53 % (1765833)Termination reason: Instruction limit
% 0.58/0.53 % (1765833)Termination phase: shuffling
% 0.58/0.53 % (1765833)Time elapsed: 0.016 s
% 0.58/0.53 % (1765833)Peak memory usage: 11 MB
% 0.58/0.53 % (1765833)Instructions burned: 75 (million)
% 0.58/0.53 % (1765832)Instruction limit reached!
% 0.58/0.53 % (1765832)------------------------------
% 0.58/0.53 % (1765832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.53 % (1765832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.53 % (1765832)CaDiCaL version: 2.1.3
% 0.58/0.53 % (1765832)Termination reason: Instruction limit
% 0.58/0.53 % (1765832)Termination phase: shuffling
% 0.58/0.53 % (1765832)Time elapsed: 0.011 s
% 0.58/0.53 % (1765832)Peak memory usage: 11 MB
% 0.58/0.53 % (1765832)Instructions burned: 26 (million)
% 0.58/0.53 % (1765844)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.58/0.53 % (1765844)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2432440093:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.58/0.56 % (1765842)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1756445989:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.58/0.56 % (1765844)Instruction limit reached!
% 0.58/0.56 % (1765844)------------------------------
% 0.58/0.56 % (1765844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.56 % (1765844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.56 % (1765844)CaDiCaL version: 2.1.3
% 0.58/0.56 % (1765844)Termination reason: Instruction limit
% 0.58/0.56 % (1765844)Termination phase: shuffling
% 0.58/0.56 % (1765844)Time elapsed: 0.002 s
% 0.58/0.56 % (1765844)Peak memory usage: 11 MB
% 0.58/0.56 % (1765844)Instructions burned: 7 (million)
% 0.58/0.56 % (1765842)Instruction limit reached!
% 0.58/0.56 % (1765842)------------------------------
% 0.58/0.56 % (1765842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.56 % (1765842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.56 % (1765842)CaDiCaL version: 2.1.3
% 0.58/0.56 % (1765842)Termination reason: Instruction limit
% 0.58/0.56 % (1765842)Termination phase: shuffling
% 0.58/0.56 % (1765842)Time elapsed: 0.002 s
% 0.58/0.56 % (1765842)Peak memory usage: 11 MB
% 0.58/0.56 % (1765842)Instructions burned: 3 (million)
% 0.58/0.56 % (1765843)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=700445434:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.58/0.56 % (1765845)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=874545618:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.58/0.56 % (1765848)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.58/0.56 % (1765848)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.58/0.56 % (1765843)Instruction limit reached!
% 0.58/0.56 % (1765843)------------------------------
% 0.58/0.56 % (1765843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.56 % (1765843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.56 % (1765843)CaDiCaL version: 2.1.3
% 0.58/0.56 % (1765843)Termination reason: Instruction limit
% 0.58/0.56 % (1765843)Termination phase: shuffling
% 0.58/0.56 % (1765843)Time elapsed: 0.003 s
% 0.58/0.56 % (1765843)Peak memory usage: 10 MB
% 0.58/0.56 % (1765843)Instructions burned: 6 (million)
% 0.58/0.56 % (1765848)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=148975409:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.58/0.56 % (1765828)Instruction limit reached!
% 0.58/0.56 % (1765828)------------------------------
% 0.58/0.56 % (1765828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.56 % (1765828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.56 % (1765828)CaDiCaL version: 2.1.3
% 0.58/0.56 % (1765828)Termination reason: Instruction limit
% 0.58/0.56 % (1765828)Termination phase: shuffling
% 0.58/0.56 % (1765828)Time elapsed: 0.035 s
% 0.58/0.56 % (1765828)Peak memory usage: 11 MB
% 0.58/0.56 % (1765828)Instructions burned: 87 (million)
% 0.58/0.56 % (1765845)Instruction limit reached!
% 0.58/0.56 % (1765845)------------------------------
% 0.58/0.56 % (1765845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.56 % (1765845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.56 % (1765845)CaDiCaL version: 2.1.3
% 0.58/0.56 % (1765845)Termination reason: Instruction limit
% 0.58/0.56 % (1765845)Termination phase: shuffling
% 0.58/0.56 % (1765845)Time elapsed: 0.006 s
% 0.58/0.56 % (1765845)Peak memory usage: 11 MB
% 0.58/0.56 % (1765845)Instructions burned: 14 (million)
% 0.58/0.56 % (1765848)Instruction limit reached!
% 0.58/0.56 % (1765848)------------------------------
% 0.58/0.56 % (1765848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.56 % (1765848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.56 % (1765848)CaDiCaL version: 2.1.3
% 0.58/0.56 % (1765848)Termination reason: Instruction limit
% 0.58/0.56 % (1765848)Termination phase: shuffling
% 1.30/0.58 % (1765848)Time elapsed: 0.007 s
% 1.30/0.58 % (1765848)Peak memory usage: 11 MB
% 1.30/0.58 % (1765848)Instructions burned: 30 (million)
% 1.30/0.58 % (1765849)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=1857934051:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.30/0.58 % (1765854)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.30/0.58 % (1765852)lrs+10_1_si=on:cs=on:random_seed=1036512185:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.30/0.58 % (1765856)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1838253333:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.30/0.58 % (1765854)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1495846012:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.30/0.58 % (1765852)Instruction limit reached!
% 1.30/0.58 % (1765852)------------------------------
% 1.30/0.58 % (1765852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.58 % (1765852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.58 % (1765852)CaDiCaL version: 2.1.3
% 1.30/0.58 % (1765852)Termination reason: Instruction limit
% 1.30/0.58 % (1765852)Termination phase: shuffling
% 1.30/0.58 % (1765852)Time elapsed: 0.004 s
% 1.30/0.58 % (1765852)Peak memory usage: 10 MB
% 1.30/0.58 % (1765852)Instructions burned: 9 (million)
% 1.30/0.58 % (1765854)Instruction limit reached!
% 1.30/0.58 % (1765854)------------------------------
% 1.30/0.58 % (1765854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.58 % (1765854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.58 % (1765854)CaDiCaL version: 2.1.3
% 1.30/0.58 % (1765854)Termination reason: Instruction limit
% 1.30/0.58 % (1765854)Termination phase: shuffling
% 1.30/0.58 % (1765854)Time elapsed: 0.002 s
% 1.30/0.58 % (1765854)Peak memory usage: 10 MB
% 1.30/0.58 % (1765854)Instructions burned: 3 (million)
% 1.30/0.58 % (1765855)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3900734126:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.30/0.58 % (1765834)Instruction limit reached!
% 1.30/0.58 % (1765834)------------------------------
% 1.30/0.58 % (1765834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.58 % (1765834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.58 % (1765834)CaDiCaL version: 2.1.3
% 1.30/0.58 % (1765834)Termination reason: Instruction limit
% 1.30/0.58 % (1765834)Termination phase: Preprocessing 3
% 1.30/0.58 % (1765834)Time elapsed: 0.067 s
% 1.30/0.58 % (1765834)Peak memory usage: 13 MB
% 1.30/0.58 % (1765834)Instructions burned: 157 (million)
% 1.30/0.58 % (1765855)Instruction limit reached!
% 1.30/0.58 % (1765855)------------------------------
% 1.30/0.58 % (1765855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.58 % (1765855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.58 % (1765855)CaDiCaL version: 2.1.3
% 1.30/0.58 % (1765855)Termination reason: Instruction limit
% 1.30/0.58 % (1765855)Termination phase: shuffling
% 1.30/0.58 % (1765855)Time elapsed: 0.016 s
% 1.30/0.58 % (1765855)Peak memory usage: 11 MB
% 1.30/0.58 % (1765855)Instructions burned: 39 (million)
% 1.30/0.58 % (1765861)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=658639496:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.30/0.58 % (1765863)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2323072716:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.58 % (1765849)Instruction limit reached!
% 1.30/0.58 % (1765849)------------------------------
% 1.30/0.58 % (1765849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.58 % (1765849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.58 % (1765849)CaDiCaL version: 2.1.3
% 1.30/0.58 % (1765849)Termination reason: Instruction limit
% 1.30/0.58 % (1765849)Termination phase: Property scanning
% 1.30/0.58 % (1765849)Time elapsed: 0.038 s
% 1.30/0.62 % (1765849)Peak memory usage: 12 MB
% 1.30/0.62 % (1765849)Instructions burned: 86 (million)
% 1.30/0.62 % (1765863)Instruction limit reached!
% 1.30/0.62 % (1765863)------------------------------
% 1.30/0.62 % (1765863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765863)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765863)Termination reason: Instruction limit
% 1.30/0.62 % (1765863)Termination phase: shuffling
% 1.30/0.62 % (1765863)Time elapsed: 0.006 s
% 1.30/0.62 % (1765863)Peak memory usage: 11 MB
% 1.30/0.62 % (1765863)Instructions burned: 14 (million)
% 1.30/0.62 % (1765861)Instruction limit reached!
% 1.30/0.62 % (1765861)------------------------------
% 1.30/0.62 % (1765861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765861)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765861)Termination reason: Instruction limit
% 1.30/0.62 % (1765861)Termination phase: shuffling
% 1.30/0.62 % (1765861)Time elapsed: 0.010 s
% 1.30/0.62 % (1765861)Peak memory usage: 11 MB
% 1.30/0.62 % (1765861)Instructions burned: 25 (million)
% 1.30/0.62 % (1765864)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3081623270:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.30/0.62 % (1765856)Refutation not found, incomplete strategy
% 1.30/0.62 % (1765856)------------------------------
% 1.30/0.62 % (1765856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765856)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765856)Termination reason: Refutation not found, incomplete strategy
% 1.30/0.62 % (1765856)Time elapsed: 0.034 s
% 1.30/0.62 % (1765856)Peak memory usage: 14 MB
% 1.30/0.62 % (1765856)Instructions burned: 153 (million)
% 1.30/0.62 % (1765856)------------------------------
% 1.30/0.62 % (1765856)------------------------------
% 1.30/0.62 % (1765865)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3065703574:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.62 % (1765872)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3674853532:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.30/0.62 % (1765865)Instruction limit reached!
% 1.30/0.62 % (1765865)------------------------------
% 1.30/0.62 % (1765865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765865)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765865)Termination reason: Instruction limit
% 1.30/0.62 % (1765865)Termination phase: shuffling
% 1.30/0.62 % (1765865)Time elapsed: 0.006 s
% 1.30/0.62 % (1765865)Peak memory usage: 11 MB
% 1.30/0.62 % (1765865)Instructions burned: 14 (million)
% 1.30/0.62 % (1765869)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2922869548:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.30/0.62 % (1765868)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1815612552:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.30/0.62 % (1765870)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2118921651:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.30/0.62 % (1765868)Instruction limit reached!
% 1.30/0.62 % (1765868)------------------------------
% 1.30/0.62 % (1765868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765868)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765868)Termination reason: Instruction limit
% 1.30/0.62 % (1765868)Termination phase: shuffling
% 1.30/0.62 % (1765868)Time elapsed: 0.002 s
% 1.30/0.62 % (1765868)Peak memory usage: 10 MB
% 1.30/0.62 % (1765868)Instructions burned: 4 (million)
% 1.30/0.62 % (1765872)Instruction limit reached!
% 1.30/0.62 % (1765872)------------------------------
% 1.30/0.62 % (1765872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765872)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765872)Termination reason: Instruction limit
% 1.30/0.62 % (1765872)Termination phase: shuffling
% 1.30/0.62 % (1765872)Time elapsed: 0.013 s
% 1.30/0.62 % (1765872)Peak memory usage: 11 MB
% 1.30/0.62 % (1765872)Instructions burned: 63 (million)
% 1.30/0.62 % (1765869)Instruction limit reached!
% 1.30/0.62 % (1765869)------------------------------
% 1.30/0.62 % (1765869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765869)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765869)Termination reason: Instruction limit
% 1.30/0.62 % (1765869)Termination phase: shuffling
% 1.30/0.62 % (1765869)Time elapsed: 0.012 s
% 1.30/0.62 % (1765869)Peak memory usage: 11 MB
% 1.30/0.62 % (1765869)Instructions burned: 28 (million)
% 1.30/0.62 % (1765870)Instruction limit reached!
% 1.30/0.62 % (1765870)------------------------------
% 1.30/0.62 % (1765870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765870)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765870)Termination reason: Instruction limit
% 1.30/0.62 % (1765870)Termination phase: shuffling
% 1.30/0.62 % (1765870)Time elapsed: 0.010 s
% 1.30/0.62 % (1765870)Peak memory usage: 11 MB
% 1.30/0.62 % (1765870)Instructions burned: 24 (million)
% 1.30/0.62 % (1765875)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.30/0.62 % (1765875)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.30/0.62 % (1765875)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3688359134:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.62 % (1765880)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=1087159412:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.30/0.62 % (1765879)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.30/0.62 % (1765879)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=498171934:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.30/0.62 % (1765875)Instruction limit reached!
% 1.30/0.62 % (1765875)------------------------------
% 1.30/0.62 % (1765875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765875)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765875)Termination reason: Instruction limit
% 1.30/0.62 % (1765875)Termination phase: shuffling
% 1.30/0.62 % (1765875)Time elapsed: 0.007 s
% 1.30/0.62 % (1765875)Peak memory usage: 11 MB
% 1.30/0.62 % (1765875)Instructions burned: 15 (million)
% 1.30/0.62 % (1765880)Instruction limit reached!
% 1.30/0.62 % (1765880)------------------------------
% 1.30/0.62 % (1765880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765880)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765880)Termination reason: Instruction limit
% 1.30/0.62 % (1765880)Termination phase: shuffling
% 1.30/0.62 % (1765880)Time elapsed: 0.007 s
% 1.30/0.62 % (1765880)Peak memory usage: 11 MB
% 1.30/0.62 % (1765880)Instructions burned: 31 (million)
% 1.30/0.62 % (1765879)Instruction limit reached!
% 1.30/0.62 % (1765879)------------------------------
% 1.30/0.62 % (1765879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765879)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765879)Termination reason: Instruction limit
% 1.30/0.62 % (1765879)Termination phase: shuffling
% 1.30/0.62 % (1765879)Time elapsed: 0.004 s
% 1.30/0.62 % (1765879)Peak memory usage: 11 MB
% 1.30/0.62 % (1765879)Instructions burned: 8 (million)
% 1.30/0.62 % (1765881)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2684888028:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.30/0.62 % (1765882)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1667436052:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.30/0.62 % (1765881)Instruction limit reached!
% 1.30/0.62 % (1765881)------------------------------
% 1.30/0.62 % (1765881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765881)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765881)Termination reason: Instruction limit
% 1.30/0.62 % (1765881)Termination phase: shuffling
% 1.30/0.62 % (1765881)Time elapsed: 0.004 s
% 1.30/0.62 % (1765881)Peak memory usage: 11 MB
% 1.30/0.62 % (1765881)Instructions burned: 8 (million)
% 1.30/0.62 % (1765887)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1289392996:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.30/0.62 % (1765882)Instruction limit reached!
% 1.30/0.62 % (1765882)------------------------------
% 1.30/0.62 % (1765882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765882)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765882)Termination reason: Instruction limit
% 1.30/0.62 % (1765882)Termination phase: shuffling
% 1.30/0.62 % (1765882)Time elapsed: 0.010 s
% 1.30/0.62 % (1765882)Peak memory usage: 11 MB
% 1.30/0.62 % (1765882)Instructions burned: 23 (million)
% 1.30/0.62 % (1765886)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1914391267:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.30/0.62 % (1765888)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1655707618:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.30/0.62 % (1765886)Instruction limit reached!
% 1.30/0.62 % (1765886)------------------------------
% 1.30/0.62 % (1765886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765886)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765886)Termination reason: Instruction limit
% 1.30/0.62 % (1765886)Termination phase: shuffling
% 1.30/0.62 % (1765886)Time elapsed: 0.008 s
% 1.30/0.62 % (1765886)Peak memory usage: 11 MB
% 1.30/0.62 % (1765886)Instructions burned: 20 (million)
% 1.30/0.62 % (1765891)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1617136847:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 1.30/0.62 % (1765893)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4206316748:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.30/0.62 % (1765831) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1765823-1765831"...
% 1.30/0.62 % (1765897)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.30/0.62 % (1765831)...printing done.
% 1.30/0.62 % (1765897)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1791586424:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.30/0.62 % (1765831)Refutation found. Thanks to Tanya!
% 1.30/0.62 % SZS status Theorem for theBenchmark
% 1.30/0.62 % SZS output start Proof for theBenchmark
% See solution above
% 1.30/0.62 % (1765831)------------------------------
% 1.30/0.62 % (1765831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.62 % (1765831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.62 % (1765831)CaDiCaL version: 2.1.3
% 1.30/0.62 % (1765831)Termination reason: Refutation
% 1.30/0.62 % (1765831)Time elapsed: 0.172 s
% 1.30/0.62 % (1765831)Peak memory usage: 16 MB
% 1.30/0.62 % (1765831)Instructions burned: 393 (million)
% 1.30/0.62 % (1765823)Success in time 0.244 s
% 1.30/0.62 % Vampire exiting
%------------------------------------------------------------------------------