%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP138^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:10:50 AM UTC 2026
% Result : Theorem 3.76s 0.88s
% Output : Refutation 3.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 9
% Syntax : Number of formulae : 71 ( 29 unt; 0 typ; 4 def)
% Number of atoms : 333 ( 111 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 510 ( 45 ~; 49 |; 0 &; 380 @)
% ( 4 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 62 ( 62 >; 0 *; 0 +; 0 <<)
% Number of symbols : 620 ( 616 usr; 19 con; 0-13 aty)
% ( 14 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 91 ( 39 sgn 30 !; 0 ?; 91 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
produc696645085lle_fm: $tType ).
thf(type_def_6,type,
set_se800614875lle_tv: $tType ).
thf(type_def_7,type,
set_set_list_char: $tType ).
thf(type_def_8,type,
set_Pa1764573435lle_tv: $tType ).
thf(type_def_9,type,
set_list_char: $tType ).
thf(type_def_10,type,
paraco1605129243lle_tv: $tType ).
thf(type_def_11,type,
paraco1604210848lle_fm: $tType ).
thf(type_def_12,type,
set_set_o: $tType ).
thf(type_def_13,type,
list_char: $tType ).
thf(type_def_14,type,
set_nat: $tType ).
thf(type_def_15,type,
set_o: $tType ).
thf(type_def_16,type,
nat: $tType ).
thf(type_def_17,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
complete_Sup_Sup_o: set_o > $o ).
thf(func_def_1,type,
finite_Fpow_o: set_o > set_set_o ).
thf(func_def_2,type,
finite1803457147t_char: set_list_char > set_set_list_char ).
thf(func_def_3,type,
finite2011762305lle_tv: set_Pa1764573435lle_tv > set_se800614875lle_tv ).
thf(func_def_4,type,
ord_less_eq_o_o: ( $o > $o ) > ( $o > $o ) > $o ).
thf(func_def_5,type,
ord_le1945897678char_o: ( list_char > $o ) > ( list_char > $o ) > $o ).
thf(func_def_6,type,
ord_le1632188418e_tv_o: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > $o ).
thf(func_def_7,type,
ord_less_eq_set_o: set_o > set_o > $o ).
thf(func_def_8,type,
ord_le1836582007t_char: set_list_char > set_list_char > $o ).
thf(func_def_9,type,
ord_less_eq_set_nat: set_nat > set_nat > $o ).
thf(func_def_10,type,
ord_le241064091lle_tv: set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > $o ).
thf(func_def_11,type,
ord_le2085948664_set_o: set_set_o > set_set_o > $o ).
thf(func_def_12,type,
ord_le263913851lle_tv: set_se800614875lle_tv > set_se800614875lle_tv > $o ).
thf(func_def_13,type,
order_Greatest_set_o: ( set_o > $o ) > set_o ).
thf(func_def_14,type,
order_350719188lle_tv: ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_15,type,
top_top_o_o: $o > $o ).
thf(func_def_16,type,
top_top_list_char_o: list_char > $o ).
thf(func_def_17,type,
top_top_nat_o: nat > $o ).
thf(func_def_18,type,
top_to1299250770e_tv_o: paraco1605129243lle_tv > $o ).
thf(func_def_19,type,
top_top_set_o: set_o ).
thf(func_def_20,type,
top_to748628679t_char: set_list_char ).
thf(func_def_21,type,
top_top_set_nat: set_nat ).
thf(func_def_22,type,
top_to1057771083lle_tv: set_Pa1764573435lle_tv ).
thf(func_def_23,type,
top_top_set_set_o: set_set_o ).
thf(func_def_24,type,
top_to697846397t_char: set_set_list_char ).
thf(func_def_25,type,
paraco1933902578domain: set_nat > set_Pa1764573435lle_tv ).
thf(func_def_26,type,
paraco1325918602e_eval: ( list_char > paraco1605129243lle_tv ) > paraco1604210848lle_fm > paraco1605129243lle_tv ).
thf(func_def_27,type,
paraco69239110le_Con: paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_28,type,
paraco1389086619le_Eql: paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_29,type,
paraco1745535428le_Eql: paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_30,type,
paraco445776468le_Neg: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_31,type,
paraco1480028776le_Pro: list_char > paraco1604210848lle_fm ).
thf(func_def_32,type,
paraco367965286_Truth: paraco1604210848lle_fm ).
thf(func_def_33,type,
paraco1344940915le_Det: $o > paraco1605129243lle_tv ).
thf(func_def_34,type,
paraco327635598_valid: paraco1604210848lle_fm > $o ).
thf(func_def_35,type,
paraco55203475lid_in: set_nat > paraco1604210848lle_fm > $o ).
thf(func_def_36,type,
produc1710735575lle_fm: ( list_char > paraco1605129243lle_tv ) > paraco1604210848lle_fm > produc696645085lle_fm ).
thf(func_def_37,type,
collect_o: ( $o > $o ) > set_o ).
thf(func_def_38,type,
collect_list_char: ( list_char > $o ) > set_list_char ).
thf(func_def_39,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(func_def_40,type,
collec1111687558lle_tv: ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_41,type,
pow_o: set_o > set_set_o ).
thf(func_def_42,type,
pow_list_char: set_list_char > set_set_list_char ).
thf(func_def_43,type,
pow_Pa475453624lle_tv: set_Pa1764573435lle_tv > set_se800614875lle_tv ).
thf(func_def_44,type,
image_o_o: ( $o > $o ) > set_o > set_o ).
thf(func_def_45,type,
image_o_list_char: ( $o > list_char ) > set_o > set_list_char ).
thf(func_def_46,type,
image_o_nat: ( $o > nat ) > set_o > set_nat ).
thf(func_def_47,type,
image_1491822472lle_tv: ( $o > paraco1605129243lle_tv ) > set_o > set_Pa1764573435lle_tv ).
thf(func_def_48,type,
image_list_char_o: ( list_char > $o ) > set_list_char > set_o ).
thf(func_def_49,type,
image_890964937t_char: ( list_char > list_char ) > set_list_char > set_list_char ).
thf(func_def_50,type,
image_1187894195lle_tv: ( list_char > paraco1605129243lle_tv ) > set_list_char > set_Pa1764573435lle_tv ).
thf(func_def_51,type,
image_nat_o: ( nat > $o ) > set_nat > set_o ).
thf(func_def_52,type,
image_nat_list_char: ( nat > list_char ) > set_nat > set_list_char ).
thf(func_def_53,type,
image_nat_nat: ( nat > nat ) > set_nat > set_nat ).
thf(func_def_54,type,
image_1151963140lle_tv: ( nat > paraco1605129243lle_tv ) > set_nat > set_Pa1764573435lle_tv ).
thf(func_def_55,type,
image_991799618e_tv_o: ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > set_o ).
thf(func_def_56,type,
image_1971766583t_char: ( paraco1605129243lle_tv > list_char ) > set_Pa1764573435lle_tv > set_list_char ).
thf(func_def_57,type,
image_376325286tv_nat: ( paraco1605129243lle_tv > nat ) > set_Pa1764573435lle_tv > set_nat ).
thf(func_def_58,type,
image_335818702lle_tv: ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_59,type,
image_set_o_set_o: ( set_o > set_o ) > set_set_o > set_set_o ).
thf(func_def_60,type,
image_30320477lle_tv: ( set_list_char > set_Pa1764573435lle_tv ) > set_set_list_char > set_se800614875lle_tv ).
thf(func_def_61,type,
member_o: $o > set_o > $o ).
thf(func_def_62,type,
member_list_char: list_char > set_list_char > $o ).
thf(func_def_63,type,
member_nat: nat > set_nat > $o ).
thf(func_def_64,type,
member266900804lle_tv: paraco1605129243lle_tv > set_Pa1764573435lle_tv > $o ).
thf(func_def_65,type,
member_set_o: set_o > set_set_o > $o ).
thf(func_def_66,type,
member1875402276lle_tv: set_Pa1764573435lle_tv > set_se800614875lle_tv > $o ).
thf(func_def_67,type,
p: paraco1604210848lle_fm ).
thf(func_def_71,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_72,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_73,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_74,type,
vIMP: $o > $o > $o ).
thf(func_def_75,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_76,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_77,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_78,type,
vNOT: $o > $o ).
thf(func_def_79,type,
vAND: $o > $o > $o ).
thf(func_def_80,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_81,type,
sP0: ( paraco1604210848lle_fm > $o ) > $o ).
thf(func_def_82,type,
sP1: ( paraco1604210848lle_fm > $o ) > $o ).
thf(func_def_83,type,
sK2: set_list_char > set_list_char > list_char ).
thf(func_def_84,type,
sK3: set_o > set_o > $o ).
thf(func_def_85,type,
sK4: set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > paraco1605129243lle_tv ).
thf(func_def_86,type,
sK5: ( list_char > $o ) > $o > list_char ).
thf(func_def_87,type,
sK6: ( list_char > list_char ) > list_char > list_char ).
thf(func_def_88,type,
sK7: ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv > list_char ).
thf(func_def_89,type,
sK8: ( $o > $o ) > $o > $o ).
thf(func_def_90,type,
sK9: ( $o > list_char ) > list_char > $o ).
thf(func_def_91,type,
sK10: ( $o > paraco1605129243lle_tv ) > paraco1605129243lle_tv > $o ).
thf(func_def_92,type,
sK11: set_list_char > ( nat > list_char ) > ( nat > $o ) > nat ).
thf(func_def_93,type,
sK12: set_list_char > ( paraco1605129243lle_tv > list_char ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_94,type,
sK13: set_Pa1764573435lle_tv > ( list_char > paraco1605129243lle_tv ) > ( list_char > $o ) > list_char ).
thf(func_def_95,type,
sK14: set_Pa1764573435lle_tv > ( nat > paraco1605129243lle_tv ) > ( nat > $o ) > nat ).
thf(func_def_96,type,
sK15: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_97,type,
sK16: set_o > ( $o > $o ) > ( $o > $o ) > $o ).
thf(func_def_98,type,
sK17: set_o > ( nat > $o ) > ( nat > $o ) > nat ).
thf(func_def_99,type,
sK18: set_o > ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_100,type,
sK19: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_101,type,
sK20: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_102,type,
sK21: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_103,type,
sK22: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_104,type,
sK23: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_105,type,
sK24: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_106,type,
sK25: ( set_o > set_o ) > set_o ).
thf(func_def_107,type,
sK26: ( set_o > set_o ) > set_o ).
thf(func_def_108,type,
sK27: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_109,type,
sK28: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_110,type,
sK29: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_111,type,
sK30: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_112,type,
sK31: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_113,type,
sK32: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_114,type,
sK33: ( set_o > set_o ) > set_o ).
thf(func_def_115,type,
sK34: ( set_o > set_o ) > set_o ).
thf(func_def_116,type,
sK35: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_117,type,
sK36: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_118,type,
sK37: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_119,type,
sK38: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_120,type,
sK39: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_121,type,
sK40: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_122,type,
sK41: ( set_o > set_o ) > set_o ).
thf(func_def_123,type,
sK42: ( set_o > set_o ) > set_o ).
thf(func_def_124,type,
sK43: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_125,type,
sK44: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_126,type,
sK45: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_127,type,
sK46: ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_128,type,
sK47: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_129,type,
sK48: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_130,type,
sK49: ( set_o > set_o ) > set_o ).
thf(func_def_131,type,
sK50: ( set_o > set_o ) > set_o ).
thf(func_def_132,type,
sK51: ( paraco1605129243lle_tv > $o ) > set_list_char > ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv ).
thf(func_def_133,type,
sK52: ( $o > $o ) > set_o > ( $o > $o ) > $o ).
thf(func_def_134,type,
sK53: ( $o > $o ) > ( $o > $o ) > set_o > $o ).
thf(func_def_135,type,
sK54: ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > set_list_char > list_char ).
thf(func_def_136,type,
sK55: ( nat > $o ) > ( nat > $o ) > nat ).
thf(func_def_137,type,
sK56: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_138,type,
sK57: ( paraco1605129243lle_tv > $o ) > set_list_char > ( list_char > paraco1605129243lle_tv ) > list_char ).
thf(func_def_139,type,
sK58: ( $o > $o ) > set_o > ( $o > $o ) > $o ).
thf(func_def_140,type,
sK59: ( nat > $o ) > ( nat > $o ) > nat ).
thf(func_def_141,type,
sK60: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_142,type,
sK61: ( $o > $o ) > ( $o > $o ) > $o ).
thf(func_def_143,type,
sK62: paraco1605129243lle_tv ).
thf(func_def_144,type,
sK63: list_char ).
thf(func_def_145,type,
sK64: $o ).
thf(func_def_146,type,
sK65: set_Pa1764573435lle_tv > paraco1605129243lle_tv ).
thf(func_def_147,type,
sK66: set_list_char > list_char ).
thf(func_def_148,type,
sK67: set_o > $o ).
thf(func_def_149,type,
sK68: set_o > ( $o > $o ) > $o > $o ).
thf(func_def_150,type,
sK69: set_list_char > ( list_char > $o ) > $o > list_char ).
thf(func_def_151,type,
sK70: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > $o > paraco1605129243lle_tv ).
thf(func_def_152,type,
sK71: set_o > ( $o > list_char ) > list_char > $o ).
thf(func_def_153,type,
sK72: set_list_char > ( list_char > list_char ) > list_char > list_char ).
thf(func_def_154,type,
sK73: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > list_char ) > list_char > paraco1605129243lle_tv ).
thf(func_def_155,type,
sK74: set_o > ( $o > paraco1605129243lle_tv ) > paraco1605129243lle_tv > $o ).
thf(func_def_156,type,
sK75: set_list_char > ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv > list_char ).
thf(func_def_157,type,
sK76: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > paraco1605129243lle_tv > paraco1605129243lle_tv ).
thf(func_def_158,type,
sK77: set_list_char > ( list_char > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_list_char ).
thf(func_def_159,type,
sK78: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_160,type,
sK79: set_o > ( $o > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_o ).
thf(func_def_161,type,
sK80: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > set_o > set_Pa1764573435lle_tv ).
thf(func_def_162,type,
sK81: set_o > ( $o > $o ) > set_o > set_o ).
thf(func_def_163,type,
sK82: set_list_char > ( $o > list_char ) > set_o > $o ).
thf(func_def_164,type,
sK83: set_list_char > ( list_char > list_char ) > set_list_char > list_char ).
thf(func_def_165,type,
sK84: set_list_char > ( paraco1605129243lle_tv > list_char ) > set_Pa1764573435lle_tv > paraco1605129243lle_tv ).
thf(func_def_166,type,
sK85: set_Pa1764573435lle_tv > ( $o > paraco1605129243lle_tv ) > set_o > $o ).
thf(func_def_167,type,
sK86: set_Pa1764573435lle_tv > ( list_char > paraco1605129243lle_tv ) > set_list_char > list_char ).
thf(func_def_168,type,
sK87: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > paraco1605129243lle_tv ).
thf(func_def_169,type,
sK88: set_o > ( $o > $o ) > set_o > $o ).
thf(func_def_170,type,
sK89: set_o > ( list_char > $o ) > set_list_char > list_char ).
thf(func_def_171,type,
sK90: set_o > ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > paraco1605129243lle_tv ).
thf(func_def_172,type,
sK91: ( paraco1605129243lle_tv > list_char ) > ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv ).
thf(func_def_173,type,
sK92: ( list_char > list_char ) > ( list_char > list_char ) > list_char ).
thf(func_def_174,type,
sK93: ( $o > list_char ) > ( list_char > $o ) > $o ).
thf(func_def_175,type,
sK94: ( list_char > $o ) > ( $o > list_char ) > list_char ).
thf(func_def_176,type,
sK95: ( $o > $o ) > ( $o > $o ) > $o ).
thf(func_def_177,type,
sK96: paraco1605129243lle_tv > ( list_char > paraco1605129243lle_tv ) > list_char ).
thf(func_def_178,type,
sK97: list_char > ( list_char > list_char ) > list_char ).
thf(func_def_179,type,
sK98: $o > ( list_char > $o ) > list_char ).
thf(func_def_180,type,
sK99: list_char > ( $o > list_char ) > $o ).
thf(func_def_181,type,
sK100: $o > ( $o > $o ) > $o ).
thf(func_def_182,type,
sK101: paraco1605129243lle_tv > ( list_char > paraco1605129243lle_tv ) > list_char ).
thf(func_def_183,type,
sK102: list_char > ( list_char > list_char ) > list_char ).
thf(func_def_184,type,
sK103: $o > ( list_char > $o ) > list_char ).
thf(func_def_185,type,
sK104: list_char > ( $o > list_char ) > $o ).
thf(func_def_186,type,
sK105: $o > ( $o > $o ) > $o ).
thf(func_def_187,type,
sK106: ( list_char > $o ) > ( list_char > $o ) > set_list_char > list_char ).
thf(func_def_188,type,
sK107: ( nat > $o ) > ( nat > $o ) > set_nat > nat ).
thf(func_def_189,type,
sK108: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > paraco1605129243lle_tv ).
thf(func_def_190,type,
sK109: ( $o > $o ) > ( $o > $o ) > set_o > $o ).
thf(func_def_191,type,
sK110: ( $o > $o ) > ( $o > $o ) > set_o > $o ).
thf(func_def_192,type,
sK111: ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > set_list_char > list_char ).
thf(func_def_193,type,
sK112: ( $o > $o ) > ( $o > $o ) > set_o > $o ).
thf(func_def_194,type,
sK113: ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > set_list_char > list_char ).
thf(func_def_195,type,
sK114: set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_196,type,
sK115: set_o > ( set_o > $o ) > set_o ).
thf(func_def_197,type,
sK116: ( set_Pa1764573435lle_tv > $o ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_198,type,
sK117: set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_199,type,
sK118: ( set_o > $o ) > ( set_o > $o ) > set_o ).
thf(func_def_200,type,
sK119: set_o > ( set_o > $o ) > set_o ).
thf(func_def_201,type,
sK120: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_202,type,
sK121: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_203,type,
sK122: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_204,type,
sK123: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_205,type,
sK124: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_206,type,
sK125: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_207,type,
sK126: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_208,type,
sK127: paraco1604210848lle_fm > list_char ).
thf(func_def_209,type,
sK128: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_210,type,
sK129: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_211,type,
sK130: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_212,type,
sK131: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_213,type,
sK132: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_214,type,
sK133: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_215,type,
sK134: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_216,type,
sK135: ( paraco1604210848lle_fm > $o ) > list_char ).
thf(func_def_217,type,
sK136: produc696645085lle_fm > list_char > paraco1605129243lle_tv ).
thf(func_def_218,type,
sK137: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_219,type,
sK138: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_220,type,
sK139: produc696645085lle_fm > list_char > paraco1605129243lle_tv ).
thf(func_def_221,type,
sK140: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_222,type,
sK141: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_223,type,
sK142: produc696645085lle_fm > list_char > paraco1605129243lle_tv ).
thf(func_def_224,type,
sK143: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_225,type,
sK144: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_226,type,
sK145: produc696645085lle_fm > list_char > paraco1605129243lle_tv ).
thf(func_def_227,type,
sK146: produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_228,type,
sK147: produc696645085lle_fm > list_char > paraco1605129243lle_tv ).
thf(func_def_229,type,
sK148: produc696645085lle_fm > list_char > paraco1605129243lle_tv ).
thf(func_def_230,type,
sK149: produc696645085lle_fm > list_char ).
thf(func_def_231,type,
sK150: list_char > paraco1605129243lle_tv ).
thf(func_def_232,type,
sK151: list_char > paraco1605129243lle_tv ).
thf(func_def_233,type,
sK152: set_o > ( $o > $o ) > $o ).
thf(func_def_234,type,
sK153: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_235,type,
sK154: set_nat > ( nat > $o ) > nat ).
thf(func_def_236,type,
sK155: set_list_char > ( list_char > $o ) > list_char ).
thf(func_def_237,type,
sK156: set_o > ( $o > $o ) > ( set_o > $o ) > set_o ).
thf(func_def_238,type,
sK157: set_o > ( $o > $o ) > ( set_o > $o ) > set_o ).
thf(func_def_239,type,
sK158: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > ( set_o > $o ) > set_o ).
thf(func_def_240,type,
sK159: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > ( set_o > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_241,type,
sK160: set_o > ( $o > paraco1605129243lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_242,type,
sK161: set_o > ( $o > paraco1605129243lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_o ).
thf(func_def_243,type,
sK162: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_244,type,
sK163: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_245,type,
sK164: set_list_char > ( list_char > paraco1605129243lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_246,type,
sK165: set_list_char > ( list_char > paraco1605129243lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_list_char ).
thf(func_def_247,type,
sK166: $o > ( $o > $o ) > $o ).
thf(func_def_248,type,
sK167: ( $o > $o ) > $o ).
thf(func_def_249,type,
sK168: list_char > ( $o > list_char ) > $o ).
thf(func_def_250,type,
sK169: ( $o > list_char ) > list_char ).
thf(func_def_251,type,
sK170: $o > ( list_char > $o ) > list_char ).
thf(func_def_252,type,
sK171: ( list_char > $o ) > $o ).
thf(func_def_253,type,
sK172: list_char > ( list_char > list_char ) > list_char ).
thf(func_def_254,type,
sK173: ( list_char > list_char ) > list_char ).
thf(func_def_255,type,
sK174: paraco1605129243lle_tv > ( list_char > paraco1605129243lle_tv ) > list_char ).
thf(func_def_256,type,
sK175: ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv ).
thf(func_def_257,type,
sK176: set_o > ( $o > $o ) > set_o > $o ).
thf(func_def_258,type,
sK177: set_list_char > ( list_char > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > list_char ).
thf(func_def_259,type,
sK178: ( $o > $o ) > set_o > set_o > set_o ).
thf(func_def_260,type,
sK179: ( paraco1605129243lle_tv > $o ) > set_o > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_261,type,
sK180: ( $o > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_o > set_o ).
thf(func_def_262,type,
sK181: ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_263,type,
sK182: ( list_char > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_list_char > set_list_char ).
thf(func_def_264,type,
sK183: ( $o > $o ) > ( $o > $o ) > $o ).
thf(func_def_265,type,
sK184: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv ).
thf(func_def_266,type,
sK185: ( nat > $o ) > ( nat > $o ) > nat ).
thf(func_def_267,type,
sK186: ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv > set_list_char > list_char ).
thf(func_def_268,type,
sK187: ( $o > $o ) > $o > set_o > $o ).
thf(func_def_270,type,
sF189:
!>[X0: $tType,X1: $tType,X2: $tType] : ( produc696645085lle_fm > ( X2 > paraco1604210848lle_fm > X1 ) > X0 > ( X0 > paraco1604210848lle_fm ) > ( produc696645085lle_fm > X2 ) > X1 ) ).
thf(func_def_271,type,
sF190:
!>[X0: $tType] : ( produc696645085lle_fm > ( produc696645085lle_fm > X0 ) > X0 ) ).
thf(func_def_272,type,
sF191: ( produc696645085lle_fm > paraco1604210848lle_fm ) > produc696645085lle_fm > paraco1604210848lle_fm ).
thf(func_def_273,type,
sF192:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > paraco1604210848lle_fm ) > ( paraco1604210848lle_fm > X0 ) > X0 ) ).
thf(func_def_274,type,
sF193: paraco1604210848lle_fm > ( produc696645085lle_fm > list_char > paraco1605129243lle_tv ) > produc696645085lle_fm > produc696645085lle_fm ).
thf(func_def_275,type,
sF194: list_char > paraco1604210848lle_fm ).
thf(func_def_276,type,
sF195:
!>[X0: $tType] : ( X0 > ( X0 > paraco1604210848lle_fm ) > paraco1604210848lle_fm ) ).
thf(func_def_277,type,
sF196: paraco1604210848lle_fm > ( paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ) > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_278,type,
sF197: ( paraco1604210848lle_fm > paraco1604210848lle_fm ) > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_279,type,
sF198:
!>[X0: $tType] : ( paraco1604210848lle_fm > ( paraco1604210848lle_fm > X0 ) > X0 ) ).
thf(func_def_280,type,
sF199:
!>[X0: $tType] : ( list_char > ( list_char > X0 ) > X0 ) ).
thf(func_def_281,type,
sF200: paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_282,type,
sF201: ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm > $o ).
thf(func_def_283,type,
sF202:
!>[X0: $tType] : ( ( paraco1604210848lle_fm > $o ) > ( ( paraco1604210848lle_fm > $o ) > X0 ) > X0 ) ).
thf(func_def_284,type,
sF203:
!>[X0: $tType] : ( X0 > ( X0 > $o ) > $o ) ).
thf(func_def_285,type,
sF204: ( ( paraco1604210848lle_fm > $o ) > $o ) > ( paraco1604210848lle_fm > $o ) > $o ).
thf(func_def_286,type,
sF205:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X2 ) > ( X1 > X0 ) > X1 > X2 ) ).
thf(func_def_287,type,
sF206: ( ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ) > ( paraco1604210848lle_fm > $o ) > paraco1604210848lle_fm ).
thf(func_def_288,type,
sF207:
!>[X0: $tType] : ( X0 > ( X0 > paraco1605129243lle_tv ) > paraco1605129243lle_tv ) ).
thf(func_def_289,type,
sF208:
!>[X0: $tType,X1: $tType] : ( paraco1604210848lle_fm > X1 > ( X1 > paraco1604210848lle_fm > X0 ) > X0 ) ).
thf(func_def_290,type,
sF209: ( list_char > paraco1605129243lle_tv ) > paraco1604210848lle_fm > paraco1605129243lle_tv ).
thf(func_def_291,type,
sF210: paraco1605129243lle_tv ).
thf(func_def_292,type,
sF211: paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_293,type,
sF212: paraco1604210848lle_fm > $o ).
thf(func_def_294,type,
sF213: paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_295,type,
sF214:
!>[X0: $tType,X1: $tType] : ( X0 > X0 > ( X0 > X0 > X1 ) > X1 ) ).
thf(func_def_296,type,
sF215: set_o > set_set_o ).
thf(func_def_297,type,
sF216:
!>[X0: $tType] : ( X0 > set_o > ( set_o > X0 > $o ) > $o ) ).
thf(func_def_298,type,
sF217:
!>[X0: $tType,X1: $tType] : ( X0 > X1 > ( X1 > X0 > $o ) > $o ) ).
thf(func_def_299,type,
sF218:
!>[X0: $tType] : ( X0 > set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > X0 > $o ) > $o ) ).
thf(func_def_300,type,
sF219: set_Pa1764573435lle_tv > set_se800614875lle_tv ).
thf(func_def_301,type,
sF220:
!>[X0: $tType,X1: $tType] : ( ( X1 > X0 > $o ) > X1 > ( X1 > X0 ) > X1 > $o ) ).
thf(func_def_302,type,
sF221: set_o > set_set_o ).
thf(func_def_303,type,
sF222:
!>[X0: $tType] : ( set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > X0 ) > X0 ) ).
thf(func_def_304,type,
sF223: ( set_o > $o ) > ( set_o > $o ) > ( ( set_o > $o ) > set_o ) > $o ).
thf(func_def_305,type,
sF224: ( ( set_o > $o ) > set_o ) > ( set_o > $o ) > set_o ).
thf(func_def_306,type,
sF225: ( set_o > $o ) > set_o > $o ).
thf(func_def_307,type,
sF226:
!>[X0: $tType] : ( ( set_o > $o ) > ( set_o > $o ) > X0 > ( X0 > ( set_o > $o ) > set_o ) > $o ) ).
thf(func_def_308,type,
sF227:
!>[X0: $tType] : ( X0 > ( X0 > ( set_o > $o ) > set_o ) > ( set_o > $o ) > set_o ) ).
thf(func_def_309,type,
sF228:
!>[X0: $tType] : ( ( X0 > $o ) > ( ( X0 > $o ) > X0 ) > X0 ) ).
thf(func_def_310,type,
sF229:
!>[X0: $tType] : ( ( set_Pa1764573435lle_tv > $o ) > X0 > ( X0 > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ) > $o ) ).
thf(func_def_311,type,
sF230:
!>[X0: $tType] : ( X0 > ( X0 > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ) ).
thf(func_def_312,type,
sF231: ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv > $o ).
thf(func_def_313,type,
sF232: ( ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ) > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_314,type,
sF233:
!>[X0: $tType] : ( ( set_Pa1764573435lle_tv > $o ) > ( set_Pa1764573435lle_tv > $o ) > X0 > ( X0 > ( set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv ) > $o ) ).
thf(func_def_315,type,
sF234:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X1 > X2 ) > X0 > X1 > X2 ) ).
thf(func_def_316,type,
sF235:
!>[X0: $tType] : ( X0 > ( X0 > set_set_o ) > set_set_o ) ).
thf(func_def_317,type,
sF236:
!>[X0: $tType] : ( set_o > ( set_o > X0 ) > X0 ) ).
thf(func_def_318,type,
sF237:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( ( X1 > X3 ) > X2 > X0 ) > ( X1 > X3 ) > X2 > X0 ) ).
thf(func_def_319,type,
sF238: set_list_char > set_set_list_char ).
thf(func_def_320,type,
sF239:
!>[X0: $tType] : ( X0 > ( X0 > set_se800614875lle_tv ) > set_se800614875lle_tv ) ).
thf(func_def_321,type,
sF240:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X1 > X3 > X2 ) > ( X2 > X0 ) > X1 > X3 > X0 ) ).
thf(func_def_322,type,
sF241: set_o > set_set_o ).
thf(func_def_323,type,
sF242:
!>[X0: $tType] : ( X0 > X0 > ( X0 > X0 > $o ) > $o ) ).
thf(func_def_324,type,
sF243: set_Pa1764573435lle_tv > set_se800614875lle_tv ).
thf(func_def_325,type,
sF244: paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm ).
thf(func_def_326,type,
sF245:
!>[X0: $tType] : ( set_list_char > ( set_list_char > X0 ) > X0 ) ).
thf(func_def_327,type,
sF246: $o > $o ).
thf(func_def_328,type,
sF247: ( list_char > paraco1605129243lle_tv ) > set_list_char > set_Pa1764573435lle_tv ).
thf(func_def_329,type,
sF248:
!>[X0: $tType,X1: $tType] : ( set_list_char > X1 > ( X1 > set_list_char > X0 ) > X0 ) ).
thf(func_def_330,type,
sF249: set_list_char > ( set_Pa1764573435lle_tv > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > paraco1605129243lle_tv ).
thf(func_def_331,type,
sF250:
!>[X0: $tType] : ( set_list_char > ( list_char > paraco1605129243lle_tv ) > ( ( list_char > paraco1605129243lle_tv ) > set_list_char > X0 ) > ( X0 > paraco1605129243lle_tv ) > paraco1605129243lle_tv ) ).
thf(func_def_332,type,
sF251: ( list_char > paraco1605129243lle_tv ) > set_list_char > ( list_char > paraco1605129243lle_tv ) > list_char ).
thf(func_def_333,type,
sF252:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( ( X1 > X0 ) > X3 > X2 ) > ( X2 > X0 ) > ( X1 > X0 ) > X3 > X0 ) ).
thf(func_def_334,type,
sF253:
!>[X0: $tType,X1: $tType] : ( set_o > X1 > ( X1 > set_o > X0 ) > X0 ) ).
thf(func_def_335,type,
sF254:
!>[X0: $tType] : ( X0 > ( X0 > X0 ) > X0 ) ).
thf(func_def_336,type,
sF255:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X1 > X0 ) > ( ( X1 > X0 ) > X2 > X3 ) > X2 > X3 ) ).
thf(func_def_337,type,
sF256:
!>[X0: $tType] : ( set_list_char > ( list_char > paraco1605129243lle_tv ) > ( ( list_char > paraco1605129243lle_tv ) > set_list_char > X0 ) > X0 ) ).
thf(func_def_338,type,
sF257: ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > set_list_char > paraco1605129243lle_tv ).
thf(func_def_339,type,
sF258:
!>[X0: $tType] : ( X0 > ( X0 > set_o > $o ) > set_o > $o ) ).
thf(func_def_340,type,
sF259: ( $o > $o ) > set_o ).
thf(func_def_341,type,
sF260: set_o > ( $o > $o ) > $o ).
thf(func_def_342,type,
sF261: ( $o > $o ) > ( $o > $o ) > $o > $o ).
thf(func_def_343,type,
sF262:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > $o ) > X1 ) > ( X0 > $o ) > X1 ) ).
thf(func_def_344,type,
sF263:
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > X0 > $o ) ).
thf(func_def_345,type,
sF264: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > $o ).
thf(func_def_346,type,
sF265: ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_347,type,
sF266: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv > $o ).
thf(func_def_348,type,
sF267:
!>[X0: $tType,X1: $tType] : ( X0 > ( ( X1 > $o ) > X0 ) > ( X1 > $o ) > ( X0 > X0 > $o ) > $o ) ).
thf(func_def_349,type,
sF268: ( nat > $o ) > set_nat ).
thf(func_def_350,type,
sF269: set_nat > ( nat > $o ) > $o ).
thf(func_def_351,type,
sF270: ( nat > $o ) > ( nat > $o ) > nat > $o ).
thf(func_def_352,type,
sF271:
!>[X0: $tType,X1: $tType] : ( ( X0 > $o ) > X1 > ( X1 > $o ) > X0 > $o ) ).
thf(func_def_353,type,
sF272:
!>[X0: $tType,X1: $tType] : ( X0 > set_o > ( X0 > X1 ) > ( X1 > set_o > $o ) > $o ) ).
thf(func_def_354,type,
sF273: set_o > ( $o > $o ) > set_o ).
thf(func_def_355,type,
sF274: set_o > ( $o > $o ) > $o > $o ).
thf(func_def_356,type,
sF275:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > X0 ) > ( X0 > $o ) > $o ) ).
thf(func_def_357,type,
sF276:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > $o ) > X1 ) > X1 > ( X0 > $o ) > ( X0 > X1 > $o ) > X1 ) ).
thf(func_def_358,type,
sF277:
!>[X0: $tType,X1: $tType] : ( ( X0 > $o ) > X1 > ( X0 > X1 > $o ) > X0 > $o ) ).
thf(func_def_359,type,
sF278:
!>[X0: $tType,X1: $tType] : ( X0 > set_Pa1764573435lle_tv > ( X0 > X1 ) > ( X1 > set_Pa1764573435lle_tv > $o ) > $o ) ).
thf(func_def_360,type,
sF279:
!>[X0: $tType,X1: $tType] : ( set_Pa1764573435lle_tv > X1 > ( X1 > set_Pa1764573435lle_tv > X0 ) > X0 ) ).
thf(func_def_361,type,
sF280: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv ).
thf(func_def_362,type,
sF281: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv > $o ).
thf(func_def_363,type,
sF282:
!>[X0: $tType,X1: $tType] : ( X0 > set_nat > ( X0 > X1 ) > ( X1 > set_nat > $o ) > $o ) ).
thf(func_def_364,type,
sF283:
!>[X0: $tType,X1: $tType] : ( set_nat > X1 > ( X1 > set_nat > X0 ) > X0 ) ).
thf(func_def_365,type,
sF284: set_nat > ( nat > $o ) > set_nat ).
thf(func_def_366,type,
sF285: set_nat > ( nat > $o ) > nat > $o ).
thf(func_def_367,type,
sF286:
!>[X0: $tType,X1: $tType] : ( X0 > set_list_char > ( X0 > X1 ) > ( X1 > set_list_char > $o ) > $o ) ).
thf(func_def_368,type,
sF287: set_list_char > ( list_char > $o ) > set_list_char ).
thf(func_def_369,type,
sF288: set_list_char > ( list_char > $o ) > list_char > $o ).
thf(func_def_370,type,
sF289: set_o > set_o > $o ).
thf(func_def_371,type,
sF290:
!>[X0: $tType] : ( ( $o > $o ) > ( ( $o > $o ) > X0 ) > X0 ) ).
thf(func_def_372,type,
sF291: ( $o > $o ) > set_o > $o > $o ).
thf(func_def_373,type,
sF292: set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > $o ).
thf(func_def_374,type,
sF293: ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_375,type,
sF294: ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > paraco1605129243lle_tv > $o ).
thf(func_def_376,type,
sF295:
!>[X0: $tType] : ( ( paraco1605129243lle_tv > $o ) > ( ( paraco1605129243lle_tv > $o ) > X0 ) > X0 ) ).
thf(func_def_377,type,
sF296:
!>[X0: $tType,X1: $tType] : ( ( X1 > $o ) > ( ( X1 > $o ) > X0 ) > ( X0 > $o ) > $o ) ).
thf(func_def_378,type,
sF297:
!>[X0: $tType] : ( X0 > ( X0 > set_nat > $o ) > set_nat > $o ) ).
thf(func_def_379,type,
sF298: ( nat > $o ) > set_nat > set_nat ).
thf(func_def_380,type,
sF299:
!>[X0: $tType,X1: $tType] : ( X0 > set_nat > ( set_nat > X0 > X1 ) > X1 ) ).
thf(func_def_381,type,
sF300: ( nat > $o ) > set_nat > nat > $o ).
thf(func_def_382,type,
sF301:
!>[X0: $tType] : ( ( nat > $o ) > ( ( nat > $o ) > X0 ) > X0 ) ).
thf(func_def_383,type,
sF302: set_list_char > set_list_char > $o ).
thf(func_def_384,type,
sF303: ( list_char > $o ) > set_list_char > set_list_char ).
thf(func_def_385,type,
sF304: ( list_char > $o ) > set_list_char > list_char > $o ).
thf(func_def_386,type,
sF305:
!>[X0: $tType] : ( ( list_char > $o ) > ( ( list_char > $o ) > X0 ) > X0 ) ).
thf(func_def_387,type,
sF306:
!>[X0: $tType,X1: $tType] : ( X1 > $o > ( $o > X1 > $o ) > X0 > $o ) ).
thf(func_def_388,type,
sF307: set_o > $o > $o ).
thf(func_def_389,type,
sF308:
!>[X0: $tType,X1: $tType] : ( X1 > ( X0 > X1 > $o ) > X0 > $o ) ).
thf(func_def_390,type,
sF309: set_Pa1764573435lle_tv > paraco1605129243lle_tv > $o ).
thf(func_def_391,type,
sF310: set_list_char > list_char > $o ).
thf(func_def_392,type,
sF311:
!>[X0: $tType] : ( X0 > ( $o > $o ) > ( ( $o > $o ) > X0 > set_o ) > set_o ) ).
thf(func_def_393,type,
sF312:
!>[X0: $tType] : ( X0 > ( paraco1605129243lle_tv > $o ) > ( ( paraco1605129243lle_tv > $o ) > X0 > set_o ) > set_o ) ).
thf(func_def_394,type,
sF313: set_Pa1764573435lle_tv > ( set_o > $o ) > ( paraco1605129243lle_tv > $o ) > $o ).
thf(func_def_395,type,
sF314: ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > set_o ).
thf(func_def_396,type,
sF315:
!>[X0: $tType] : ( X0 > ( $o > paraco1605129243lle_tv ) > ( ( $o > paraco1605129243lle_tv ) > X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_397,type,
sF316: set_o > ( set_Pa1764573435lle_tv > $o ) > ( $o > paraco1605129243lle_tv ) > $o ).
thf(func_def_398,type,
sF317: ( $o > paraco1605129243lle_tv ) > set_o > set_Pa1764573435lle_tv ).
thf(func_def_399,type,
sF318:
!>[X0: $tType] : ( X0 > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > ( ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_400,type,
sF319:
!>[X0: $tType] : ( X0 > ( list_char > paraco1605129243lle_tv ) > ( ( list_char > paraco1605129243lle_tv ) > X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_401,type,
sF320: set_list_char > ( set_Pa1764573435lle_tv > $o ) > ( list_char > paraco1605129243lle_tv ) > $o ).
thf(func_def_402,type,
sF321:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > ( X1 > $o ) > X2 ) > X0 > ( X1 > $o ) > X2 ) ).
thf(func_def_403,type,
sF322:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > ( X0 > X1 ) > X0 ) > ( X0 > X1 ) > X1 ) ).
thf(func_def_404,type,
sF323:
!>[X0: $tType] : ( X0 > ( X0 > ( list_char > X0 ) > list_char ) > ( list_char > X0 ) > X0 ) ).
thf(func_def_405,type,
sF324:
!>[X0: $tType,X1: $tType] : ( X0 > ( $o > $o ) > ( ( $o > $o ) > X0 > X1 ) > X1 ) ).
thf(func_def_406,type,
sF325:
!>[X0: $tType] : ( ( X0 > $o ) > ( $o > $o ) > X0 > $o ) ).
thf(func_def_407,type,
sF326:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( $o > X0 ) > X1 > X2 ) > ( $o > X0 ) > X1 > X2 ) ).
thf(func_def_408,type,
sF327: ( $o > list_char ) > ( list_char > $o ) > list_char ).
thf(func_def_409,type,
sF328:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > list_char ) > X1 > X2 ) > ( X0 > list_char ) > X1 > X2 ) ).
thf(func_def_410,type,
sF329:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > X0 ) > ( X0 > list_char ) > list_char ) ).
thf(func_def_411,type,
sF330:
!>[X0: $tType] : ( X0 > ( X0 > list_char ) > list_char ) ).
thf(func_def_412,type,
sF331:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( list_char > X0 ) > X1 > X2 ) > ( list_char > X0 ) > X1 > X2 ) ).
thf(func_def_413,type,
sF332: ( list_char > paraco1605129243lle_tv ) > ( paraco1605129243lle_tv > list_char ) > paraco1605129243lle_tv ).
thf(func_def_414,type,
sF333:
!>[X0: $tType,X1: $tType] : ( ( $o > X1 ) > ( ( $o > X1 ) > set_o > X0 ) > X0 ) ).
thf(func_def_415,type,
sF334:
!>[X0: $tType] : ( ( $o > X0 ) > ( ( $o > X0 ) > $o ) > $o ) ).
thf(func_def_416,type,
sF335: ( list_char > $o ) > $o > $o ).
thf(func_def_417,type,
sF336: ( list_char > $o ) > set_o ).
thf(func_def_418,type,
sF337:
!>[X0: $tType] : ( $o > ( $o > X0 ) > X0 ) ).
thf(func_def_419,type,
sF338: ( $o > $o ) > set_o > set_o ).
thf(func_def_420,type,
sF339: ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_421,type,
sF340:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > $o ) > X1 > X2 ) > ( X0 > $o ) > X1 > X2 ) ).
thf(func_def_422,type,
sF341:
!>[X0: $tType,X1: $tType] : ( ( set_Pa1764573435lle_tv > ( X1 > paraco1605129243lle_tv ) > X0 > X1 ) > set_Pa1764573435lle_tv > X0 > ( X1 > paraco1605129243lle_tv ) > paraco1605129243lle_tv ) ).
thf(func_def_423,type,
sF342:
!>[X0: $tType,X1: $tType] : ( set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > list_char ) > ( X1 > X0 > $o ) > X0 > ( ( paraco1605129243lle_tv > list_char ) > set_Pa1764573435lle_tv > X1 ) > $o ) ).
thf(func_def_424,type,
sF343:
!>[X0: $tType,X1: $tType] : ( ( set_list_char > ( X1 > list_char ) > X0 > X1 ) > set_list_char > X0 > ( X1 > list_char ) > list_char ) ).
thf(func_def_425,type,
sF344: set_o > ( ( $o > $o ) > set_o > set_o ) > ( $o > $o ) > set_o ).
thf(func_def_426,type,
sF345:
!>[X0: $tType,X1: $tType] : ( X0 > ( paraco1605129243lle_tv > $o ) > ( ( paraco1605129243lle_tv > $o ) > X0 > X1 ) > X1 ) ).
thf(func_def_427,type,
sF346:
!>[X0: $tType,X1: $tType] : ( X0 > ( $o > paraco1605129243lle_tv ) > ( ( $o > paraco1605129243lle_tv ) > X0 > X1 ) > X1 ) ).
thf(func_def_428,type,
sF347: set_Pa1764573435lle_tv > ( ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_429,type,
sF348:
!>[X0: $tType,X1: $tType] : ( X0 > ( list_char > paraco1605129243lle_tv ) > ( ( list_char > paraco1605129243lle_tv ) > X0 > X1 ) > X1 ) ).
thf(func_def_430,type,
sF349: $o > set_o > $o ).
thf(func_def_431,type,
sF350: ( list_char > paraco1605129243lle_tv ) > list_char > paraco1605129243lle_tv ).
thf(func_def_432,type,
sF351:
!>[X0: $tType] : ( set_o > set_o > ( set_o > set_o > X0 ) > X0 ) ).
thf(func_def_433,type,
sF352:
!>[X0: $tType] : ( X0 > ( X0 > set_o > set_o ) > set_o > set_o ) ).
thf(func_def_434,type,
sF353:
!>[X0: $tType] : ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > X0 ) > X0 ) ).
thf(func_def_435,type,
sF354:
!>[X0: $tType] : ( X0 > ( X0 > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) ).
thf(func_def_436,type,
sF355: set_o > $o ).
thf(func_def_437,type,
sF356: set_Pa1764573435lle_tv > $o ).
thf(func_def_438,type,
sF357: set_list_char > $o ).
thf(func_def_439,type,
sF358:
!>[X0: $tType] : ( $o > X0 > $o ) ).
thf(func_def_440,type,
sF359:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > $o ) > X1 ) > X1 ) ).
thf(func_def_441,type,
sF360:
!>[X0: $tType] : ( X0 > $o ) ).
thf(func_def_442,type,
sF361:
!>[X0: $tType,X1: $tType] : ( X0 > ( ( X1 > $o ) > X0 ) > ( X1 > X0 > $o ) > ( X1 > $o ) > ( X0 > X0 > $o ) > $o ) ).
thf(func_def_443,type,
sF362:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > X0 > ( ( paraco1605129243lle_tv > paraco1605129243lle_tv ) > X0 > X0 ) > X1 ) ).
thf(func_def_444,type,
sF363:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > paraco1605129243lle_tv ) > X1 > X2 ) > ( X0 > paraco1605129243lle_tv ) > X1 > X2 ) ).
thf(func_def_445,type,
sF364:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( list_char > paraco1605129243lle_tv ) > ( ( list_char > paraco1605129243lle_tv ) > X1 > X0 ) > ( X0 > X2 ) > X1 > X2 ) ).
thf(func_def_446,type,
sF365:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( $o > paraco1605129243lle_tv ) > ( ( $o > paraco1605129243lle_tv ) > X1 > X0 ) > ( X0 > X2 ) > X1 > X2 ) ).
thf(func_def_447,type,
sF366:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( paraco1605129243lle_tv > list_char ) > ( ( paraco1605129243lle_tv > list_char ) > X1 > X0 ) > ( X0 > X2 ) > X1 > X2 ) ).
thf(func_def_448,type,
sF367:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( list_char > list_char ) > X0 > ( ( list_char > list_char ) > X0 > X0 ) > X1 ) ).
thf(func_def_449,type,
sF368:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( $o > list_char ) > ( ( $o > list_char ) > X1 > X0 ) > ( X0 > X2 ) > X1 > X2 ) ).
thf(func_def_450,type,
sF369:
!>[X0: $tType,X1: $tType] : ( ( paraco1605129243lle_tv > $o ) > X0 > ( ( paraco1605129243lle_tv > $o ) > X0 > X1 ) > ( X1 > $o ) > $o ) ).
thf(func_def_451,type,
sF370:
!>[X0: $tType,X1: $tType] : ( ( list_char > $o ) > X0 > ( ( list_char > $o ) > X0 > X1 ) > ( X1 > $o ) > $o ) ).
thf(func_def_452,type,
sF371:
!>[X0: $tType,X1: $tType] : ( X0 > ( list_char > $o ) > ( ( list_char > $o ) > X0 > X1 ) > X1 ) ).
thf(func_def_453,type,
sF372:
!>[X0: $tType] : ( X0 > ( $o > $o ) > ( ( $o > $o ) > X0 > X0 ) > ( X0 > $o ) > $o ) ).
thf(func_def_454,type,
sF373:
!>[X0: $tType,X1: $tType] : ( ( X0 > X0 ) > ( X0 > X1 ) > X0 > X1 ) ).
thf(func_def_455,type,
sF374:
!>[X0: $tType,X1: $tType] : ( set_list_char > ( list_char > X1 ) > ( ( list_char > X1 ) > set_list_char > X0 ) > X0 ) ).
thf(func_def_456,type,
sF375:
!>[X0: $tType,X1: $tType] : ( X0 > ( X1 > paraco1605129243lle_tv ) > ( ( X1 > paraco1605129243lle_tv ) > X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_457,type,
sF376:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > X0 ) > ( X0 > X0 ) > list_char > X0 ) ).
thf(func_def_458,type,
sF377:
!>[X0: $tType] : ( X0 > ( X0 > set_o ) > set_o ) ).
thf(func_def_459,type,
sF378:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X2 > $o ) > X0 > ( ( X1 > $o ) > X0 ) > ( X1 > X0 > $o ) > ( X1 > X2 ) > X0 ) ).
thf(func_def_460,type,
sF379:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 > $o ) > ( X0 > $o ) > X0 > X1 > X0 > $o ) ).
thf(func_def_461,type,
sF380:
!>[X0: $tType] : ( X0 > ( X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_462,type,
sF381:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 > $o ) > ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv > X1 > X0 > $o ) ).
thf(func_def_463,type,
sF382:
!>[X0: $tType,X1: $tType] : ( ( paraco1605129243lle_tv > $o ) > X1 > ( ( X0 > $o ) > X1 ) > ( X0 > paraco1605129243lle_tv ) > ( X0 > X1 > $o ) > X1 ) ).
thf(func_def_464,type,
sF383:
!>[X0: $tType] : ( ( X0 > $o ) > set_Pa1764573435lle_tv > X0 > paraco1605129243lle_tv > $o ) ).
thf(func_def_465,type,
sF384:
!>[X0: $tType] : ( X0 > ( X0 > set_nat ) > set_nat ) ).
thf(func_def_466,type,
sF385:
!>[X0: $tType,X1: $tType] : ( ( nat > $o ) > X1 > ( ( X0 > $o ) > X1 ) > ( X0 > nat ) > ( X0 > X1 > $o ) > X1 ) ).
thf(func_def_467,type,
sF386: nat > set_nat > ( nat > $o ) > nat > $o ).
thf(func_def_468,type,
sF387:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 > $o ) > ( nat > $o ) > nat > X1 > X0 > $o ) ).
thf(func_def_469,type,
sF388:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > $o ) > ( X1 > X2 > $o ) > X0 > X2 > X1 > $o ) ).
thf(func_def_470,type,
sF389:
!>[X0: $tType,X1: $tType] : ( ( $o > $o ) > X1 > ( ( X0 > $o ) > X1 ) > $o > ( X0 > X1 > $o ) > X1 ) ).
thf(func_def_471,type,
sF390:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 > $o ) > ( $o > $o ) > $o > X1 > X0 > $o ) ).
thf(func_def_472,type,
sF391:
!>[X0: $tType,X1: $tType] : ( ( $o > $o ) > X1 > ( ( X0 > $o ) > X1 ) > ( X0 > $o ) > ( X0 > X1 > $o ) > X1 ) ).
thf(func_def_473,type,
sF392: $o > set_o > ( $o > $o ) > $o > $o ).
thf(func_def_474,type,
sF393: paraco1605129243lle_tv > set_Pa1764573435lle_tv > $o ).
thf(func_def_475,type,
sF394:
!>[X0: $tType] : ( X0 > ( X0 > set_list_char > $o ) > set_list_char > $o ) ).
thf(func_def_476,type,
sF395:
!>[X0: $tType] : ( X0 > ( X0 > X0 > $o ) > $o ) ).
thf(func_def_477,type,
sF396:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X0 > X2 ) > X0 > X1 > X3 > X2 ) ).
thf(func_def_478,type,
sF397:
!>[X0: $tType,X1: $tType] : ( ( X1 > X0 > $o ) > X0 > X0 > $o ) ).
thf(func_def_479,type,
sF398:
!>[X0: $tType] : ( ( $o > $o ) > ( ( $o > $o ) > X0 ) > ( X0 > $o ) > $o ) ).
thf(func_def_480,type,
sF399:
!>[X0: $tType] : ( ( paraco1605129243lle_tv > $o ) > ( ( paraco1605129243lle_tv > $o ) > X0 ) > ( X0 > $o ) > $o ) ).
thf(func_def_481,type,
sF400:
!>[X0: $tType] : ( ( nat > $o ) > ( ( nat > $o ) > X0 ) > ( X0 > $o ) > $o ) ).
thf(func_def_482,type,
sF401:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 > X0 > $o ) ).
thf(func_def_483,type,
sF402: ( paraco1605129243lle_tv > $o ) > paraco1605129243lle_tv > $o ).
thf(func_def_484,type,
sF403: ( nat > $o ) > nat > $o ).
thf(func_def_485,type,
sF404:
!>[X0: $tType] : ( paraco1605129243lle_tv > ( paraco1605129243lle_tv > X0 ) > X0 ) ).
thf(func_def_486,type,
sF405:
!>[X0: $tType,X1: $tType] : ( X0 > paraco1605129243lle_tv > ( paraco1605129243lle_tv > X0 > X1 ) > X1 ) ).
thf(func_def_487,type,
sF406:
!>[X0: $tType,X1: $tType,X2: $tType] : ( X1 > ( X1 > set_list_char > X0 ) > ( X0 > X2 ) > set_list_char > X2 ) ).
thf(func_def_488,type,
sF407: set_o > ( $o > set_o > $o ) > $o > $o ).
thf(func_def_489,type,
sF408: ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > ( paraco1605129243lle_tv > $o ) > $o ).
thf(func_def_490,type,
sF409: ( nat > $o ) > ( nat > $o ) > ( nat > $o ) > $o ).
thf(func_def_491,type,
sF410:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > ( X0 > X1 > $o ) > X0 > $o ) ).
thf(func_def_492,type,
sF411:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > $o ) > X1 ) > X1 > ( X0 > X1 > $o ) > X1 ) ).
thf(func_def_493,type,
sF412: ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > ( list_char > paraco1605129243lle_tv ) > set_list_char > paraco1605129243lle_tv ).
thf(func_def_494,type,
sF413: ( list_char > paraco1605129243lle_tv ) > set_list_char > ( list_char > paraco1605129243lle_tv ) > list_char ).
thf(func_def_495,type,
sF414:
!>[X0: $tType] : ( set_o > ( $o > $o ) > ( ( $o > $o ) > set_o > X0 ) > X0 ) ).
thf(func_def_496,type,
sF415: ( ( set_o > set_o ) > set_o ) > ( set_o > set_o ) > set_o ).
thf(func_def_497,type,
sF416: ( ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ) > ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_498,type,
sF417: ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv > set_o ).
thf(func_def_499,type,
sF418: set_Pa1764573435lle_tv > set_o > ( set_Pa1764573435lle_tv > set_o ) > $o ).
thf(func_def_500,type,
sF419: ( set_Pa1764573435lle_tv > set_o ) > ( ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_501,type,
sF420: ( ( set_o > set_Pa1764573435lle_tv ) > set_o ) > ( set_o > set_Pa1764573435lle_tv ) > set_o ).
thf(func_def_502,type,
sF421: ( set_o > set_Pa1764573435lle_tv ) > set_o > set_Pa1764573435lle_tv ).
thf(func_def_503,type,
sF422: set_o > set_Pa1764573435lle_tv > ( set_o > set_Pa1764573435lle_tv ) > $o ).
thf(func_def_504,type,
sF423: ( set_o > set_Pa1764573435lle_tv ) > ( ( set_o > set_Pa1764573435lle_tv ) > set_o ) > set_Pa1764573435lle_tv ).
thf(func_def_505,type,
sF424:
!>[X0: $tType] : ( ( X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv > X0 > $o ) ).
thf(func_def_506,type,
sF425: ( ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) > ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_507,type,
sF426:
!>[X0: $tType] : ( X0 > ( X0 > set_o ) > set_o > $o ) ).
thf(func_def_508,type,
sF427: set_Pa1764573435lle_tv > ( set_o > set_Pa1764573435lle_tv ) > set_o > $o ).
thf(func_def_509,type,
sF428: set_o > ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv > $o ).
thf(func_def_510,type,
sF429: ( set_o > set_o ) > set_o > set_o ).
thf(func_def_511,type,
sF430: set_o > ( set_o > set_Pa1764573435lle_tv ) > set_o > $o ).
thf(func_def_512,type,
sF431: set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > set_o ) > set_Pa1764573435lle_tv > $o ).
thf(func_def_513,type,
sF432: ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv > set_Pa1764573435lle_tv ).
thf(func_def_514,type,
sF433:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 > X0 > $o ) ).
thf(func_def_515,type,
sF434:
!>[X0: $tType,X1: $tType] : ( ( paraco1605129243lle_tv > $o ) > ( ( paraco1605129243lle_tv > $o ) > X0 ) > ( X0 > X1 ) > X1 ) ).
thf(func_def_516,type,
sF435:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X2 ) > ( ( X1 > $o ) > X0 ) > ( X1 > $o ) > X2 ) ).
thf(func_def_517,type,
sF436:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > $o ) > X2 ) > ( X2 > X1 ) > set_Pa1764573435lle_tv > ( X0 > $o ) > ( X1 > set_Pa1764573435lle_tv > $o ) > $o ) ).
thf(func_def_518,type,
sF437:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > $o ) > X2 ) > ( X2 > X1 ) > set_list_char > ( X0 > $o ) > ( X1 > set_list_char > $o ) > $o ) ).
thf(func_def_519,type,
sF438:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > X0 ) > $o > X0 ) ).
thf(func_def_520,type,
sF439:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( ( X1 > list_char ) > X3 > X2 ) > ( X2 > X0 ) > ( X1 > list_char ) > X3 > X0 ) ).
thf(func_def_521,type,
sF440:
!>[X0: $tType,X1: $tType] : ( X0 > ( X1 > $o ) > ( ( X1 > $o ) > X0 > set_o ) > set_o ) ).
thf(func_def_522,type,
sF441:
!>[X0: $tType] : ( X0 > ( X0 > set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv > $o ) ).
thf(func_def_523,type,
sF442: $o > paraco1605129243lle_tv ).
thf(func_def_524,type,
sF443:
!>[X0: $tType,X1: $tType] : ( ( X1 > $o ) > X1 > X0 > $o ) ).
thf(func_def_525,type,
sF444:
!>[X0: $tType,X1: $tType] : ( ( X1 > X0 > $o ) > ( ( X1 > $o ) > ( X1 > $o ) > $o ) > X0 > X0 > $o ) ).
thf(func_def_526,type,
sF445:
!>[X0: $tType] : ( ( $o > X0 ) > X0 ) ).
thf(func_def_527,type,
sF446:
!>[X0: $tType] : ( ( $o > X0 ) > X0 ) ).
thf(func_def_528,type,
sF447:
!>[X0: $tType] : ( ( $o > X0 ) > ( ( $o > X0 ) > X0 ) > X0 ) ).
thf(func_def_529,type,
sF448:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X0 > X2 ) > ( ( X0 > X2 ) > X1 > X3 > X2 ) > X1 > X3 > X2 ) ).
thf(func_def_530,type,
sF449:
!>[X0: $tType,X1: $tType,X2: $tType] : ( X1 > ( X1 > X2 ) > X0 > X2 ) ).
thf(func_def_531,type,
sF450:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X2 ) > ( ( X0 > X2 ) > X1 ) > X1 ) ).
thf(func_def_532,type,
sF451:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > $o ) > X2 ) > ( X2 > X1 ) > ( X0 > $o ) > X1 ) ).
thf(func_def_533,type,
sF452:
!>[X0: $tType,X1: $tType] : ( ( X1 > $o ) > ( ( X1 > $o ) > X0 ) > X0 ) ).
thf(func_def_534,type,
sF453:
!>[X0: $tType] : ( ( X0 > set_Pa1764573435lle_tv ) > X0 > set_Pa1764573435lle_tv ) ).
thf(func_def_535,type,
sF454:
!>[X0: $tType] : ( ( set_o > set_Pa1764573435lle_tv ) > ( ( set_o > set_Pa1764573435lle_tv ) > X0 ) > X0 ) ).
thf(func_def_536,type,
sF455: set_o > ( set_o > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_537,type,
sF456: set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > set_o ) > set_o ).
thf(func_def_538,type,
sF457:
!>[X0: $tType,X1: $tType] : ( ( list_char > paraco1605129243lle_tv ) > X1 > X0 > ( ( list_char > paraco1605129243lle_tv ) > X1 > X0 > list_char ) > list_char ) ).
thf(func_def_539,type,
sF458:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( X2 > ( X1 > X4 ) > X0 > ( ( X1 > X4 ) > X0 > X2 > X3 ) > X3 ) ).
thf(func_def_540,type,
sF459:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X2 ) > ( ( X0 > X2 ) > X1 > X0 ) > ( X0 > X2 ) > X1 > X2 ) ).
thf(func_def_541,type,
sF460:
!>[X0: $tType] : ( ( nat > $o ) > ( nat > $o ) > ( ( nat > $o ) > ( nat > $o ) > X0 ) > X0 ) ).
thf(func_def_542,type,
sF461:
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > ( ( X0 > $o ) > ( X0 > $o ) > X0 ) > X0 ) ).
thf(func_def_543,type,
sF462:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( X2 > X4 > ( X0 > X1 ) > ( X4 > ( X0 > X1 ) > X2 > X3 ) > X3 ) ).
thf(func_def_544,type,
sF463:
!>[X0: $tType] : ( X0 > X0 > ( X0 > X0 > $o ) > X0 > X0 > $o ) ).
thf(func_def_545,type,
sF464:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X2 > X0 ) > X1 > ( ( X2 > X0 ) > X1 > $o ) > $o ) ).
thf(func_def_546,type,
sF465: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > set_Pa1764573435lle_tv > $o ) > paraco1605129243lle_tv > $o ).
thf(func_def_547,type,
sF466:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( $o > X4 > X2 > ( X0 > X1 ) > ( X4 > ( X0 > X1 ) > $o > X2 > X3 ) > X3 ) ).
thf(func_def_548,type,
sF467:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType,X6: $tType] : ( X0 > X2 > ( X6 > X4 ) > ( X1 > X5 ) > ( ( X6 > X4 ) > ( X1 > X5 ) > X0 > X2 > X3 > $o ) > X3 > $o ) ).
thf(func_def_549,type,
sF468:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > $o ) > ( X2 > X1 > $o ) > X1 > X0 > ( ( X2 > X1 > $o ) > ( X0 > $o ) > X0 > X1 > X2 > $o ) > X2 > $o ) ).
thf(func_def_550,type,
sF469:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X2 > X2 ) > ( X0 > X2 ) > X0 > X1 > X2 ) ).
thf(func_def_551,type,
sF470:
!>[X0: $tType,X1: $tType] : ( X0 > ( X1 > X1 ) > ( ( X1 > X1 ) > X0 > X0 ) > X0 ) ).
thf(func_def_552,type,
sF471:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( ( X1 > X2 ) > X0 > ( ( X3 > X4 ) > X0 > X1 ) > ( X3 > X4 ) > X2 ) ).
thf(func_def_553,type,
sF472:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( ( X1 > paraco1605129243lle_tv ) > X3 > X2 ) > ( X2 > X0 ) > ( X1 > paraco1605129243lle_tv ) > X3 > X0 ) ).
thf(func_def_554,type,
sF473:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X1 ) > ( X1 > X2 ) > X0 > X2 ) ).
thf(func_def_555,type,
sF474: ( set_list_char > $o ) > set_list_char > $o ).
thf(func_def_556,type,
sF475:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X2 > X0 ) > X1 > ( ( X2 > X0 ) > X1 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_557,type,
sF476:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X2 > X0 ) > X1 > ( ( X2 > X0 ) > X1 > set_o ) > set_o ) ).
thf(func_def_558,type,
sF477:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( X0 > ( X0 > X1 > X2 > X3 ) > X2 > X1 > X3 ) ).
thf(func_def_559,type,
sF478:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > X1 ) > $o ) > ( X0 > X1 ) > $o ) ).
thf(func_def_560,type,
sF479:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X1 > X0 ) > ( ( X1 > X0 ) > ( X0 > X1 ) > paraco1605129243lle_tv ) > paraco1605129243lle_tv ) ).
thf(func_def_561,type,
sF480:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X1 > X0 ) > ( ( X1 > X0 ) > ( X0 > X1 ) > list_char ) > list_char ) ).
thf(func_def_562,type,
sF481:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > ( list_char > X1 ) > X2 ) > X0 > ( list_char > X1 ) > X2 ) ).
thf(func_def_563,type,
sF482:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( X0 > ( X0 > ( X1 > X3 ) > X2 ) > ( X1 > X3 ) > X2 ) ).
thf(func_def_564,type,
sF483: set_list_char > ( list_char > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_565,type,
sF484: set_o > ( ( $o > paraco1605129243lle_tv ) > set_o > set_Pa1764573435lle_tv ) > ( $o > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_566,type,
sF485: set_o > ( $o > paraco1605129243lle_tv ) > set_Pa1764573435lle_tv ).
thf(func_def_567,type,
sF486: set_Pa1764573435lle_tv > ( ( paraco1605129243lle_tv > $o ) > set_Pa1764573435lle_tv > set_o ) > ( paraco1605129243lle_tv > $o ) > set_o ).
thf(func_def_568,type,
sF487: set_Pa1764573435lle_tv > ( paraco1605129243lle_tv > $o ) > set_o ).
thf(func_def_569,type,
sF488:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 > $o ) > X0 > X1 > $o ) ).
thf(func_def_570,type,
sF489:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > ( X0 > X2 ) > X1 ) > X0 > ( X0 > X2 ) > X1 ) ).
thf(func_def_571,type,
sF490: set_list_char > ( set_list_char > set_list_char > $o ) > set_list_char > $o ).
thf(func_def_572,type,
sF491: set_Pa1764573435lle_tv > ( set_Pa1764573435lle_tv > set_Pa1764573435lle_tv > $o ) > set_Pa1764573435lle_tv > $o ).
thf(func_def_573,type,
sF492: set_o > ( set_o > set_o > $o ) > set_o > $o ).
thf(func_def_574,type,
sF493:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( X3 > ( X3 > X0 > ( X1 > X3 > X2 ) > X2 ) > ( X1 > X3 > X2 ) > X0 > X2 ) ).
thf(func_def_575,type,
sF494:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( ( X2 > X3 > $o ) > X4 > X1 > ( X4 > X1 > ( X2 > X3 > $o ) > X0 ) > X0 ) ).
thf(func_def_576,type,
sF495:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > ( X1 > $o ) > X2 > $o ) > X0 > ( X1 > $o ) > X2 > $o ) ).
thf(func_def_577,type,
sF496:
!>[X0: $tType] : ( X0 > set_nat > ( set_nat > X0 > $o ) > $o ) ).
thf(func_def_578,type,
sF497: ( nat > $o ) > set_nat ).
thf(func_def_579,type,
sF498: ( ( nat > $o ) > set_nat ) > ( nat > $o ) > set_nat ).
thf(func_def_580,type,
sF499:
!>[X0: $tType,X1: $tType] : ( ( ( X1 > $o ) > X0 ) > ( X1 > $o ) > X0 ) ).
thf(func_def_581,type,
sF500: ( $o > $o ) > set_o ).
thf(func_def_582,type,
sF501: ( ( $o > $o ) > set_o ) > ( $o > $o ) > set_o ).
thf(func_def_583,type,
sF502:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( list_char > paraco1605129243lle_tv ) > X0 > X1 > ( X0 > ( list_char > paraco1605129243lle_tv ) > X1 > X2 ) > X2 ) ).
thf(func_def_584,type,
sF503: ( set_Pa1764573435lle_tv > set_se800614875lle_tv ) > set_Pa1764573435lle_tv > set_se800614875lle_tv ).
thf(func_def_585,type,
sF504: ( set_o > set_set_o ) > set_o > set_set_o ).
thf(func_def_586,type,
sF505:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > X0 > ( X0 > ( X0 > X1 ) > X1 ) > X1 ) ).
thf(func_def_587,type,
sF506: ( set_o > $o ) > ( ( set_o > $o ) > set_o ) > set_o ).
thf(func_def_588,type,
sF507:
!>[X0: $tType,X1: $tType,X2: $tType] : ( X1 > X2 > ( X1 > X2 > X0 ) > ( X2 > X1 > ( X1 > X2 > X0 ) > X0 ) > X0 ) ).
thf(func_def_589,type,
sF508:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X1 > X0 ) > X1 > X2 ) > ( X1 > X0 ) > X1 > X2 ) ).
thf(func_def_590,type,
sF509:
!>[X0: $tType] : ( X0 > ( X0 > paraco1604210848lle_fm > paraco1604210848lle_fm ) > paraco1604210848lle_fm > paraco1604210848lle_fm ) ).
thf(func_def_591,type,
sF510:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X2 > X0 ) > X1 > ( ( X2 > X0 ) > X1 > produc696645085lle_fm ) > produc696645085lle_fm ) ).
thf(func_def_592,type,
sF511:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > paraco1604210848lle_fm ) > X1 > X2 ) > ( X0 > paraco1604210848lle_fm ) > X1 > X2 ) ).
thf(func_def_593,type,
sF512:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > ( produc696645085lle_fm > X1 ) > X2 ) > X0 > ( produc696645085lle_fm > X1 ) > X2 ) ).
thf(func_def_594,type,
sF513:
!>[X0: $tType,X1: $tType] : ( X0 > ( X1 > $o ) > ( ( X1 > $o ) > X0 > X1 > $o ) > X1 > $o ) ).
thf(func_def_595,type,
sF514:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X1 > X2 > $o ) > X0 > X1 > X2 > $o ) ).
thf(func_def_596,type,
sF515:
!>[X0: $tType,X1: $tType] : ( ( X0 > $o ) > X1 > ( X1 > ( X0 > $o ) > X0 > $o ) > X0 > $o ) ).
thf(func_def_597,type,
sF516:
!>[X0: $tType] : ( X0 > ( $o > $o ) > ( ( $o > $o ) > X0 > $o > $o ) > $o > $o ) ).
thf(func_def_598,type,
sF517:
!>[X0: $tType,X1: $tType] : ( X0 > ( X1 > $o ) > ( ( X1 > $o ) > X0 > X0 ) > X0 ) ).
thf(func_def_599,type,
sF518:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( X4 > ( X5 > X4 > ( X2 > X3 > X0 ) > X1 ) > ( X2 > X3 > X0 ) > X5 > X1 ) ).
thf(func_def_600,type,
sF519:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > X1 ) > set_o ) > ( X0 > X1 ) > set_o ) ).
thf(func_def_601,type,
sF520:
!>[X0: $tType,X1: $tType] : ( X0 > X1 > ( X1 > X0 > set_o ) > set_o ) ).
thf(func_def_602,type,
sF521:
!>[X0: $tType,X1: $tType] : ( X0 > X1 > ( X1 > X0 > set_Pa1764573435lle_tv ) > set_Pa1764573435lle_tv ) ).
thf(func_def_603,type,
sF522:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X1 > X0 ) > ( ( X1 > X0 ) > ( X2 > X3 ) > list_char ) > ( X2 > X3 ) > list_char ) ).
thf(func_def_604,type,
sF523:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X1 > X0 ) > ( ( X1 > X0 ) > ( X2 > X3 ) > paraco1605129243lle_tv ) > ( X2 > X3 ) > paraco1605129243lle_tv ) ).
thf(func_def_605,type,
sF524:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X0 > X2 ) > ( X2 > X3 ) > X0 > X1 > X3 ) ).
thf(func_def_606,type,
sF525:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( X0 > ( X3 > X4 > $o ) > X2 > X1 > ( ( X3 > X4 > $o ) > X1 > X0 > X2 > X3 > $o ) > X3 > $o ) ).
thf(func_def_607,type,
sF526:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( X2 > ( X1 > X4 ) > ( X5 > ( X1 > X4 ) > X0 > X2 > X3 > $o ) > X0 > X5 > X3 > $o ) ).
thf(func_def_608,type,
sF527:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( X0 > X4 > X2 > X1 > ( X4 > X1 > X0 > X2 > X3 ) > X3 ) ).
thf(func_def_609,type,
sF528:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( X1 > ( X1 > X3 > ( X1 > X3 > X0 ) > X2 ) > ( X1 > X3 > X0 ) > X3 > X2 ) ).
thf(func_def_610,type,
sF529:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( X0 > $o ) > ( ( X0 > $o ) > ( X1 > X3 ) > X2 ) > ( X1 > X3 ) > X2 ) ).
thf(func_def_611,type,
sF530:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( X0 > ( X0 > X1 > X3 > X2 ) > X1 > X3 > X2 ) ).
thf(func_def_612,type,
sF531:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( ( X2 > X3 > X0 ) > X4 > X3 > ( X4 > X3 > ( X2 > X3 > X0 ) > X1 ) > X1 ) ).
thf(func_def_613,type,
sF532:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( X0 > X4 > X2 > X1 > ( X4 > X1 > X0 > X2 > X3 > $o ) > X3 > $o ) ).
thf(func_def_614,type,
sF533:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( X2 > X4 > X1 > ( X4 > X1 > X2 > X3 > X0 ) > X3 > X0 ) ).
thf(f1,axiom,
( ( paraco1933902578domain
@ ( collect_nat
@ ^ [X0: nat] : $true ) )
= ( collec1111687558lle_tv
@ ^ [X1: paraco1605129243lle_tv] : $true ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_universal__domain) ).
thf(f203,axiom,
( top_top_set_nat
= ( collect_nat
@ ^ [X0: nat] : $true ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_UNIV__def) ).
thf(f204,axiom,
( top_to1057771083lle_tv
= ( collec1111687558lle_tv
@ ^ [X0: paraco1605129243lle_tv] : $true ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_UNIV__def) ).
thf(f255,axiom,
! [X0: set_Pa1764573435lle_tv] : ( ord_le241064091lle_tv @ X0 @ top_to1057771083lle_tv ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_subset__UNIV) ).
thf(f355,conjecture,
! [X0: list_char > paraco1605129243lle_tv] :
( ( ( paraco1325918602e_eval @ X0 @ p )
= ( paraco1344940915le_Det @ $true ) )
!= ( ~ ! [X0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [X1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ X0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(f356,negated_conjecture,
~ ! [X0: list_char > paraco1605129243lle_tv] :
( ( ( paraco1325918602e_eval @ X0 @ p )
= ( paraco1344940915le_Det @ $true ) )
!= ( ~ ! [X0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [X1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ X0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f355]) ).
thf(f357,plain,
( ( paraco1933902578domain
@ ( collect_nat
@ ^ [X0: nat] : $true ) )
= ( collec1111687558lle_tv
@ ^ [X1: paraco1605129243lle_tv] : $true ) ),
inference(rectify,[],[f1]) ).
thf(f358,plain,
( ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) )
= ( collec1111687558lle_tv
@ ^ [Y0: paraco1605129243lle_tv] : $true ) ),
inference(fool_elimination,[],[f357]) ).
thf(f740,plain,
( top_top_set_nat
= ( collect_nat
@ ^ [X0: nat] : $true ) ),
inference(rectify,[],[f203]) ).
thf(f741,plain,
( top_top_set_nat
= ( collect_nat
@ ^ [Y0: nat] : $true ) ),
inference(fool_elimination,[],[f740]) ).
thf(f742,plain,
( top_to1057771083lle_tv
= ( collec1111687558lle_tv
@ ^ [X0: paraco1605129243lle_tv] : $true ) ),
inference(rectify,[],[f204]) ).
thf(f743,plain,
( top_to1057771083lle_tv
= ( collec1111687558lle_tv
@ ^ [Y0: paraco1605129243lle_tv] : $true ) ),
inference(fool_elimination,[],[f742]) ).
thf(f841,plain,
! [X0: set_Pa1764573435lle_tv] : ( ord_le241064091lle_tv @ X0 @ top_to1057771083lle_tv ),
inference(rectify,[],[f255]) ).
thf(f842,plain,
! [X0: set_Pa1764573435lle_tv] :
( ( ord_le241064091lle_tv @ X0 @ top_to1057771083lle_tv )
= $true ),
inference(fool_elimination,[],[f841]) ).
thf(f957,plain,
~ ! [X0: list_char > paraco1605129243lle_tv] :
( ( ( paraco1325918602e_eval @ X0 @ p )
= ( paraco1344940915le_Det @ $true ) )
!= ( ~ ! [X1: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X1 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [X2: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ X1 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
inference(rectify,[],[f356]) ).
thf(f958,plain,
~ ( ( ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
!= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ) ),
inference(fool_elimination,[],[f957]) ).
thf(f971,plain,
( ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ),
inference(flattening,[],[f958]) ).
thf(f1371,plain,
( ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) )
= ( collec1111687558lle_tv
@ ^ [Y0: paraco1605129243lle_tv] : $true ) ),
inference(cnf_transformation,[],[f358]) ).
thf(f1620,plain,
( top_top_set_nat
= ( collect_nat
@ ^ [Y0: nat] : $true ) ),
inference(cnf_transformation,[],[f741]) ).
thf(f1621,plain,
( top_to1057771083lle_tv
= ( collec1111687558lle_tv
@ ^ [Y0: paraco1605129243lle_tv] : $true ) ),
inference(cnf_transformation,[],[f743]) ).
thf(f1686,plain,
! [X0: set_Pa1764573435lle_tv] :
( ( ord_le241064091lle_tv @ X0 @ top_to1057771083lle_tv )
= $true ),
inference(cnf_transformation,[],[f842]) ).
thf(f1832,plain,
( ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ),
inference(cnf_transformation,[],[f971]) ).
thf(f1901,plain,
( ( $true
= ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) )
| ( $false
= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ) ),
inference(iff_proxy_clausification,[],[f1832]) ).
thf(f1902,plain,
( ( $false
= ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) )
| ( $true
= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ) ),
inference(iff_proxy_clausification,[],[f1832]) ).
thf(f1903,plain,
( ( $false
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) )
@ sK150 ) )
| ( $true
= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f1902]) ).
thf(f1904,plain,
( ( $false
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) )
@ sK150 ) )
| ( $false
= ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f1903]) ).
thf(f1905,plain,
( ( $false
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) )
@ sK150 ) )
| ( $false
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
@ sK151 ) ) ),
inference(sigma_proxy_clausification,[],[f1904]) ).
thf(f1906,plain,
( ( $false
= ( ( paraco1325918602e_eval @ sK150 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
| ( $false
= ( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ sK151 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ sK151 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
inference(beta-eta_normalization,[],[f1905]) ).
thf(f1907,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1325918602e_eval @ sK150 @ p ) )
| ( $false
= ( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ sK151 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ sK151 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
inference(equality_proxy_clausification,[],[f1906]) ).
thf(f1908,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1325918602e_eval @ sK150 @ p ) )
| ( $false
= ( ( paraco1325918602e_eval @ sK151 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ),
inference(imp_proxy_clausification,[],[f1907]) ).
thf(f1910,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1325918602e_eval @ sK150 @ p ) )
| ( ( paraco1344940915le_Det @ $true )
!= ( paraco1325918602e_eval @ sK151 @ p ) ) ),
inference(equality_proxy_clausification,[],[f1908]) ).
thf(f1911,plain,
! [X1: list_char > paraco1605129243lle_tv] :
( ( $true
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) )
@ X1 ) )
| ( $false
= ( ~ ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f1901]) ).
thf(f1912,plain,
! [X1: list_char > paraco1605129243lle_tv] :
( ( $true
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) )
@ X1 ) )
| ( $true
= ( !! @ ( list_char > paraco1605129243lle_tv )
@ ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f1911]) ).
thf(f1913,plain,
! [X2: list_char > paraco1605129243lle_tv,X1: list_char > paraco1605129243lle_tv] :
( ( $true
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: list_char > paraco1605129243lle_tv] :
( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ Y0 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y1: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ Y0 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f1912]) ).
thf(f1914,plain,
! [X2: list_char > paraco1605129243lle_tv,X1: list_char > paraco1605129243lle_tv] :
( ( $true
= ( ( paraco1325918602e_eval @ X1 @ p )
= ( paraco1344940915le_Det @ $true ) ) )
| ( $true
= ( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ X2 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
inference(beta-eta_normalization,[],[f1913]) ).
thf(f1915,plain,
! [X2: list_char > paraco1605129243lle_tv,X1: list_char > paraco1605129243lle_tv] :
( ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X1 @ p ) )
| ( $true
= ( ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) )
=> ( ( paraco1325918602e_eval @ X2 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ) ),
inference(equality_proxy_clausification,[],[f1914]) ).
thf(f1916,plain,
! [X2: list_char > paraco1605129243lle_tv,X1: list_char > paraco1605129243lle_tv] :
( ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X1 @ p ) )
| ( $false
= ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) ) )
| ( $true
= ( ( paraco1325918602e_eval @ X2 @ p )
= ( paraco1344940915le_Det @ $true ) ) ) ),
inference(imp_proxy_clausification,[],[f1915]) ).
thf(f1917,plain,
! [X2: list_char > paraco1605129243lle_tv,X1: list_char > paraco1605129243lle_tv] :
( ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X1 @ p ) )
| ( $false
= ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) ) )
| ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) ) ),
inference(equality_proxy_clausification,[],[f1916]) ).
thf(f2417,definition,
( spl188_2
<=> ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ sK150 @ p ) ) ),
introduced(definition,[new_symbols(definition,[spl188_2])],[avatar_definition]) ).
thf(f2419,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1325918602e_eval @ sK150 @ p ) )
| spl188_2 ),
inference(avatar_component_clause,[],[f2417]) ).
thf(f2422,definition,
( spl188_3
<=> ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ sK151 @ p ) ) ),
introduced(definition,[new_symbols(definition,[spl188_3])],[avatar_definition]) ).
thf(f2424,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1325918602e_eval @ sK151 @ p ) )
| spl188_3 ),
inference(avatar_component_clause,[],[f2422]) ).
thf(f2425,plain,
( ~ spl188_3
| ~ spl188_2 ),
inference(avatar_split_clause,[],[f1910,f2417,f2422]) ).
thf(f2427,definition,
( spl188_4
<=> ! [X2: list_char > paraco1605129243lle_tv] :
( ( $false
= ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) ) )
| ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) ) ) ),
introduced(definition,[new_symbols(definition,[spl188_4])],[avatar_definition]) ).
thf(f2428,plain,
( ! [X2: list_char > paraco1605129243lle_tv] :
( ( $false
= ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char )
@ ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) ) )
| ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) ) )
| ~ spl188_4 ),
inference(avatar_component_clause,[],[f2427]) ).
thf(f2430,definition,
( spl188_5
<=> ! [X1: list_char > paraco1605129243lle_tv] :
( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X1 @ p ) ) ),
introduced(definition,[new_symbols(definition,[spl188_5])],[avatar_definition]) ).
thf(f2431,plain,
( ! [X1: list_char > paraco1605129243lle_tv] :
( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X1 @ p ) )
| ~ spl188_5 ),
inference(avatar_component_clause,[],[f2430]) ).
thf(f2432,plain,
( spl188_4
| spl188_5 ),
inference(avatar_split_clause,[],[f1917,f2430,f2427]) ).
thf(f2945,plain,
( top_to1057771083lle_tv
= ( paraco1933902578domain
@ ( collect_nat
@ ^ [Y0: nat] : $true ) ) ),
inference(forward_demodulation,[],[f1371,f1621]) ).
thf(f2955,plain,
( top_to1057771083lle_tv
= ( paraco1933902578domain @ top_top_set_nat ) ),
inference(forward_demodulation,[],[f2945,f1620]) ).
thf(f3309,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1344940915le_Det @ $true ) )
| spl188_3
| ~ spl188_5 ),
inference(constrained_superposition,[],[f2424,f2431]) ).
thf(f3310,plain,
( $false
| spl188_3
| ~ spl188_5 ),
inference(trivial_inequality_removal,[],[f3309]) ).
thf(f3311,plain,
( spl188_3
| ~ spl188_5 ),
inference(avatar_contradiction_clause,[],[f3310]) ).
thf(f3312,plain,
( ! [X2: list_char > paraco1605129243lle_tv] :
( ( $false
= ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char ) @ ( paraco1933902578domain @ top_top_set_nat ) ) )
| ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) ) )
| ~ spl188_4 ),
inference(forward_demodulation,[],[f2428,f1620]) ).
thf(f3313,plain,
( ! [X2: list_char > paraco1605129243lle_tv] :
( ( $false
= ( ord_le241064091lle_tv @ ( image_1187894195lle_tv @ X2 @ top_to748628679t_char ) @ top_to1057771083lle_tv ) )
| ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) ) )
| ~ spl188_4 ),
inference(forward_demodulation,[],[f3312,f2955]) ).
thf(f3314,plain,
( ! [X2: list_char > paraco1605129243lle_tv] :
( ( $true = $false )
| ( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) ) )
| ~ spl188_4 ),
inference(forward_demodulation,[],[f3313,f1686]) ).
thf(f3315,plain,
( ! [X2: list_char > paraco1605129243lle_tv] :
( ( paraco1344940915le_Det @ $true )
= ( paraco1325918602e_eval @ X2 @ p ) )
| ~ spl188_4 ),
inference(trivial_inequality_removal,[],[f3314]) ).
thf(f3316,plain,
( spl188_5
| ~ spl188_4 ),
inference(avatar_split_clause,[],[f3315,f2427,f2430]) ).
thf(f3317,plain,
( ( ( paraco1344940915le_Det @ $true )
!= ( paraco1344940915le_Det @ $true ) )
| spl188_2
| ~ spl188_5 ),
inference(constrained_superposition,[],[f2419,f2431]) ).
thf(f3318,plain,
( $false
| spl188_2
| ~ spl188_5 ),
inference(trivial_inequality_removal,[],[f3317]) ).
thf(f3319,plain,
( spl188_2
| ~ spl188_5 ),
inference(avatar_contradiction_clause,[],[f3318]) ).
cnf(s2,plain,
( ~ spl188_2
| ~ spl188_3 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s3,plain,
( spl188_4
| spl188_5 ),
inference(sat_conversion,[],[f2432]) ).
cnf(s4,plain,
( spl188_3
| ~ spl188_5 ),
inference(sat_conversion,[],[f3311]) ).
cnf(s5,plain,
( ~ spl188_4
| spl188_5 ),
inference(sat_conversion,[],[f3316]) ).
cnf(s6,plain,
( spl188_2
| ~ spl188_5 ),
inference(sat_conversion,[],[f3319]) ).
cnf(s7,plain,
spl188_5,
inference(rat,[],[s3,s5]) ).
cnf(s8,plain,
spl188_2,
inference(rat,[],[s6,s7]) ).
cnf(s9,plain,
spl188_3,
inference(rat,[],[s4,s7]) ).
cnf(s11,plain,
$false,
inference(rat,[],[s2,s9,s8]) ).
thf(f3320,plain,
$false,
inference(avatar_sat_refutation,[],[s11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP138^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n018.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 20:01:27 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/0.88 % (571139)Will run a generic schedule for satisfiability detection.
% 3.76/0.88 % (571145)% WARNING: option uhcvi not known.
% 3.76/0.88 % (571145)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1817872466:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.76/0.88 % (571144)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2498589080_2999 on theBenchmark for (2999ds/0Mi)
% 3.76/0.88 % (571146)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=882931180:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.76/0.88 % (571147)dis+10_1_sil=32000:sp=arity:random_seed=249665194:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.76/0.88 % (571148)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2667834800:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.76/0.88 % (571150)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3514679901:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.76/0.88 % (571149)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1791279885:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.76/0.88 % (571145)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % (571148)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % (571150)Instruction limit reached!
% 3.76/0.88 % (571150)------------------------------
% 3.76/0.88 % (571150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571150)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571150)Termination reason: Instruction limit
% 3.76/0.88 % (571150)Termination phase: Saturation
% 3.76/0.88 % (571150)Time elapsed: 0.036 s
% 3.76/0.88 % (571150)Peak memory usage: 13 MB
% 3.76/0.88 % (571150)Instructions burned: 161 (million)
% 3.76/0.88 % (571147)Instruction limit reached!
% 3.76/0.88 % (571147)------------------------------
% 3.76/0.88 % (571147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571147)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571147)Termination reason: Instruction limit
% 3.76/0.88 % (571147)Termination phase: Property scanning
% 3.76/0.88 % (571147)Time elapsed: 0.043 s
% 3.76/0.88 % (571147)Peak memory usage: 12 MB
% 3.76/0.88 % (571147)Instructions burned: 104 (million)
% 3.76/0.88 % (571148)Instruction limit reached!
% 3.76/0.88 % (571148)------------------------------
% 3.76/0.88 % (571148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571148)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571148)Termination reason: Instruction limit
% 3.76/0.88 % (571148)Termination phase: Property scanning
% 3.76/0.88 % (571148)Time elapsed: 0.048 s
% 3.76/0.88 % (571148)Peak memory usage: 11 MB
% 3.76/0.88 % (571148)Instructions burned: 117 (million)
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571145)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.76/0.88 % (571158)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2251402021:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.76/0.88 % (571149)Instruction limit reached!
% 3.76/0.88 % (571149)------------------------------
% 3.76/0.88 % (571149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571149)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571149)Termination reason: Instruction limit
% 3.76/0.88 % (571149)Termination phase: Saturation
% 3.76/0.88 % (571149)Time elapsed: 0.054 s
% 3.76/0.88 % (571149)Peak memory usage: 13 MB
% 3.76/0.88 % (571149)Instructions burned: 131 (million)
% 3.76/0.88 % (571159)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2539053588:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.76/0.88 % (571160)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4095427150:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.76/0.88 % (571162)ott-21_1_sil=16000:fs=off:random_seed=3434416813:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571163)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3615764559:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.76/0.88 % (571167)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1898103902:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.76/0.88 % (571160)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571159)Instruction limit reached!
% 3.76/0.88 % (571159)------------------------------
% 3.76/0.88 % (571159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571159)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571159)Termination reason: Instruction limit
% 3.76/0.88 % (571159)Termination phase: Saturation
% 3.76/0.88 % (571159)Time elapsed: 0.054 s
% 3.76/0.88 % (571159)Peak memory usage: 13 MB
% 3.76/0.88 % (571159)Instructions burned: 132 (million)
% 3.76/0.88 % (571160)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.76/0.88 % (571170)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2220999705:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 3.76/0.88 % (571171)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=371400684:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 3.76/0.88 % (571162)Instruction limit reached!
% 3.76/0.88 % (571162)------------------------------
% 3.76/0.88 % (571162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571162)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571162)Termination reason: Instruction limit
% 3.76/0.88 % (571162)Termination phase: Saturation
% 3.76/0.88 % (571162)Time elapsed: 0.075 s
% 3.76/0.88 % (571162)Peak memory usage: 13 MB
% 3.76/0.88 % (571162)Instructions burned: 181 (million)
% 3.76/0.88 % (571174)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1708042661:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 3.76/0.88 % (571174)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571176)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1565711695:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 3.76/0.88 % (571176)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % (571160)Instruction limit reached!
% 3.76/0.88 % (571160)------------------------------
% 3.76/0.88 % (571160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571160)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571160)Termination reason: Instruction limit
% 3.76/0.88 % (571160)Termination phase: Saturation
% 3.76/0.88 % (571160)Time elapsed: 0.299 s
% 3.76/0.88 % (571160)Peak memory usage: 16 MB
% 3.76/0.88 % (571160)Instructions burned: 685 (million)
% 3.76/0.88 % (571178)fmb+10_1_sil=64000:random_seed=4138885758:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 3.76/0.88 % (571163)Instruction limit reached!
% 3.76/0.88 % (571163)------------------------------
% 3.76/0.88 % (571163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571163)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571163)Termination reason: Instruction limit
% 3.76/0.88 % (571163)Termination phase: Saturation
% 3.76/0.88 % (571163)Time elapsed: 0.333 s
% 3.76/0.88 % (571163)Peak memory usage: 14 MB
% 3.76/0.88 % (571163)Instructions burned: 479 (million)
% 3.76/0.88 % (571170)Instruction limit reached!
% 3.76/0.88 % (571170)------------------------------
% 3.76/0.88 % (571170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571170)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571170)Termination reason: Instruction limit
% 3.76/0.88 % (571170)Termination phase: Saturation
% 3.76/0.88 % (571170)Time elapsed: 0.296 s
% 3.76/0.88 % (571170)Peak memory usage: 20 MB
% 3.76/0.88 % (571170)Instructions burned: 1183 (million)
% 3.76/0.88 % (571178)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.76/0.88 % (571181)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=928453091:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571180)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2921280809:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 3.76/0.88 % (571183)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2031133223:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571186)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3267092830:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 3.76/0.88 % (571174)Instruction limit reached!
% 3.76/0.88 % (571174)------------------------------
% 3.76/0.88 % (571174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.88 % (571174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.88 % (571174)CaDiCaL version: 2.1.3
% 3.76/0.88 % (571174)Termination reason: Instruction limit
% 3.76/0.88 % (571174)Termination phase: Saturation
% 3.76/0.88 % (571174)Time elapsed: 0.309 s
% 3.76/0.88 % (571174)Peak memory usage: 17 MB
% 3.76/0.88 % (571174)Instructions burned: 693 (million)
% 3.76/0.88 % (571183)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % (571186)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571188)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1561888797:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 3.76/0.88 % (571186)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.76/0.88 % (571190)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2064536442:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571192)ott-2_1_sil=16000:newcnf=on:random_seed=80227141:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 3.76/0.88 % Exception at run slice level
% 3.76/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.76/0.88 % (571192)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.76/0.88 % (571194)ott+10_1_sil=32000:tgt=ground:random_seed=3003970132:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 3.76/0.88 % (571186) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-571139-571186"...
% 3.76/0.88 % (571186)...printing done.
% 3.76/0.88 % (571186)Refutation found. Thanks to Tanya!
% 3.76/0.88 % SZS status Theorem for theBenchmark
% 3.76/0.88 % SZS output start Proof for theBenchmark
% See solution above
% 3.76/0.89 % (571186)------------------------------
% 3.76/0.89 % (571186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.89 % (571186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.89 % (571186)CaDiCaL version: 2.1.3
% 3.76/0.89 % (571186)Termination reason: Refutation
% 3.76/0.89 % (571186)Time elapsed: 0.139 s
% 3.76/0.89 % (571186)Peak memory usage: 17 MB
% 3.76/0.89 % (571186)Instructions burned: 533 (million)
% 3.76/0.89 % (571139)Success in time 0.659 s
% 3.76/0.89 % Vampire exiting
%------------------------------------------------------------------------------