%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : CSR111+2 : TPTP v6.4.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_nitpick %d %s % Computer : n142.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.36.3.el7.x86_64 % CPULimit : 300s % DateTime : Tue Jan 17 13:16:02 EST 2017 % Result : Satisfiable 69.37s % Output : FiniteModel 69.48s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : CSR111+2 : TPTP v6.4.0. Released v3.5.0. % 0.00/0.04 % Command : isabelle tptp_nitpick %d %s % 0.03/0.24 % Computer : n142.star.cs.uiowa.edu % 0.03/0.24 % Model : x86_64 x86_64 % 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.24 % Memory : 32218.75MB % 0.03/0.24 % OS : Linux 3.10.0-327.36.3.el7.x86_64 % 0.03/0.24 % CPULimit : 300 % 0.03/0.24 % DateTime : Sat Jan 14 02:53:33 CST 2017 % 0.03/0.24 % CPUTime : % 69.37/42.31 Nitpicking formula... % 69.37/42.31 Timestamp: 02:53:43 % 69.37/42.31 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 69.37/42.31 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 69.37/42.31 Batch 1 of 20: Trying 5 scopes: % 69.37/42.31 card TPTP_Interpret.ind = 1 % 69.37/42.31 card TPTP_Interpret.ind = 2 % 69.37/42.31 card TPTP_Interpret.ind = 3 % 69.37/42.31 card TPTP_Interpret.ind = 4 % 69.37/42.31 card TPTP_Interpret.ind = 5 % 69.37/42.31 % SZS status Satisfiable % SZS output start FiniteModel % 69.37/42.31 Nitpick found a model for card TPTP_Interpret.ind = 5: % 69.37/42.31 % 69.37/42.31 Constants: % 69.37/42.31 bnd_affiliatedwith = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.37/42.31 bnd_agent_generic = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.37/42.31 bnd_airport_physical = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.37/42.31 bnd_airporthasiatacode = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.37/42.31 bnd_applicationcontext = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_arg1isa = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False)) % 69.37/42.31 bnd_arg2isa = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False)) % 69.37/42.31 bnd_artifact = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_artsupplies = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_aspatialinformationstore = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_aspatialthing = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_binarypredicate = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := True) % 69.37/42.31 bnd_borderson = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := True), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := False)) % 69.37/42.31 bnd_c_affiliatedwith = i1 % 69.37/42.31 bnd_c_airport_physical = i2 % 69.37/42.31 bnd_c_airporthasiatacode = i1 % 69.37/42.31 bnd_c_ap_martha_stewart_omnimedia_names_chairman = i2 % 69.37/42.31 bnd_c_applicationcontext = i4 % 69.37/42.31 bnd_c_artifact = i4 % 69.37/42.31 bnd_c_artsupplies = i4 % 69.37/42.31 bnd_c_aspatialinformationstore = i4 % 69.37/42.31 bnd_c_aspatialthing = i4 % 69.37/42.31 bnd_c_basekb = i2 % 69.37/42.31 bnd_c_beloitcollege = i1 % 69.37/42.31 bnd_c_calendarsmt = i2 % 69.37/42.31 bnd_c_calendarsvocabularymt = i2 % 69.37/42.31 bnd_c_citynamedfn = i5 % 69.37/42.31 bnd_c_cityofbostonma = i1 % 69.37/42.31 bnd_c_collection = i1 % 69.37/42.31 bnd_c_computerdataartifact = i4 % 69.37/42.31 bnd_c_contentmtofcdafromeventfn = i5 % 69.37/42.31 bnd_c_contextofpcwfn = i5 % 69.37/42.31 bnd_c_corecyclmt = i2 % 69.37/42.31 bnd_c_correctivelensprescription = i2 % 69.37/42.31 bnd_c_currentworlddatacollectormt_nonhomocentric = i2 % 69.37/42.31 bnd_c_cyclistsmt = i2 % 69.37/42.31 bnd_c_cycnounlearnermt = i2 % 69.37/42.31 bnd_c_cycorpproductsmt = i2 % 69.37/42.31 bnd_c_directionoftranslation_throughout = i5 % 69.37/42.31 bnd_c_disjointwith = i1 % 69.37/42.31 bnd_c_enduringthing_localized = i4 % 69.37/42.31 bnd_c_englishmt = i1 % 69.37/42.31 bnd_c_ethnicgroupsmt = i2 % 69.37/42.31 bnd_c_ethnicgroupsvocabularymt = i2 % 69.37/42.31 bnd_c_executionbyfiringsquad = i1 % 69.37/42.31 bnd_c_few = i1 % 69.37/42.31 bnd_c_firstordercollection = i1 % 69.37/42.31 bnd_c_fixedordercollection = i1 % 69.37/42.31 bnd_c_footballteam = i2 % 69.37/42.31 bnd_c_france = i5 % 69.37/42.31 bnd_c_furpelt = i4 % 69.37/42.31 bnd_c_generictemporalmt = i2 % 69.37/42.31 bnd_c_genlmt = i1 % 69.37/42.31 bnd_c_genlpreds = i1 % 69.37/42.31 bnd_c_genls = i1 % 69.37/42.31 bnd_c_geographicalregion = i4 % 69.37/42.31 bnd_c_geographicalsubregions = i1 % 69.37/42.31 bnd_c_geographymt = i2 % 69.37/42.31 bnd_c_geolevel_1 = i3 % 69.37/42.31 bnd_c_geolevel_3 = i3 % 69.37/42.31 bnd_c_geolevel_4 = i4 % 69.37/42.31 bnd_c_geolocation_x14_y39 = i2 % 69.37/42.31 bnd_c_geolocation_x53_y74 = i2 % 69.37/42.31 bnd_c_geolocation_x76_y23 = i2 % 69.37/42.31 bnd_c_georegion_l1_x2_y0 = i2 % 69.37/42.31 bnd_c_georegion_l2_x5_y8 = i2 % 69.37/42.31 bnd_c_georegion_l2_x8_y2 = i2 % 69.37/42.31 bnd_c_georegion_l3_x11_y2 = i2 % 69.37/42.31 bnd_c_georegion_l3_x15_y24 = i2 % 69.37/42.31 bnd_c_georegion_l3_x17_y24 = i2 % 69.37/42.31 bnd_c_georegion_l3_x25_y7 = i2 % 69.37/42.31 bnd_c_georegion_l3_x4_y13 = i2 % 69.37/42.31 bnd_c_georegion_l4_x14_y39 = i2 % 69.37/42.31 bnd_c_georegion_l4_x27_y64 = i5 % 69.37/42.31 bnd_c_georegion_l4_x27_y65 = i2 % 69.37/42.31 bnd_c_georegion_l4_x29_y75 = i5 % 69.37/42.31 bnd_c_georegion_l4_x29_y76 = i2 % 69.37/42.31 bnd_c_georegion_l4_x35_y7 = i2 % 69.37/42.31 bnd_c_georegion_l4_x36_y50 = i5 % 69.37/42.31 bnd_c_georegion_l4_x37_y50 = i5 % 69.37/42.31 bnd_c_georegion_l4_x38_y24 = i5 % 69.37/42.31 bnd_c_georegion_l4_x39_y24 = i2 % 69.37/42.31 bnd_c_georegion_l4_x45_y10 = i2 % 69.37/42.31 bnd_c_georegion_l4_x45_y72 = i2 % 69.37/42.31 bnd_c_georegion_l4_x45_y9 = i5 % 69.37/42.31 bnd_c_georegion_l4_x53_y74 = i2 % 69.37/42.31 bnd_c_georegion_l4_x56_y47 = i5 % 69.37/42.31 bnd_c_georegion_l4_x57_y47 = i2 % 69.37/42.31 bnd_c_georegion_l4_x75_y75 = i5 % 69.37/42.31 bnd_c_georegion_l4_x76_y23 = i2 % 69.37/42.31 bnd_c_gregoriancalendarmt = i2 % 69.37/42.31 bnd_c_hasmembers = i1 % 69.37/42.31 bnd_c_hpkb_subnationalagent = i1 % 69.37/42.31 bnd_c_hpkbvocabmt = i2 % 69.37/42.31 bnd_c_humansociallifemt = i2 % 69.37/42.31 bnd_c_inanimateobject = i4 % 69.37/42.31 bnd_c_inanimateobject_nonnatural = i4 % 69.37/42.31 bnd_c_individual = i4 % 69.37/42.31 bnd_c_inregion = i1 % 69.37/42.31 bnd_c_instancewithrelationtofn = i5 % 69.37/42.31 bnd_c_intangible = i1 % 69.37/42.31 bnd_c_intangibleindividual = i4 % 69.37/42.31 bnd_c_issuingaprescription = i1 % 69.37/42.31 bnd_c_keinteractionresourcetestmt = i2 % 69.37/42.31 bnd_c_knowledgefragmentd3mt = i2 % 69.37/42.31 bnd_c_ldscdemonstrationspindleheadmt = i2 % 69.37/42.31 bnd_c_ldscgeneralcollectormt = i2 % 69.37/42.31 bnd_c_location_underspecified = i3 % 69.37/42.31 bnd_c_logicaltruthmt = i2 % 69.37/42.31 bnd_c_machinelearningspindleheadmt = i5 % 69.37/42.31 bnd_c_marriagelicensedocument = i2 % 69.37/42.31 bnd_c_massmediadatamt = i2 % 69.37/42.31 bnd_c_mathematicalorcomputationalthing = i1 % 69.37/42.31 bnd_c_mathematicalthing = i1 % 69.37/42.31 bnd_c_microtheory = i4 % 69.37/42.31 bnd_c_militaryperson = i4 % 69.37/42.31 bnd_c_miptdatabase19681997_termsmt = i2 % 69.37/42.31 bnd_c_most = i1 % 69.37/42.31 bnd_c_movement_translationevent = i1 % 69.37/42.31 bnd_c_navypersonnel = i4 % 69.37/42.31 bnd_c_no = i1 % 69.37/42.31 bnd_c_nooescapearchitecturemt = i2 % 69.37/42.31 bnd_c_objectfoundinlocation = i4 % 69.37/42.31 bnd_c_orderingpredicate = i1 % 69.37/42.31 bnd_c_organizationdatamt = i2 % 69.37/42.31 bnd_c_orientation = i1 % 69.37/42.31 bnd_c_orientationvector = i2 % 69.37/42.31 bnd_c_partiallyintangibleindividual = i4 % 69.37/42.31 bnd_c_partiallytangible = i4 % 69.37/42.31 bnd_c_patterndetectormt = i2 % 69.37/42.31 bnd_c_peopledatamt = i2 % 69.37/42.31 bnd_c_physicalorderingpredicate = i1 % 69.37/42.31 bnd_c_products = i5 % 69.37/42.31 bnd_c_pushingababycarriage = i1 % 69.37/42.31 bnd_c_pushingwithfingers = i1 % 69.37/42.31 bnd_c_pushingwithopenhand = i1 % 69.37/42.31 bnd_c_reasoningaboutpossibleantecedentsmt = i2 % 69.37/42.31 bnd_c_reflexivebinarypredicate = i1 % 69.37/42.31 bnd_c_relationallexistsfn = i5 % 69.37/42.31 bnd_c_relationexistsallfn = i3 % 69.37/42.31 bnd_c_ridgeline_topographical = i4 % 69.37/42.31 bnd_c_runningshorts = i4 % 69.37/42.31 bnd_c_setorcollection = i1 % 69.37/42.31 bnd_c_shavingrazor_manual = i1 % 69.37/42.31 bnd_c_ship = i3 % 69.37/42.31 bnd_c_spatialthing_nonsituational = i3 % 69.37/42.31 bnd_c_state_geopolitical = i1 % 69.37/42.31 bnd_c_subcollectionofwithrelationfromtypefn = i5 % 69.37/42.31 bnd_c_subcollectionofwithrelationtofn = i5 % 69.37/42.31 bnd_c_subcollectionofwithrelationtotypefn = i5 % 69.37/42.31 bnd_c_subsetof = i1 % 69.37/42.31 bnd_c_supplies = i4 % 69.37/42.31 bnd_c_terrorist = i2 % 69.37/42.31 bnd_c_terroristgroup = i1 % 69.37/42.31 bnd_c_testvocabularymt = i2 % 69.37/42.31 bnd_c_theprototypicalfurpelt = i5 % 69.37/42.31 bnd_c_theprototypicalshavingrazor_manual = i1 % 69.37/42.31 bnd_c_thing = i3 % 69.37/42.31 bnd_c_timehasnoendmt = i2 % 69.37/42.31 bnd_c_tptp_8_271 = i1 % 69.37/42.31 bnd_c_tptp_8_875 = i1 % 69.37/42.31 bnd_c_tptp_8_968 = i1 % 69.37/42.31 bnd_c_tptp_9_51 = i1 % 69.37/42.31 bnd_c_tptp_9_720 = i1 % 69.37/42.31 bnd_c_tptp_member1672_mt = i2 % 69.37/42.31 bnd_c_tptp_member2089_mt = i2 % 69.37/42.31 bnd_c_tptp_member2356_mt = i2 % 69.37/42.31 bnd_c_tptp_member235_mt = i2 % 69.37/42.31 bnd_c_tptp_member237_mt = i2 % 69.37/42.31 bnd_c_tptp_member2610_mt = i2 % 69.37/42.31 bnd_c_tptp_member2668_mt = i2 % 69.37/42.31 bnd_c_tptp_member2701_mt = i2 % 69.37/42.31 bnd_c_tptp_member2831_mt = i2 % 69.37/42.31 bnd_c_tptp_member2862_mt = i2 % 69.37/42.31 bnd_c_tptp_member3205_mt = i2 % 69.37/42.31 bnd_c_tptp_member3356_mt = i1 % 69.37/42.31 bnd_c_tptp_member3393_mt = i2 % 69.37/42.31 bnd_c_tptp_member3515_mt = i2 % 69.37/42.31 bnd_c_tptp_member3633_mt = i2 % 69.37/42.31 bnd_c_tptp_member3717_mt = i2 % 69.37/42.31 bnd_c_tptp_member3993_mt = i2 % 69.37/42.31 bnd_c_tptp_member698_mt = i2 % 69.37/42.31 bnd_c_tptp_member974_mt = i2 % 69.37/42.31 bnd_c_tptp_spindlecollectormt = i2 % 69.37/42.31 bnd_c_tptp_spindleheadmt = i5 % 69.37/42.31 bnd_c_tptpartsupplies = i5 % 69.37/42.31 bnd_c_tptpcol_0_0 = i4 % 69.37/42.31 bnd_c_tptpcol_10_109061 = i4 % 69.37/42.31 bnd_c_tptpcol_10_118020 = i1 % 69.37/42.31 bnd_c_tptpcol_10_18567 = i1 % 69.37/42.31 bnd_c_tptpcol_10_22022 = i1 % 69.37/42.31 bnd_c_tptpcol_10_26886 = i1 % 69.37/42.31 bnd_c_tptpcol_10_40324 = i3 % 69.37/42.31 bnd_c_tptpcol_10_72710 = i4 % 69.37/42.31 bnd_c_tptpcol_10_92166 = i4 % 69.37/42.31 bnd_c_tptpcol_10_93700 = i4 % 69.37/42.31 bnd_c_tptpcol_11_109125 = i4 % 69.37/42.31 bnd_c_tptpcol_11_118084 = i1 % 69.37/42.31 bnd_c_tptpcol_11_18631 = i1 % 69.37/42.31 bnd_c_tptpcol_11_22023 = i1 % 69.37/42.31 bnd_c_tptpcol_11_26887 = i1 % 69.37/42.31 bnd_c_tptpcol_11_40388 = i3 % 69.37/42.31 bnd_c_tptpcol_11_72774 = i4 % 69.37/42.31 bnd_c_tptpcol_11_92230 = i4 % 69.37/42.31 bnd_c_tptpcol_11_93764 = i4 % 69.37/42.31 bnd_c_tptpcol_12_109157 = i4 % 69.37/42.31 bnd_c_tptpcol_12_118116 = i1 % 69.37/42.31 bnd_c_tptpcol_12_18663 = i1 % 69.37/42.31 bnd_c_tptpcol_12_22055 = i1 % 69.37/42.31 bnd_c_tptpcol_12_26919 = i1 % 69.37/42.31 bnd_c_tptpcol_12_40420 = i3 % 69.37/42.31 bnd_c_tptpcol_12_72775 = i4 % 69.37/42.31 bnd_c_tptpcol_12_92262 = i4 % 69.37/42.31 bnd_c_tptpcol_12_93765 = i4 % 69.37/42.31 bnd_c_tptpcol_13_109173 = i4 % 69.37/42.31 bnd_c_tptpcol_13_118117 = i1 % 69.37/42.31 bnd_c_tptpcol_13_18664 = i1 % 69.37/42.31 bnd_c_tptpcol_13_22071 = i1 % 69.37/42.31 bnd_c_tptpcol_13_26920 = i1 % 69.37/42.31 bnd_c_tptpcol_13_40421 = i3 % 69.37/42.31 bnd_c_tptpcol_13_72791 = i4 % 69.37/42.31 bnd_c_tptpcol_13_92263 = i4 % 69.37/42.31 bnd_c_tptpcol_13_93766 = i4 % 69.37/42.31 bnd_c_tptpcol_14_109181 = i4 % 69.37/42.31 bnd_c_tptpcol_14_118118 = i1 % 69.37/42.31 bnd_c_tptpcol_14_22072 = i1 % 69.37/42.31 bnd_c_tptpcol_14_26921 = i1 % 69.37/42.31 bnd_c_tptpcol_14_40429 = i3 % 69.37/42.31 bnd_c_tptpcol_14_72792 = i4 % 69.37/42.31 bnd_c_tptpcol_14_92264 = i4 % 69.37/42.31 bnd_c_tptpcol_14_93774 = i4 % 69.37/42.31 bnd_c_tptpcol_15_109185 = i4 % 69.37/42.31 bnd_c_tptpcol_15_130923 = i1 % 69.37/42.31 bnd_c_tptpcol_15_130931 = i1 % 69.37/42.31 bnd_c_tptpcol_15_22076 = i1 % 69.37/42.31 bnd_c_tptpcol_15_26925 = i1 % 69.37/42.31 bnd_c_tptpcol_15_30970 = i1 % 69.37/42.31 bnd_c_tptpcol_15_4027 = i1 % 69.37/42.31 bnd_c_tptpcol_15_40430 = i4 % 69.37/42.31 bnd_c_tptpcol_15_50957 = i1 % 69.37/42.31 bnd_c_tptpcol_15_72793 = i4 % 69.37/42.31 bnd_c_tptpcol_15_92268 = i4 % 69.37/42.31 bnd_c_tptpcol_15_93775 = i4 % 69.37/42.31 bnd_c_tptpcol_16_10258 = i1 % 69.37/42.31 bnd_c_tptpcol_16_130924 = i1 % 69.37/42.31 bnd_c_tptpcol_16_130933 = i1 % 69.37/42.31 bnd_c_tptpcol_16_25972 = i1 % 69.37/42.31 bnd_c_tptpcol_16_26926 = i1 % 69.37/42.31 bnd_c_tptpcol_16_26939 = i1 % 69.37/42.31 bnd_c_tptpcol_16_27189 = i1 % 69.37/42.31 bnd_c_tptpcol_16_29490 = i1 % 69.37/42.31 bnd_c_tptpcol_16_30972 = i1 % 69.37/42.31 bnd_c_tptpcol_16_31868 = i1 % 69.37/42.31 bnd_c_tptpcol_16_4451 = i1 % 69.37/42.31 bnd_c_tptpcol_16_50958 = i1 % 69.37/42.31 bnd_c_tptpcol_16_62187 = i1 % 69.37/42.31 bnd_c_tptpcol_16_72795 = i4 % 69.37/42.31 bnd_c_tptpcol_16_7738 = i1 % 69.37/42.31 bnd_c_tptpcol_16_8886 = i1 % 69.37/42.31 bnd_c_tptpcol_16_92269 = i4 % 69.37/42.31 bnd_c_tptpcol_1_1 = i1 % 69.37/42.31 bnd_c_tptpcol_1_65536 = i4 % 69.37/42.31 bnd_c_tptpcol_2_2 = i1 % 69.37/42.31 bnd_c_tptpcol_2_65537 = i4 % 69.37/42.31 bnd_c_tptpcol_2_98304 = i4 % 69.37/42.31 bnd_c_tptpcol_3_114688 = i1 % 69.37/42.31 bnd_c_tptpcol_3_16386 = i1 % 69.37/42.31 bnd_c_tptpcol_3_65538 = i4 % 69.37/42.31 bnd_c_tptpcol_3_81921 = i4 % 69.37/42.31 bnd_c_tptpcol_3_98305 = i4 % 69.37/42.31 bnd_c_tptpcol_4_106497 = i4 % 69.37/42.31 bnd_c_tptpcol_4_114689 = i1 % 69.37/42.31 bnd_c_tptpcol_4_16387 = i1 % 69.37/42.31 bnd_c_tptpcol_4_24578 = i1 % 69.37/42.31 bnd_c_tptpcol_4_65539 = i4 % 69.37/42.31 bnd_c_tptpcol_4_90113 = i4 % 69.37/42.31 bnd_c_tptpcol_5_106498 = i4 % 69.37/42.31 bnd_c_tptpcol_5_110593 = i4 % 69.37/42.31 bnd_c_tptpcol_5_114690 = i1 % 69.37/42.31 bnd_c_tptpcol_5_16388 = i1 % 69.37/42.31 bnd_c_tptpcol_5_20483 = i1 % 69.37/42.31 bnd_c_tptpcol_5_24579 = i1 % 69.37/42.31 bnd_c_tptpcol_5_69635 = i4 % 69.37/42.31 bnd_c_tptpcol_5_90114 = i4 % 69.37/42.31 bnd_c_tptpcol_6_108546 = i4 % 69.37/42.31 bnd_c_tptpcol_6_112641 = i4 % 69.37/42.31 bnd_c_tptpcol_6_116738 = i1 % 69.37/42.31 bnd_c_tptpcol_6_18436 = i1 % 69.37/42.31 bnd_c_tptpcol_6_20484 = i1 % 69.37/42.31 bnd_c_tptpcol_6_26627 = i1 % 69.37/42.31 bnd_c_tptpcol_6_71683 = i4 % 69.37/42.31 bnd_c_tptpcol_6_92162 = i4 % 69.37/42.31 bnd_c_tptpcol_7_108547 = i4 % 69.37/42.31 bnd_c_tptpcol_7_113665 = i4 % 69.37/42.31 bnd_c_tptpcol_7_117762 = i1 % 69.37/42.31 bnd_c_tptpcol_7_18437 = i1 % 69.37/42.31 bnd_c_tptpcol_7_21508 = i1 % 69.37/42.31 bnd_c_tptpcol_7_26628 = i1 % 69.37/42.31 bnd_c_tptpcol_7_39939 = i3 % 69.37/42.31 bnd_c_tptpcol_7_72707 = i4 % 69.37/42.31 bnd_c_tptpcol_7_92163 = i4 % 69.37/42.31 bnd_c_tptpcol_7_93186 = i4 % 69.37/42.31 bnd_c_tptpcol_8_109059 = i4 % 69.37/42.31 bnd_c_tptpcol_8_114177 = i4 % 69.37/42.31 bnd_c_tptpcol_8_117763 = i1 % 69.37/42.31 bnd_c_tptpcol_8_18438 = i1 % 69.37/42.31 bnd_c_tptpcol_8_22020 = i1 % 69.37/42.31 bnd_c_tptpcol_8_26629 = i1 % 69.37/42.31 bnd_c_tptpcol_8_39940 = i3 % 69.37/42.31 bnd_c_tptpcol_8_72708 = i4 % 69.37/42.31 bnd_c_tptpcol_8_92164 = i4 % 69.37/42.31 bnd_c_tptpcol_8_93698 = i4 % 69.37/42.31 bnd_c_tptpcol_9_109060 = i4 % 69.37/42.31 bnd_c_tptpcol_9_118019 = i1 % 69.37/42.31 bnd_c_tptpcol_9_18439 = i1 % 69.37/42.31 bnd_c_tptpcol_9_22021 = i1 % 69.37/42.31 bnd_c_tptpcol_9_26885 = i1 % 69.37/42.31 bnd_c_tptpcol_9_40196 = i3 % 69.37/42.31 bnd_c_tptpcol_9_72709 = i4 % 69.37/42.31 bnd_c_tptpcol_9_92165 = i4 % 69.37/42.31 bnd_c_tptpcol_9_93699 = i4 % 69.37/42.31 bnd_c_tptpexecutionbyfiringsquad_90 = i1 % 69.37/42.31 bnd_c_tptpgeo_member1_mt = i2 % 69.37/42.31 bnd_c_tptpgeo_member2_mt = i2 % 69.37/42.31 bnd_c_tptpgeo_member3_mt = i5 % 69.37/42.31 bnd_c_tptpgeo_member4_mt = i1 % 69.37/42.31 bnd_c_tptpgeo_member5_mt = i2 % 69.37/42.31 bnd_c_tptpgeo_member7_mt = i2 % 69.37/42.31 bnd_c_tptpgeo_member8_mt = i2 % 69.37/42.31 bnd_c_tptpgeo_spindlecollectormt = i2 % 69.37/42.31 bnd_c_tptpgeo_spindleheadmt = i2 % 69.37/42.31 bnd_c_tptpmarriagelicensedocument = i5 % 69.37/42.31 bnd_c_tptpnavypersonnel_3 = i5 % 69.37/42.31 bnd_c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 69.37/42.31 = i1 % 69.37/42.31 bnd_c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 % 69.37/42.31 = i2 % 69.37/42.31 bnd_c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 % 69.37/42.31 = i2 % 69.37/42.31 bnd_c_tptpofobject = i5 % 69.37/42.31 bnd_c_tptpquantityfn_1 = i5 % 69.37/42.31 bnd_c_tptpquantityfn_13 = i5 % 69.37/42.31 bnd_c_tptpquantityfn_14 = i5 % 69.37/42.31 bnd_c_tptpquantityfn_2 = i5 % 69.37/42.31 bnd_c_tptpquantityfn_21 = i5 % 69.37/42.31 bnd_c_tptpquantityfn_6 = i5 % 69.37/42.31 bnd_c_tptpridgeline_topographical = i5 % 69.37/42.31 bnd_c_tptprunningshorts = i5 % 69.37/42.31 bnd_c_tptptptpcol_16_25985 = i5 % 69.37/42.31 bnd_c_tptptptpcol_16_8398 = i5 % 69.37/42.31 bnd_c_tptptypes_5_387 = i1 % 69.37/42.31 bnd_c_tptptypes_5_802 = i5 % 69.37/42.31 bnd_c_tptptypes_6_388 = i1 % 69.37/42.31 bnd_c_tptptypes_6_818 = i5 % 69.37/42.31 bnd_c_tptptypes_7_389 = i1 % 69.37/42.31 bnd_c_tptptypes_7_396 = i1 % 69.37/42.31 bnd_c_tptptypes_7_691 = i1 % 69.37/42.31 bnd_c_tptptypes_7_819 = i5 % 69.37/42.31 bnd_c_tptptypes_8_390 = i1 % 69.37/42.31 bnd_c_tptptypes_8_400 = i1 % 69.37/42.31 bnd_c_tptptypes_8_692 = i1 % 69.37/42.31 bnd_c_tptptypes_8_823 = i5 % 69.37/42.31 bnd_c_tptptypes_9_401 = i1 % 69.37/42.31 bnd_c_tptptypes_9_693 = i1 % 69.37/42.31 bnd_c_tptptypes_9_824 = i5 % 69.37/42.31 bnd_c_trajector_underspecified = i4 % 69.37/42.31 bnd_c_transitivebinarypredicate = i1 % 69.37/42.31 bnd_c_translation_0_885 = i1 % 69.37/42.31 bnd_c_translation_14 = i1 % 69.37/42.31 bnd_c_translation_21 = i1 % 69.37/42.31 bnd_c_translation_3 = i2 % 69.37/42.31 bnd_c_translation_32 = i1 % 69.37/42.31 bnd_c_translation_33 = i1 % 69.37/42.31 bnd_c_translation_7 = i1 % 69.37/42.31 bnd_c_unitedstatesgeographydualistmt = i2 % 69.37/42.31 bnd_c_unitedstatesgeographypeoplemt = i2 % 69.37/42.31 bnd_c_unitedstatessociallifemt = i2 % 69.37/42.31 bnd_c_unitvectorinterval = i1 % 69.37/42.31 bnd_c_universalvocabularymt = i5 % 69.37/42.31 bnd_c_urlfn = i5 % 69.37/42.31 bnd_c_urlreferentfn = i5 % 69.37/42.31 bnd_c_wamt_evalinitial_p14 = i5 % 69.37/42.31 bnd_c_wanica_districtsuriname = i1 % 69.37/42.31 bnd_c_worldcompletedualistgeographymt = i2 % 69.37/42.31 bnd_c_worldgeographydualistmt = i2 % 69.37/42.31 bnd_c_worldgeographymt = i2 % 69.37/42.31 bnd_c_xskijump_thegame = i5 % 69.37/42.31 bnd_city = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_collection = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.37/42.31 bnd_computerdataartifact = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_controlcharacterfreestring = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.37/42.31 bnd_correctivelensprescription = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.37/42.31 bnd_creationordestructionevent = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.37/42.31 bnd_directionoftranslation_throughout = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.37/42.31 bnd_disjointwith = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.37/42.31 bnd_enduringthing_localized = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.37/42.31 bnd_executionbyfiringsquad = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.37/42.31 bnd_f_citynamedfn = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i5), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i5), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i5), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i5)) % 69.37/42.31 bnd_f_contentmtofcdafromeventfn = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)) % 69.37/42.31 bnd_f_contextofpcwfn = % 69.37/42.31 (\<lambda>x. _)(i1 := i2, i2 := i2, i3 := i5, i4 := i5, i5 := i5) % 69.37/42.31 bnd_f_instancewithrelationtofn = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2))) % 69.37/42.31 bnd_f_relationallexistsfn = % 69.37/42.31 (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i1, i2 := i2, i3 := i3, i4 := i2, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i4, i3 := i3, i4 := i2, i5 := i2), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i2, i3 := i4, i4 := i3, i5 := i3), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i4, i5 := i3), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i4)), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i4, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i4, i3 := i2, i4 := i3, i5 := i3), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i2, i5 := i3), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i4, i5 := i2), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i4)), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i4, i2 := i3, i3 := i2, i4 := i2, i5 := i3), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i4, i3 := i3, i4 := i3, i5 := i3), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i4, i5 := i3), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i4, i2 := i3, i3 := i3, i4 := i3, i5 := i2), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i4, i5 := i3), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i4)), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i4, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i3, i5 := i3), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i4, i5 := i3), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i4))), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i4, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i4, i3 := i3, i4 := i3, i5 := i3), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i2, i3 := i4, i4 := i3, i5 := i3), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i4, i5 := i3), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i2)), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.37/42.31 i2 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i2, i5 := i3), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i2), % 69.37/42.31 i4 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i4, i5 := i3), % 69.37/42.31 i5 := (\<lambda>x. _) % 69.37/42.31 (i1 := i2, i2 := i3, i3 := i2, i4 := i3, i5 := i4)), % 69.37/42.31 i3 := (\<lambda>x. _) % 69.37/42.31 (i1 := (\<lambda>x. _) % 69.37/42.31 (i1 := i4, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i4, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i4)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i4, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i4)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i4, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i4))), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i1, i2 := i2, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i4, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i4, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i4)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i4, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i4, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i4)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i4, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i4, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i4)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i4, i2 := i2, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i4, i3 := i3, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i4)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i4, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i2, i4 := i4, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i2))), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i1, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i3)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i2, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i3)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i3, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i2)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i2, i5 := i3)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i3, i5 := i3))), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i2, i4 := i3, i5 := i3)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i2, i4 := i2, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i3)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i3, i5 := i3)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i3, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i2, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i2)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i3, i5 := i3), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i3, i3 := i2, i4 := i2, i5 := i3), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i3, i2 := i2, i3 := i3, i4 := i3, i5 := i3)))) % 69.48/42.31 bnd_f_relationexistsallfn = % 69.48/42.31 (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i1, i2 := i2, i3 := i1, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2))), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i1, i4 := i1, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i5))), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i1, i2 := i2, i3 := i1, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i5, i5 := i2)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i5))), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i1, i2 := i2, i3 := i1, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i1, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i5), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i5)), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i5, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i5), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2))), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i1, i4 := i1, i5 := i2), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i3 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i4 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.31 i5 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.31 i2 := (\<lambda>x. _) % 69.48/42.31 (i1 := (\<lambda>x. _) % 69.48/42.31 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i5)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i2), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i5, i5 := i2), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i5, i3 := i2, i4 := i2, i5 := i2), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i2, i2 := i2, i3 := i5, i4 := i2, i5 := i5)))) % 69.48/42.32 bnd_f_subcollectionofwithrelationfromtypefn = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i4, i4 := i4, i5 := i4)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1))) % 69.48/42.32 bnd_f_subcollectionofwithrelationtofn = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i4, i4 := i3, i5 := i3)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i3, i5 := i4)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i3, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i3, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i3, i3 := i4, i4 := i3, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i3, i3 := i3, i4 := i3, i5 := i3), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i3, i3 := i4, i4 := i3, i5 := i3)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i4, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i1, i4 := i4, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i4, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i1, i4 := i1, i5 := i1)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i1, i3 := i4, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i1, i3 := i1, i4 := i1, i5 := i4), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1))) % 69.48/42.32 bnd_f_subcollectionofwithrelationtotypefn = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i3, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i3, i2 := i4, i3 := i1, i4 := i3, i5 := i4)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i3, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i4), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i4, i3 := i4, i4 := i4, i5 := i1)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i1, i3 := i1, i4 := i1, i5 := i4), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i1, i3 := i1, i4 := i1, i5 := i4), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i4, i5 := i1)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i4, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i4, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i4), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i4, i5 := i1)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i1), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i1, i5 := i4), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i1, i4 := i4, i5 := i1), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i1, i3 := i4, i4 := i1, i5 := i1), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := i1, i2 := i4, i3 := i1, i4 := i1, i5 := i1))) % 69.48/42.32 bnd_f_tptpquantityfn_1 = % 69.48/42.32 (\<lambda>x. _)(i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i1) % 69.48/42.32 bnd_f_tptpquantityfn_13 = % 69.48/42.32 (\<lambda>x. _)(i1 := i5, i2 := i5, i3 := i5, i4 := i5, i5 := i1) % 69.48/42.32 bnd_f_tptpquantityfn_14 = % 69.48/42.32 (\<lambda>x. _)(i1 := i1, i2 := i5, i3 := i5, i4 := i5, i5 := i5) % 69.48/42.32 bnd_f_tptpquantityfn_2 = % 69.48/42.32 (\<lambda>x. _)(i1 := i5, i2 := i5, i3 := i5, i4 := i1, i5 := i5) % 69.48/42.32 bnd_f_tptpquantityfn_21 = % 69.48/42.32 (\<lambda>x. _)(i1 := i5, i2 := i5, i3 := i5, i4 := i1, i5 := i5) % 69.48/42.32 bnd_f_tptpquantityfn_6 = % 69.48/42.32 (\<lambda>x. _)(i1 := i1, i2 := i5, i3 := i5, i4 := i5, i5 := i5) % 69.48/42.32 bnd_f_urlfn = % 69.48/42.32 (\<lambda>x. _)(i1 := i5, i2 := i3, i3 := i1, i4 := i3, i5 := i3) % 69.48/42.32 bnd_f_urlreferentfn = % 69.48/42.32 (\<lambda>x. _)(i1 := i2, i2 := i2, i3 := i2, i4 := i2, i5 := i2) % 69.48/42.32 bnd_few = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_firstordercollection = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_fixedordercollection = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_footballteam = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_function_denotational = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := True) % 69.48/42.32 bnd_furpelt = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_genlinverse = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_genlmt = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True)) % 69.48/42.32 bnd_genlpreds = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)) % 69.48/42.32 bnd_genls = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_geographicallysubsumes = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_geographicalregion = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_geographicalsubregions = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := True)) % 69.48/42.32 bnd_geolevel_1 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_geolevel_3 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_geolevel_4 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_geopoliticalsubdivision = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_hasmembers = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_hpkb_subnationalagent = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_inanimateobject = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_inanimateobject_nonnatural = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_individual = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_inregion = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)) % 69.48/42.32 bnd_intangible = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_intangibleindividual = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_isa = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False)) % 69.48/42.32 bnd_issuingaprescription = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_location_underspecified = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_marriagelicensedocument = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_mathematicalorcomputationalthing = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_mathematicalthing = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_microtheory = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_militaryperson = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_most = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_movement_translationevent = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_mtvisible = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_n_1 = i5 % 69.48/42.32 bnd_n_170 = i4 % 69.48/42.32 bnd_n_2 = i5 % 69.48/42.32 bnd_n_232 = i1 % 69.48/42.32 bnd_n_3 = i4 % 69.48/42.32 bnd_n_328 = i5 % 69.48/42.32 bnd_n_4 = i5 % 69.48/42.32 bnd_n_414 = i1 % 69.48/42.32 bnd_n_468 = i5 % 69.48/42.32 bnd_n_756 = i4 % 69.48/42.32 bnd_natargument = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True))) % 69.48/42.32 bnd_natfunction = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := True)) % 69.48/42.32 bnd_navypersonnel = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_no = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_objectfoundinlocation = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_orderingpredicate = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_organization = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_orientation = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_orientationvector = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_partiallyintangibleindividual = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_partiallytangible = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_physicalorderingpredicate = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_positiveinteger = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := True) % 69.48/42.32 bnd_predicate = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_prettystring = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True)) % 69.48/42.32 bnd_products = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_pushingababycarriage = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_pushingwithfingers = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_pushingwithopenhand = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_razor = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_reflexivebinarypredicate = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_relation = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_relationallexists = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False))) % 69.48/42.32 bnd_relationallinstance = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := False, i5 := True), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False))) % 69.48/42.32 bnd_relationexistsall = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False)), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, % 69.48/42.32 i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, % 69.48/42.32 i5 := False))) % 69.48/42.32 bnd_resultisaarg = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := True)) % 69.48/42.32 bnd_ridgeline_topographical = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_runningshorts = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_s_agen = i1 % 69.48/42.32 bnd_s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf = i5 % 69.48/42.32 bnd_s_http_memberstripodcomindygalfordtriviahtm = i3 % 69.48/42.32 bnd_s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml % 69.48/42.32 = i2 % 69.48/42.32 bnd_s_http_webnjiteducjohnsontreebiochhtm = i3 % 69.48/42.32 bnd_s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml = i3 % 69.48/42.32 bnd_s_http_wwwarthritis_symptomcoma_cbursitishtm = i3 % 69.48/42.32 bnd_s_http_wwwfuntriviacomplayquizcfmqid60926origin = i3 % 69.48/42.32 bnd_s_http_wwwinformationblastcomtechnical_university_of_munichhtml = i5 % 69.48/42.32 bnd_s_http_wwwpoweripodsearchinfobrown_ipodhtml = i3 % 69.48/42.32 bnd_s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988 = i3 % 69.48/42.32 bnd_s_http_wwwthedailybulletincompostcardsmar9chtm = i3 % 69.48/42.32 bnd_s_terroristthathasbeenamemberofaterroristorganization = i5 % 69.48/42.32 bnd_s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege = i5 % 69.48/42.32 bnd_s_tlh = i1 % 69.48/42.32 bnd_setorcollection = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_shavingrazor_manual = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_ship = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_spatialthing_localized = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_spatialthing_nonsituational = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_state_geopolitical = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_stringoflengthfn3 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible % 69.48/42.32 = (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup % 69.48/42.32 = (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent % 69.48/42.32 = (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma % 69.48/42.32 = (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription % 69.48/42.32 = (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_subevents = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_subregions = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_subsetof = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := True, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_supplies = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_terrorist = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_terroristgroup = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_thing = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptp_8_271 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptp_8_875 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptp_8_968 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptp_9_51 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptp_9_720 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptpcol_0_0 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_10_109061 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_10_118020 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_10_18567 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_10_22022 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_10_26886 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_10_40324 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_10_72710 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_10_92166 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_10_93700 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_11_109125 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_11_118084 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_11_18631 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_11_22023 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_11_26887 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_11_40388 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_11_72774 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_11_92230 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_11_93764 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_12_109157 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_12_118116 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_12_18663 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_12_22055 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_12_26919 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_12_40420 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_12_72775 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_12_92262 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_12_93765 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_13_109173 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_13_118117 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_13_18664 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_13_22071 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_13_26920 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_13_40421 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_13_72791 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_13_92263 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_13_93766 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_14_109181 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_14_118118 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_14_22072 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_14_26921 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_14_40429 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_14_72792 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_14_92264 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_14_93774 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_15_109185 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_15_130923 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_130931 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_22076 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_26925 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_30970 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_4027 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_40430 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_15_50957 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_15_72793 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_15_92268 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_15_93775 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_16_10258 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_130924 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_130933 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_25972 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_26926 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_26939 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_27189 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_29490 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_30972 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_31868 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_4451 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_50958 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_62187 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_72795 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_16_7738 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_8886 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_16_92269 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_1_1 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_1_65536 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_2_2 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_2_65537 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_2_98304 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_3_114688 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_3_16386 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_3_65538 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_3_81921 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_3_98305 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_4_106497 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_4_114689 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_4_16387 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_4_24578 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_4_65539 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_4_90113 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_5_106498 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_5_110593 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_5_114690 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_5_16388 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_5_20483 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_5_24579 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_5_28674 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_tptpcol_5_69635 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_5_90114 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_6_108546 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_6_112641 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_6_116738 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_6_18436 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_6_20484 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_6_26627 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_6_71683 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_6_92162 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_7_108547 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_7_113665 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_7_117762 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_7_18437 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_7_21508 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_7_26628 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_7_39939 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_7_7172 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False) % 69.48/42.32 bnd_tptpcol_7_72707 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_7_92163 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_7_93186 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_8_109059 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_8_114177 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_8_117763 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_8_18438 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_8_22020 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_8_26629 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_8_39940 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_8_72708 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_8_92164 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_8_93698 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_9_109060 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_9_118019 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_9_18439 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_9_22021 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_9_26885 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_tptpcol_9_40196 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := True) % 69.48/42.32 bnd_tptpcol_9_72709 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_9_92165 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpcol_9_93699 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptpofobject = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptpquantity = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_tptptypes_5_387 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_5_802 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_6_388 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_6_818 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_7_389 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_7_396 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_7_691 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := True, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_7_819 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_8_390 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_8_400 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_8_692 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_8_823 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_9_401 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_9_693 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_tptptypes_9_824 = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i2 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i3 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i4 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False), % 69.48/42.32 i5 := (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False)) % 69.48/42.32 bnd_trajector_underspecified = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := False, i2 := True, i3 := False, i4 := False, i5 := True) % 69.48/42.32 bnd_transitivebinarypredicate = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 bnd_uniformresourcelocator = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := False, i5 := True) % 69.48/42.32 bnd_unitvectorinterval = % 69.48/42.32 (\<lambda>x. _) % 69.48/42.32 (i1 := True, i2 := False, i3 := True, i4 := True, i5 := False) % 69.48/42.32 % SZS output end FiniteModel % 69.48/42.32 Total time: 32.0 s %------------------------------------------------------------------------------