%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : SYO581+1 : TPTP v9.0.0. Released v5.5.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Sat Jun 21 05:41:55 AM UTC 2025 % Result : CounterSatisfiable 2.28s 2.47s % Output : Model 2.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYO581+1 : TPTP v9.0.0. Released v5.5.0. % 0.07/0.13 % Command : run_E %s %d THM % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 20 13:11:48 EDT 2025 % 0.12/0.35 % CPUTime : % 2.28/2.47 % SZS status CounterSatisfiable % 2.28/2.47 % SZS output start Model % 2.28/2.47 tff(tptp_fun__i_val_12_type, type, ( % 2.28/2.47 tptp_fun__i_val_12: $i)). % 2.28/2.47 tff(k!513_type, type, ( % 2.28/2.47 k!513: $i > $i)). % 2.28/2.47 tff(tptp_fun__i_val_48_type, type, ( % 2.28/2.47 tptp_fun__i_val_48: $i)). % 2.28/2.47 tff(k04_buttercup10464_type, type, ( % 2.28/2.47 k04_buttercup10464: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_63_type, type, ( % 2.28/2.47 tptp_fun__i_val_63: $i)). % 2.28/2.47 tff(b48_buttercup10440_type, type, ( % 2.28/2.47 b48_buttercup10440: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_366_type, type, ( % 2.28/2.47 tptp_fun__i_val_366: $i)). % 2.28/2.47 tff(b48_buttercup10320_type, type, ( % 2.28/2.47 b48_buttercup10320: $i > $o)). % 2.28/2.47 tff(k04_buttercup10535_type, type, ( % 2.28/2.47 k04_buttercup10535: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_270_type, type, ( % 2.28/2.47 tptp_fun__i_val_270: $i)). % 2.28/2.47 tff(tptp_fun__i_val_148_type, type, ( % 2.28/2.47 tptp_fun__i_val_148: $i)). % 2.28/2.47 tff(b48_buttercup10421_type, type, ( % 2.28/2.47 b48_buttercup10421: $i > $o)). % 2.28/2.47 tff(k04_buttercup10559_type, type, ( % 2.28/2.47 k04_buttercup10559: $i > $o)). % 2.28/2.47 tff(b48_buttercup10365_type, type, ( % 2.28/2.47 b48_buttercup10365: $i > $o)). % 2.28/2.47 tff(b48_buttercup10513_type, type, ( % 2.28/2.47 b48_buttercup10513: $i > $o)). % 2.28/2.47 tff(b48_buttercup10318_type, type, ( % 2.28/2.47 b48_buttercup10318: $i > $o)). % 2.28/2.47 tff(b48_buttercup10269_type, type, ( % 2.28/2.47 b48_buttercup10269: $i > $o)). % 2.28/2.47 tff(b48_buttercup10332_type, type, ( % 2.28/2.47 b48_buttercup10332: $i > $o)). % 2.28/2.47 tff(b48_buttercup10427_type, type, ( % 2.28/2.47 b48_buttercup10427: $i > $o)). % 2.28/2.47 tff(b48_buttercup10231_type, type, ( % 2.28/2.47 b48_buttercup10231: $i > $o)). % 2.28/2.47 tff(b48_buttercup10604_type, type, ( % 2.28/2.47 b48_buttercup10604: $i > $o)). % 2.28/2.47 tff(k04_buttercup10425_type, type, ( % 2.28/2.47 k04_buttercup10425: $i > $o)). % 2.28/2.47 tff(b48_buttercup10531_type, type, ( % 2.28/2.47 b48_buttercup10531: $i > $o)). % 2.28/2.47 tff(k04_buttercup10473_type, type, ( % 2.28/2.47 k04_buttercup10473: $i > $o)). % 2.28/2.47 tff(k04_buttercup10482_type, type, ( % 2.28/2.47 k04_buttercup10482: $i > $o)). % 2.28/2.47 tff(b48_buttercup10247_type, type, ( % 2.28/2.47 b48_buttercup10247: $i > $o)). % 2.28/2.47 tff(b48_buttercup10514_type, type, ( % 2.28/2.47 b48_buttercup10514: $i > $o)). % 2.28/2.47 tff(b48_buttercup10271_type, type, ( % 2.28/2.47 b48_buttercup10271: $i > $o)). % 2.28/2.47 tff(b48_buttercup10326_type, type, ( % 2.28/2.47 b48_buttercup10326: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_83_type, type, ( % 2.28/2.47 tptp_fun__i_val_83: $i)). % 2.28/2.47 tff(tptp_fun__i_val_94_type, type, ( % 2.28/2.47 tptp_fun__i_val_94: $i)). % 2.28/2.47 tff(k04_buttercup10225_type, type, ( % 2.28/2.47 k04_buttercup10225: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_70_type, type, ( % 2.28/2.47 tptp_fun__i_val_70: $i)). % 2.28/2.47 tff(b48_buttercup10029_type, type, ( % 2.28/2.47 b48_buttercup10029: $i > $o)). % 2.28/2.47 tff(b48_buttercup10490_type, type, ( % 2.28/2.47 b48_buttercup10490: $i > $o)). % 2.28/2.47 tff(k04_buttercup10084_type, type, ( % 2.28/2.47 k04_buttercup10084: $i > $o)). % 2.28/2.47 tff(k04_buttercup10371_type, type, ( % 2.28/2.47 k04_buttercup10371: $i > $o)). % 2.28/2.47 tff(k04_buttercup10064_type, type, ( % 2.28/2.47 k04_buttercup10064: $i > $o)). % 2.28/2.47 tff(k04_buttercup10424_type, type, ( % 2.28/2.47 k04_buttercup10424: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_248_type, type, ( % 2.28/2.47 tptp_fun__i_val_248: $i)). % 2.28/2.47 tff(b48_buttercup10167_type, type, ( % 2.28/2.47 b48_buttercup10167: $i > $o)). % 2.28/2.47 tff(b48_buttercup10279_type, type, ( % 2.28/2.47 b48_buttercup10279: $i > $o)). % 2.28/2.47 tff(k04_buttercup10631_type, type, ( % 2.28/2.47 k04_buttercup10631: $i > $o)). % 2.28/2.47 tff(k04_buttercup10586_type, type, ( % 2.28/2.47 k04_buttercup10586: $i > $o)). % 2.28/2.47 tff(k04_buttercup10244_type, type, ( % 2.28/2.47 k04_buttercup10244: $i > $o)). % 2.28/2.47 tff(b48_buttercup10460_type, type, ( % 2.28/2.47 b48_buttercup10460: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_314_type, type, ( % 2.28/2.47 tptp_fun__i_val_314: $i)). % 2.28/2.47 tff(tptp_fun__i_val_150_type, type, ( % 2.28/2.47 tptp_fun__i_val_150: $i)). % 2.28/2.47 tff(k04_buttercup10462_type, type, ( % 2.28/2.47 k04_buttercup10462: $i > $o)). % 2.28/2.47 tff(k04_buttercup10061_type, type, ( % 2.28/2.47 k04_buttercup10061: $i > $o)). % 2.28/2.47 tff(k04_buttercup10351_type, type, ( % 2.28/2.47 k04_buttercup10351: $i > $o)). % 2.28/2.47 tff(b48_buttercup10076_type, type, ( % 2.28/2.47 b48_buttercup10076: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_361_type, type, ( % 2.28/2.47 tptp_fun__i_val_361: $i)). % 2.28/2.47 tff(b48_buttercup10487_type, type, ( % 2.28/2.47 b48_buttercup10487: $i > $o)). % 2.28/2.47 tff(k04_buttercup10470_type, type, ( % 2.28/2.47 k04_buttercup10470: $i > $o)). % 2.28/2.47 tff(b48_buttercup10143_type, type, ( % 2.28/2.47 b48_buttercup10143: $i > $o)). % 2.28/2.47 tff(b48_buttercup10186_type, type, ( % 2.28/2.47 b48_buttercup10186: $i > $o)). % 2.28/2.47 tff(b48_buttercup10121_type, type, ( % 2.28/2.47 b48_buttercup10121: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_362_type, type, ( % 2.28/2.47 tptp_fun__i_val_362: $i)). % 2.28/2.47 tff(b48_buttercup10120_type, type, ( % 2.28/2.47 b48_buttercup10120: $i > $o)). % 2.28/2.47 tff(b48_buttercup10267_type, type, ( % 2.28/2.47 b48_buttercup10267: $i > $o)). % 2.28/2.47 tff(b48_buttercup10082_type, type, ( % 2.28/2.47 b48_buttercup10082: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_275_type, type, ( % 2.28/2.47 tptp_fun__i_val_275: $i)). % 2.28/2.47 tff(b48_buttercup10173_type, type, ( % 2.28/2.47 b48_buttercup10173: $i > $o)). % 2.28/2.47 tff(b48_buttercup10161_type, type, ( % 2.28/2.47 b48_buttercup10161: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_335_type, type, ( % 2.28/2.47 tptp_fun__i_val_335: $i)). % 2.28/2.47 tff(b48_buttercup10159_type, type, ( % 2.28/2.47 b48_buttercup10159: $i > $o)). % 2.28/2.47 tff(b48_buttercup10180_type, type, ( % 2.28/2.47 b48_buttercup10180: $i > $o)). % 2.28/2.47 tff(k04_buttercup10437_type, type, ( % 2.28/2.47 k04_buttercup10437: $i > $o)). % 2.28/2.47 tff(k04_buttercup10303_type, type, ( % 2.28/2.47 k04_buttercup10303: $i > $o)). % 2.28/2.47 tff(b48_buttercup10386_type, type, ( % 2.28/2.47 b48_buttercup10386: $i > $o)). % 2.28/2.47 tff(b48_buttercup10050_type, type, ( % 2.28/2.47 b48_buttercup10050: $i > $o)). % 2.28/2.47 tff(b48_buttercup10276_type, type, ( % 2.28/2.47 b48_buttercup10276: $i > $o)). % 2.28/2.47 tff(b48_buttercup10274_type, type, ( % 2.28/2.47 b48_buttercup10274: $i > $o)). % 2.28/2.47 tff(k04_buttercup10400_type, type, ( % 2.28/2.47 k04_buttercup10400: $i > $o)). % 2.28/2.47 tff(b48_buttercup10561_type, type, ( % 2.28/2.47 b48_buttercup10561: $i > $o)). % 2.28/2.47 tff(b48_buttercup10289_type, type, ( % 2.28/2.47 b48_buttercup10289: $i > $o)). % 2.28/2.47 tff(k04_buttercup10602_type, type, ( % 2.28/2.47 k04_buttercup10602: $i > $o)). % 2.28/2.47 tff(b48_buttercup10632_type, type, ( % 2.28/2.47 b48_buttercup10632: $i > $o)). % 2.28/2.47 tff(k04_buttercup10039_type, type, ( % 2.28/2.47 k04_buttercup10039: $i > $o)). % 2.28/2.47 tff(k04_buttercup10051_type, type, ( % 2.28/2.47 k04_buttercup10051: $i > $o)). % 2.28/2.47 tff(b48_buttercup10542_type, type, ( % 2.28/2.47 b48_buttercup10542: $i > $o)). % 2.28/2.47 tff(k04_buttercup10132_type, type, ( % 2.28/2.47 k04_buttercup10132: $i > $o)). % 2.28/2.47 tff(k04_buttercup10391_type, type, ( % 2.28/2.47 k04_buttercup10391: $i > $o)). % 2.28/2.47 tff(k04_buttercup10293_type, type, ( % 2.28/2.47 k04_buttercup10293: $i > $o)). % 2.28/2.47 tff(b48_buttercup10552_type, type, ( % 2.28/2.47 b48_buttercup10552: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_337_type, type, ( % 2.28/2.47 tptp_fun__i_val_337: $i)). % 2.28/2.47 tff(b48_buttercup10398_type, type, ( % 2.28/2.47 b48_buttercup10398: $i > $o)). % 2.28/2.47 tff(b48_buttercup10240_type, type, ( % 2.28/2.47 b48_buttercup10240: $i > $o)). % 2.28/2.47 tff(k04_buttercup10044_type, type, ( % 2.28/2.47 k04_buttercup10044: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_106_type, type, ( % 2.28/2.47 tptp_fun__i_val_106: $i)). % 2.28/2.47 tff(tptp_fun__i_val_253_type, type, ( % 2.28/2.47 tptp_fun__i_val_253: $i)). % 2.28/2.47 tff(b48_buttercup10043_type, type, ( % 2.28/2.47 b48_buttercup10043: $i > $o)). % 2.28/2.47 tff(b48_buttercup10530_type, type, ( % 2.28/2.47 b48_buttercup10530: $i > $o)). % 2.28/2.47 tff(k04_buttercup10637_type, type, ( % 2.28/2.47 k04_buttercup10637: $i > $o)). % 2.28/2.47 tff(k04_buttercup10357_type, type, ( % 2.28/2.47 k04_buttercup10357: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_238_type, type, ( % 2.28/2.47 tptp_fun__i_val_238: $i)). % 2.28/2.47 tff(tptp_fun__i_val_264_type, type, ( % 2.28/2.47 tptp_fun__i_val_264: $i)). % 2.28/2.47 tff(b48_buttercup10361_type, type, ( % 2.28/2.47 b48_buttercup10361: $i > $o)). % 2.28/2.47 tff(b48_buttercup10434_type, type, ( % 2.28/2.47 b48_buttercup10434: $i > $o)). % 2.28/2.47 tff(k04_buttercup10117_type, type, ( % 2.28/2.47 k04_buttercup10117: $i > $o)). % 2.28/2.47 tff(b48_buttercup10045_type, type, ( % 2.28/2.47 b48_buttercup10045: $i > $o)). % 2.28/2.47 tff(k04_buttercup10385_type, type, ( % 2.28/2.47 k04_buttercup10385: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_32_type, type, ( % 2.28/2.47 tptp_fun__i_val_32: $i)). % 2.28/2.47 tff(b48_buttercup10334_type, type, ( % 2.28/2.47 b48_buttercup10334: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_281_type, type, ( % 2.28/2.47 tptp_fun__i_val_281: $i)). % 2.28/2.47 tff(b48_buttercup10478_type, type, ( % 2.28/2.47 b48_buttercup10478: $i > $o)). % 2.28/2.47 tff(b48_buttercup10606_type, type, ( % 2.28/2.47 b48_buttercup10606: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_81_type, type, ( % 2.28/2.47 tptp_fun__i_val_81: $i)). % 2.28/2.47 tff(b48_buttercup10214_type, type, ( % 2.28/2.47 b48_buttercup10214: $i > $o)). % 2.28/2.47 tff(k04_buttercup10181_type, type, ( % 2.28/2.47 k04_buttercup10181: $i > $o)). % 2.28/2.47 tff(b48_buttercup10383_type, type, ( % 2.28/2.47 b48_buttercup10383: $i > $o)). % 2.28/2.47 tff(b48_buttercup10359_type, type, ( % 2.28/2.47 b48_buttercup10359: $i > $o)). % 2.28/2.47 tff(k04_buttercup10125_type, type, ( % 2.28/2.47 k04_buttercup10125: $i > $o)). % 2.28/2.47 tff(b48_buttercup10046_type, type, ( % 2.28/2.47 b48_buttercup10046: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_13_type, type, ( % 2.28/2.47 tptp_fun__i_val_13: $i)). % 2.28/2.47 tff(tptp_fun__i_val_17_type, type, ( % 2.28/2.47 tptp_fun__i_val_17: $i)). % 2.28/2.47 tff(k04_buttercup10026_type, type, ( % 2.28/2.47 k04_buttercup10026: $i > $o)). % 2.28/2.47 tff(k04_buttercup10342_type, type, ( % 2.28/2.47 k04_buttercup10342: $i > $o)). % 2.28/2.47 tff(k04_buttercup10495_type, type, ( % 2.28/2.47 k04_buttercup10495: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_429_type, type, ( % 2.28/2.47 tptp_fun__i_val_429: $i)). % 2.28/2.47 tff(b48_buttercup10454_type, type, ( % 2.28/2.47 b48_buttercup10454: $i > $o)). % 2.28/2.47 tff(k04_buttercup10316_type, type, ( % 2.28/2.47 k04_buttercup10316: $i > $o)). % 2.28/2.47 tff(k04_buttercup10369_type, type, ( % 2.28/2.47 k04_buttercup10369: $i > $o)). % 2.28/2.47 tff(k04_buttercup10477_type, type, ( % 2.28/2.47 k04_buttercup10477: $i > $o)). % 2.28/2.47 tff(b48_buttercup10182_type, type, ( % 2.28/2.47 b48_buttercup10182: $i > $o)). % 2.28/2.47 tff(b48_buttercup10451_type, type, ( % 2.28/2.47 b48_buttercup10451: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_449_type, type, ( % 2.28/2.47 tptp_fun__i_val_449: $i)). % 2.28/2.47 tff(tptp_fun__i_val_236_type, type, ( % 2.28/2.47 tptp_fun__i_val_236: $i)). % 2.28/2.47 tff(k04_buttercup10453_type, type, ( % 2.28/2.47 k04_buttercup10453: $i > $o)). % 2.28/2.47 tff(b48_buttercup10115_type, type, ( % 2.28/2.47 b48_buttercup10115: $i > $o)). % 2.28/2.47 tff(b48_buttercup10272_type, type, ( % 2.28/2.47 b48_buttercup10272: $i > $o)). % 2.28/2.47 tff(b48_buttercup10446_type, type, ( % 2.28/2.47 b48_buttercup10446: $i > $o)). % 2.28/2.47 tff(k04_buttercup10329_type, type, ( % 2.28/2.47 k04_buttercup10329: $i > $o)). % 2.28/2.47 tff(b48_buttercup10196_type, type, ( % 2.28/2.47 b48_buttercup10196: $i > $o)). % 2.28/2.47 tff(b48_buttercup10370_type, type, ( % 2.28/2.47 b48_buttercup10370: $i > $o)). % 2.28/2.47 tff(b48_buttercup10024_type, type, ( % 2.28/2.47 b48_buttercup10024: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_433_type, type, ( % 2.28/2.47 tptp_fun__i_val_433: $i)). % 2.28/2.47 tff(b48_buttercup10110_type, type, ( % 2.28/2.47 b48_buttercup10110: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_382_type, type, ( % 2.28/2.47 tptp_fun__i_val_382: $i)). % 2.28/2.47 tff(tptp_fun__i_val_196_type, type, ( % 2.28/2.47 tptp_fun__i_val_196: $i)). % 2.28/2.47 tff(b48_buttercup10031_type, type, ( % 2.28/2.47 b48_buttercup10031: $i > $o)). % 2.28/2.47 tff(k04_buttercup10611_type, type, ( % 2.28/2.47 k04_buttercup10611: $i > $o)). % 2.28/2.47 tff(k04_buttercup10298_type, type, ( % 2.28/2.47 k04_buttercup10298: $i > $o)). % 2.28/2.47 tff(k04_buttercup10389_type, type, ( % 2.28/2.47 k04_buttercup10389: $i > $o)). % 2.28/2.47 tff(b48_buttercup10374_type, type, ( % 2.28/2.47 b48_buttercup10374: $i > $o)). % 2.28/2.47 tff(b48_buttercup10624_type, type, ( % 2.28/2.47 b48_buttercup10624: $i > $o)). % 2.28/2.47 tff(b48_buttercup10268_type, type, ( % 2.28/2.47 b48_buttercup10268: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_27_type, type, ( % 2.28/2.47 tptp_fun__i_val_27: $i)). % 2.28/2.47 tff(tptp_fun__i_val_60_type, type, ( % 2.28/2.47 tptp_fun__i_val_60: $i)). % 2.28/2.47 tff(tptp_fun__i_val_61_type, type, ( % 2.28/2.47 tptp_fun__i_val_61: $i)). % 2.28/2.47 tff(tptp_fun__i_val_23_type, type, ( % 2.28/2.47 tptp_fun__i_val_23: $i)). % 2.28/2.47 tff(tptp_fun__i_val_26_type, type, ( % 2.28/2.47 tptp_fun__i_val_26: $i)). % 2.28/2.47 tff(tptp_fun__i_val_54_type, type, ( % 2.28/2.47 tptp_fun__i_val_54: $i)). % 2.28/2.47 tff(tptp_fun__i_val_406_type, type, ( % 2.28/2.47 tptp_fun__i_val_406: $i)). % 2.28/2.47 tff(k04_buttercup10100_type, type, ( % 2.28/2.47 k04_buttercup10100: $i > $o)). % 2.28/2.47 tff(b48_buttercup10007_type, type, ( % 2.28/2.47 b48_buttercup10007: $i > $o)). % 2.28/2.47 tff(b48_buttercup10201_type, type, ( % 2.28/2.47 b48_buttercup10201: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_100_type, type, ( % 2.28/2.47 tptp_fun__i_val_100: $i)). % 2.28/2.47 tff(k04_buttercup10282_type, type, ( % 2.28/2.47 k04_buttercup10282: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_84_type, type, ( % 2.28/2.47 tptp_fun__i_val_84: $i)). % 2.28/2.47 tff(b48_buttercup10092_type, type, ( % 2.28/2.47 b48_buttercup10092: $i > $o)). % 2.28/2.47 tff(b48_buttercup10377_type, type, ( % 2.28/2.47 b48_buttercup10377: $i > $o)). % 2.28/2.47 tff(k04_buttercup10628_type, type, ( % 2.28/2.47 k04_buttercup10628: $i > $o)). % 2.28/2.47 tff(b48_buttercup10589_type, type, ( % 2.28/2.47 b48_buttercup10589: $i > $o)). % 2.28/2.47 tff(b48_buttercup10548_type, type, ( % 2.28/2.47 b48_buttercup10548: $i > $o)). % 2.28/2.47 tff(b48_buttercup10541_type, type, ( % 2.28/2.47 b48_buttercup10541: $i > $o)). % 2.28/2.47 tff(b48_buttercup10119_type, type, ( % 2.28/2.47 b48_buttercup10119: $i > $o)). % 2.28/2.47 tff(b48_buttercup10636_type, type, ( % 2.28/2.47 b48_buttercup10636: $i > $o)). % 2.28/2.47 tff(b48_buttercup10616_type, type, ( % 2.28/2.47 b48_buttercup10616: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_64_type, type, ( % 2.28/2.47 tptp_fun__i_val_64: $i)). % 2.28/2.47 tff(k04_buttercup10364_type, type, ( % 2.28/2.47 k04_buttercup10364: $i > $o)). % 2.28/2.47 tff(b48_buttercup10582_type, type, ( % 2.28/2.47 b48_buttercup10582: $i > $o)). % 2.28/2.47 tff(b48_buttercup10526_type, type, ( % 2.28/2.47 b48_buttercup10526: $i > $o)). % 2.28/2.47 tff(k04_buttercup10404_type, type, ( % 2.28/2.47 k04_buttercup10404: $i > $o)). % 2.28/2.47 tff(b48_buttercup10474_type, type, ( % 2.28/2.47 b48_buttercup10474: $i > $o)). % 2.28/2.47 tff(k04_buttercup10376_type, type, ( % 2.28/2.47 k04_buttercup10376: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_324_type, type, ( % 2.28/2.47 tptp_fun__i_val_324: $i)). % 2.28/2.47 tff(b48_buttercup10489_type, type, ( % 2.28/2.47 b48_buttercup10489: $i > $o)). % 2.28/2.47 tff(b48_buttercup10367_type, type, ( % 2.28/2.47 b48_buttercup10367: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_386_type, type, ( % 2.28/2.47 tptp_fun__i_val_386: $i)). % 2.28/2.47 tff(b48_buttercup10133_type, type, ( % 2.28/2.47 b48_buttercup10133: $i > $o)). % 2.28/2.47 tff(k04_buttercup10555_type, type, ( % 2.28/2.47 k04_buttercup10555: $i > $o)). % 2.28/2.47 tff(b48_buttercup10538_type, type, ( % 2.28/2.47 b48_buttercup10538: $i > $o)). % 2.28/2.47 tff(b48_buttercup10549_type, type, ( % 2.28/2.47 b48_buttercup10549: $i > $o)). % 2.28/2.47 tff(tptp_fun__i_val_38_type, type, ( % 2.28/2.47 tptp_fun__i_val_38: $i)). % 2.28/2.47 tff(tptp_fun__i_val_39_type, type, ( % 2.28/2.47 tptp_fun__i_val_39: $i)). % 2.28/2.47 tff(tptp_fun__i_val_98_type, type, ( % 2.28/2.47 tptp_fun__i_val_98: $i)). % 2.28/2.47 tff(b48_buttercup10515_type, type, ( % 2.28/2.47 b48_buttercup10515: $i > $o)). % 2.28/2.47 tff(b48_buttercup10642_type, type, ( % 2.28/2.47 b48_buttercup10642: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_321_type, type, ( % 2.28/2.48 tptp_fun__i_val_321: $i)). % 2.28/2.48 tff(b48_buttercup10307_type, type, ( % 2.28/2.48 b48_buttercup10307: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_44_type, type, ( % 2.28/2.48 tptp_fun__i_val_44: $i)). % 2.28/2.48 tff(b48_buttercup10085_type, type, ( % 2.28/2.48 b48_buttercup10085: $i > $o)). % 2.28/2.48 tff(k04_buttercup10049_type, type, ( % 2.28/2.48 k04_buttercup10049: $i > $o)). % 2.28/2.48 tff(b48_buttercup10563_type, type, ( % 2.28/2.48 b48_buttercup10563: $i > $o)). % 2.28/2.48 tff(k04_buttercup10153_type, type, ( % 2.28/2.48 k04_buttercup10153: $i > $o)). % 2.28/2.48 tff(k04_buttercup10445_type, type, ( % 2.28/2.48 k04_buttercup10445: $i > $o)). % 2.28/2.48 tff(b48_buttercup10072_type, type, ( % 2.28/2.48 b48_buttercup10072: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_421_type, type, ( % 2.28/2.48 tptp_fun__i_val_421: $i)). % 2.28/2.48 tff(b48_buttercup10228_type, type, ( % 2.28/2.48 b48_buttercup10228: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_243_type, type, ( % 2.28/2.48 tptp_fun__i_val_243: $i)). % 2.28/2.48 tff(b48_buttercup10169_type, type, ( % 2.28/2.48 b48_buttercup10169: $i > $o)). % 2.28/2.48 tff(b48_buttercup10150_type, type, ( % 2.28/2.48 b48_buttercup10150: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_400_type, type, ( % 2.28/2.48 tptp_fun__i_val_400: $i)). % 2.28/2.48 tff(b48_buttercup10021_type, type, ( % 2.28/2.48 b48_buttercup10021: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_313_type, type, ( % 2.28/2.48 tptp_fun__i_val_313: $i)). % 2.28/2.48 tff(b48_buttercup10519_type, type, ( % 2.28/2.48 b48_buttercup10519: $i > $o)). % 2.28/2.48 tff(b48_buttercup10479_type, type, ( % 2.28/2.48 b48_buttercup10479: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_458_type, type, ( % 2.28/2.48 tptp_fun__i_val_458: $i)). % 2.28/2.48 tff(b48_buttercup10308_type, type, ( % 2.28/2.48 b48_buttercup10308: $i > $o)). % 2.28/2.48 tff(b48_buttercup10275_type, type, ( % 2.28/2.48 b48_buttercup10275: $i > $o)). % 2.28/2.48 tff(b48_buttercup10433_type, type, ( % 2.28/2.48 b48_buttercup10433: $i > $o)). % 2.28/2.48 tff(k04_buttercup10492_type, type, ( % 2.28/2.48 k04_buttercup10492: $i > $o)). % 2.28/2.48 tff(b48_buttercup10278_type, type, ( % 2.28/2.48 b48_buttercup10278: $i > $o)). % 2.28/2.48 tff(b48_buttercup10562_type, type, ( % 2.28/2.48 b48_buttercup10562: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_410_type, type, ( % 2.28/2.48 tptp_fun__i_val_410: $i)). % 2.28/2.48 tff(b48_buttercup10109_type, type, ( % 2.28/2.48 b48_buttercup10109: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_442_type, type, ( % 2.28/2.48 tptp_fun__i_val_442: $i)). % 2.28/2.48 tff(tptp_fun__i_val_231_type, type, ( % 2.28/2.48 tptp_fun__i_val_231: $i)). % 2.28/2.48 tff(k04_buttercup10219_type, type, ( % 2.28/2.48 k04_buttercup10219: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_451_type, type, ( % 2.28/2.48 tptp_fun__i_val_451: $i)). % 2.28/2.48 tff(b48_buttercup10227_type, type, ( % 2.28/2.48 b48_buttercup10227: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_216_type, type, ( % 2.28/2.48 tptp_fun__i_val_216: $i)). % 2.28/2.48 tff(tptp_fun__i_val_300_type, type, ( % 2.28/2.48 tptp_fun__i_val_300: $i)). % 2.28/2.48 tff(k04_buttercup10221_type, type, ( % 2.28/2.48 k04_buttercup10221: $i > $o)). % 2.28/2.48 tff(k04_buttercup10540_type, type, ( % 2.28/2.48 k04_buttercup10540: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_202_type, type, ( % 2.28/2.48 tptp_fun__i_val_202: $i)). % 2.28/2.48 tff(tptp_fun__i_val_389_type, type, ( % 2.28/2.48 tptp_fun__i_val_389: $i)). % 2.28/2.48 tff(tptp_fun__i_val_247_type, type, ( % 2.28/2.48 tptp_fun__i_val_247: $i)). % 2.28/2.48 tff(b48_buttercup10166_type, type, ( % 2.28/2.48 b48_buttercup10166: $i > $o)). % 2.28/2.48 tff(b48_buttercup10646_type, type, ( % 2.28/2.48 b48_buttercup10646: $i > $o)). % 2.28/2.48 tff(k04_buttercup10074_type, type, ( % 2.28/2.48 k04_buttercup10074: $i > $o)). % 2.28/2.48 tff(b48_buttercup10283_type, type, ( % 2.28/2.48 b48_buttercup10283: $i > $o)). % 2.28/2.48 tff(b48_buttercup10086_type, type, ( % 2.28/2.48 b48_buttercup10086: $i > $o)). % 2.28/2.48 tff(k04_buttercup10641_type, type, ( % 2.28/2.48 k04_buttercup10641: $i > $o)). % 2.28/2.48 tff(k04_buttercup10147_type, type, ( % 2.28/2.48 k04_buttercup10147: $i > $o)). % 2.28/2.48 tff(b48_buttercup10507_type, type, ( % 2.28/2.48 b48_buttercup10507: $i > $o)). % 2.28/2.48 tff(k04_buttercup10238_type, type, ( % 2.28/2.48 k04_buttercup10238: $i > $o)). % 2.28/2.48 tff(k04_buttercup10012_type, type, ( % 2.28/2.48 k04_buttercup10012: $i > $o)). % 2.28/2.48 tff(b48_buttercup10411_type, type, ( % 2.28/2.48 b48_buttercup10411: $i > $o)). % 2.28/2.48 tff(k04_buttercup10599_type, type, ( % 2.28/2.48 k04_buttercup10599: $i > $o)). % 2.28/2.48 tff(b48_buttercup10638_type, type, ( % 2.28/2.48 b48_buttercup10638: $i > $o)). % 2.28/2.48 tff(b48_buttercup10294_type, type, ( % 2.28/2.48 b48_buttercup10294: $i > $o)). % 2.28/2.48 tff(k04_buttercup10567_type, type, ( % 2.28/2.48 k04_buttercup10567: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_310_type, type, ( % 2.28/2.48 tptp_fun__i_val_310: $i)). % 2.28/2.48 tff(b48_buttercup10019_type, type, ( % 2.28/2.48 b48_buttercup10019: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_380_type, type, ( % 2.28/2.48 tptp_fun__i_val_380: $i)). % 2.28/2.48 tff(tptp_fun__i_val_211_type, type, ( % 2.28/2.48 tptp_fun__i_val_211: $i)). % 2.28/2.48 tff(b48_buttercup10034_type, type, ( % 2.28/2.48 b48_buttercup10034: $i > $o)). % 2.28/2.48 tff(k04_buttercup10337_type, type, ( % 2.28/2.48 k04_buttercup10337: $i > $o)). % 2.28/2.48 tff(k04_buttercup10347_type, type, ( % 2.28/2.48 k04_buttercup10347: $i > $o)). % 2.28/2.48 tff(k04_buttercup10449_type, type, ( % 2.28/2.48 k04_buttercup10449: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_415_type, type, ( % 2.28/2.48 tptp_fun__i_val_415: $i)). % 2.28/2.48 tff(tptp_fun__i_val_156_type, type, ( % 2.28/2.48 tptp_fun__i_val_156: $i)). % 2.28/2.48 tff(b48_buttercup10220_type, type, ( % 2.28/2.48 b48_buttercup10220: $i > $o)). % 2.28/2.48 tff(b48_buttercup10417_type, type, ( % 2.28/2.48 b48_buttercup10417: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_315_type, type, ( % 2.28/2.48 tptp_fun__i_val_315: $i)). % 2.28/2.48 tff(b48_buttercup10467_type, type, ( % 2.28/2.48 b48_buttercup10467: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_301_type, type, ( % 2.28/2.48 tptp_fun__i_val_301: $i)). % 2.28/2.48 tff(b48_buttercup10483_type, type, ( % 2.28/2.48 b48_buttercup10483: $i > $o)). % 2.28/2.48 tff(k04_buttercup10430_type, type, ( % 2.28/2.48 k04_buttercup10430: $i > $o)). % 2.28/2.48 tff(k04_buttercup10356_type, type, ( % 2.28/2.48 k04_buttercup10356: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_333_type, type, ( % 2.28/2.48 tptp_fun__i_val_333: $i)). % 2.28/2.48 tff(b48_buttercup10154_type, type, ( % 2.28/2.48 b48_buttercup10154: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_198_type, type, ( % 2.28/2.48 tptp_fun__i_val_198: $i)). % 2.28/2.48 tff(k04_buttercup10135_type, type, ( % 2.28/2.48 k04_buttercup10135: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_278_type, type, ( % 2.28/2.48 tptp_fun__i_val_278: $i)). % 2.28/2.48 tff(b48_buttercup10070_type, type, ( % 2.28/2.48 b48_buttercup10070: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_370_type, type, ( % 2.28/2.48 tptp_fun__i_val_370: $i)). % 2.28/2.48 tff(b48_buttercup10521_type, type, ( % 2.28/2.48 b48_buttercup10521: $i > $o)). % 2.28/2.48 tff(b48_buttercup10290_type, type, ( % 2.28/2.48 b48_buttercup10290: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_302_type, type, ( % 2.28/2.48 tptp_fun__i_val_302: $i)). % 2.28/2.48 tff(b48_buttercup10068_type, type, ( % 2.28/2.48 b48_buttercup10068: $i > $o)). % 2.28/2.48 tff(k04_buttercup10255_type, type, ( % 2.28/2.48 k04_buttercup10255: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_177_type, type, ( % 2.28/2.48 tptp_fun__i_val_177: $i)). % 2.28/2.48 tff(tptp_fun__i_val_401_type, type, ( % 2.28/2.48 tptp_fun__i_val_401: $i)). % 2.28/2.48 tff(b48_buttercup10253_type, type, ( % 2.28/2.48 b48_buttercup10253: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_316_type, type, ( % 2.28/2.48 tptp_fun__i_val_316: $i)). % 2.28/2.48 tff(b48_buttercup10466_type, type, ( % 2.28/2.48 b48_buttercup10466: $i > $o)). % 2.28/2.48 tff(k04_buttercup10067_type, type, ( % 2.28/2.48 k04_buttercup10067: $i > $o)). % 2.28/2.48 tff(k04_buttercup10252_type, type, ( % 2.28/2.48 k04_buttercup10252: $i > $o)). % 2.28/2.48 tff(b48_buttercup10013_type, type, ( % 2.28/2.48 b48_buttercup10013: $i > $o)). % 2.28/2.48 tff(b48_buttercup10596_type, type, ( % 2.28/2.48 b48_buttercup10596: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_332_type, type, ( % 2.28/2.48 tptp_fun__i_val_332: $i)). % 2.28/2.48 tff(b48_buttercup10156_type, type, ( % 2.28/2.48 b48_buttercup10156: $i > $o)). % 2.28/2.48 tff(k04_buttercup10510_type, type, ( % 2.28/2.48 k04_buttercup10510: $i > $o)). % 2.28/2.48 tff(b48_buttercup10199_type, type, ( % 2.28/2.48 b48_buttercup10199: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_448_type, type, ( % 2.28/2.48 tptp_fun__i_val_448: $i)). % 2.28/2.48 tff(b48_buttercup10195_type, type, ( % 2.28/2.48 b48_buttercup10195: $i > $o)). % 2.28/2.48 tff(b48_buttercup10493_type, type, ( % 2.28/2.48 b48_buttercup10493: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_95_type, type, ( % 2.28/2.48 tptp_fun__i_val_95: $i)). % 2.28/2.48 tff(tptp_fun__i_val_99_type, type, ( % 2.28/2.48 tptp_fun__i_val_99: $i)). % 2.28/2.48 tff(k04_buttercup10419_type, type, ( % 2.28/2.48 k04_buttercup10419: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_276_type, type, ( % 2.28/2.48 tptp_fun__i_val_276: $i)). % 2.28/2.48 tff(b48_buttercup10174_type, type, ( % 2.28/2.48 b48_buttercup10174: $i > $o)). % 2.28/2.48 tff(b48_buttercup10065_type, type, ( % 2.28/2.48 b48_buttercup10065: $i > $o)). % 2.28/2.48 tff(b48_buttercup10410_type, type, ( % 2.28/2.48 b48_buttercup10410: $i > $o)). % 2.28/2.48 tff(k04_buttercup10200_type, type, ( % 2.28/2.48 k04_buttercup10200: $i > $o)). % 2.28/2.48 tff(b48_buttercup10130_type, type, ( % 2.28/2.48 b48_buttercup10130: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_170_type, type, ( % 2.28/2.48 tptp_fun__i_val_170: $i)). % 2.28/2.48 tff(tptp_fun__i_val_85_type, type, ( % 2.28/2.48 tptp_fun__i_val_85: $i)). % 2.28/2.48 tff(tptp_fun__i_val_249_type, type, ( % 2.28/2.48 tptp_fun__i_val_249: $i)). % 2.28/2.48 tff(tptp_fun__i_val_86_type, type, ( % 2.28/2.48 tptp_fun__i_val_86: $i)). % 2.28/2.48 tff(b48_buttercup10261_type, type, ( % 2.28/2.48 b48_buttercup10261: $i > $o)). % 2.28/2.48 tff(k04_buttercup10382_type, type, ( % 2.28/2.48 k04_buttercup10382: $i > $o)). % 2.28/2.48 tff(b48_buttercup10640_type, type, ( % 2.28/2.48 b48_buttercup10640: $i > $o)). % 2.28/2.48 tff(k04_buttercup10408_type, type, ( % 2.28/2.48 k04_buttercup10408: $i > $o)). % 2.28/2.48 tff(b48_buttercup10442_type, type, ( % 2.28/2.48 b48_buttercup10442: $i > $o)). % 2.28/2.48 tff(k04_buttercup10539_type, type, ( % 2.28/2.48 k04_buttercup10539: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_105_type, type, ( % 2.28/2.48 tptp_fun__i_val_105: $i)). % 2.28/2.48 tff(tptp_fun__i_val_251_type, type, ( % 2.28/2.48 tptp_fun__i_val_251: $i)). % 2.28/2.48 tff(k04_buttercup10373_type, type, ( % 2.28/2.48 k04_buttercup10373: $i > $o)). % 2.28/2.48 tff(k04_buttercup10380_type, type, ( % 2.28/2.48 k04_buttercup10380: $i > $o)). % 2.28/2.48 tff(k04_buttercup10622_type, type, ( % 2.28/2.48 k04_buttercup10622: $i > $o)). % 2.28/2.48 tff(b48_buttercup10260_type, type, ( % 2.28/2.48 b48_buttercup10260: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_59_type, type, ( % 2.28/2.48 tptp_fun__i_val_59: $i)). % 2.28/2.48 tff(b48_buttercup10381_type, type, ( % 2.28/2.48 b48_buttercup10381: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_450_type, type, ( % 2.28/2.48 tptp_fun__i_val_450: $i)). % 2.28/2.48 tff(b48_buttercup10193_type, type, ( % 2.28/2.48 b48_buttercup10193: $i > $o)). % 2.28/2.48 tff(b48_buttercup10612_type, type, ( % 2.28/2.48 b48_buttercup10612: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_418_type, type, ( % 2.28/2.48 tptp_fun__i_val_418: $i)). % 2.28/2.48 tff(b48_buttercup10348_type, type, ( % 2.28/2.48 b48_buttercup10348: $i > $o)). % 2.28/2.48 tff(k04_buttercup10312_type, type, ( % 2.28/2.48 k04_buttercup10312: $i > $o)). % 2.28/2.48 tff(k04_buttercup10296_type, type, ( % 2.28/2.48 k04_buttercup10296: $i > $o)). % 2.28/2.48 tff(k04_buttercup10643_type, type, ( % 2.28/2.48 k04_buttercup10643: $i > $o)). % 2.28/2.48 tff(b48_buttercup10609_type, type, ( % 2.28/2.48 b48_buttercup10609: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_323_type, type, ( % 2.28/2.48 tptp_fun__i_val_323: $i)). % 2.28/2.48 tff(tptp_fun__i_val_462_type, type, ( % 2.28/2.48 tptp_fun__i_val_462: $i)). % 2.28/2.48 tff(b48_buttercup10305_type, type, ( % 2.28/2.48 b48_buttercup10305: $i > $o)). % 2.28/2.48 tff(k04_buttercup10172_type, type, ( % 2.28/2.48 k04_buttercup10172: $i > $o)). % 2.28/2.48 tff(k04_buttercup10042_type, type, ( % 2.28/2.48 k04_buttercup10042: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_108_type, type, ( % 2.28/2.48 tptp_fun__i_val_108: $i)). % 2.28/2.48 tff(tptp_fun__i_val_250_type, type, ( % 2.28/2.48 tptp_fun__i_val_250: $i)). % 2.28/2.48 tff(tptp_fun__i_val_432_type, type, ( % 2.28/2.48 tptp_fun__i_val_432: $i)). % 2.28/2.48 tff(b48_buttercup10111_type, type, ( % 2.28/2.48 b48_buttercup10111: $i > $o)). % 2.28/2.48 tff(b48_buttercup10104_type, type, ( % 2.28/2.48 b48_buttercup10104: $i > $o)). % 2.28/2.48 tff(k04_buttercup10236_type, type, ( % 2.28/2.48 k04_buttercup10236: $i > $o)). % 2.28/2.48 tff(k04_buttercup10028_type, type, ( % 2.28/2.48 k04_buttercup10028: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_317_type, type, ( % 2.28/2.48 tptp_fun__i_val_317: $i)). % 2.28/2.48 tff(b48_buttercup10465_type, type, ( % 2.28/2.48 b48_buttercup10465: $i > $o)). % 2.28/2.48 tff(k04_buttercup10524_type, type, ( % 2.28/2.48 k04_buttercup10524: $i > $o)). % 2.28/2.48 tff(k04_buttercup10048_type, type, ( % 2.28/2.48 k04_buttercup10048: $i > $o)). % 2.28/2.48 tff(b48_buttercup10496_type, type, ( % 2.28/2.48 b48_buttercup10496: $i > $o)). % 2.28/2.48 tff(k04_buttercup10626_type, type, ( % 2.28/2.48 k04_buttercup10626: $i > $o)). % 2.28/2.48 tff(b48_buttercup10394_type, type, ( % 2.28/2.48 b48_buttercup10394: $i > $o)). % 2.28/2.48 tff(b48_buttercup10313_type, type, ( % 2.28/2.48 b48_buttercup10313: $i > $o)). % 2.28/2.48 tff(k04_buttercup10504_type, type, ( % 2.28/2.48 k04_buttercup10504: $i > $o)). % 2.28/2.48 tff(k04_buttercup10164_type, type, ( % 2.28/2.48 k04_buttercup10164: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_372_type, type, ( % 2.28/2.48 tptp_fun__i_val_372: $i)). % 2.28/2.48 tff(b48_buttercup10570_type, type, ( % 2.28/2.48 b48_buttercup10570: $i > $o)). % 2.28/2.48 tff(b48_buttercup10575_type, type, ( % 2.28/2.48 b48_buttercup10575: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_423_type, type, ( % 2.28/2.48 tptp_fun__i_val_423: $i)). % 2.28/2.48 tff(b48_buttercup10343_type, type, ( % 2.28/2.48 b48_buttercup10343: $i > $o)). % 2.28/2.48 tff(b48_buttercup10197_type, type, ( % 2.28/2.48 b48_buttercup10197: $i > $o)). % 2.28/2.48 tff(b48_buttercup10450_type, type, ( % 2.28/2.48 b48_buttercup10450: $i > $o)). % 2.28/2.48 tff(k04_buttercup10097_type, type, ( % 2.28/2.48 k04_buttercup10097: $i > $o)). % 2.28/2.48 tff(b48_buttercup10502_type, type, ( % 2.28/2.48 b48_buttercup10502: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_422_type, type, ( % 2.28/2.48 tptp_fun__i_val_422: $i)). % 2.28/2.48 tff(b48_buttercup10344_type, type, ( % 2.28/2.48 b48_buttercup10344: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_258_type, type, ( % 2.28/2.48 tptp_fun__i_val_258: $i)). % 2.28/2.48 tff(b48_buttercup10441_type, type, ( % 2.28/2.48 b48_buttercup10441: $i > $o)). % 2.28/2.48 tff(b48_buttercup10469_type, type, ( % 2.28/2.48 b48_buttercup10469: $i > $o)). % 2.28/2.48 tff(b48_buttercup10309_type, type, ( % 2.28/2.48 b48_buttercup10309: $i > $o)). % 2.28/2.48 tff(b48_buttercup10471_type, type, ( % 2.28/2.48 b48_buttercup10471: $i > $o)). % 2.28/2.48 tff(k04_buttercup10142_type, type, ( % 2.28/2.48 k04_buttercup10142: $i > $o)). % 2.28/2.48 tff(k04_buttercup10033_type, type, ( % 2.28/2.48 k04_buttercup10033: $i > $o)). % 2.28/2.48 tff(b48_buttercup10198_type, type, ( % 2.28/2.48 b48_buttercup10198: $i > $o)). % 2.28/2.48 tff(k04_buttercup10259_type, type, ( % 2.28/2.48 k04_buttercup10259: $i > $o)). % 2.28/2.48 tff(b48_buttercup10300_type, type, ( % 2.28/2.48 b48_buttercup10300: $i > $o)). % 2.28/2.48 tff(b48_buttercup10512_type, type, ( % 2.28/2.48 b48_buttercup10512: $i > $o)). % 2.28/2.48 tff(k04_buttercup10547_type, type, ( % 2.28/2.48 k04_buttercup10547: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_271_type, type, ( % 2.28/2.48 tptp_fun__i_val_271: $i)). % 2.28/2.48 tff(b48_buttercup10160_type, type, ( % 2.28/2.48 b48_buttercup10160: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_412_type, type, ( % 2.28/2.48 tptp_fun__i_val_412: $i)). % 2.28/2.48 tff(b48_buttercup10518_type, type, ( % 2.28/2.48 b48_buttercup10518: $i > $o)). % 2.28/2.48 tff(b48_buttercup10629_type, type, ( % 2.28/2.48 b48_buttercup10629: $i > $o)). % 2.28/2.48 tff(k04_buttercup10139_type, type, ( % 2.28/2.48 k04_buttercup10139: $i > $o)). % 2.28/2.48 tff(b48_buttercup10176_type, type, ( % 2.28/2.48 b48_buttercup10176: $i > $o)). % 2.28/2.48 tff(b48_buttercup10273_type, type, ( % 2.28/2.48 b48_buttercup10273: $i > $o)). % 2.28/2.48 tff(k04_buttercup10546_type, type, ( % 2.28/2.48 k04_buttercup10546: $i > $o)). % 2.28/2.48 tff(b48_buttercup10378_type, type, ( % 2.28/2.48 b48_buttercup10378: $i > $o)). % 2.28/2.48 tff(k04_buttercup10234_type, type, ( % 2.28/2.48 k04_buttercup10234: $i > $o)). % 2.28/2.48 tff(b48_buttercup10217_type, type, ( % 2.28/2.48 b48_buttercup10217: $i > $o)). % 2.28/2.48 tff(k04_buttercup10057_type, type, ( % 2.28/2.48 k04_buttercup10057: $i > $o)). % 2.28/2.48 tff(b48_buttercup10402_type, type, ( % 2.28/2.48 b48_buttercup10402: $i > $o)). % 2.28/2.48 tff(k04_buttercup10325_type, type, ( % 2.28/2.48 k04_buttercup10325: $i > $o)). % 2.28/2.48 tff(b48_buttercup10102_type, type, ( % 2.28/2.48 b48_buttercup10102: $i > $o)). % 2.28/2.48 tff(b48_buttercup10208_type, type, ( % 2.28/2.48 b48_buttercup10208: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_404_type, type, ( % 2.28/2.48 tptp_fun__i_val_404: $i)). % 2.28/2.48 tff(b48_buttercup10456_type, type, ( % 2.28/2.48 b48_buttercup10456: $i > $o)). % 2.28/2.48 tff(b48_buttercup10277_type, type, ( % 2.28/2.48 b48_buttercup10277: $i > $o)). % 2.28/2.48 tff(k04_buttercup10529_type, type, ( % 2.28/2.48 k04_buttercup10529: $i > $o)). % 2.28/2.48 tff(b48_buttercup10545_type, type, ( % 2.28/2.48 b48_buttercup10545: $i > $o)). % 2.28/2.48 tff(b48_buttercup10353_type, type, ( % 2.28/2.48 b48_buttercup10353: $i > $o)). % 2.28/2.48 tff(k04_buttercup10415_type, type, ( % 2.28/2.48 k04_buttercup10415: $i > $o)). % 2.28/2.48 tff(b48_buttercup10035_type, type, ( % 2.28/2.48 b48_buttercup10035: $i > $o)). % 2.28/2.48 tff(k04_buttercup10635_type, type, ( % 2.28/2.48 k04_buttercup10635: $i > $o)). % 2.28/2.48 tff(k04_buttercup10581_type, type, ( % 2.28/2.48 k04_buttercup10581: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_420_type, type, ( % 2.28/2.48 tptp_fun__i_val_420: $i)). % 2.28/2.48 tff(b48_buttercup10229_type, type, ( % 2.28/2.48 b48_buttercup10229: $i > $o)). % 2.28/2.48 tff(k04_buttercup10360_type, type, ( % 2.28/2.48 k04_buttercup10360: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_118_type, type, ( % 2.28/2.48 tptp_fun__i_val_118: $i)). % 2.28/2.48 tff(tptp_fun__i_val_387_type, type, ( % 2.28/2.48 tptp_fun__i_val_387: $i)). % 2.28/2.48 tff(k04_buttercup10516_type, type, ( % 2.28/2.48 k04_buttercup10516: $i > $o)). % 2.28/2.48 tff(k04_buttercup10551_type, type, ( % 2.28/2.48 k04_buttercup10551: $i > $o)). % 2.28/2.48 tff(b48_buttercup10299_type, type, ( % 2.28/2.48 b48_buttercup10299: $i > $o)). % 2.28/2.48 tff(b48_buttercup10522_type, type, ( % 2.28/2.48 b48_buttercup10522: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_282_type, type, ( % 2.28/2.48 tptp_fun__i_val_282: $i)). % 2.28/2.48 tff(b48_buttercup10075_type, type, ( % 2.28/2.48 b48_buttercup10075: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_399_type, type, ( % 2.28/2.48 tptp_fun__i_val_399: $i)). % 2.28/2.48 tff(b48_buttercup10022_type, type, ( % 2.28/2.48 b48_buttercup10022: $i > $o)). % 2.28/2.48 tff(k04_buttercup10578_type, type, ( % 2.28/2.48 k04_buttercup10578: $i > $o)). % 2.28/2.48 tff(b48_buttercup10108_type, type, ( % 2.28/2.48 b48_buttercup10108: $i > $o)). % 2.28/2.48 tff(k04_buttercup10190_type, type, ( % 2.28/2.48 k04_buttercup10190: $i > $o)). % 2.28/2.48 tff(b48_buttercup10222_type, type, ( % 2.28/2.48 b48_buttercup10222: $i > $o)). % 2.28/2.48 tff(k04_buttercup10286_type, type, ( % 2.28/2.48 k04_buttercup10286: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_101_type, type, ( % 2.28/2.48 tptp_fun__i_val_101: $i)). % 2.28/2.48 tff(tptp_fun__i_val_242_type, type, ( % 2.28/2.48 tptp_fun__i_val_242: $i)). % 2.28/2.48 tff(k04_buttercup10593_type, type, ( % 2.28/2.48 k04_buttercup10593: $i > $o)). % 2.28/2.48 tff(k04_buttercup10333_type, type, ( % 2.28/2.48 k04_buttercup10333: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_408_type, type, ( % 2.28/2.48 tptp_fun__i_val_408: $i)). % 2.28/2.48 tff(tptp_fun__i_val_222_type, type, ( % 2.28/2.48 tptp_fun__i_val_222: $i)). % 2.28/2.48 tff(k04_buttercup10620_type, type, ( % 2.28/2.48 k04_buttercup10620: $i > $o)). % 2.28/2.48 tff(b48_buttercup10443_type, type, ( % 2.28/2.48 b48_buttercup10443: $i > $o)). % 2.28/2.48 tff(b48_buttercup10248_type, type, ( % 2.28/2.48 b48_buttercup10248: $i > $o)). % 2.28/2.48 tff(k04_buttercup10619_type, type, ( % 2.28/2.48 k04_buttercup10619: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_369_type, type, ( % 2.28/2.48 tptp_fun__i_val_369: $i)). % 2.28/2.48 tff(b48_buttercup10574_type, type, ( % 2.28/2.48 b48_buttercup10574: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_20_type, type, ( % 2.28/2.48 tptp_fun__i_val_20: $i)). % 2.28/2.48 tff(tptp_fun__i_val_40_type, type, ( % 2.28/2.48 tptp_fun__i_val_40: $i)). % 2.28/2.48 tff(k04_buttercup10204_type, type, ( % 2.28/2.48 k04_buttercup10204: $i > $o)). % 2.28/2.48 tff(k04_buttercup10184_type, type, ( % 2.28/2.48 k04_buttercup10184: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_265_type, type, ( % 2.28/2.48 tptp_fun__i_val_265: $i)). % 2.28/2.48 tff(b48_buttercup10362_type, type, ( % 2.28/2.48 b48_buttercup10362: $i > $o)). % 2.28/2.48 tff(k04_buttercup10499_type, type, ( % 2.28/2.48 k04_buttercup10499: $i > $o)). % 2.28/2.48 tff(b48_buttercup10054_type, type, ( % 2.28/2.48 b48_buttercup10054: $i > $o)). % 2.28/2.48 tff(b48_buttercup10291_type, type, ( % 2.28/2.48 b48_buttercup10291: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_181_type, type, ( % 2.28/2.48 tptp_fun__i_val_181: $i)). % 2.28/2.48 tff(k04_buttercup10000_type, type, ( % 2.28/2.48 k04_buttercup10000: $i > $o)). % 2.28/2.48 tff(k04_buttercup10053_type, type, ( % 2.28/2.48 k04_buttercup10053: $i > $o)). % 2.28/2.48 tff(k04_buttercup10486_type, type, ( % 2.28/2.48 k04_buttercup10486: $i > $o)). % 2.28/2.48 tff(k04_buttercup10079_type, type, ( % 2.28/2.48 k04_buttercup10079: $i > $o)). % 2.28/2.48 tff(k04_buttercup10089_type, type, ( % 2.28/2.48 k04_buttercup10089: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_443_type, type, ( % 2.28/2.48 tptp_fun__i_val_443: $i)). % 2.28/2.48 tff(tptp_fun__i_val_235_type, type, ( % 2.28/2.48 tptp_fun__i_val_235: $i)). % 2.28/2.48 tff(b48_buttercup10210_type, type, ( % 2.28/2.48 b48_buttercup10210: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_182_type, type, ( % 2.28/2.48 tptp_fun__i_val_182: $i)). % 2.28/2.48 tff(k04_buttercup10004_type, type, ( % 2.28/2.48 k04_buttercup10004: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_384_type, type, ( % 2.28/2.48 tptp_fun__i_val_384: $i)). % 2.28/2.48 tff(b48_buttercup10134_type, type, ( % 2.28/2.48 b48_buttercup10134: $i > $o)). % 2.28/2.48 tff(k04_buttercup10397_type, type, ( % 2.28/2.48 k04_buttercup10397: $i > $o)). % 2.28/2.48 tff(b48_buttercup10605_type, type, ( % 2.28/2.48 b48_buttercup10605: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_441_type, type, ( % 2.28/2.48 tptp_fun__i_val_441: $i)). % 2.28/2.48 tff(b48_buttercup10520_type, type, ( % 2.28/2.48 b48_buttercup10520: $i > $o)). % 2.28/2.48 tff(k04_buttercup10095_type, type, ( % 2.28/2.48 k04_buttercup10095: $i > $o)). % 2.28/2.48 tff(k04_buttercup10544_type, type, ( % 2.28/2.48 k04_buttercup10544: $i > $o)). % 2.28/2.48 tff(b48_buttercup10322_type, type, ( % 2.28/2.48 b48_buttercup10322: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_336_type, type, ( % 2.28/2.48 tptp_fun__i_val_336: $i)). % 2.28/2.48 tff(b48_buttercup10158_type, type, ( % 2.28/2.48 b48_buttercup10158: $i > $o)). % 2.28/2.48 tff(k04_buttercup10288_type, type, ( % 2.28/2.48 k04_buttercup10288: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_103_type, type, ( % 2.28/2.48 tptp_fun__i_val_103: $i)). % 2.28/2.48 tff(tptp_fun__i_val_426_type, type, ( % 2.28/2.48 tptp_fun__i_val_426: $i)). % 2.28/2.48 tff(k04_buttercup10608_type, type, ( % 2.28/2.48 k04_buttercup10608: $i > $o)). % 2.28/2.48 tff(b48_buttercup10266_type, type, ( % 2.28/2.48 b48_buttercup10266: $i > $o)). % 2.28/2.48 tff(k04_buttercup10213_type, type, ( % 2.28/2.48 k04_buttercup10213: $i > $o)). % 2.28/2.48 tff(b48_buttercup10420_type, type, ( % 2.28/2.48 b48_buttercup10420: $i > $o)). % 2.28/2.48 tff(k04_buttercup10016_type, type, ( % 2.28/2.48 k04_buttercup10016: $i > $o)). % 2.28/2.48 tff(b48_buttercup10107_type, type, ( % 2.28/2.48 b48_buttercup10107: $i > $o)). % 2.28/2.48 tff(tptp_fun__i_val_439_type, type, ( % 2.28/2.48 tptp_fun__i_val_439: $i)). % 2.28/2.48 tff(tptp_fun__i_val_205_type, type, ( % 2.28/2.48 tptp_fun__i_val_205: $i)). % 2.28/2.48 tff(tptp_fun__i_val_127_type, type, ( % 2.28/2.48 tptp_fun__i_val_127: $i)). % 2.28/2.48 tff(tptp_fun__i_val_146_type, type, ( % 2.28/2.48 tptp_fun__i_val_146: $i)). % 2.28/2.48 tff(tptp_fun__i_val_279_type, type, ( % 2.28/2.48 tptp_fun__i_val_279: $i)). % 2.28/2.48 tff(tptp_fun__i_val_145_type, type, ( % 2.28/2.48 tptp_fun__i_val_145: $i)). % 2.28/2.48 tff(tptp_fun__i_val_102_type, type, ( % 2.28/2.48 tptp_fun__i_val_102: $i)). % 2.28/2.48 tff(tptp_fun__i_val_72_type, type, ( % 2.28/2.48 tptp_fun__i_val_72: $i)). % 2.28/2.48 tff(tptp_fun__i_val_343_type, type, ( % 2.28/2.48 tptp_fun__i_val_343: $i)). % 2.28/2.48 tff(tptp_fun__i_val_293_type, type, ( % 2.28/2.48 tptp_fun__i_val_293: $i)). % 2.28/2.48 tff(tptp_fun__i_val_165_type, type, ( % 2.28/2.48 tptp_fun__i_val_165: $i)). % 2.28/2.48 tff(tptp_fun__i_val_299_type, type, ( % 2.28/2.48 tptp_fun__i_val_299: $i)). % 2.28/2.48 tff(tptp_fun__i_val_453_type, type, ( % 2.28/2.48 tptp_fun__i_val_453: $i)). % 2.28/2.48 tff(tptp_fun__i_val_388_type, type, ( % 2.28/2.48 tptp_fun__i_val_388: $i)). % 2.28/2.48 tff(tptp_fun__i_val_45_type, type, ( % 2.28/2.48 tptp_fun__i_val_45: $i)). % 2.28/2.48 tff(tptp_fun__i_val_269_type, type, ( % 2.28/2.48 tptp_fun__i_val_269: $i)). % 2.28/2.48 tff(tptp_fun__i_val_143_type, type, ( % 2.28/2.48 tptp_fun__i_val_143: $i)). % 2.28/2.48 tff(tptp_fun__i_val_260_type, type, ( % 2.28/2.48 tptp_fun__i_val_260: $i)). % 2.28/2.48 tff(tptp_fun__i_val_261_type, type, ( % 2.28/2.48 tptp_fun__i_val_261: $i)). % 2.28/2.48 tff(tptp_fun__i_val_1_type, type, ( % 2.28/2.48 tptp_fun__i_val_1: $i)). % 2.28/2.48 tff(tptp_fun__i_val_255_type, type, ( % 2.28/2.48 tptp_fun__i_val_255: $i)). % 2.28/2.48 tff(tptp_fun__i_val_0_type, type, ( % 2.28/2.48 tptp_fun__i_val_0: $i)). % 2.28/2.48 tff(tptp_fun__i_val_68_type, type, ( % 2.28/2.48 tptp_fun__i_val_68: $i)). % 2.28/2.48 tff(tptp_fun__i_val_139_type, type, ( % 2.28/2.48 tptp_fun__i_val_139: $i)). % 2.28/2.48 tff(tptp_fun__i_val_36_type, type, ( % 2.28/2.48 tptp_fun__i_val_36: $i)). % 2.28/2.48 tff(tptp_fun__i_val_312_type, type, ( % 2.28/2.48 tptp_fun__i_val_312: $i)). % 2.28/2.48 tff(tptp_fun__i_val_46_type, type, ( % 2.28/2.48 tptp_fun__i_val_46: $i)). % 2.28/2.48 tff(tptp_fun__i_val_425_type, type, ( % 2.28/2.48 tptp_fun__i_val_425: $i)). % 2.28/2.48 tff(tptp_fun__i_val_138_type, type, ( % 2.28/2.48 tptp_fun__i_val_138: $i)). % 2.28/2.48 tff(tptp_fun__i_val_77_type, type, ( % 2.28/2.48 tptp_fun__i_val_77: $i)). % 2.28/2.48 tff(tptp_fun__i_val_89_type, type, ( % 2.28/2.48 tptp_fun__i_val_89: $i)). % 2.28/2.48 tff(tptp_fun__i_val_378_type, type, ( % 2.28/2.48 tptp_fun__i_val_378: $i)). % 2.28/2.48 tff(tptp_fun__i_val_80_type, type, ( % 2.28/2.48 tptp_fun__i_val_80: $i)). % 2.28/2.48 tff(tptp_fun__i_val_306_type, type, ( % 2.28/2.48 tptp_fun__i_val_306: $i)). % 2.28/2.48 tff(tptp_fun__i_val_394_type, type, ( % 2.28/2.48 tptp_fun__i_val_394: $i)). % 2.28/2.48 tff(tptp_fun__i_val_290_type, type, ( % 2.28/2.48 tptp_fun__i_val_290: $i)). % 2.28/2.48 tff(tptp_fun__i_val_254_type, type, ( % 2.28/2.48 tptp_fun__i_val_254: $i)). % 2.28/2.48 tff(tptp_fun__i_val_129_type, type, ( % 2.28/2.48 tptp_fun__i_val_129: $i)). % 2.28/2.48 tff(tptp_fun__i_val_397_type, type, ( % 2.28/2.48 tptp_fun__i_val_397: $i)). % 2.28/2.48 tff(tptp_fun__i_val_37_type, type, ( % 2.28/2.48 tptp_fun__i_val_37: $i)). % 2.28/2.48 tff(tptp_fun__i_val_208_type, type, ( % 2.28/2.48 tptp_fun__i_val_208: $i)). % 2.28/2.48 tff(tptp_fun__i_val_97_type, type, ( % 2.28/2.48 tptp_fun__i_val_97: $i)). % 2.28/2.48 tff(tptp_fun__i_val_434_type, type, ( % 2.28/2.48 tptp_fun__i_val_434: $i)). % 2.28/2.48 tff(tptp_fun__i_val_93_type, type, ( % 2.28/2.48 tptp_fun__i_val_93: $i)). % 2.28/2.48 tff(tptp_fun__i_val_147_type, type, ( % 2.28/2.48 tptp_fun__i_val_147: $i)). % 2.28/2.48 tff(tptp_fun__i_val_34_type, type, ( % 2.28/2.48 tptp_fun__i_val_34: $i)). % 2.28/2.48 tff(tptp_fun__i_val_179_type, type, ( % 2.28/2.48 tptp_fun__i_val_179: $i)). % 2.28/2.48 tff(tptp_fun__i_val_427_type, type, ( % 2.28/2.48 tptp_fun__i_val_427: $i)). % 2.28/2.48 tff(tptp_fun__i_val_225_type, type, ( % 2.28/2.48 tptp_fun__i_val_225: $i)). % 2.28/2.48 tff(tptp_fun__i_val_153_type, type, ( % 2.28/2.48 tptp_fun__i_val_153: $i)). % 2.28/2.48 tff(tptp_fun__i_val_277_type, type, ( % 2.28/2.48 tptp_fun__i_val_277: $i)). % 2.28/2.48 tff(tptp_fun__i_val_438_type, type, ( % 2.28/2.48 tptp_fun__i_val_438: $i)). % 2.28/2.48 tff(tptp_fun__i_val_303_type, type, ( % 2.28/2.48 tptp_fun__i_val_303: $i)). % 2.28/2.48 tff(tptp_fun__i_val_192_type, type, ( % 2.28/2.48 tptp_fun__i_val_192: $i)). % 2.28/2.48 tff(tptp_fun__i_val_8_type, type, ( % 2.28/2.48 tptp_fun__i_val_8: $i)). % 2.28/2.48 tff(tptp_fun__i_val_178_type, type, ( % 2.28/2.48 tptp_fun__i_val_178: $i)). % 2.28/2.48 tff(tptp_fun__i_val_125_type, type, ( % 2.28/2.48 tptp_fun__i_val_125: $i)). % 2.28/2.48 tff(tptp_fun__i_val_229_type, type, ( % 2.28/2.48 tptp_fun__i_val_229: $i)). % 2.28/2.48 tff(tptp_fun__i_val_204_type, type, ( % 2.28/2.48 tptp_fun__i_val_204: $i)). % 2.28/2.48 tff(tptp_fun__i_val_339_type, type, ( % 2.28/2.48 tptp_fun__i_val_339: $i)). % 2.28/2.48 tff(tptp_fun__i_val_296_type, type, ( % 2.28/2.48 tptp_fun__i_val_296: $i)). % 2.28/2.48 tff(tptp_fun__i_val_417_type, type, ( % 2.28/2.48 tptp_fun__i_val_417: $i)). % 2.28/2.48 tff(tptp_fun__i_val_368_type, type, ( % 2.28/2.48 tptp_fun__i_val_368: $i)). % 2.28/2.48 tff(tptp_fun__i_val_2_type, type, ( % 2.28/2.48 tptp_fun__i_val_2: $i)). % 2.28/2.48 tff(tptp_fun__i_val_379_type, type, ( % 2.28/2.48 tptp_fun__i_val_379: $i)). % 2.28/2.48 tff(tptp_fun__i_val_234_type, type, ( % 2.28/2.48 tptp_fun__i_val_234: $i)). % 2.28/2.48 tff(tptp_fun__i_val_377_type, type, ( % 2.28/2.48 tptp_fun__i_val_377: $i)). % 2.28/2.48 tff(tptp_fun__i_val_252_type, type, ( % 2.28/2.48 tptp_fun__i_val_252: $i)). % 2.28/2.48 tff(tptp_fun__i_val_69_type, type, ( % 2.28/2.48 tptp_fun__i_val_69: $i)). % 2.28/2.48 tff(tptp_fun__i_val_140_type, type, ( % 2.28/2.48 tptp_fun__i_val_140: $i)). % 2.28/2.48 tff(tptp_fun__i_val_355_type, type, ( % 2.28/2.48 tptp_fun__i_val_355: $i)). % 2.28/2.48 tff(tptp_fun__i_val_160_type, type, ( % 2.28/2.48 tptp_fun__i_val_160: $i)). % 2.28/2.48 tff(tptp_fun__i_val_25_type, type, ( % 2.28/2.48 tptp_fun__i_val_25: $i)). % 2.28/2.48 tff(tptp_fun__i_val_107_type, type, ( % 2.28/2.48 tptp_fun__i_val_107: $i)). % 2.28/2.48 tff(tptp_fun__i_val_392_type, type, ( % 2.28/2.48 tptp_fun__i_val_392: $i)). % 2.28/2.48 tff(tptp_fun__i_val_130_type, type, ( % 2.28/2.48 tptp_fun__i_val_130: $i)). % 2.28/2.48 tff(tptp_fun__i_val_111_type, type, ( % 2.28/2.48 tptp_fun__i_val_111: $i)). % 2.28/2.48 tff(tptp_fun__i_val_357_type, type, ( % 2.28/2.48 tptp_fun__i_val_357: $i)). % 2.28/2.48 tff(tptp_fun__i_val_322_type, type, ( % 2.28/2.48 tptp_fun__i_val_322: $i)). % 2.28/2.48 tff(tptp_fun__i_val_223_type, type, ( % 2.28/2.48 tptp_fun__i_val_223: $i)). % 2.28/2.48 tff(tptp_fun__i_val_164_type, type, ( % 2.28/2.48 tptp_fun__i_val_164: $i)). % 2.28/2.48 tff(tptp_fun__i_val_424_type, type, ( % 2.28/2.48 tptp_fun__i_val_424: $i)). % 2.28/2.48 tff(tptp_fun__i_val_232_type, type, ( % 2.28/2.48 tptp_fun__i_val_232: $i)). % 2.28/2.48 tff(tptp_fun__i_val_220_type, type, ( % 2.28/2.48 tptp_fun__i_val_220: $i)). % 2.28/2.48 tff(tptp_fun__i_val_52_type, type, ( % 2.28/2.48 tptp_fun__i_val_52: $i)). % 2.28/2.48 tff(tptp_fun__i_val_132_type, type, ( % 2.28/2.48 tptp_fun__i_val_132: $i)). % 2.28/2.48 tff(tptp_fun__i_val_411_type, type, ( % 2.28/2.48 tptp_fun__i_val_411: $i)). % 2.28/2.48 tff(tptp_fun__i_val_188_type, type, ( % 2.28/2.48 tptp_fun__i_val_188: $i)). % 2.28/2.48 tff(tptp_fun__i_val_116_type, type, ( % 2.28/2.48 tptp_fun__i_val_116: $i)). % 2.28/2.48 tff(tptp_fun__i_val_210_type, type, ( % 2.28/2.48 tptp_fun__i_val_210: $i)). % 2.28/2.48 tff(tptp_fun__i_val_298_type, type, ( % 2.28/2.48 tptp_fun__i_val_298: $i)). % 2.28/2.48 tff(tptp_fun__i_val_461_type, type, ( % 2.28/2.48 tptp_fun__i_val_461: $i)). % 2.28/2.48 tff(tptp_fun__i_val_351_type, type, ( % 2.28/2.48 tptp_fun__i_val_351: $i)). % 2.28/2.48 tff(tptp_fun__i_val_87_type, type, ( % 2.28/2.48 tptp_fun__i_val_87: $i)). % 2.28/2.48 tff(tptp_fun__i_val_57_type, type, ( % 2.28/2.48 tptp_fun__i_val_57: $i)). % 2.28/2.48 tff(tptp_fun__i_val_440_type, type, ( % 2.28/2.48 tptp_fun__i_val_440: $i)). % 2.28/2.48 tff(tptp_fun__i_val_444_type, type, ( % 2.28/2.48 tptp_fun__i_val_444: $i)). % 2.28/2.48 tff(tptp_fun__i_val_331_type, type, ( % 2.28/2.48 tptp_fun__i_val_331: $i)). % 2.28/2.48 tff(tptp_fun__i_val_163_type, type, ( % 2.28/2.48 tptp_fun__i_val_163: $i)). % 2.28/2.48 tff(tptp_fun__i_val_189_type, type, ( % 2.28/2.48 tptp_fun__i_val_189: $i)). % 2.28/2.48 tff(tptp_fun__i_val_71_type, type, ( % 2.28/2.48 tptp_fun__i_val_71: $i)). % 2.28/2.48 tff(tptp_fun__i_val_190_type, type, ( % 2.28/2.48 tptp_fun__i_val_190: $i)). % 2.28/2.48 tff(tptp_fun__i_val_4_type, type, ( % 2.28/2.48 tptp_fun__i_val_4: $i)). % 2.28/2.48 tff(tptp_fun__i_val_133_type, type, ( % 2.28/2.48 tptp_fun__i_val_133: $i)). % 2.28/2.48 tff(tptp_fun__i_val_55_type, type, ( % 2.28/2.48 tptp_fun__i_val_55: $i)). % 2.28/2.48 tff(tptp_fun__i_val_452_type, type, ( % 2.28/2.48 tptp_fun__i_val_452: $i)). % 2.28/2.48 tff(tptp_fun__i_val_274_type, type, ( % 2.28/2.48 tptp_fun__i_val_274: $i)). % 2.28/2.48 tff(tptp_fun__i_val_297_type, type, ( % 2.28/2.48 tptp_fun__i_val_297: $i)). % 2.28/2.48 tff(tptp_fun__i_val_183_type, type, ( % 2.28/2.48 tptp_fun__i_val_183: $i)). % 2.28/2.48 tff(tptp_fun__i_val_221_type, type, ( % 2.28/2.48 tptp_fun__i_val_221: $i)). % 2.28/2.48 tff(tptp_fun__i_val_141_type, type, ( % 2.28/2.48 tptp_fun__i_val_141: $i)). % 2.28/2.48 tff(tptp_fun__i_val_326_type, type, ( % 2.28/2.48 tptp_fun__i_val_326: $i)). % 2.28/2.48 tff(tptp_fun__i_val_175_type, type, ( % 2.28/2.48 tptp_fun__i_val_175: $i)). % 2.28/2.48 tff(tptp_fun__i_val_187_type, type, ( % 2.28/2.48 tptp_fun__i_val_187: $i)). % 2.28/2.48 tff(tptp_fun__i_val_65_type, type, ( % 2.28/2.48 tptp_fun__i_val_65: $i)). % 2.28/2.48 tff(tptp_fun__i_val_66_type, type, ( % 2.28/2.48 tptp_fun__i_val_66: $i)). % 2.28/2.48 tff(tptp_fun__i_val_304_type, type, ( % 2.28/2.48 tptp_fun__i_val_304: $i)). % 2.28/2.48 tff(tptp_fun__i_val_30_type, type, ( % 2.28/2.48 tptp_fun__i_val_30: $i)). % 2.28/2.48 tff(tptp_fun__i_val_309_type, type, ( % 2.28/2.48 tptp_fun__i_val_309: $i)). % 2.28/2.48 tff(tptp_fun__i_val_121_type, type, ( % 2.28/2.48 tptp_fun__i_val_121: $i)). % 2.28/2.48 tff(tptp_fun__i_val_51_type, type, ( % 2.28/2.48 tptp_fun__i_val_51: $i)). % 2.28/2.48 tff(tptp_fun__i_val_11_type, type, ( % 2.28/2.48 tptp_fun__i_val_11: $i)). % 2.28/2.48 tff(tptp_fun__i_val_203_type, type, ( % 2.28/2.48 tptp_fun__i_val_203: $i)). % 2.28/2.48 tff(tptp_fun__i_val_67_type, type, ( % 2.28/2.48 tptp_fun__i_val_67: $i)). % 2.28/2.48 tff(tptp_fun__i_val_245_type, type, ( % 2.28/2.48 tptp_fun__i_val_245: $i)). % 2.28/2.48 tff(tptp_fun__i_val_131_type, type, ( % 2.28/2.48 tptp_fun__i_val_131: $i)). % 2.28/2.48 tff(tptp_fun__i_val_227_type, type, ( % 2.28/2.48 tptp_fun__i_val_227: $i)). % 2.28/2.48 tff(tptp_fun__i_val_244_type, type, ( % 2.28/2.48 tptp_fun__i_val_244: $i)). % 2.28/2.48 tff(tptp_fun__i_val_344_type, type, ( % 2.28/2.48 tptp_fun__i_val_344: $i)). % 2.28/2.48 tff(tptp_fun__i_val_78_type, type, ( % 2.28/2.48 tptp_fun__i_val_78: $i)). % 2.28/2.48 tff(tptp_fun__i_val_292_type, type, ( % 2.28/2.48 tptp_fun__i_val_292: $i)). % 2.28/2.48 tff(tptp_fun__i_val_294_type, type, ( % 2.28/2.48 tptp_fun__i_val_294: $i)). % 2.28/2.48 tff(tptp_fun__i_val_168_type, type, ( % 2.28/2.48 tptp_fun__i_val_168: $i)). % 2.28/2.48 tff(tptp_fun__i_val_75_type, type, ( % 2.28/2.48 tptp_fun__i_val_75: $i)). % 2.28/2.48 tff(tptp_fun__i_val_144_type, type, ( % 2.28/2.48 tptp_fun__i_val_144: $i)). % 2.28/2.48 tff(tptp_fun__i_val_6_type, type, ( % 2.28/2.48 tptp_fun__i_val_6: $i)). % 2.28/2.48 tff(tptp_fun__i_val_376_type, type, ( % 2.28/2.48 tptp_fun__i_val_376: $i)). % 2.28/2.48 tff(tptp_fun__i_val_21_type, type, ( % 2.28/2.48 tptp_fun__i_val_21: $i)). % 2.28/2.48 tff(tptp_fun__i_val_135_type, type, ( % 2.28/2.48 tptp_fun__i_val_135: $i)). % 2.28/2.48 tff(tptp_fun__i_val_459_type, type, ( % 2.28/2.48 tptp_fun__i_val_459: $i)). % 2.28/2.48 tff(tptp_fun__i_val_134_type, type, ( % 2.28/2.48 tptp_fun__i_val_134: $i)). % 2.28/2.48 tff(tptp_fun__i_val_246_type, type, ( % 2.28/2.48 tptp_fun__i_val_246: $i)). % 2.28/2.48 tff(tptp_fun__i_val_73_type, type, ( % 2.28/2.48 tptp_fun__i_val_73: $i)). % 2.28/2.48 tff(tptp_fun__i_val_375_type, type, ( % 2.28/2.48 tptp_fun__i_val_375: $i)). % 2.28/2.48 tff(tptp_fun__i_val_447_type, type, ( % 2.28/2.48 tptp_fun__i_val_447: $i)). % 2.28/2.48 tff(tptp_fun__i_val_154_type, type, ( % 2.28/2.48 tptp_fun__i_val_154: $i)). % 2.28/2.48 tff(tptp_fun__i_val_217_type, type, ( % 2.28/2.48 tptp_fun__i_val_217: $i)). % 2.28/2.48 tff(tptp_fun__i_val_354_type, type, ( % 2.28/2.48 tptp_fun__i_val_354: $i)). % 2.28/2.48 tff(tptp_fun__i_val_92_type, type, ( % 2.28/2.48 tptp_fun__i_val_92: $i)). % 2.28/2.48 tff(tptp_fun__i_val_120_type, type, ( % 2.28/2.48 tptp_fun__i_val_120: $i)). % 2.28/2.48 tff(tptp_fun__i_val_340_type, type, ( % 2.28/2.48 tptp_fun__i_val_340: $i)). % 2.28/2.48 tff(tptp_fun__i_val_33_type, type, ( % 2.28/2.48 tptp_fun__i_val_33: $i)). % 2.28/2.48 tff(tptp_fun__i_val_409_type, type, ( % 2.28/2.48 tptp_fun__i_val_409: $i)). % 2.28/2.48 tff(tptp_fun__i_val_237_type, type, ( % 2.28/2.48 tptp_fun__i_val_237: $i)). % 2.28/2.48 tff(tptp_fun__i_val_256_type, type, ( % 2.28/2.48 tptp_fun__i_val_256: $i)). % 2.28/2.48 tff(tptp_fun__i_val_259_type, type, ( % 2.28/2.48 tptp_fun__i_val_259: $i)). % 2.28/2.48 tff(tptp_fun__i_val_325_type, type, ( % 2.28/2.48 tptp_fun__i_val_325: $i)). % 2.28/2.48 tff(tptp_fun__i_val_128_type, type, ( % 2.28/2.48 tptp_fun__i_val_128: $i)). % 2.28/2.48 tff(tptp_fun__i_val_197_type, type, ( % 2.28/2.48 tptp_fun__i_val_197: $i)). % 2.28/2.48 tff(tptp_fun__i_val_31_type, type, ( % 2.28/2.48 tptp_fun__i_val_31: $i)). % 2.28/2.48 tff(tptp_fun__i_val_365_type, type, ( % 2.28/2.48 tptp_fun__i_val_365: $i)). % 2.28/2.48 tff(tptp_fun__i_val_346_type, type, ( % 2.28/2.48 tptp_fun__i_val_346: $i)). % 2.28/2.48 tff(tptp_fun__i_val_268_type, type, ( % 2.28/2.48 tptp_fun__i_val_268: $i)). % 2.28/2.48 tff(tptp_fun__i_val_349_type, type, ( % 2.28/2.48 tptp_fun__i_val_349: $i)). % 2.28/2.48 tff(tptp_fun__i_val_218_type, type, ( % 2.28/2.48 tptp_fun__i_val_218: $i)). % 2.28/2.48 tff(tptp_fun__i_val_7_type, type, ( % 2.28/2.48 tptp_fun__i_val_7: $i)). % 2.28/2.48 tff(tptp_fun__i_val_446_type, type, ( % 2.28/2.48 tptp_fun__i_val_446: $i)). % 2.28/2.48 tff(tptp_fun__i_val_158_type, type, ( % 2.28/2.48 tptp_fun__i_val_158: $i)). % 2.28/2.48 tff(tptp_fun__i_val_79_type, type, ( % 2.28/2.48 tptp_fun__i_val_79: $i)). % 2.28/2.48 tff(tptp_fun__i_val_96_type, type, ( % 2.28/2.48 tptp_fun__i_val_96: $i)). % 2.28/2.48 tff(tptp_fun__i_val_47_type, type, ( % 2.28/2.48 tptp_fun__i_val_47: $i)). % 2.28/2.48 tff(tptp_fun__i_val_456_type, type, ( % 2.28/2.48 tptp_fun__i_val_456: $i)). % 2.28/2.48 tff(tptp_fun__i_val_19_type, type, ( % 2.28/2.48 tptp_fun__i_val_19: $i)). % 2.28/2.48 tff(tptp_fun__i_val_435_type, type, ( % 2.28/2.48 tptp_fun__i_val_435: $i)). % 2.28/2.48 tff(tptp_fun__i_val_157_type, type, ( % 2.28/2.48 tptp_fun__i_val_157: $i)). % 2.28/2.48 tff(tptp_fun__i_val_176_type, type, ( % 2.28/2.48 tptp_fun__i_val_176: $i)). % 2.28/2.48 tff(tptp_fun__i_val_374_type, type, ( % 2.28/2.48 tptp_fun__i_val_374: $i)). % 2.28/2.48 tff(tptp_fun__i_val_206_type, type, ( % 2.28/2.48 tptp_fun__i_val_206: $i)). % 2.28/2.48 tff(tptp_fun__i_val_123_type, type, ( % 2.28/2.48 tptp_fun__i_val_123: $i)). % 2.28/2.48 tff(tptp_fun__i_val_114_type, type, ( % 2.28/2.48 tptp_fun__i_val_114: $i)). % 2.28/2.48 tff(tptp_fun__i_val_460_type, type, ( % 2.28/2.48 tptp_fun__i_val_460: $i)). % 2.28/2.48 tff(tptp_fun__i_val_109_type, type, ( % 2.28/2.48 tptp_fun__i_val_109: $i)). % 2.28/2.48 tff(tptp_fun__i_val_419_type, type, ( % 2.28/2.48 tptp_fun__i_val_419: $i)). % 2.28/2.48 tff(tptp_fun__i_val_454_type, type, ( % 2.28/2.48 tptp_fun__i_val_454: $i)). % 2.28/2.48 tff(tptp_fun__i_val_41_type, type, ( % 2.28/2.48 tptp_fun__i_val_41: $i)). % 2.28/2.48 tff(tptp_fun__i_val_185_type, type, ( % 2.28/2.48 tptp_fun__i_val_185: $i)). % 2.28/2.48 tff(tptp_fun__i_val_239_type, type, ( % 2.28/2.48 tptp_fun__i_val_239: $i)). % 2.28/2.48 tff(tptp_fun__i_val_186_type, type, ( % 2.28/2.48 tptp_fun__i_val_186: $i)). % 2.28/2.48 tff(tptp_fun__i_val_151_type, type, ( % 2.28/2.48 tptp_fun__i_val_151: $i)). % 2.28/2.48 tff(tptp_fun__i_val_207_type, type, ( % 2.28/2.48 tptp_fun__i_val_207: $i)). % 2.28/2.48 tff(tptp_fun__i_val_289_type, type, ( % 2.28/2.48 tptp_fun__i_val_289: $i)). % 2.28/2.48 tff(tptp_fun__i_val_445_type, type, ( % 2.28/2.48 tptp_fun__i_val_445: $i)). % 2.28/2.48 tff(tptp_fun__i_val_402_type, type, ( % 2.28/2.48 tptp_fun__i_val_402: $i)). % 2.28/2.48 tff(tptp_fun__i_val_76_type, type, ( % 2.28/2.48 tptp_fun__i_val_76: $i)). % 2.28/2.48 tff(tptp_fun__i_val_171_type, type, ( % 2.28/2.48 tptp_fun__i_val_171: $i)). % 2.28/2.48 tff(tptp_fun__i_val_58_type, type, ( % 2.28/2.48 tptp_fun__i_val_58: $i)). % 2.28/2.48 tff(tptp_fun__i_val_219_type, type, ( % 2.28/2.48 tptp_fun__i_val_219: $i)). % 2.28/2.48 tff(tptp_fun__i_val_43_type, type, ( % 2.28/2.48 tptp_fun__i_val_43: $i)). % 2.28/2.48 tff(tptp_fun__i_val_342_type, type, ( % 2.28/2.48 tptp_fun__i_val_342: $i)). % 2.28/2.48 tff(tptp_fun__i_val_110_type, type, ( % 2.28/2.48 tptp_fun__i_val_110: $i)). % 2.28/2.48 tff(tptp_fun__i_val_338_type, type, ( % 2.28/2.48 tptp_fun__i_val_338: $i)). % 2.28/2.48 tff(tptp_fun__i_val_263_type, type, ( % 2.28/2.48 tptp_fun__i_val_263: $i)). % 2.28/2.48 tff(tptp_fun__i_val_136_type, type, ( % 2.28/2.48 tptp_fun__i_val_136: $i)). % 2.28/2.48 tff(tptp_fun__i_val_358_type, type, ( % 2.28/2.48 tptp_fun__i_val_358: $i)). % 2.28/2.48 tff(tptp_fun__i_val_363_type, type, ( % 2.28/2.48 tptp_fun__i_val_363: $i)). % 2.28/2.48 tff(tptp_fun__i_val_347_type, type, ( % 2.28/2.48 tptp_fun__i_val_347: $i)). % 2.28/2.48 tff(tptp_fun__i_val_341_type, type, ( % 2.28/2.48 tptp_fun__i_val_341: $i)). % 2.28/2.48 tff(tptp_fun__i_val_364_type, type, ( % 2.28/2.48 tptp_fun__i_val_364: $i)). % 2.28/2.48 tff(tptp_fun__i_val_172_type, type, ( % 2.28/2.48 tptp_fun__i_val_172: $i)). % 2.28/2.48 tff(tptp_fun__i_val_155_type, type, ( % 2.28/2.48 tptp_fun__i_val_155: $i)). % 2.28/2.48 tff(tptp_fun__i_val_212_type, type, ( % 2.28/2.48 tptp_fun__i_val_212: $i)). % 2.28/2.48 tff(tptp_fun__i_val_42_type, type, ( % 2.28/2.48 tptp_fun__i_val_42: $i)). % 2.28/2.48 tff(tptp_fun__i_val_328_type, type, ( % 2.28/2.48 tptp_fun__i_val_328: $i)). % 2.28/2.48 tff(tptp_fun__i_val_280_type, type, ( % 2.28/2.48 tptp_fun__i_val_280: $i)). % 2.28/2.48 tff(tptp_fun__i_val_262_type, type, ( % 2.28/2.48 tptp_fun__i_val_262: $i)). % 2.28/2.48 tff(tptp_fun__i_val_398_type, type, ( % 2.28/2.48 tptp_fun__i_val_398: $i)). % 2.28/2.48 tff(tptp_fun__i_val_383_type, type, ( % 2.28/2.48 tptp_fun__i_val_383: $i)). % 2.28/2.48 tff(tptp_fun__i_val_90_type, type, ( % 2.28/2.48 tptp_fun__i_val_90: $i)). % 2.28/2.48 tff(tptp_fun__i_val_318_type, type, ( % 2.28/2.48 tptp_fun__i_val_318: $i)). % 2.28/2.48 tff(tptp_fun__i_val_174_type, type, ( % 2.28/2.48 tptp_fun__i_val_174: $i)). % 2.28/2.48 tff(tptp_fun__i_val_319_type, type, ( % 2.28/2.48 tptp_fun__i_val_319: $i)). % 2.28/2.48 tff(tptp_fun__i_val_74_type, type, ( % 2.28/2.48 tptp_fun__i_val_74: $i)). % 2.28/2.48 tff(tptp_fun__i_val_201_type, type, ( % 2.28/2.48 tptp_fun__i_val_201: $i)). % 2.28/2.48 tff(tptp_fun__i_val_371_type, type, ( % 2.28/2.48 tptp_fun__i_val_371: $i)). % 2.28/2.48 tff(tptp_fun__i_val_199_type, type, ( % 2.28/2.48 tptp_fun__i_val_199: $i)). % 2.28/2.48 tff(tptp_fun__i_val_180_type, type, ( % 2.28/2.48 tptp_fun__i_val_180: $i)). % 2.28/2.48 tff(tptp_fun__i_val_214_type, type, ( % 2.28/2.48 tptp_fun__i_val_214: $i)). % 2.28/2.48 tff(tptp_fun__i_val_352_type, type, ( % 2.28/2.48 tptp_fun__i_val_352: $i)). % 2.28/2.48 tff(tptp_fun__i_val_240_type, type, ( % 2.28/2.48 tptp_fun__i_val_240: $i)). % 2.28/2.48 tff(tptp_fun__i_val_53_type, type, ( % 2.28/2.48 tptp_fun__i_val_53: $i)). % 2.28/2.48 tff(tptp_fun__i_val_273_type, type, ( % 2.28/2.48 tptp_fun__i_val_273: $i)). % 2.28/2.48 tff(tptp_fun__i_val_291_type, type, ( % 2.28/2.48 tptp_fun__i_val_291: $i)). % 2.28/2.48 tff(tptp_fun__i_val_49_type, type, ( % 2.28/2.48 tptp_fun__i_val_49: $i)). % 2.28/2.48 tff(tptp_fun__i_val_311_type, type, ( % 2.28/2.48 tptp_fun__i_val_311: $i)). % 2.28/2.48 tff(tptp_fun__i_val_126_type, type, ( % 2.28/2.48 tptp_fun__i_val_126: $i)). % 2.28/2.48 tff(tptp_fun__i_val_360_type, type, ( % 2.28/2.48 tptp_fun__i_val_360: $i)). % 2.28/2.48 tff(tptp_fun__i_val_15_type, type, ( % 2.28/2.48 tptp_fun__i_val_15: $i)). % 2.28/2.48 tff(tptp_fun__i_val_283_type, type, ( % 2.28/2.48 tptp_fun__i_val_283: $i)). % 2.28/2.48 tff(tptp_fun__i_val_403_type, type, ( % 2.28/2.48 tptp_fun__i_val_403: $i)). % 2.28/2.48 tff(tptp_fun__i_val_215_type, type, ( % 2.28/2.48 tptp_fun__i_val_215: $i)). % 2.28/2.48 tff(tptp_fun__i_val_308_type, type, ( % 2.28/2.48 tptp_fun__i_val_308: $i)). % 2.28/2.48 tff(tptp_fun__i_val_295_type, type, ( % 2.28/2.48 tptp_fun__i_val_295: $i)). % 2.28/2.48 tff(tptp_fun__i_val_391_type, type, ( % 2.28/2.48 tptp_fun__i_val_391: $i)). % 2.28/2.48 tff(tptp_fun__i_val_228_type, type, ( % 2.28/2.48 tptp_fun__i_val_228: $i)). % 2.28/2.48 tff(tptp_fun__i_val_413_type, type, ( % 2.28/2.48 tptp_fun__i_val_413: $i)). % 2.28/2.48 tff(tptp_fun__i_val_28_type, type, ( % 2.28/2.48 tptp_fun__i_val_28: $i)). % 2.28/2.48 tff(tptp_fun__i_val_3_type, type, ( % 2.28/2.48 tptp_fun__i_val_3: $i)). % 2.28/2.48 tff(tptp_fun__i_val_390_type, type, ( % 2.28/2.48 tptp_fun__i_val_390: $i)). % 2.28/2.48 tff(tptp_fun__i_val_195_type, type, ( % 2.28/2.48 tptp_fun__i_val_195: $i)). % 2.28/2.48 tff(tptp_fun__i_val_112_type, type, ( % 2.28/2.48 tptp_fun__i_val_112: $i)). % 2.28/2.48 tff(tptp_fun__i_val_213_type, type, ( % 2.28/2.48 tptp_fun__i_val_213: $i)). % 2.28/2.48 tff(tptp_fun__i_val_62_type, type, ( % 2.28/2.48 tptp_fun__i_val_62: $i)). % 2.28/2.48 tff(tptp_fun__i_val_230_type, type, ( % 2.28/2.48 tptp_fun__i_val_230: $i)). % 2.28/2.48 tff(tptp_fun__i_val_10_type, type, ( % 2.28/2.48 tptp_fun__i_val_10: $i)). % 2.28/2.48 tff(tptp_fun__i_val_191_type, type, ( % 2.28/2.48 tptp_fun__i_val_191: $i)). % 2.28/2.48 tff(tptp_fun__i_val_169_type, type, ( % 2.28/2.48 tptp_fun__i_val_169: $i)). % 2.28/2.48 tff(tptp_fun__i_val_113_type, type, ( % 2.28/2.48 tptp_fun__i_val_113: $i)). % 2.28/2.48 tff(tptp_fun__i_val_286_type, type, ( % 2.28/2.48 tptp_fun__i_val_286: $i)). % 2.28/2.48 tff(tptp_fun__i_val_124_type, type, ( % 2.28/2.48 tptp_fun__i_val_124: $i)). % 2.28/2.48 tff(tptp_fun__i_val_161_type, type, ( % 2.28/2.48 tptp_fun__i_val_161: $i)). % 2.28/2.48 tff(tptp_fun__i_val_166_type, type, ( % 2.28/2.48 tptp_fun__i_val_166: $i)). % 2.28/2.48 tff(tptp_fun__i_val_285_type, type, ( % 2.28/2.48 tptp_fun__i_val_285: $i)). % 2.28/2.48 tff(tptp_fun__i_val_18_type, type, ( % 2.28/2.48 tptp_fun__i_val_18: $i)). % 2.28/2.48 tff(tptp_fun__i_val_428_type, type, ( % 2.28/2.48 tptp_fun__i_val_428: $i)). % 2.28/2.48 tff(tptp_fun__i_val_56_type, type, ( % 2.28/2.48 tptp_fun__i_val_56: $i)). % 2.28/2.48 tff(tptp_fun__i_val_272_type, type, ( % 2.28/2.48 tptp_fun__i_val_272: $i)). % 2.28/2.48 tff(tptp_fun__i_val_320_type, type, ( % 2.28/2.48 tptp_fun__i_val_320: $i)). % 2.28/2.48 tff(tptp_fun__i_val_119_type, type, ( % 2.28/2.48 tptp_fun__i_val_119: $i)). % 2.28/2.48 tff(tptp_fun__i_val_142_type, type, ( % 2.28/2.48 tptp_fun__i_val_142: $i)). % 2.28/2.48 tff(tptp_fun__i_val_455_type, type, ( % 2.28/2.48 tptp_fun__i_val_455: $i)). % 2.28/2.48 tff(tptp_fun__i_val_395_type, type, ( % 2.28/2.48 tptp_fun__i_val_395: $i)). % 2.28/2.48 tff(tptp_fun__i_val_50_type, type, ( % 2.28/2.48 tptp_fun__i_val_50: $i)). % 2.28/2.48 tff(tptp_fun__i_val_330_type, type, ( % 2.28/2.48 tptp_fun__i_val_330: $i)). % 2.28/2.48 tff(tptp_fun__i_val_329_type, type, ( % 2.28/2.48 tptp_fun__i_val_329: $i)). % 2.28/2.48 tff(tptp_fun__i_val_393_type, type, ( % 2.28/2.48 tptp_fun__i_val_393: $i)). % 2.28/2.48 tff(tptp_fun__i_val_137_type, type, ( % 2.28/2.48 tptp_fun__i_val_137: $i)). % 2.28/2.48 tff(tptp_fun__i_val_385_type, type, ( % 2.28/2.48 tptp_fun__i_val_385: $i)). % 2.28/2.48 tff(tptp_fun__i_val_257_type, type, ( % 2.28/2.48 tptp_fun__i_val_257: $i)). % 2.28/2.48 tff(tptp_fun__i_val_9_type, type, ( % 2.28/2.48 tptp_fun__i_val_9: $i)). % 2.28/2.48 tff(tptp_fun__i_val_16_type, type, ( % 2.28/2.48 tptp_fun__i_val_16: $i)). % 2.28/2.48 tff(tptp_fun__i_val_22_type, type, ( % 2.28/2.48 tptp_fun__i_val_22: $i)). % 2.28/2.48 tff(tptp_fun__i_val_284_type, type, ( % 2.28/2.48 tptp_fun__i_val_284: $i)). % 2.28/2.48 tff(tptp_fun__i_val_209_type, type, ( % 2.28/2.48 tptp_fun__i_val_209: $i)). % 2.28/2.48 tff(tptp_fun__i_val_356_type, type, ( % 2.28/2.48 tptp_fun__i_val_356: $i)). % 2.28/2.48 tff(tptp_fun__i_val_407_type, type, ( % 2.28/2.48 tptp_fun__i_val_407: $i)). % 2.28/2.48 tff(tptp_fun__i_val_345_type, type, ( % 2.28/2.48 tptp_fun__i_val_345: $i)). % 2.28/2.48 tff(tptp_fun__i_val_173_type, type, ( % 2.28/2.48 tptp_fun__i_val_173: $i)). % 2.28/2.48 tff(tptp_fun__i_val_396_type, type, ( % 2.28/2.48 tptp_fun__i_val_396: $i)). % 2.28/2.48 tff(tptp_fun__i_val_226_type, type, ( % 2.28/2.48 tptp_fun__i_val_226: $i)). % 2.28/2.48 tff(tptp_fun__i_val_152_type, type, ( % 2.28/2.48 tptp_fun__i_val_152: $i)). % 2.28/2.48 tff(tptp_fun__i_val_381_type, type, ( % 2.28/2.48 tptp_fun__i_val_381: $i)). % 2.28/2.48 tff(tptp_fun__i_val_82_type, type, ( % 2.28/2.48 tptp_fun__i_val_82: $i)). % 2.28/2.48 tff(tptp_fun__i_val_350_type, type, ( % 2.28/2.48 tptp_fun__i_val_350: $i)). % 2.28/2.48 tff(tptp_fun__i_val_414_type, type, ( % 2.28/2.48 tptp_fun__i_val_414: $i)). % 2.28/2.48 tff(tptp_fun__i_val_334_type, type, ( % 2.28/2.48 tptp_fun__i_val_334: $i)). % 2.28/2.48 tff(tptp_fun__i_val_35_type, type, ( % 2.28/2.48 tptp_fun__i_val_35: $i)). % 2.28/2.48 tff(tptp_fun__i_val_359_type, type, ( % 2.28/2.48 tptp_fun__i_val_359: $i)). % 2.28/2.48 tff(tptp_fun__i_val_167_type, type, ( % 2.28/2.48 tptp_fun__i_val_167: $i)). % 2.28/2.48 tff(tptp_fun__i_val_117_type, type, ( % 2.28/2.48 tptp_fun__i_val_117: $i)). % 2.28/2.48 tff(tptp_fun__i_val_194_type, type, ( % 2.28/2.48 tptp_fun__i_val_194: $i)). % 2.28/2.48 tff(tptp_fun__i_val_88_type, type, ( % 2.28/2.48 tptp_fun__i_val_88: $i)). % 2.28/2.48 tff(tptp_fun__i_val_193_type, type, ( % 2.28/2.48 tptp_fun__i_val_193: $i)). % 2.28/2.48 tff(tptp_fun__i_val_267_type, type, ( % 2.28/2.48 tptp_fun__i_val_267: $i)). % 2.28/2.48 tff(tptp_fun__i_val_149_type, type, ( % 2.28/2.48 tptp_fun__i_val_149: $i)). % 2.28/2.48 tff(tptp_fun__i_val_373_type, type, ( % 2.28/2.48 tptp_fun__i_val_373: $i)). % 2.28/2.48 tff(tptp_fun__i_val_162_type, type, ( % 2.28/2.48 tptp_fun__i_val_162: $i)). % 2.28/2.48 tff(tptp_fun__i_val_241_type, type, ( % 2.28/2.48 tptp_fun__i_val_241: $i)). % 2.28/2.48 tff(tptp_fun__i_val_307_type, type, ( % 2.28/2.48 tptp_fun__i_val_307: $i)). % 2.28/2.48 tff(tptp_fun__i_val_436_type, type, ( % 2.28/2.48 tptp_fun__i_val_436: $i)). % 2.28/2.48 tff(tptp_fun__i_val_184_type, type, ( % 2.28/2.48 tptp_fun__i_val_184: $i)). % 2.28/2.48 tff(tptp_fun__i_val_287_type, type, ( % 2.28/2.48 tptp_fun__i_val_287: $i)). % 2.28/2.48 tff(tptp_fun__i_val_159_type, type, ( % 2.28/2.48 tptp_fun__i_val_159: $i)). % 2.28/2.48 tff(tptp_fun__i_val_115_type, type, ( % 2.28/2.48 tptp_fun__i_val_115: $i)). % 2.28/2.48 tff(tptp_fun__i_val_305_type, type, ( % 2.28/2.48 tptp_fun__i_val_305: $i)). % 2.28/2.48 tff(tptp_fun__i_val_431_type, type, ( % 2.28/2.48 tptp_fun__i_val_431: $i)). % 2.28/2.48 tff(tptp_fun__i_val_104_type, type, ( % 2.28/2.48 tptp_fun__i_val_104: $i)). % 2.28/2.48 tff(tptp_fun__i_val_91_type, type, ( % 2.28/2.48 tptp_fun__i_val_91: $i)). % 2.28/2.48 tff(tptp_fun__i_val_416_type, type, ( % 2.28/2.48 tptp_fun__i_val_416: $i)). % 2.28/2.48 tff(tptp_fun__i_val_29_type, type, ( % 2.28/2.48 tptp_fun__i_val_29: $i)). % 2.28/2.48 tff(tptp_fun__i_val_233_type, type, ( % 2.28/2.48 tptp_fun__i_val_233: $i)). % 2.28/2.48 tff(tptp_fun__i_val_367_type, type, ( % 2.28/2.48 tptp_fun__i_val_367: $i)). % 2.28/2.48 tff(tptp_fun__i_val_14_type, type, ( % 2.28/2.48 tptp_fun__i_val_14: $i)). % 2.28/2.48 tff(tptp_fun__i_val_24_type, type, ( % 2.28/2.48 tptp_fun__i_val_24: $i)). % 2.28/2.48 tff(tptp_fun__i_val_122_type, type, ( % 2.28/2.48 tptp_fun__i_val_122: $i)). % 2.28/2.48 tff(tptp_fun__i_val_288_type, type, ( % 2.28/2.48 tptp_fun__i_val_288: $i)). % 2.28/2.48 tff(tptp_fun__i_val_405_type, type, ( % 2.28/2.48 tptp_fun__i_val_405: $i)). % 2.28/2.48 tff(tptp_fun__i_val_5_type, type, ( % 2.28/2.48 tptp_fun__i_val_5: $i)). % 2.28/2.48 tff(tptp_fun__i_val_200_type, type, ( % 2.28/2.48 tptp_fun__i_val_200: $i)). % 2.28/2.48 tff(tptp_fun__i_val_430_type, type, ( % 2.28/2.48 tptp_fun__i_val_430: $i)). % 2.28/2.48 tff(tptp_fun__i_val_437_type, type, ( % 2.28/2.48 tptp_fun__i_val_437: $i)). % 2.28/2.48 tff(tptp_fun__i_val_353_type, type, ( % 2.28/2.48 tptp_fun__i_val_353: $i)). % 2.28/2.48 tff(tptp_fun__i_val_224_type, type, ( % 2.28/2.48 tptp_fun__i_val_224: $i)). % 2.28/2.48 tff(tptp_fun__i_val_348_type, type, ( % 2.28/2.48 tptp_fun__i_val_348: $i)). % 2.28/2.48 tff(tptp_fun__i_val_457_type, type, ( % 2.28/2.48 tptp_fun__i_val_457: $i)). % 2.28/2.48 tff(b48_buttercup10422_type, type, ( % 2.28/2.48 b48_buttercup10422: $i > $o)). % 2.28/2.48 tff(k04_buttercup10639_type, type, ( % 2.28/2.48 k04_buttercup10639: $i > $o)). % 2.28/2.48 tff(b48_buttercup10098_type, type, ( % 2.28/2.48 b48_buttercup10098: $i > $o)). % 2.28/2.48 tff(b48_buttercup10358_type, type, ( % 2.28/2.48 b48_buttercup10358: $i > $o)). % 2.28/2.48 tff(b48_buttercup10170_type, type, ( % 2.28/2.48 b48_buttercup10170: $i > $o)). % 2.28/2.48 tff(b48_buttercup10052_type, type, ( % 2.28/2.48 b48_buttercup10052: $i > $o)). % 2.28/2.48 tff(b48_buttercup10191_type, type, ( % 2.28/2.48 b48_buttercup10191: $i > $o)). % 2.28/2.48 tff(k04_buttercup10096_type, type, ( % 2.28/2.48 k04_buttercup10096: $i > $o)). % 2.28/2.48 tff(b48_buttercup10405_type, type, ( % 2.28/2.48 b48_buttercup10405: $i > $o)). % 2.28/2.48 tff(k04_buttercup10506_type, type, ( % 2.28/2.48 k04_buttercup10506: $i > $o)). % 2.28/2.48 tff(k04_buttercup10406_type, type, ( % 2.28/2.48 k04_buttercup10406: $i > $o)). % 2.28/2.48 tff(b48_buttercup10579_type, type, ( % 2.28/2.48 b48_buttercup10579: $i > $o)). % 2.28/2.48 tff(b48_buttercup10572_type, type, ( % 2.28/2.48 b48_buttercup10572: $i > $o)). % 2.28/2.48 tff(b48_buttercup10458_type, type, ( % 2.28/2.48 b48_buttercup10458: $i > $o)). % 2.28/2.48 tff(b48_buttercup10179_type, type, ( % 2.28/2.48 b48_buttercup10179: $i > $o)). % 2.28/2.48 tff(b48_buttercup10352_type, type, ( % 2.28/2.48 b48_buttercup10352: $i > $o)). % 2.28/2.48 tff(k04_buttercup10517_type, type, ( % 2.28/2.48 k04_buttercup10517: $i > $o)). % 2.28/2.48 tff(k04_buttercup10206_type, type, ( % 2.28/2.48 k04_buttercup10206: $i > $o)). % 2.28/2.48 tff(b48_buttercup10058_type, type, ( % 2.28/2.48 b48_buttercup10058: $i > $o)). % 2.28/2.48 tff(formula1, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10464(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!12))))). % 2.28/2.48 tff(formula2, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10440(X0) <=> (~(k!513(X0) = $i!val!63)))). % 2.28/2.48 tff(formula3, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10320(X0) <=> (k!513(X0) = $i!val!366))). % 2.28/2.48 tff(formula4, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10535(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula5, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10421(X0) <=> ((k!513(X0) = $i!val!148) | (k!513(X0) = $i!val!270)))). % 2.28/2.48 tff(formula6, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10559(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula7, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10365(X0) <=> $true)). % 2.28/2.48 tff(formula8, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10513(X0) <=> $true)). % 2.28/2.48 tff(formula9, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10318(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula10, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10269(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula11, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10332(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula12, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10427(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula13, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10231(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula14, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10604(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula15, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10425(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula16, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10531(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula17, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10473(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula18, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10482(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula19, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10247(X0) <=> $true)). % 2.28/2.48 tff(formula20, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10514(X0) <=> $true)). % 2.28/2.48 tff(formula21, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10271(X0) <=> $true)). % 2.28/2.48 tff(formula22, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10326(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula23, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10225(X0) <=> ((~(k!513(X0) = $i!val!94)) & (~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!83))))). % 2.28/2.48 tff(formula24, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10029(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!70))))). % 2.28/2.48 tff(formula25, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10490(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula26, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10084(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula27, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10371(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula28, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10064(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula29, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10424(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula30, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10167(X0) <=> (k!513(X0) = $i!val!248))). % 2.28/2.48 tff(formula31, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10279(X0) <=> $true)). % 2.28/2.48 tff(formula32, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10631(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula33, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10586(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula34, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10244(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula35, axiom, % 2.28/2.48 b48_buttercup10460($i!val!314) <=> $true). % 2.28/2.48 tff(formula36, axiom, % 2.28/2.48 b48_buttercup10460($i!val!150) <=> $true). % 2.28/2.48 tff(formula37, axiom, % 2.28/2.48 b48_buttercup10460($i!val!48) <=> $false). % 2.28/2.48 tff(formula38, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!314 = X0)) | (($i!val!150 = X0)) | (($i!val!48 = X0)))) => (b48_buttercup10460(X0) <=> k04_buttercup10462(X0)))). % 2.28/2.48 tff(formula39, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10061(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula40, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10351(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula41, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10076(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula42, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10487(X0) <=> (k!513(X0) = $i!val!361))). % 2.28/2.48 tff(formula43, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10470(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula44, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10143(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula45, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10186(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula46, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10121(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula47, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10120(X0) <=> (k!513(X0) = $i!val!362))). % 2.28/2.48 tff(formula48, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10267(X0) <=> $true)). % 2.28/2.48 tff(formula49, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10082(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula50, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10173(X0) <=> (k!513(X0) = $i!val!275))). % 2.28/2.48 tff(formula51, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10161(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula52, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10159(X0) <=> (k!513(X0) = $i!val!335))). % 2.28/2.48 tff(formula53, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10180(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula54, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10437(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula55, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10303(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula56, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10386(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula57, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10050(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula58, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10276(X0) <=> $true)). % 2.28/2.48 tff(formula59, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10274(X0) <=> $true)). % 2.28/2.48 tff(formula60, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10400(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula61, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10561(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula62, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10289(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula63, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10602(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula64, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10632(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula65, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10039(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula66, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10051(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula67, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10542(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula68, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10132(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula69, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10391(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula70, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10293(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula71, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10552(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula72, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10398(X0) <=> (k!513(X0) = $i!val!337))). % 2.28/2.48 tff(formula73, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10240(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula74, axiom, % 2.28/2.48 k04_buttercup10044($i!val!106) <=> $true). % 2.28/2.48 tff(formula75, axiom, % 2.28/2.48 k04_buttercup10044($i!val!253) <=> $true). % 2.28/2.48 tff(formula76, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!106 = X0)) | (($i!val!253 = X0)))) => (k04_buttercup10044(X0) <=> b48_buttercup10043(X0)))). % 2.28/2.48 tff(formula77, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10530(X0) <=> $true)). % 2.28/2.48 tff(formula78, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10637(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula79, axiom, % 2.28/2.48 k04_buttercup10357($i!val!238) <=> $true). % 2.28/2.48 tff(formula80, axiom, % 2.28/2.48 k04_buttercup10357($i!val!264) <=> $true). % 2.28/2.48 tff(formula81, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!238 = X0)) | (($i!val!264 = X0)))) => (k04_buttercup10357(X0) <=> b48_buttercup10361(X0)))). % 2.28/2.48 tff(formula82, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10434(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula83, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10117(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula84, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10045(X0) <=> $true)). % 2.28/2.48 tff(formula85, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10385(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula86, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10334(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!32))))). % 2.28/2.48 tff(formula87, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10478(X0) <=> (k!513(X0) = $i!val!281))). % 2.28/2.48 tff(formula88, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10606(X0) <=> $true)). % 2.28/2.48 tff(formula89, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10214(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!81))))). % 2.28/2.48 tff(formula90, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10181(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula91, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10383(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula92, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10359(X0) <=> $true)). % 2.28/2.48 tff(formula93, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10125(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula94, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10046(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula95, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10026(X0) <=> ((~(k!513(X0) = $i!val!70)) & (~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!17)) & (~(k!513(X0) = $i!val!13))))). % 2.28/2.48 tff(formula96, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10342(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula97, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10495(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula98, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10454(X0) <=> (k!513(X0) = $i!val!429))). % 2.28/2.48 tff(formula99, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10316(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula100, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10369(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula101, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10477(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula102, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10462(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula103, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10182(X0) <=> $true)). % 2.28/2.48 tff(formula104, axiom, % 2.28/2.48 b48_buttercup10451($i!val!449) <=> $true). % 2.28/2.48 tff(formula105, axiom, % 2.28/2.48 b48_buttercup10451($i!val!236) <=> $true). % 2.28/2.48 tff(formula106, axiom, % 2.28/2.48 b48_buttercup10451($i!val!48) <=> $false). % 2.28/2.48 tff(formula107, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!449 = X0)) | (($i!val!236 = X0)) | (($i!val!48 = X0)))) => (b48_buttercup10451(X0) <=> k04_buttercup10453(X0)))). % 2.28/2.48 tff(formula108, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10115(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula109, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10272(X0) <=> $true)). % 2.28/2.48 tff(formula110, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10446(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula111, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10329(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula112, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10196(X0) <=> $true)). % 2.28/2.48 tff(formula113, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10370(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula114, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10024(X0) <=> $true)). % 2.28/2.48 tff(formula115, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10110(X0) <=> (k!513(X0) = $i!val!433))). % 2.28/2.48 tff(formula116, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10031(X0) <=> ((k!513(X0) = $i!val!196) | (k!513(X0) = $i!val!382)))). % 2.28/2.48 tff(formula117, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10611(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula118, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10298(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula119, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10389(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula120, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10374(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula121, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10624(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula122, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10268(X0) <=> $true)). % 2.28/2.48 tff(formula123, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10100(X0) <=> ((~(k!513(X0) = $i!val!406)) & (~(k!513(X0) = $i!val!54)) & (~(k!513(X0) = $i!val!26)) & (~(k!513(X0) = $i!val!23)) & (~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!61)) & (~(k!513(X0) = $i!val!60)) & (~(k!513(X0) = $i!val!27))))). % 2.28/2.48 tff(formula124, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10007(X0) <=> $true)). % 2.28/2.48 tff(formula125, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10201(X0) <=> $true)). % 2.28/2.48 tff(formula126, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10282(X0) <=> (k!513(X0) = $i!val!100))). % 2.28/2.48 tff(formula127, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10092(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!84))))). % 2.28/2.48 tff(formula128, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10377(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula129, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10628(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula130, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10589(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula131, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10548(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula132, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10541(X0) <=> $true)). % 2.28/2.48 tff(formula133, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10119(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula134, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10636(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula135, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10616(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula136, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10364(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!64))))). % 2.28/2.48 tff(formula137, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10582(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula138, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10526(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula139, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10404(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula140, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10474(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula141, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10376(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula142, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10489(X0) <=> (k!513(X0) = $i!val!324))). % 2.28/2.48 tff(formula143, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10367(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula144, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10133(X0) <=> (k!513(X0) = $i!val!386))). % 2.28/2.48 tff(formula145, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10555(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula146, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10538(X0) <=> $true)). % 2.28/2.48 tff(formula147, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10549(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula148, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10515(X0) <=> ((~(k!513(X0) = $i!val!98)) & (~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!39)) & (~(k!513(X0) = $i!val!38))))). % 2.28/2.48 tff(formula149, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10642(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula150, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10307(X0) <=> (k!513(X0) = $i!val!321))). % 2.28/2.48 tff(formula151, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10085(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!44))))). % 2.28/2.48 tff(formula152, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10049(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula153, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10563(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula154, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10153(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula155, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10445(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula156, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10072(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula157, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10228(X0) <=> (k!513(X0) = $i!val!421))). % 2.28/2.48 tff(formula158, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10169(X0) <=> (k!513(X0) = $i!val!243))). % 2.28/2.48 tff(formula159, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10150(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula160, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10021(X0) <=> (k!513(X0) = $i!val!400))). % 2.28/2.48 tff(formula161, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10519(X0) <=> (k!513(X0) = $i!val!313))). % 2.28/2.48 tff(formula162, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10479(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula163, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10308(X0) <=> (k!513(X0) = $i!val!458))). % 2.28/2.48 tff(formula164, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10275(X0) <=> $true)). % 2.28/2.48 tff(formula165, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10433(X0) <=> $true)). % 2.28/2.48 tff(formula166, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10043(X0) <=> $true)). % 2.28/2.48 tff(formula167, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10492(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula168, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10278(X0) <=> $true)). % 2.28/2.48 tff(formula169, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10562(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula170, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10109(X0) <=> (k!513(X0) = $i!val!410))). % 2.28/2.48 tff(formula171, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10219(X0) <=> ((k!513(X0) = $i!val!231) | (k!513(X0) = $i!val!442)))). % 2.28/2.48 tff(formula172, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10227(X0) <=> (k!513(X0) = $i!val!451))). % 2.28/2.48 tff(formula173, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10221(X0) <=> ((k!513(X0) = $i!val!300) | (k!513(X0) = $i!val!216)))). % 2.28/2.48 tff(formula174, axiom, % 2.28/2.48 k04_buttercup10540($i!val!202) <=> $true). % 2.28/2.48 tff(formula175, axiom, % 2.28/2.48 k04_buttercup10540($i!val!389) <=> $true). % 2.28/2.48 tff(formula176, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!202 = X0)) | (($i!val!389 = X0)))) => (k04_buttercup10540(X0) <=> b48_buttercup10541(X0)))). % 2.28/2.48 tff(formula177, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10166(X0) <=> (k!513(X0) = $i!val!247))). % 2.28/2.48 tff(formula178, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10646(X0) <=> $true)). % 2.28/2.48 tff(formula179, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10074(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula180, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10283(X0) <=> $true)). % 2.28/2.48 tff(formula181, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10086(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula182, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10641(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula183, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10147(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula184, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10507(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula185, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10238(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula186, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10012(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula187, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10411(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula188, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10599(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula189, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10638(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula190, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10294(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula191, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10567(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula192, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10019(X0) <=> (k!513(X0) = $i!val!310))). % 2.28/2.48 tff(formula193, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10034(X0) <=> ((k!513(X0) = $i!val!211) | (k!513(X0) = $i!val!380)))). % 2.28/2.48 tff(formula194, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10337(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula195, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10347(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula196, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10449(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula197, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10220(X0) <=> ((k!513(X0) = $i!val!156) | (k!513(X0) = $i!val!415)))). % 2.28/2.48 tff(formula198, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10417(X0) <=> (~(k!513(X0) = $i!val!98)))). % 2.28/2.48 tff(formula199, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10467(X0) <=> (k!513(X0) = $i!val!315))). % 2.28/2.48 tff(formula200, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10483(X0) <=> (k!513(X0) = $i!val!301))). % 2.28/2.48 tff(formula201, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10430(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula202, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10356(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula203, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10154(X0) <=> (k!513(X0) = $i!val!333))). % 2.28/2.48 tff(formula204, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10135(X0) <=> (k!513(X0) = $i!val!198))). % 2.28/2.48 tff(formula205, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10070(X0) <=> (k!513(X0) = $i!val!278))). % 2.28/2.48 tff(formula206, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10521(X0) <=> (k!513(X0) = $i!val!370))). % 2.28/2.48 tff(formula207, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10290(X0) <=> $true)). % 2.28/2.48 tff(formula208, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10068(X0) <=> (k!513(X0) = $i!val!302))). % 2.28/2.48 tff(formula209, axiom, % 2.28/2.48 k04_buttercup10255($i!val!177) <=> $true). % 2.28/2.48 tff(formula210, axiom, % 2.28/2.48 k04_buttercup10255($i!val!401) <=> $true). % 2.28/2.48 tff(formula211, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!177 = X0)) | (($i!val!401 = X0)))) => (k04_buttercup10255(X0) <=> b48_buttercup10253(X0)))). % 2.28/2.48 tff(formula212, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10466(X0) <=> (k!513(X0) = $i!val!316))). % 2.28/2.48 tff(formula213, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10067(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula214, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10252(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula215, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10013(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula216, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10596(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula217, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10156(X0) <=> (k!513(X0) = $i!val!332))). % 2.28/2.48 tff(formula218, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10510(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula219, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10199(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula220, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10195(X0) <=> (k!513(X0) = $i!val!448))). % 2.28/2.48 tff(formula221, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10493(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula222, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10419(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!99)) & (~(k!513(X0) = $i!val!95))))). % 2.28/2.48 tff(formula223, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10174(X0) <=> (k!513(X0) = $i!val!276))). % 2.28/2.48 tff(formula224, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10065(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula225, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10410(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula226, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10200(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula227, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10130(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula228, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10261(X0) <=> ((~(X0 = $i!val!86)) & (~(X0 = $i!val!249)) & (~(X0 = $i!val!85)) & (~(X0 = $i!val!170))))). % 2.28/2.48 tff(formula229, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10382(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula230, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10640(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula231, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10408(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula232, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10442(X0) <=> (~(k!513(X0) = $i!val!63)))). % 2.28/2.48 tff(formula233, axiom, % 2.28/2.48 k04_buttercup10539($i!val!105) <=> $true). % 2.28/2.48 tff(formula234, axiom, % 2.28/2.48 k04_buttercup10539($i!val!251) <=> $true). % 2.28/2.48 tff(formula235, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!105 = X0)) | (($i!val!251 = X0)))) => (k04_buttercup10539(X0) <=> b48_buttercup10538(X0)))). % 2.28/2.48 tff(formula236, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10373(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula237, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10380(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula238, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10622(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!26))))). % 2.28/2.48 tff(formula239, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10260(X0) <=> ((X0 = $i!val!249) & (~(X0 = $i!val!85)) & (~(X0 = $i!val!170))))). % 2.28/2.48 tff(formula240, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10381(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!59))))). % 2.28/2.48 tff(formula241, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10193(X0) <=> (k!513(X0) = $i!val!450))). % 2.28/2.48 tff(formula242, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10612(X0) <=> $true)). % 2.28/2.48 tff(formula243, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10348(X0) <=> (k!513(X0) = $i!val!418))). % 2.28/2.48 tff(formula244, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10312(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula245, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10296(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula246, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10643(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula247, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10609(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula248, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10305(X0) <=> ((k!513(X0) = $i!val!462) | (k!513(X0) = $i!val!323)))). % 2.28/2.48 tff(formula249, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10172(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula250, axiom, % 2.28/2.48 k04_buttercup10042($i!val!108) <=> $true). % 2.28/2.48 tff(formula251, axiom, % 2.28/2.48 k04_buttercup10042($i!val!250) <=> $true). % 2.28/2.48 tff(formula252, axiom, % 2.28/2.48 ![X0: $i] : ((~((($i!val!108 = X0)) | (($i!val!250 = X0)))) => (k04_buttercup10042(X0) <=> b48_buttercup10045(X0)))). % 2.28/2.48 tff(formula253, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10111(X0) <=> (k!513(X0) = $i!val!432))). % 2.28/2.48 tff(formula254, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10104(X0) <=> (k!513(X0) = $i!val!406))). % 2.28/2.48 tff(formula255, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10236(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula256, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10028(X0) <=> ((k!513(X0) = $i!val!211) | (k!513(X0) = $i!val!380)))). % 2.28/2.48 tff(formula257, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10361(X0) <=> $true)). % 2.28/2.48 tff(formula258, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10465(X0) <=> (k!513(X0) = $i!val!317))). % 2.28/2.48 tff(formula259, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10524(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula260, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10048(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula261, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10496(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula262, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10626(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula263, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10394(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula264, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10313(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula265, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10504(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula266, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10164(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula267, axiom, % 2.28/2.48 ![X0: $i] : (k04_buttercup10453(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.48 tff(formula268, axiom, % 2.28/2.48 ![X0: $i] : (b48_buttercup10570(X0) <=> (k!513(X0) = $i!val!372))). % 2.28/2.49 tff(formula269, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10575(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula270, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10343(X0) <=> (k!513(X0) = $i!val!423))). % 2.28/2.49 tff(formula271, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10197(X0) <=> $true)). % 2.28/2.49 tff(formula272, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10450(X0) <=> $true)). % 2.28/2.49 tff(formula273, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10097(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!59))))). % 2.28/2.49 tff(formula274, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10502(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula275, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10344(X0) <=> (k!513(X0) = $i!val!422))). % 2.28/2.49 tff(formula276, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10441(X0) <=> (k!513(X0) = $i!val!258))). % 2.28/2.49 tff(formula277, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10469(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula278, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10309(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula279, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10471(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula280, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10142(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!44))))). % 2.28/2.49 tff(formula281, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10033(X0) <=> ((k!513(X0) = $i!val!382) | (k!513(X0) = $i!val!196)))). % 2.28/2.49 tff(formula282, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10198(X0) <=> $true)). % 2.28/2.49 tff(formula283, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10259(X0) <=> $true)). % 2.28/2.49 tff(formula284, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10300(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula285, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10512(X0) <=> $true)). % 2.28/2.49 tff(formula286, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10547(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula287, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10160(X0) <=> (k!513(X0) = $i!val!271))). % 2.28/2.49 tff(formula288, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10518(X0) <=> (k!513(X0) = $i!val!412))). % 2.28/2.49 tff(formula289, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10629(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula290, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10139(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula291, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10176(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula292, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10273(X0) <=> $true)). % 2.28/2.49 tff(formula293, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10546(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula294, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10378(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula295, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10234(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula296, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10217(X0) <=> ((k!513(X0) = $i!val!231) | (k!513(X0) = $i!val!442)))). % 2.28/2.49 tff(formula297, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10057(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula298, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10402(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula299, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10325(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula300, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10102(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!26)) & (~(k!513(X0) = $i!val!23))))). % 2.28/2.49 tff(formula301, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10208(X0) <=> ((k!513(X0) = $i!val!216) | (k!513(X0) = $i!val!300)))). % 2.28/2.49 tff(formula302, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10456(X0) <=> (k!513(X0) = $i!val!404))). % 2.28/2.49 tff(formula303, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10277(X0) <=> $true)). % 2.28/2.49 tff(formula304, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10529(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula305, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10545(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula306, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10353(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula307, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10415(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula308, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10035(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula309, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10635(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula310, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10581(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula311, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10229(X0) <=> (k!513(X0) = $i!val!420))). % 2.28/2.49 tff(formula312, axiom, % 2.28/2.49 k04_buttercup10360($i!val!118) <=> $true). % 2.28/2.49 tff(formula313, axiom, % 2.28/2.49 k04_buttercup10360($i!val!387) <=> $true). % 2.28/2.49 tff(formula314, axiom, % 2.28/2.49 ![X0: $i] : ((~((($i!val!118 = X0)) | (($i!val!387 = X0)))) => (k04_buttercup10360(X0) <=> b48_buttercup10359(X0)))). % 2.28/2.49 tff(formula315, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10516(X0) <=> ((~(k!513(X0) = $i!val!98)) & (~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!39))))). % 2.28/2.49 tff(formula316, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10551(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula317, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10299(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula318, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10522(X0) <=> $true)). % 2.28/2.49 tff(formula319, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10075(X0) <=> (k!513(X0) = $i!val!282))). % 2.28/2.49 tff(formula320, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10022(X0) <=> (k!513(X0) = $i!val!399))). % 2.28/2.49 tff(formula321, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10578(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula322, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10108(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!26)) & (~(k!513(X0) = $i!val!54))))). % 2.28/2.49 tff(formula323, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10190(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula324, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10222(X0) <=> (~(k!513(X0) = $i!val!94)))). % 2.28/2.49 tff(formula325, axiom, % 2.28/2.49 k04_buttercup10286($i!val!101) <=> $true). % 2.28/2.49 tff(formula326, axiom, % 2.28/2.49 k04_buttercup10286($i!val!242) <=> $true). % 2.28/2.49 tff(formula327, axiom, % 2.28/2.49 ![X0: $i] : ((~((($i!val!101 = X0)) | (($i!val!242 = X0)))) => (k04_buttercup10286(X0) <=> b48_buttercup10283(X0)))). % 2.28/2.49 tff(formula328, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10593(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula329, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10333(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula330, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10620(X0) <=> ((k!513(X0) = $i!val!222) | (k!513(X0) = $i!val!408)))). % 2.28/2.49 tff(formula331, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10443(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula332, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10248(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula333, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10619(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!26))))). % 2.28/2.49 tff(formula334, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10574(X0) <=> (k!513(X0) = $i!val!369))). % 2.28/2.49 tff(formula335, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10204(X0) <=> ((~(k!513(X0) = $i!val!216)) & (~(k!513(X0) = $i!val!300)) & (~(k!513(X0) = $i!val!81)) & (~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!40)) & (~(k!513(X0) = $i!val!20))))). % 2.28/2.49 tff(formula336, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10184(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula337, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10362(X0) <=> (k!513(X0) = $i!val!265))). % 2.28/2.49 tff(formula338, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10499(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula339, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10054(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula340, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10291(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula341, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10000(X0) <=> (k!513(X0) = $i!val!181))). % 2.28/2.49 tff(formula342, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10053(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!70))))). % 2.28/2.49 tff(formula343, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10486(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula344, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10079(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula345, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10089(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula346, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10210(X0) <=> ((k!513(X0) = $i!val!235) | (k!513(X0) = $i!val!443)))). % 2.28/2.49 tff(formula347, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10004(X0) <=> (k!513(X0) = $i!val!182))). % 2.28/2.49 tff(formula348, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10134(X0) <=> (k!513(X0) = $i!val!384))). % 2.28/2.49 tff(formula349, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10397(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula350, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10605(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula351, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10520(X0) <=> (k!513(X0) = $i!val!441))). % 2.28/2.49 tff(formula352, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10095(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula353, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10544(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula354, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10322(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula355, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10158(X0) <=> (k!513(X0) = $i!val!336))). % 2.28/2.49 tff(formula356, axiom, % 2.28/2.49 k04_buttercup10288($i!val!103) <=> $true). % 2.28/2.49 tff(formula357, axiom, % 2.28/2.49 k04_buttercup10288($i!val!426) <=> $true). % 2.28/2.49 tff(formula358, axiom, % 2.28/2.49 ![X0: $i] : ((~((($i!val!103 = X0)) | (($i!val!426 = X0)))) => (k04_buttercup10288(X0) <=> b48_buttercup10290(X0)))). % 2.28/2.49 tff(formula359, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10608(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!81))))). % 2.28/2.49 tff(formula360, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10266(X0) <=> $true)). % 2.28/2.49 tff(formula361, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10213(X0) <=> ((k!513(X0) = $i!val!443) | (k!513(X0) = $i!val!235)))). % 2.28/2.49 tff(formula362, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10420(X0) <=> $true)). % 2.28/2.49 tff(formula363, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10253(X0) <=> $true)). % 2.28/2.49 tff(formula364, axiom, % 2.28/2.49 ![X0: $i] : (k04_buttercup10016(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.28/2.49 tff(formula365, axiom, % 2.28/2.49 ![X0: $i] : (b48_buttercup10107(X0) <=> ((k!513(X0) = $i!val!222) | (k!513(X0) = $i!val!408)))). % 2.28/2.49 tff(formula366, axiom, % 2.28/2.49 k!513($i!val!439) = $i!val!439). % 2.28/2.49 tff(formula367, axiom, % 2.28/2.49 k!513($i!val!205) = $i!val!205). % 2.28/2.49 tff(formula368, axiom, % 2.28/2.49 k!513($i!val!127) = $i!val!127). % 2.28/2.49 tff(formula369, axiom, % 2.28/2.49 k!513($i!val!146) = $i!val!146). % 2.28/2.49 tff(formula370, axiom, % 2.28/2.49 k!513($i!val!279) = $i!val!279). % 2.28/2.49 tff(formula371, axiom, % 2.28/2.49 k!513($i!val!145) = $i!val!145). % 2.28/2.49 tff(formula372, axiom, % 2.28/2.49 k!513($i!val!102) = $i!val!102). % 2.28/2.49 tff(formula373, axiom, % 2.28/2.49 k!513($i!val!231) = $i!val!231). % 2.28/2.49 tff(formula374, axiom, % 2.28/2.49 k!513($i!val!72) = $i!val!72). % 2.28/2.49 tff(formula375, axiom, % 2.28/2.49 k!513($i!val!343) = $i!val!343). % 2.28/2.49 tff(formula376, axiom, % 2.28/2.49 k!513($i!val!386) = $i!val!386). % 2.28/2.49 tff(formula377, axiom, % 2.28/2.49 k!513($i!val!293) = $i!val!293). % 2.28/2.49 tff(formula378, axiom, % 2.28/2.49 k!513($i!val!165) = $i!val!165). % 2.28/2.49 tff(formula379, axiom, % 2.28/2.49 k!513($i!val!299) = $i!val!299). % 2.28/2.49 tff(formula380, axiom, % 2.28/2.49 k!513($i!val!453) = $i!val!453). % 2.28/2.49 tff(formula381, axiom, % 2.28/2.49 k!513($i!val!388) = $i!val!388). % 2.28/2.49 tff(formula382, axiom, % 2.28/2.49 k!513($i!val!45) = $i!val!45). % 2.28/2.49 tff(formula383, axiom, % 2.28/2.49 k!513($i!val!269) = $i!val!269). % 2.28/2.49 tff(formula384, axiom, % 2.28/2.49 k!513($i!val!143) = $i!val!143). % 2.28/2.49 tff(formula385, axiom, % 2.28/2.49 k!513($i!val!260) = $i!val!260). % 2.28/2.49 tff(formula386, axiom, % 2.28/2.49 k!513($i!val!261) = $i!val!261). % 2.28/2.49 tff(formula387, axiom, % 2.28/2.49 k!513($i!val!1) = $i!val!1). % 2.28/2.49 tff(formula388, axiom, % 2.28/2.49 k!513($i!val!255) = $i!val!255). % 2.28/2.49 tff(formula389, axiom, % 2.28/2.49 k!513($i!val!0) = $i!val!0). % 2.28/2.49 tff(formula390, axiom, % 2.28/2.49 k!513($i!val!68) = $i!val!68). % 2.28/2.49 tff(formula391, axiom, % 2.28/2.49 k!513($i!val!449) = $i!val!449). % 2.28/2.49 tff(formula392, axiom, % 2.28/2.49 k!513($i!val!139) = $i!val!139). % 2.28/2.49 tff(formula393, axiom, % 2.28/2.49 k!513($i!val!36) = $i!val!36). % 2.28/2.49 tff(formula394, axiom, % 2.28/2.49 k!513($i!val!312) = $i!val!312). % 2.28/2.49 tff(formula395, axiom, % 2.28/2.49 k!513($i!val!46) = $i!val!46). % 2.28/2.49 tff(formula396, axiom, % 2.28/2.49 k!513($i!val!425) = $i!val!425). % 2.28/2.49 tff(formula397, axiom, % 2.28/2.49 k!513($i!val!100) = $i!val!100). % 2.28/2.49 tff(formula398, axiom, % 2.28/2.49 k!513($i!val!138) = $i!val!138). % 2.28/2.49 tff(formula399, axiom, % 2.28/2.49 k!513($i!val!77) = $i!val!77). % 2.28/2.49 tff(formula400, axiom, % 2.28/2.49 k!513($i!val!89) = $i!val!89). % 2.28/2.49 tff(formula401, axiom, % 2.28/2.49 k!513($i!val!378) = $i!val!378). % 2.28/2.49 tff(formula402, axiom, % 2.28/2.49 k!513($i!val!80) = $i!val!80). % 2.28/2.49 tff(formula403, axiom, % 2.28/2.49 k!513($i!val!306) = $i!val!306). % 2.28/2.49 tff(formula404, axiom, % 2.28/2.49 k!513($i!val!394) = $i!val!394). % 2.28/2.49 tff(formula405, axiom, % 2.28/2.49 k!513($i!val!290) = $i!val!290). % 2.28/2.49 tff(formula406, axiom, % 2.28/2.49 k!513($i!val!254) = $i!val!254). % 2.28/2.49 tff(formula407, axiom, % 2.28/2.49 k!513($i!val!129) = $i!val!129). % 2.28/2.49 tff(formula408, axiom, % 2.28/2.49 k!513($i!val!397) = $i!val!397). % 2.28/2.49 tff(formula409, axiom, % 2.28/2.49 k!513($i!val!37) = $i!val!37). % 2.28/2.49 tff(formula410, axiom, % 2.28/2.49 k!513($i!val!208) = $i!val!208). % 2.28/2.49 tff(formula411, axiom, % 2.28/2.49 k!513($i!val!97) = $i!val!97). % 2.28/2.49 tff(formula412, axiom, % 2.28/2.49 k!513($i!val!434) = $i!val!434). % 2.28/2.49 tff(formula413, axiom, % 2.28/2.49 k!513($i!val!93) = $i!val!93). % 2.28/2.49 tff(formula414, axiom, % 2.28/2.49 k!513($i!val!147) = $i!val!147). % 2.28/2.49 tff(formula415, axiom, % 2.28/2.49 k!513($i!val!324) = $i!val!324). % 2.28/2.49 tff(formula416, axiom, % 2.28/2.49 k!513($i!val!34) = $i!val!34). % 2.28/2.49 tff(formula417, axiom, % 2.28/2.49 k!513($i!val!198) = $i!val!198). % 2.28/2.49 tff(formula418, axiom, % 2.28/2.49 k!513($i!val!26) = $i!val!26). % 2.28/2.49 tff(formula419, axiom, % 2.28/2.49 k!513($i!val!179) = $i!val!179). % 2.28/2.49 tff(formula420, axiom, % 2.28/2.49 k!513($i!val!427) = $i!val!427). % 2.28/2.49 tff(formula421, axiom, % 2.28/2.49 k!513($i!val!225) = $i!val!225). % 2.28/2.49 tff(formula422, axiom, % 2.28/2.49 k!513($i!val!153) = $i!val!153). % 2.28/2.49 tff(formula423, axiom, % 2.28/2.49 k!513($i!val!277) = $i!val!277). % 2.28/2.49 tff(formula424, axiom, % 2.28/2.49 k!513($i!val!438) = $i!val!438). % 2.28/2.49 tff(formula425, axiom, % 2.28/2.49 k!513($i!val!303) = $i!val!303). % 2.28/2.49 tff(formula426, axiom, % 2.28/2.49 k!513($i!val!192) = $i!val!192). % 2.28/2.49 tff(formula427, axiom, % 2.28/2.49 k!513($i!val!8) = $i!val!8). % 2.28/2.49 tff(formula428, axiom, % 2.28/2.49 k!513($i!val!178) = $i!val!178). % 2.28/2.49 tff(formula429, axiom, % 2.28/2.49 k!513($i!val!125) = $i!val!125). % 2.28/2.49 tff(formula430, axiom, % 2.28/2.49 k!513($i!val!450) = $i!val!450). % 2.28/2.49 tff(formula431, axiom, % 2.28/2.49 k!513($i!val!229) = $i!val!229). % 2.28/2.49 tff(formula432, axiom, % 2.28/2.49 k!513($i!val!315) = $i!val!315). % 2.28/2.49 tff(formula433, axiom, % 2.28/2.49 k!513($i!val!204) = $i!val!204). % 2.28/2.49 tff(formula434, axiom, % 2.28/2.49 k!513($i!val!339) = $i!val!339). % 2.28/2.49 tff(formula435, axiom, % 2.28/2.49 k!513($i!val!296) = $i!val!296). % 2.28/2.49 tff(formula436, axiom, % 2.28/2.49 k!513($i!val!417) = $i!val!417). % 2.28/2.49 tff(formula437, axiom, % 2.28/2.49 k!513($i!val!64) = $i!val!64). % 2.28/2.49 tff(formula438, axiom, % 2.28/2.49 k!513($i!val!368) = $i!val!368). % 2.28/2.49 tff(formula439, axiom, % 2.28/2.49 k!513($i!val!2) = $i!val!2). % 2.28/2.49 tff(formula440, axiom, % 2.28/2.49 k!513($i!val!379) = $i!val!379). % 2.28/2.49 tff(formula441, axiom, % 2.28/2.49 k!513($i!val!234) = $i!val!234). % 2.28/2.49 tff(formula442, axiom, % 2.28/2.49 k!513($i!val!377) = $i!val!377). % 2.28/2.49 tff(formula443, axiom, % 2.28/2.49 k!513($i!val!252) = $i!val!252). % 2.28/2.49 tff(formula444, axiom, % 2.28/2.49 k!513($i!val!69) = $i!val!69). % 2.28/2.49 tff(formula445, axiom, % 2.28/2.49 k!513($i!val!61) = $i!val!61). % 2.28/2.49 tff(formula446, axiom, % 2.28/2.49 k!513($i!val!140) = $i!val!140). % 2.28/2.49 tff(formula447, axiom, % 2.28/2.49 k!513($i!val!355) = $i!val!355). % 2.28/2.49 tff(formula448, axiom, % 2.28/2.49 k!513($i!val!23) = $i!val!23). % 2.28/2.49 tff(formula449, axiom, % 2.28/2.49 k!513($i!val!160) = $i!val!160). % 2.28/2.49 tff(formula450, axiom, % 2.28/2.49 k!513($i!val!84) = $i!val!84). % 2.28/2.49 tff(formula451, axiom, % 2.28/2.49 k!513($i!val!25) = $i!val!25). % 2.28/2.49 tff(formula452, axiom, % 2.28/2.49 k!513($i!val!107) = $i!val!107). % 2.28/2.49 tff(formula453, axiom, % 2.28/2.49 k!513($i!val!392) = $i!val!392). % 2.28/2.49 tff(formula454, axiom, % 2.28/2.49 k!513($i!val!423) = $i!val!423). % 2.28/2.49 tff(formula455, axiom, % 2.28/2.49 k!513($i!val!63) = $i!val!63). % 2.28/2.49 tff(formula456, axiom, % 2.28/2.49 k!513($i!val!130) = $i!val!130). % 2.28/2.49 tff(formula457, axiom, % 2.28/2.49 k!513($i!val!111) = $i!val!111). % 2.28/2.49 tff(formula458, axiom, % 2.28/2.49 k!513($i!val!357) = $i!val!357). % 2.28/2.49 tff(formula459, axiom, % 2.28/2.49 k!513($i!val!335) = $i!val!335). % 2.28/2.49 tff(formula460, axiom, % 2.28/2.49 k!513($i!val!322) = $i!val!322). % 2.28/2.49 tff(formula461, axiom, % 2.28/2.49 k!513($i!val!223) = $i!val!223). % 2.28/2.49 tff(formula462, axiom, % 2.28/2.49 k!513($i!val!164) = $i!val!164). % 2.28/2.49 tff(formula463, axiom, % 2.28/2.49 k!513($i!val!424) = $i!val!424). % 2.28/2.49 tff(formula464, axiom, % 2.28/2.49 k!513($i!val!232) = $i!val!232). % 2.28/2.49 tff(formula465, axiom, % 2.28/2.49 k!513($i!val!17) = $i!val!17). % 2.28/2.49 tff(formula466, axiom, % 2.28/2.49 k!513($i!val!220) = $i!val!220). % 2.28/2.49 tff(formula467, axiom, % 2.28/2.49 k!513($i!val!301) = $i!val!301). % 2.28/2.49 tff(formula468, axiom, % 2.28/2.49 k!513($i!val!99) = $i!val!99). % 2.28/2.49 tff(formula469, axiom, % 2.28/2.49 k!513($i!val!52) = $i!val!52). % 2.28/2.49 tff(formula470, axiom, % 2.28/2.49 k!513($i!val!216) = $i!val!216). % 2.28/2.49 tff(formula471, axiom, % 2.28/2.49 k!513($i!val!132) = $i!val!132). % 2.28/2.49 tff(formula472, axiom, % 2.28/2.49 k!513($i!val!411) = $i!val!411). % 2.28/2.49 tff(formula473, axiom, % 2.28/2.49 k!513($i!val!188) = $i!val!188). % 2.28/2.49 tff(formula474, axiom, % 2.28/2.49 k!513($i!val!116) = $i!val!116). % 2.28/2.49 tff(formula475, axiom, % 2.28/2.49 k!513($i!val!210) = $i!val!210). % 2.28/2.49 tff(formula476, axiom, % 2.28/2.49 k!513($i!val!298) = $i!val!298). % 2.28/2.49 tff(formula477, axiom, % 2.28/2.49 k!513($i!val!461) = $i!val!461). % 2.28/2.49 tff(formula478, axiom, % 2.28/2.49 k!513($i!val!351) = $i!val!351). % 2.28/2.49 tff(formula479, axiom, % 2.28/2.49 k!513($i!val!87) = $i!val!87). % 2.28/2.49 tff(formula480, axiom, % 2.28/2.49 k!513($i!val!57) = $i!val!57). % 2.28/2.49 tff(formula481, axiom, % 2.28/2.49 k!513($i!val!440) = $i!val!440). % 2.28/2.49 tff(formula482, axiom, % 2.28/2.49 k!513($i!val!444) = $i!val!444). % 2.28/2.49 tff(formula483, axiom, % 2.28/2.49 k!513($i!val!331) = $i!val!331). % 2.28/2.49 tff(formula484, axiom, % 2.28/2.49 k!513($i!val!163) = $i!val!163). % 2.28/2.49 tff(formula485, axiom, % 2.28/2.49 k!513($i!val!189) = $i!val!189). % 2.28/2.49 tff(formula486, axiom, % 2.28/2.49 k!513($i!val!71) = $i!val!71). % 2.28/2.49 tff(formula487, axiom, % 2.28/2.49 k!513($i!val!380) = $i!val!380). % 2.28/2.49 tff(formula488, axiom, % 2.28/2.49 k!513($i!val!190) = $i!val!190). % 2.28/2.49 tff(formula489, axiom, % 2.28/2.49 k!513($i!val!362) = $i!val!362). % 2.28/2.49 tff(formula490, axiom, % 2.28/2.49 k!513($i!val!83) = $i!val!83). % 2.28/2.49 tff(formula491, axiom, % 2.28/2.49 k!513($i!val!276) = $i!val!276). % 2.28/2.49 tff(formula492, axiom, % 2.28/2.49 k!513($i!val!4) = $i!val!4). % 2.28/2.49 tff(formula493, axiom, % 2.28/2.49 k!513($i!val!133) = $i!val!133). % 2.28/2.49 tff(formula494, axiom, % 2.28/2.49 k!513($i!val!55) = $i!val!55). % 2.28/2.49 tff(formula495, axiom, % 2.28/2.49 k!513($i!val!452) = $i!val!452). % 2.28/2.49 tff(formula496, axiom, % 2.28/2.49 k!513($i!val!274) = $i!val!274). % 2.28/2.49 tff(formula497, axiom, % 2.28/2.49 k!513($i!val!297) = $i!val!297). % 2.28/2.49 tff(formula498, axiom, % 2.28/2.49 k!513($i!val!183) = $i!val!183). % 2.28/2.49 tff(formula499, axiom, % 2.28/2.49 k!513($i!val!221) = $i!val!221). % 2.28/2.49 tff(formula500, axiom, % 2.28/2.49 k!513($i!val!141) = $i!val!141). % 2.28/2.49 tff(formula501, axiom, % 2.28/2.49 k!513($i!val!300) = $i!val!300). % 2.28/2.49 tff(formula502, axiom, % 2.28/2.49 k!513($i!val!326) = $i!val!326). % 2.28/2.49 tff(formula503, axiom, % 2.28/2.49 k!513($i!val!175) = $i!val!175). % 2.28/2.49 tff(formula504, axiom, % 2.28/2.49 k!513($i!val!187) = $i!val!187). % 2.28/2.49 tff(formula505, axiom, % 2.28/2.49 k!513($i!val!65) = $i!val!65). % 2.28/2.49 tff(formula506, axiom, % 2.28/2.49 k!513($i!val!66) = $i!val!66). % 2.28/2.49 tff(formula507, axiom, % 2.28/2.49 k!513($i!val!304) = $i!val!304). % 2.28/2.49 tff(formula508, axiom, % 2.28/2.49 k!513($i!val!13) = $i!val!13). % 2.28/2.49 tff(formula509, axiom, % 2.28/2.49 k!513($i!val!30) = $i!val!30). % 2.28/2.49 tff(formula510, axiom, % 2.28/2.49 k!513($i!val!181) = $i!val!181). % 2.28/2.49 tff(formula511, axiom, % 2.28/2.49 k!513($i!val!432) = $i!val!432). % 2.28/2.49 tff(formula512, axiom, % 2.28/2.49 k!513($i!val!309) = $i!val!309). % 2.28/2.49 tff(formula513, axiom, % 2.28/2.49 k!513($i!val!121) = $i!val!121). % 2.28/2.49 tff(formula514, axiom, % 2.28/2.49 k!513($i!val!196) = $i!val!196). % 2.28/2.49 tff(formula515, axiom, % 2.28/2.49 k!513($i!val!265) = $i!val!265). % 2.28/2.49 tff(formula516, axiom, % 2.28/2.49 k!513($i!val!51) = $i!val!51). % 2.28/2.49 tff(formula517, axiom, % 2.28/2.49 k!513($i!val!11) = $i!val!11). % 2.28/2.49 tff(formula518, axiom, % 2.28/2.49 k!513($i!val!203) = $i!val!203). % 2.28/2.49 tff(formula519, axiom, % 2.28/2.49 k!513($i!val!67) = $i!val!67). % 2.28/2.49 tff(formula520, axiom, % 2.28/2.49 k!513($i!val!245) = $i!val!245). % 2.28/2.49 tff(formula521, axiom, % 2.28/2.49 k!513($i!val!70) = $i!val!70). % 2.28/2.49 tff(formula522, axiom, % 2.28/2.49 k!513($i!val!131) = $i!val!131). % 2.28/2.49 tff(formula523, axiom, % 2.28/2.49 k!513($i!val!227) = $i!val!227). % 2.28/2.49 tff(formula524, axiom, % 2.28/2.49 k!513($i!val!372) = $i!val!372). % 2.28/2.49 tff(formula525, axiom, % 2.28/2.49 k!513($i!val!244) = $i!val!244). % 2.28/2.49 tff(formula526, axiom, % 2.28/2.49 k!513($i!val!344) = $i!val!344). % 2.28/2.49 tff(formula527, axiom, % 2.28/2.49 k!513($i!val!78) = $i!val!78). % 2.28/2.49 tff(formula528, axiom, % 2.28/2.49 k!513($i!val!292) = $i!val!292). % 2.28/2.49 tff(formula529, axiom, % 2.28/2.49 k!513($i!val!54) = $i!val!54). % 2.28/2.49 tff(formula530, axiom, % 2.28/2.49 k!513($i!val!294) = $i!val!294). % 2.28/2.49 tff(formula531, axiom, % 2.28/2.49 k!513($i!val!168) = $i!val!168). % 2.28/2.49 tff(formula532, axiom, % 2.28/2.49 k!513($i!val!75) = $i!val!75). % 2.28/2.49 tff(formula533, axiom, % 2.28/2.49 k!513($i!val!144) = $i!val!144). % 2.28/2.49 tff(formula534, axiom, % 2.28/2.49 k!513($i!val!6) = $i!val!6). % 2.28/2.49 tff(formula535, axiom, % 2.28/2.49 k!513($i!val!376) = $i!val!376). % 2.28/2.49 tff(formula536, axiom, % 2.28/2.49 k!513($i!val!21) = $i!val!21). % 2.28/2.49 tff(formula537, axiom, % 2.28/2.49 k!513($i!val!302) = $i!val!302). % 2.28/2.49 tff(formula538, axiom, % 2.28/2.49 k!513($i!val!332) = $i!val!332). % 2.28/2.49 tff(formula539, axiom, % 2.28/2.49 k!513($i!val!148) = $i!val!148). % 2.28/2.49 tff(formula540, axiom, % 2.28/2.49 k!513($i!val!135) = $i!val!135). % 2.28/2.49 tff(formula541, axiom, % 2.28/2.49 k!513($i!val!459) = $i!val!459). % 2.28/2.49 tff(formula542, axiom, % 2.28/2.49 k!513($i!val!333) = $i!val!333). % 2.28/2.49 tff(formula543, axiom, % 2.28/2.49 k!513($i!val!458) = $i!val!458). % 2.28/2.49 tff(formula544, axiom, % 2.28/2.49 k!513($i!val!134) = $i!val!134). % 2.28/2.49 tff(formula545, axiom, % 2.28/2.49 k!513($i!val!246) = $i!val!246). % 2.28/2.49 tff(formula546, axiom, % 2.28/2.49 k!513($i!val!73) = $i!val!73). % 2.28/2.49 tff(formula547, axiom, % 2.28/2.49 k!513($i!val!375) = $i!val!375). % 2.28/2.49 tff(formula548, axiom, % 2.28/2.49 k!513($i!val!447) = $i!val!447). % 2.28/2.49 tff(formula549, axiom, % 2.28/2.49 k!513($i!val!154) = $i!val!154). % 2.28/2.49 tff(formula550, axiom, % 2.28/2.49 k!513($i!val!156) = $i!val!156). % 2.28/2.49 tff(formula551, axiom, % 2.28/2.49 k!513($i!val!217) = $i!val!217). % 2.28/2.49 tff(formula552, axiom, % 2.28/2.49 k!513($i!val!44) = $i!val!44). % 2.28/2.49 tff(formula553, axiom, % 2.28/2.49 k!513($i!val!258) = $i!val!258). % 2.28/2.49 tff(formula554, axiom, % 2.28/2.49 k!513($i!val!354) = $i!val!354). % 2.28/2.49 tff(formula555, axiom, % 2.28/2.49 k!513($i!val!92) = $i!val!92). % 2.28/2.49 tff(formula556, axiom, % 2.28/2.49 k!513($i!val!98) = $i!val!98). % 2.28/2.49 tff(formula557, axiom, % 2.28/2.49 k!513($i!val!120) = $i!val!120). % 2.28/2.49 tff(formula558, axiom, % 2.28/2.49 k!513($i!val!408) = $i!val!408). % 2.28/2.49 tff(formula559, axiom, % 2.28/2.49 k!513($i!val!382) = $i!val!382). % 2.28/2.49 tff(formula560, axiom, % 2.28/2.49 k!513($i!val!323) = $i!val!323). % 2.28/2.49 tff(formula561, axiom, % 2.28/2.49 k!513($i!val!340) = $i!val!340). % 2.28/2.49 tff(formula562, axiom, % 2.28/2.49 k!513($i!val!33) = $i!val!33). % 2.28/2.49 tff(formula563, axiom, % 2.28/2.49 k!513($i!val!409) = $i!val!409). % 2.28/2.49 tff(formula564, axiom, % 2.28/2.49 k!513($i!val!237) = $i!val!237). % 2.28/2.49 tff(formula565, axiom, % 2.28/2.49 k!513($i!val!256) = $i!val!256). % 2.28/2.49 tff(formula566, axiom, % 2.28/2.49 k!513($i!val!259) = $i!val!259). % 2.28/2.49 tff(formula567, axiom, % 2.28/2.49 k!513($i!val!422) = $i!val!422). % 2.28/2.49 tff(formula568, axiom, % 2.28/2.49 k!513($i!val!366) = $i!val!366). % 2.28/2.49 tff(formula569, axiom, % 2.28/2.49 k!513($i!val!325) = $i!val!325). % 2.28/2.49 tff(formula570, axiom, % 2.28/2.49 k!513($i!val!310) = $i!val!310). % 2.28/2.49 tff(formula571, axiom, % 2.28/2.49 k!513($i!val!321) = $i!val!321). % 2.28/2.49 tff(formula572, axiom, % 2.28/2.49 k!513($i!val!128) = $i!val!128). % 2.28/2.49 tff(formula573, axiom, % 2.28/2.49 k!513($i!val!317) = $i!val!317). % 2.28/2.49 tff(formula574, axiom, % 2.28/2.49 k!513($i!val!197) = $i!val!197). % 2.28/2.49 tff(formula575, axiom, % 2.28/2.49 k!513($i!val!31) = $i!val!31). % 2.28/2.49 tff(formula576, axiom, % 2.28/2.49 k!513($i!val!313) = $i!val!313). % 2.28/2.49 tff(formula577, axiom, % 2.28/2.49 k!513($i!val!365) = $i!val!365). % 2.28/2.49 tff(formula578, axiom, % 2.28/2.49 k!513($i!val!384) = $i!val!384). % 2.28/2.49 tff(formula579, axiom, % 2.28/2.49 k!513($i!val!346) = $i!val!346). % 2.28/2.49 tff(formula580, axiom, % 2.28/2.49 k!513($i!val!268) = $i!val!268). % 2.28/2.49 tff(formula581, axiom, % 2.28/2.49 k!513($i!val!349) = $i!val!349). % 2.28/2.49 tff(formula582, axiom, % 2.28/2.49 k!513($i!val!218) = $i!val!218). % 2.28/2.49 tff(formula583, axiom, % 2.28/2.49 k!513($i!val!12) = $i!val!12). % 2.28/2.49 tff(formula584, axiom, % 2.28/2.49 k!513($i!val!7) = $i!val!7). % 2.28/2.49 tff(formula585, axiom, % 2.28/2.49 k!513($i!val!446) = $i!val!446). % 2.28/2.49 tff(formula586, axiom, % 2.28/2.49 k!513($i!val!158) = $i!val!158). % 2.28/2.49 tff(formula587, axiom, % 2.28/2.49 k!513($i!val!79) = $i!val!79). % 2.28/2.49 tff(formula588, axiom, % 2.28/2.49 k!513($i!val!400) = $i!val!400). % 2.28/2.49 tff(formula589, axiom, % 2.28/2.49 k!513($i!val!96) = $i!val!96). % 2.28/2.49 tff(formula590, axiom, % 2.28/2.49 k!513($i!val!47) = $i!val!47). % 2.28/2.49 tff(formula591, axiom, % 2.28/2.49 k!513($i!val!456) = $i!val!456). % 2.28/2.49 tff(formula592, axiom, % 2.28/2.49 k!513($i!val!19) = $i!val!19). % 2.28/2.49 tff(formula593, axiom, % 2.28/2.49 k!513($i!val!435) = $i!val!435). % 2.28/2.49 tff(formula594, axiom, % 2.28/2.49 k!513($i!val!157) = $i!val!157). % 2.28/2.49 tff(formula595, axiom, % 2.28/2.49 k!513($i!val!176) = $i!val!176). % 2.28/2.49 tff(formula596, axiom, % 2.28/2.49 k!513($i!val!374) = $i!val!374). % 2.28/2.49 tff(formula597, axiom, % 2.28/2.49 k!513($i!val!39) = $i!val!39). % 2.28/2.49 tff(formula598, axiom, % 2.28/2.49 k!513($i!val!32) = $i!val!32). % 2.28/2.49 tff(formula599, axiom, % 2.28/2.49 k!513($i!val!406) = $i!val!406). % 2.28/2.49 tff(formula600, axiom, % 2.28/2.49 k!513($i!val!206) = $i!val!206). % 2.28/2.49 tff(formula601, axiom, % 2.28/2.49 k!513($i!val!123) = $i!val!123). % 2.28/2.49 tff(formula602, axiom, % 2.28/2.49 k!513($i!val!114) = $i!val!114). % 2.28/2.49 tff(formula603, axiom, % 2.28/2.49 k!513($i!val!460) = $i!val!460). % 2.28/2.49 tff(formula604, axiom, % 2.28/2.49 k!513($i!val!109) = $i!val!109). % 2.28/2.49 tff(formula605, axiom, % 2.28/2.49 k!513($i!val!419) = $i!val!419). % 2.28/2.49 tff(formula606, axiom, % 2.28/2.49 k!513($i!val!271) = $i!val!271). % 2.28/2.49 tff(formula607, axiom, % 2.28/2.49 k!513($i!val!454) = $i!val!454). % 2.28/2.49 tff(formula608, axiom, % 2.28/2.49 k!513($i!val!41) = $i!val!41). % 2.28/2.49 tff(formula609, axiom, % 2.28/2.49 k!513($i!val!38) = $i!val!38). % 2.28/2.49 tff(formula610, axiom, % 2.28/2.49 k!513($i!val!48) = $i!val!48). % 2.28/2.49 tff(formula611, axiom, % 2.28/2.49 k!513($i!val!20) = $i!val!20). % 2.28/2.49 tff(formula612, axiom, % 2.28/2.49 k!513($i!val!185) = $i!val!185). % 2.28/2.49 tff(formula613, axiom, % 2.28/2.49 k!513($i!val!239) = $i!val!239). % 2.28/2.49 tff(formula614, axiom, % 2.28/2.49 k!513($i!val!186) = $i!val!186). % 2.28/2.49 tff(formula615, axiom, % 2.28/2.49 k!513($i!val!151) = $i!val!151). % 2.28/2.49 tff(formula616, axiom, % 2.28/2.49 k!513($i!val!207) = $i!val!207). % 2.28/2.49 tff(formula617, axiom, % 2.28/2.49 k!513($i!val!289) = $i!val!289). % 2.28/2.49 tff(formula618, axiom, % 2.28/2.49 k!513($i!val!270) = $i!val!270). % 2.28/2.49 tff(formula619, axiom, % 2.28/2.49 k!513($i!val!445) = $i!val!445). % 2.28/2.49 tff(formula620, axiom, % 2.28/2.49 k!513($i!val!451) = $i!val!451). % 2.28/2.49 tff(formula621, axiom, % 2.28/2.49 k!513($i!val!442) = $i!val!442). % 2.28/2.49 tff(formula622, axiom, % 2.28/2.49 k!513($i!val!402) = $i!val!402). % 2.28/2.49 tff(formula623, axiom, % 2.28/2.49 k!513($i!val!76) = $i!val!76). % 2.28/2.49 tff(formula624, axiom, % 2.28/2.49 k!513($i!val!171) = $i!val!171). % 2.28/2.49 tff(formula625, axiom, % 2.28/2.49 k!513($i!val!58) = $i!val!58). % 2.28/2.49 tff(formula626, axiom, % 2.28/2.49 k!513($i!val!219) = $i!val!219). % 2.28/2.49 tff(formula627, axiom, % 2.28/2.49 k!513($i!val!43) = $i!val!43). % 2.28/2.49 tff(formula628, axiom, % 2.28/2.49 k!513($i!val!342) = $i!val!342). % 2.28/2.49 tff(formula629, axiom, % 2.28/2.49 k!513($i!val!110) = $i!val!110). % 2.28/2.49 tff(formula630, axiom, % 2.28/2.49 k!513($i!val!338) = $i!val!338). % 2.28/2.49 tff(formula631, axiom, % 2.28/2.49 k!513($i!val!263) = $i!val!263). % 2.28/2.49 tff(formula632, axiom, % 2.28/2.49 k!513($i!val!136) = $i!val!136). % 2.28/2.49 tff(formula633, axiom, % 2.28/2.49 k!513($i!val!358) = $i!val!358). % 2.28/2.49 tff(formula634, axiom, % 2.28/2.49 k!513($i!val!363) = $i!val!363). % 2.28/2.49 tff(formula635, axiom, % 2.28/2.49 k!513($i!val!347) = $i!val!347). % 2.28/2.49 tff(formula636, axiom, % 2.28/2.49 k!513($i!val!341) = $i!val!341). % 2.28/2.49 tff(formula637, axiom, % 2.28/2.49 k!513($i!val!364) = $i!val!364). % 2.28/2.49 tff(formula638, axiom, % 2.28/2.49 k!513($i!val!222) = $i!val!222). % 2.28/2.49 tff(formula639, axiom, % 2.28/2.49 k!513($i!val!172) = $i!val!172). % 2.28/2.49 tff(formula640, axiom, % 2.28/2.49 k!513($i!val!275) = $i!val!275). % 2.28/2.49 tff(formula641, axiom, % 2.28/2.49 k!513($i!val!155) = $i!val!155). % 2.28/2.49 tff(formula642, axiom, % 2.28/2.49 k!513($i!val!212) = $i!val!212). % 2.28/2.49 tff(formula643, axiom, % 2.28/2.49 k!513($i!val!42) = $i!val!42). % 2.28/2.49 tff(formula644, axiom, % 2.28/2.49 k!513($i!val!328) = $i!val!328). % 2.28/2.49 tff(formula645, axiom, % 2.28/2.49 k!513($i!val!280) = $i!val!280). % 2.28/2.49 tff(formula646, axiom, % 2.28/2.49 k!513($i!val!40) = $i!val!40). % 2.28/2.49 tff(formula647, axiom, % 2.28/2.49 k!513($i!val!262) = $i!val!262). % 2.28/2.49 tff(formula648, axiom, % 2.28/2.49 k!513($i!val!412) = $i!val!412). % 2.28/2.49 tff(formula649, axiom, % 2.28/2.49 k!513($i!val!398) = $i!val!398). % 2.28/2.49 tff(formula650, axiom, % 2.28/2.49 k!513($i!val!383) = $i!val!383). % 2.28/2.49 tff(formula651, axiom, % 2.28/2.49 k!513($i!val!90) = $i!val!90). % 2.28/2.49 tff(formula652, axiom, % 2.28/2.49 k!513($i!val!318) = $i!val!318). % 2.28/2.49 tff(formula653, axiom, % 2.28/2.49 k!513($i!val!174) = $i!val!174). % 2.28/2.49 tff(formula654, axiom, % 2.28/2.49 k!513($i!val!319) = $i!val!319). % 2.28/2.49 tff(formula655, axiom, % 2.28/2.49 k!513($i!val!74) = $i!val!74). % 2.28/2.49 tff(formula656, axiom, % 2.28/2.49 k!513($i!val!201) = $i!val!201). % 2.28/2.49 tff(formula657, axiom, % 2.28/2.49 k!513($i!val!420) = $i!val!420). % 2.28/2.49 tff(formula658, axiom, % 2.28/2.49 k!513($i!val!371) = $i!val!371). % 2.28/2.49 tff(formula659, axiom, % 2.28/2.49 k!513($i!val!199) = $i!val!199). % 2.28/2.49 tff(formula660, axiom, % 2.28/2.49 k!513($i!val!180) = $i!val!180). % 2.28/2.49 tff(formula661, axiom, % 2.28/2.49 k!513($i!val!281) = $i!val!281). % 2.28/2.49 tff(formula662, axiom, % 2.28/2.49 k!513($i!val!214) = $i!val!214). % 2.28/2.49 tff(formula663, axiom, % 2.28/2.49 k!513($i!val!352) = $i!val!352). % 2.28/2.49 tff(formula664, axiom, % 2.28/2.49 k!513($i!val!240) = $i!val!240). % 2.28/2.49 tff(formula665, axiom, % 2.28/2.49 k!513($i!val!53) = $i!val!53). % 2.28/2.49 tff(formula666, axiom, % 2.28/2.49 k!513($i!val!410) = $i!val!410). % 2.28/2.49 tff(formula667, axiom, % 2.28/2.49 k!513($i!val!273) = $i!val!273). % 2.28/2.49 tff(formula668, axiom, % 2.28/2.49 k!513($i!val!59) = $i!val!59). % 2.28/2.49 tff(formula669, axiom, % 2.28/2.49 k!513($i!val!291) = $i!val!291). % 2.28/2.49 tff(formula670, axiom, % 2.28/2.49 k!513($i!val!49) = $i!val!49). % 2.28/2.49 tff(formula671, axiom, % 2.28/2.49 k!513($i!val!311) = $i!val!311). % 2.28/2.49 tff(formula672, axiom, % 2.28/2.49 k!513($i!val!126) = $i!val!126). % 2.28/2.49 tff(formula673, axiom, % 2.28/2.49 k!513($i!val!360) = $i!val!360). % 2.28/2.49 tff(formula674, axiom, % 2.28/2.49 k!513($i!val!15) = $i!val!15). % 2.28/2.49 tff(formula675, axiom, % 2.28/2.49 k!513($i!val!283) = $i!val!283). % 2.28/2.49 tff(formula676, axiom, % 2.28/2.49 k!513($i!val!403) = $i!val!403). % 2.28/2.49 tff(formula677, axiom, % 2.28/2.49 k!513($i!val!215) = $i!val!215). % 2.28/2.49 tff(formula678, axiom, % 2.28/2.49 k!513($i!val!94) = $i!val!94). % 2.28/2.49 tff(formula679, axiom, % 2.28/2.49 k!513($i!val!337) = $i!val!337). % 2.28/2.49 tff(formula680, axiom, % 2.28/2.49 k!513($i!val!308) = $i!val!308). % 2.28/2.49 tff(formula681, axiom, % 2.28/2.49 k!513($i!val!295) = $i!val!295). % 2.28/2.49 tff(formula682, axiom, % 2.28/2.49 k!513($i!val!391) = $i!val!391). % 2.28/2.49 tff(formula683, axiom, % 2.28/2.49 k!513($i!val!228) = $i!val!228). % 2.28/2.49 tff(formula684, axiom, % 2.28/2.49 k!513($i!val!247) = $i!val!247). % 2.28/2.49 tff(formula685, axiom, % 2.28/2.49 k!513($i!val!235) = $i!val!235). % 2.28/2.49 tff(formula686, axiom, % 2.28/2.49 k!513($i!val!413) = $i!val!413). % 2.28/2.49 tff(formula687, axiom, % 2.28/2.49 k!513($i!val!28) = $i!val!28). % 2.28/2.49 tff(formula688, axiom, % 2.28/2.49 k!513($i!val!3) = $i!val!3). % 2.28/2.49 tff(formula689, axiom, % 2.28/2.49 k!513($i!val!390) = $i!val!390). % 2.28/2.49 tff(formula690, axiom, % 2.28/2.49 k!513($i!val!195) = $i!val!195). % 2.28/2.49 tff(formula691, axiom, % 2.28/2.49 k!513($i!val!112) = $i!val!112). % 2.28/2.49 tff(formula692, axiom, % 2.28/2.49 k!513($i!val!213) = $i!val!213). % 2.28/2.49 tff(formula693, axiom, % 2.28/2.49 k!513($i!val!62) = $i!val!62). % 2.28/2.49 tff(formula694, axiom, % 2.28/2.49 k!513($i!val!230) = $i!val!230). % 2.28/2.49 tff(formula695, axiom, % 2.28/2.49 k!513($i!val!433) = $i!val!433). % 2.28/2.49 tff(formula696, axiom, % 2.28/2.49 k!513($i!val!10) = $i!val!10). % 2.28/2.49 tff(formula697, axiom, % 2.28/2.49 k!513($i!val!191) = $i!val!191). % 2.28/2.49 tff(formula698, axiom, % 2.28/2.49 k!513($i!val!169) = $i!val!169). % 2.28/2.49 tff(formula699, axiom, % 2.28/2.49 k!513($i!val!236) = $i!val!236). % 2.28/2.49 tff(formula700, axiom, % 2.28/2.49 k!513($i!val!113) = $i!val!113). % 2.28/2.49 tff(formula701, axiom, % 2.28/2.49 k!513($i!val!361) = $i!val!361). % 2.28/2.49 tff(formula702, axiom, % 2.28/2.49 k!513($i!val!286) = $i!val!286). % 2.28/2.49 tff(formula703, axiom, % 2.28/2.49 k!513($i!val!124) = $i!val!124). % 2.28/2.49 tff(formula704, axiom, % 2.28/2.49 k!513($i!val!462) = $i!val!462). % 2.28/2.49 tff(formula705, axiom, % 2.28/2.49 k!513($i!val!161) = $i!val!161). % 2.28/2.49 tff(formula706, axiom, % 2.28/2.49 k!513($i!val!166) = $i!val!166). % 2.28/2.49 tff(formula707, axiom, % 2.28/2.49 k!513($i!val!285) = $i!val!285). % 2.28/2.49 tff(formula708, axiom, % 2.28/2.49 k!513($i!val!248) = $i!val!248). % 2.28/2.49 tff(formula709, axiom, % 2.28/2.49 k!513($i!val!443) = $i!val!443). % 2.28/2.49 tff(formula710, axiom, % 2.28/2.49 k!513($i!val!18) = $i!val!18). % 2.28/2.49 tff(formula711, axiom, % 2.28/2.49 k!513($i!val!60) = $i!val!60). % 2.28/2.49 tff(formula712, axiom, % 2.28/2.49 k!513($i!val!369) = $i!val!369). % 2.28/2.49 tff(formula713, axiom, % 2.28/2.49 k!513($i!val!421) = $i!val!421). % 2.28/2.49 tff(formula714, axiom, % 2.28/2.49 k!513($i!val!428) = $i!val!428). % 2.28/2.49 tff(formula715, axiom, % 2.28/2.49 k!513($i!val!56) = $i!val!56). % 2.28/2.49 tff(formula716, axiom, % 2.28/2.49 k!513($i!val!272) = $i!val!272). % 2.28/2.49 tff(formula717, axiom, % 2.28/2.49 k!513($i!val!95) = $i!val!95). % 2.28/2.49 tff(formula718, axiom, % 2.28/2.49 k!513($i!val!320) = $i!val!320). % 2.28/2.49 tff(formula719, axiom, % 2.28/2.49 k!513($i!val!119) = $i!val!119). % 2.28/2.49 tff(formula720, axiom, % 2.28/2.49 k!513($i!val!142) = $i!val!142). % 2.28/2.49 tff(formula721, axiom, % 2.28/2.49 k!513($i!val!455) = $i!val!455). % 2.28/2.49 tff(formula722, axiom, % 2.28/2.49 k!513($i!val!395) = $i!val!395). % 2.28/2.49 tff(formula723, axiom, % 2.28/2.49 k!513($i!val!50) = $i!val!50). % 2.28/2.49 tff(formula724, axiom, % 2.28/2.49 k!513($i!val!330) = $i!val!330). % 2.28/2.49 tff(formula725, axiom, % 2.28/2.49 k!513($i!val!314) = $i!val!314). % 2.28/2.49 tff(formula726, axiom, % 2.28/2.49 k!513($i!val!441) = $i!val!441). % 2.28/2.49 tff(formula727, axiom, % 2.28/2.49 k!513($i!val!329) = $i!val!329). % 2.28/2.49 tff(formula728, axiom, % 2.28/2.49 k!513($i!val!393) = $i!val!393). % 2.28/2.49 tff(formula729, axiom, % 2.28/2.49 k!513($i!val!137) = $i!val!137). % 2.28/2.49 tff(formula730, axiom, % 2.28/2.49 k!513($i!val!385) = $i!val!385). % 2.28/2.49 tff(formula731, axiom, % 2.28/2.49 k!513($i!val!257) = $i!val!257). % 2.28/2.49 tff(formula732, axiom, % 2.28/2.49 k!513($i!val!9) = $i!val!9). % 2.28/2.49 tff(formula733, axiom, % 2.28/2.49 k!513($i!val!16) = $i!val!16). % 2.28/2.49 tff(formula734, axiom, % 2.28/2.49 k!513($i!val!316) = $i!val!316). % 2.28/2.49 tff(formula735, axiom, % 2.28/2.49 k!513($i!val!22) = $i!val!22). % 2.28/2.49 tff(formula736, axiom, % 2.28/2.49 k!513($i!val!284) = $i!val!284). % 2.28/2.49 tff(formula737, axiom, % 2.28/2.49 k!513($i!val!336) = $i!val!336). % 2.28/2.49 tff(formula738, axiom, % 2.28/2.49 k!513($i!val!209) = $i!val!209). % 2.28/2.49 tff(formula739, axiom, % 2.28/2.49 k!513($i!val!356) = $i!val!356). % 2.28/2.49 tff(formula740, axiom, % 2.28/2.49 k!513($i!val!211) = $i!val!211). % 2.28/2.49 tff(formula741, axiom, % 2.28/2.49 k!513($i!val!407) = $i!val!407). % 2.28/2.49 tff(formula742, axiom, % 2.28/2.49 k!513($i!val!345) = $i!val!345). % 2.28/2.49 tff(formula743, axiom, % 2.28/2.49 k!513($i!val!173) = $i!val!173). % 2.28/2.49 tff(formula744, axiom, % 2.28/2.49 k!513($i!val!150) = $i!val!150). % 2.28/2.49 tff(formula745, axiom, % 2.28/2.49 k!513($i!val!396) = $i!val!396). % 2.28/2.49 tff(formula746, axiom, % 2.28/2.49 k!513($i!val!226) = $i!val!226). % 2.28/2.49 tff(formula747, axiom, % 2.28/2.49 k!513($i!val!152) = $i!val!152). % 2.28/2.49 tff(formula748, axiom, % 2.28/2.49 k!513($i!val!381) = $i!val!381). % 2.28/2.49 tff(formula749, axiom, % 2.28/2.49 k!513($i!val!82) = $i!val!82). % 2.28/2.49 tff(formula750, axiom, % 2.28/2.49 k!513($i!val!350) = $i!val!350). % 2.28/2.49 tff(formula751, axiom, % 2.28/2.49 k!513($i!val!414) = $i!val!414). % 2.28/2.49 tff(formula752, axiom, % 2.28/2.49 k!513($i!val!334) = $i!val!334). % 2.28/2.49 tff(formula753, axiom, % 2.28/2.49 k!513($i!val!35) = $i!val!35). % 2.28/2.49 tff(formula754, axiom, % 2.28/2.49 k!513($i!val!415) = $i!val!415). % 2.28/2.49 tff(formula755, axiom, % 2.28/2.49 k!513($i!val!359) = $i!val!359). % 2.28/2.49 tff(formula756, axiom, % 2.28/2.49 k!513($i!val!167) = $i!val!167). % 2.28/2.49 tff(formula757, axiom, % 2.28/2.49 k!513($i!val!117) = $i!val!117). % 2.28/2.49 tff(formula758, axiom, % 2.28/2.49 k!513($i!val!194) = $i!val!194). % 2.28/2.49 tff(formula759, axiom, % 2.28/2.49 k!513($i!val!370) = $i!val!370). % 2.28/2.49 tff(formula760, axiom, % 2.28/2.49 k!513($i!val!88) = $i!val!88). % 2.28/2.49 tff(formula761, axiom, % 2.28/2.49 k!513($i!val!193) = $i!val!193). % 2.28/2.49 tff(formula762, axiom, % 2.28/2.49 k!513($i!val!267) = $i!val!267). % 2.28/2.49 tff(formula763, axiom, % 2.28/2.49 k!513($i!val!149) = $i!val!149). % 2.28/2.49 tff(formula764, axiom, % 2.28/2.49 k!513($i!val!373) = $i!val!373). % 2.28/2.49 tff(formula765, axiom, % 2.28/2.49 k!513($i!val!162) = $i!val!162). % 2.28/2.49 tff(formula766, axiom, % 2.28/2.49 k!513($i!val!241) = $i!val!241). % 2.28/2.49 tff(formula767, axiom, % 2.28/2.49 k!513($i!val!429) = $i!val!429). % 2.28/2.49 tff(formula768, axiom, % 2.28/2.49 k!513($i!val!307) = $i!val!307). % 2.28/2.49 tff(formula769, axiom, % 2.28/2.49 k!513($i!val!282) = $i!val!282). % 2.28/2.49 tff(formula770, axiom, % 2.28/2.49 k!513($i!val!436) = $i!val!436). % 2.28/2.49 tff(formula771, axiom, % 2.28/2.49 k!513($i!val!81) = $i!val!81). % 2.28/2.49 tff(formula772, axiom, % 2.28/2.49 k!513($i!val!184) = $i!val!184). % 2.28/2.49 tff(formula773, axiom, % 2.28/2.49 k!513($i!val!287) = $i!val!287). % 2.28/2.49 tff(formula774, axiom, % 2.28/2.49 k!513($i!val!159) = $i!val!159). % 2.28/2.49 tff(formula775, axiom, % 2.28/2.49 k!513($i!val!399) = $i!val!399). % 2.28/2.49 tff(formula776, axiom, % 2.28/2.49 k!513($i!val!115) = $i!val!115). % 2.28/2.49 tff(formula777, axiom, % 2.28/2.49 k!513($i!val!305) = $i!val!305). % 2.28/2.49 tff(formula778, axiom, % 2.28/2.49 k!513($i!val!431) = $i!val!431). % 2.28/2.49 tff(formula779, axiom, % 2.28/2.49 k!513($i!val!278) = $i!val!278). % 2.28/2.49 tff(formula780, axiom, % 2.28/2.49 k!513($i!val!104) = $i!val!104). % 2.28/2.49 tff(formula781, axiom, % 2.28/2.49 k!513($i!val!91) = $i!val!91). % 2.28/2.49 tff(formula782, axiom, % 2.28/2.49 k!513($i!val!416) = $i!val!416). % 2.28/2.49 tff(formula783, axiom, % 2.28/2.49 k!513($i!val!29) = $i!val!29). % 2.28/2.49 tff(formula784, axiom, % 2.28/2.49 k!513($i!val!233) = $i!val!233). % 2.28/2.49 tff(formula785, axiom, % 2.28/2.49 k!513($i!val!367) = $i!val!367). % 2.28/2.49 tff(formula786, axiom, % 2.28/2.49 k!513($i!val!404) = $i!val!404). % 2.28/2.49 tff(formula787, axiom, % 2.28/2.49 k!513($i!val!14) = $i!val!14). % 2.28/2.49 tff(formula788, axiom, % 2.28/2.49 k!513($i!val!24) = $i!val!24). % 2.28/2.49 tff(formula789, axiom, % 2.28/2.49 k!513($i!val!122) = $i!val!122). % 2.28/2.49 tff(formula790, axiom, % 2.28/2.49 k!513($i!val!448) = $i!val!448). % 2.28/2.49 tff(formula791, axiom, % 2.28/2.49 k!513($i!val!288) = $i!val!288). % 2.28/2.49 tff(formula792, axiom, % 2.28/2.49 k!513($i!val!405) = $i!val!405). % 2.28/2.49 tff(formula793, axiom, % 2.28/2.49 k!513($i!val!5) = $i!val!5). % 2.28/2.49 tff(formula794, axiom, % 2.28/2.49 k!513($i!val!200) = $i!val!200). % 2.28/2.49 tff(formula795, axiom, % 2.28/2.49 k!513($i!val!430) = $i!val!430). % 2.28/2.49 tff(formula796, axiom, % 2.28/2.49 k!513($i!val!437) = $i!val!437). % 2.28/2.49 tff(formula797, axiom, % 2.28/2.49 k!513($i!val!353) = $i!val!353). % 2.28/2.49 tff(formula798, axiom, % 2.28/2.49 k!513($i!val!418) = $i!val!418). % 2.28/2.49 tff(formula799, axiom, % 2.28/2.49 k!513($i!val!27) = $i!val!27). % 2.28/2.49 tff(formula800, axiom, % 2.28/2.49 k!513($i!val!224) = $i!val!224). % 2.28/2.49 tff(formula801, axiom, % 2.28/2.49 k!513($i!val!348) = $i!val!348). % 2.28/2.49 tff(formula802, axiom, % 2.28/2.49 k!513($i!val!182) = $i!val!182). % 2.28/2.49 tff(formula803, axiom, % 2.28/2.49 k!513($i!val!457) = $i!val!457). % 2.28/2.49 tff(formula804, axiom, % 2.28/2.49 ![X0: $i] : ((~((($i!val!439 = X0)) | (($i!val!205 = X0)) | (($i!val!127 = X0)) | (($i!val!146 = X0)) | (($i!val!279 = X0)) | (($i!val!145 = X0)) | (($i!val!102 = X0)) | (($i!val!231 = X0)) | (($i!val!72 = X0)) | (($i!val!343 = X0)) | (($i!val!386 = X0)) | (($i!val!293 = X0)) | (($i!val!165 = X0)) | (($i!val!299 = X0)) | (($i!val!453 = X0)) | (($i!val!388 = X0)) | (($i!val!45 = X0)) | (($i!val!269 = X0)) | (($i!val!143 = X0)) | (($i!val!260 = X0)) | (($i!val!261 = X0)) | (($i!val!1 = X0)) | (($i!val!255 = X0)) | (($i!val!0 = X0)) | (($i!val!68 = X0)) | (($i!val!449 = X0)) | (($i!val!139 = X0)) | (($i!val!36 = X0)) | (($i!val!312 = X0)) | (($i!val!46 = X0)) | (($i!val!425 = X0)) | (($i!val!100 = X0)) | (($i!val!138 = X0)) | (($i!val!77 = X0)) | (($i!val!89 = X0)) | (($i!val!378 = X0)) | (($i!val!80 = X0)) | (($i!val!306 = X0)) | (($i!val!394 = X0)) | (($i!val!290 = X0)) | (($i!val!254 = X0)) | (($i!val!129 = X0)) | (($i!val!397 = X0)) | (($i!val!37 = X0)) | (($i!val!208 = X0)) | (($i!val!97 = X0)) | (($i!val!434 = X0)) | (($i!val!93 = X0)) | (($i!val!147 = X0)) | (($i!val!324 = X0)) | (($i!val!34 = X0)) | (($i!val!198 = X0)) | (($i!val!26 = X0)) | (($i!val!179 = X0)) | (($i!val!427 = X0)) | (($i!val!225 = X0)) | (($i!val!153 = X0)) | (($i!val!277 = X0)) | (($i!val!438 = X0)) | (($i!val!303 = X0)) | (($i!val!192 = X0)) | (($i!val!8 = X0)) | (($i!val!178 = X0)) | (($i!val!125 = X0)) | (($i!val!450 = X0)) | (($i!val!229 = X0)) | (($i!val!315 = X0)) | (($i!val!204 = X0)) | (($i!val!339 = X0)) | (($i!val!296 = X0)) | (($i!val!417 = X0)) | (($i!val!64 = X0)) | (($i!val!368 = X0)) | (($i!val!2 = X0)) | (($i!val!379 = X0)) | (($i!val!234 = X0)) | (($i!val!377 = X0)) | (($i!val!252 = X0)) | (($i!val!69 = X0)) | (($i!val!61 = X0)) | (($i!val!140 = X0)) | (($i!val!355 = X0)) | (($i!val!23 = X0)) | (($i!val!160 = X0)) | (($i!val!84 = X0)) | (($i!val!25 = X0)) | (($i!val!107 = X0)) | (($i!val!392 = X0)) | (($i!val!423 = X0)) | (($i!val!63 = X0)) | (($i!val!130 = X0)) | (($i!val!111 = X0)) | (($i!val!357 = X0)) | (($i!val!335 = X0)) | (($i!val!322 = X0)) | (($i!val!223 = X0)) | (($i!val!164 = X0)) | (($i!val!424 = X0)) | (($i!val!232 = X0)) | (($i!val!17 = X0)) | (($i!val!220 = X0)) | (($i!val!301 = X0)) | (($i!val!99 = X0)) | (($i!val!52 = X0)) | (($i!val!216 = X0)) | (($i!val!132 = X0)) | (($i!val!411 = X0)) | (($i!val!188 = X0)) | (($i!val!116 = X0)) | (($i!val!210 = X0)) | (($i!val!298 = X0)) | (($i!val!461 = X0)) | (($i!val!351 = X0)) | (($i!val!87 = X0)) | (($i!val!57 = X0)) | (($i!val!440 = X0)) | (($i!val!444 = X0)) | (($i!val!331 = X0)) | (($i!val!163 = X0)) | (($i!val!189 = X0)) | (($i!val!71 = X0)) | (($i!val!380 = X0)) | (($i!val!190 = X0)) | (($i!val!362 = X0)) | (($i!val!83 = X0)) | (($i!val!276 = X0)) | (($i!val!4 = X0)) | (($i!val!133 = X0)) | (($i!val!55 = X0)) | (($i!val!452 = X0)) | (($i!val!274 = X0)) | (($i!val!297 = X0)) | (($i!val!183 = X0)) | (($i!val!221 = X0)) | (($i!val!141 = X0)) | (($i!val!300 = X0)) | (($i!val!326 = X0)) | (($i!val!175 = X0)) | (($i!val!187 = X0)) | (($i!val!65 = X0)) | (($i!val!66 = X0)) | (($i!val!304 = X0)) | (($i!val!13 = X0)) | (($i!val!30 = X0)) | (($i!val!181 = X0)) | (($i!val!432 = X0)) | (($i!val!309 = X0)) | (($i!val!121 = X0)) | (($i!val!196 = X0)) | (($i!val!265 = X0)) | (($i!val!51 = X0)) | (($i!val!11 = X0)) | (($i!val!203 = X0)) | (($i!val!67 = X0)) | (($i!val!245 = X0)) | (($i!val!70 = X0)) | (($i!val!131 = X0)) | (($i!val!227 = X0)) | (($i!val!372 = X0)) | (($i!val!244 = X0)) | (($i!val!344 = X0)) | (($i!val!78 = X0)) | (($i!val!292 = X0)) | (($i!val!54 = X0)) | (($i!val!294 = X0)) | (($i!val!168 = X0)) | (($i!val!75 = X0)) | (($i!val!144 = X0)) | (($i!val!6 = X0)) | (($i!val!376 = X0)) | (($i!val!21 = X0)) | (($i!val!302 = X0)) | (($i!val!332 = X0)) | (($i!val!148 = X0)) | (($i!val!135 = X0)) | (($i!val!459 = X0)) | (($i!val!333 = X0)) | (($i!val!458 = X0)) | (($i!val!134 = X0)) | (($i!val!246 = X0)) | (($i!val!73 = X0)) | (($i!val!375 = X0)) | (($i!val!447 = X0)) | (($i!val!154 = X0)) | (($i!val!156 = X0)) | (($i!val!217 = X0)) | (($i!val!44 = X0)) | (($i!val!258 = X0)) | (($i!val!354 = X0)) | (($i!val!92 = X0)) | (($i!val!98 = X0)) | (($i!val!120 = X0)) | (($i!val!408 = X0)) | (($i!val!382 = X0)) | (($i!val!323 = X0)) | (($i!val!340 = X0)) | (($i!val!33 = X0)) | (($i!val!409 = X0)) | (($i!val!237 = X0)) | (($i!val!256 = X0)) | (($i!val!259 = X0)) | (($i!val!422 = X0)) | (($i!val!366 = X0)) | (($i!val!325 = X0)) | (($i!val!310 = X0)) | (($i!val!321 = X0)) | (($i!val!128 = X0)) | (($i!val!317 = X0)) | (($i!val!197 = X0)) | (($i!val!31 = X0)) | (($i!val!313 = X0)) | (($i!val!365 = X0)) | (($i!val!384 = X0)) | (($i!val!346 = X0)) | (($i!val!268 = X0)) | (($i!val!349 = X0)) | (($i!val!218 = X0)) | (($i!val!12 = X0)) | (($i!val!7 = X0)) | (($i!val!446 = X0)) | (($i!val!158 = X0)) | (($i!val!79 = X0)) | (($i!val!400 = X0)) | (($i!val!96 = X0)) | (($i!val!47 = X0)) | (($i!val!456 = X0)) | (($i!val!19 = X0)) | (($i!val!435 = X0)) | (($i!val!157 = X0)) | (($i!val!176 = X0)) | (($i!val!374 = X0)) | (($i!val!39 = X0)) | (($i!val!32 = X0)) | (($i!val!406 = X0)) | (($i!val!206 = X0)) | (($i!val!123 = X0)) | (($i!val!114 = X0)) | (($i!val!460 = X0)) | (($i!val!109 = X0)) | (($i!val!419 = X0)) | (($i!val!271 = X0)) | (($i!val!454 = X0)) | (($i!val!41 = X0)) | (($i!val!38 = X0)) | (($i!val!48 = X0)) | (($i!val!20 = X0)) | (($i!val!185 = X0)) | (($i!val!239 = X0)) | (($i!val!186 = X0)) | (($i!val!151 = X0)) | (($i!val!207 = X0)) | (($i!val!289 = X0)) | (($i!val!270 = X0)) | (($i!val!445 = X0)) | (($i!val!451 = X0)) | (($i!val!442 = X0)) | (($i!val!402 = X0)) | (($i!val!76 = X0)) | (($i!val!171 = X0)) | (($i!val!58 = X0)) | (($i!val!219 = X0)) | (($i!val!43 = X0)) | (($i!val!342 = X0)) | (($i!val!110 = X0)) | (($i!val!338 = X0)) | (($i!val!263 = X0)) | (($i!val!136 = X0)) | (($i!val!358 = X0)) | (($i!val!363 = X0)) | (($i!val!347 = X0)) | (($i!val!341 = X0)) | (($i!val!364 = X0)) | (($i!val!222 = X0)) | (($i!val!172 = X0)) | (($i!val!275 = X0)) | (($i!val!155 = X0)) | (($i!val!212 = X0)) | (($i!val!42 = X0)) | (($i!val!328 = X0)) | (($i!val!280 = X0)) | (($i!val!40 = X0)) | (($i!val!262 = X0)) | (($i!val!412 = X0)) | (($i!val!398 = X0)) | (($i!val!383 = X0)) | (($i!val!90 = X0)) | (($i!val!318 = X0)) | (($i!val!174 = X0)) | (($i!val!319 = X0)) | (($i!val!74 = X0)) | (($i!val!201 = X0)) | (($i!val!420 = X0)) | (($i!val!371 = X0)) | (($i!val!199 = X0)) | (($i!val!180 = X0)) | (($i!val!281 = X0)) | (($i!val!214 = X0)) | (($i!val!352 = X0)) | (($i!val!240 = X0)) | (($i!val!53 = X0)) | (($i!val!410 = X0)) | (($i!val!273 = X0)) | (($i!val!59 = X0)) | (($i!val!291 = X0)) | (($i!val!49 = X0)) | (($i!val!311 = X0)) | (($i!val!126 = X0)) | (($i!val!360 = X0)) | (($i!val!15 = X0)) | (($i!val!283 = X0)) | (($i!val!403 = X0)) | (($i!val!215 = X0)) | (($i!val!94 = X0)) | (($i!val!337 = X0)) | (($i!val!308 = X0)) | (($i!val!295 = X0)) | (($i!val!391 = X0)) | (($i!val!228 = X0)) | (($i!val!247 = X0)) | (($i!val!235 = X0)) | (($i!val!413 = X0)) | (($i!val!28 = X0)) | (($i!val!3 = X0)) | (($i!val!390 = X0)) | (($i!val!195 = X0)) | (($i!val!112 = X0)) | (($i!val!213 = X0)) | (($i!val!62 = X0)) | (($i!val!230 = X0)) | (($i!val!433 = X0)) | (($i!val!10 = X0)) | (($i!val!191 = X0)) | (($i!val!169 = X0)) | (($i!val!236 = X0)) | (($i!val!113 = X0)) | (($i!val!361 = X0)) | (($i!val!286 = X0)) | (($i!val!124 = X0)) | (($i!val!462 = X0)) | (($i!val!161 = X0)) | (($i!val!166 = X0)) | (($i!val!285 = X0)) | (($i!val!248 = X0)) | (($i!val!443 = X0)) | (($i!val!18 = X0)) | (($i!val!60 = X0)) | (($i!val!369 = X0)) | (($i!val!421 = X0)) | (($i!val!428 = X0)) | (($i!val!56 = X0)) | (($i!val!272 = X0)) | (($i!val!95 = X0)) | (($i!val!320 = X0)) | (($i!val!119 = X0)) | (($i!val!142 = X0)) | (($i!val!455 = X0)) | (($i!val!395 = X0)) | (($i!val!50 = X0)) | (($i!val!330 = X0)) | (($i!val!314 = X0)) | (($i!val!441 = X0)) | (($i!val!329 = X0)) | (($i!val!393 = X0)) | (($i!val!137 = X0)) | (($i!val!385 = X0)) | (($i!val!257 = X0)) | (($i!val!9 = X0)) | (($i!val!16 = X0)) | (($i!val!316 = X0)) | (($i!val!22 = X0)) | (($i!val!284 = X0)) | (($i!val!336 = X0)) | (($i!val!209 = X0)) | (($i!val!356 = X0)) | (($i!val!211 = X0)) | (($i!val!407 = X0)) | (($i!val!345 = X0)) | (($i!val!173 = X0)) | (($i!val!150 = X0)) | (($i!val!396 = X0)) | (($i!val!226 = X0)) | (($i!val!152 = X0)) | (($i!val!381 = X0)) | (($i!val!82 = X0)) | (($i!val!350 = X0)) | (($i!val!414 = X0)) | (($i!val!334 = X0)) | (($i!val!35 = X0)) | (($i!val!415 = X0)) | (($i!val!359 = X0)) | (($i!val!167 = X0)) | (($i!val!117 = X0)) | (($i!val!194 = X0)) | (($i!val!370 = X0)) | (($i!val!88 = X0)) | (($i!val!193 = X0)) | (($i!val!267 = X0)) | (($i!val!149 = X0)) | (($i!val!373 = X0)) | (($i!val!162 = X0)) | (($i!val!241 = X0)) | (($i!val!429 = X0)) | (($i!val!307 = X0)) | (($i!val!282 = X0)) | (($i!val!436 = X0)) | (($i!val!81 = X0)) | (($i!val!184 = X0)) | (($i!val!287 = X0)) | (($i!val!159 = X0)) | (($i!val!399 = X0)) | (($i!val!115 = X0)) | (($i!val!305 = X0)) | (($i!val!431 = X0)) | (($i!val!278 = X0)) | (($i!val!104 = X0)) | (($i!val!91 = X0)) | (($i!val!416 = X0)) | (($i!val!29 = X0)) | (($i!val!233 = X0)) | (($i!val!367 = X0)) | (($i!val!404 = X0)) | (($i!val!14 = X0)) | (($i!val!24 = X0)) | (($i!val!122 = X0)) | (($i!val!448 = X0)) | (($i!val!288 = X0)) | (($i!val!405 = X0)) | (($i!val!5 = X0)) | (($i!val!200 = X0)) | (($i!val!430 = X0)) | (($i!val!437 = X0)) | (($i!val!353 = X0)) | (($i!val!418 = X0)) | (($i!val!27 = X0)) | (($i!val!224 = X0)) | (($i!val!348 = X0)) | (($i!val!182 = X0)) | (($i!val!457 = X0)))) => (k!513(X0) = $i!val!243))). % 2.35/2.51 tff(formula805, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10422(X0) <=> (k!513(X0) = $i!val!417))). % 2.35/2.51 tff(formula806, axiom, % 2.35/2.51 ![X0: $i] : (k04_buttercup10639(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula807, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10098(X0) <=> $true)). % 2.35/2.51 tff(formula808, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10358(X0) <=> $true)). % 2.35/2.51 tff(formula809, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10170(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula810, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10052(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula811, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10191(X0) <=> (k!513(X0) = $i!val!452))). % 2.35/2.51 tff(formula812, axiom, % 2.35/2.51 ![X0: $i] : (k04_buttercup10096(X0) <=> ((~(k!513(X0) = $i!val!48)) & (~(k!513(X0) = $i!val!84))))). % 2.35/2.51 tff(formula813, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10405(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula814, axiom, % 2.35/2.51 ![X0: $i] : (k04_buttercup10506(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula815, axiom, % 2.35/2.51 ![X0: $i] : (k04_buttercup10406(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula816, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10579(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 tff(formula817, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10572(X0) <=> (k!513(X0) = $i!val!457))). % 2.35/2.51 tff(formula818, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10458(X0) <=> (~(k!513(X0) = $i!val!11)))). % 2.35/2.51 tff(formula819, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10179(X0) <=> (k!513(X0) = $i!val!272))). % 2.35/2.51 tff(formula820, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10352(X0) <=> (k!513(X0) = $i!val!455))). % 2.35/2.51 tff(formula821, axiom, % 2.35/2.51 ![X0: $i] : (k04_buttercup10517(X0) <=> ((k!513(X0) = $i!val!148) | (k!513(X0) = $i!val!270)))). % 2.35/2.51 tff(formula822, axiom, % 2.35/2.51 ![X0: $i] : (k04_buttercup10206(X0) <=> ((k!513(X0) = $i!val!156) | (k!513(X0) = $i!val!415)))). % 2.35/2.51 tff(formula823, axiom, % 2.35/2.51 ![X0: $i] : (b48_buttercup10058(X0) <=> (~(k!513(X0) = $i!val!48)))). % 2.35/2.51 % SZS output end Model % 2.35/2.52 % E exiting %------------------------------------------------------------------------------