%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : LCL643+1.015 : TPTP v9.3.1. Released v4.0.0. % Transfm : NO INFORMATION % Format : NO INFORMATION % Command : run_E %s %d THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 03:00:21 PM UTC 2026 % Result : CounterSatisfiable 119.26s 119.54s % Output : Model 119.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL643+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_E %s %d THM % 0.09/0.35 % Computer : n014.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 5 15:39:14 UTC 2026 % 0.09/0.35 % CPUTime : % 119.26/119.54 % SZS status CounterSatisfiable % 119.26/119.54 % SZS output start Model % 119.26/119.54 tff(tptp_fun__i_val_137_type, type, ( % 119.26/119.54 tptp_fun__i_val_137: $i)). % 119.26/119.54 tff(k!3259_type, type, ( % 119.26/119.54 k!3259: $i > $i)). % 119.26/119.54 tff(tptp_fun__i_val_155_type, type, ( % 119.26/119.54 tptp_fun__i_val_155: $i)). % 119.26/119.54 tff(tptp_fun__i_val_158_type, type, ( % 119.26/119.54 tptp_fun__i_val_158: $i)). % 119.26/119.54 tff(tptp_fun__i_val_175_type, type, ( % 119.26/119.54 tptp_fun__i_val_175: $i)). % 119.26/119.54 tff(tptp_fun__i_val_180_type, type, ( % 119.26/119.54 tptp_fun__i_val_180: $i)). % 119.26/119.54 tff(tptp_fun__i_val_189_type, type, ( % 119.26/119.54 tptp_fun__i_val_189: $i)). % 119.26/119.54 tff(tptp_fun__i_val_191_type, type, ( % 119.26/119.54 tptp_fun__i_val_191: $i)). % 119.26/119.54 tff(tptp_fun__i_val_187_type, type, ( % 119.26/119.54 tptp_fun__i_val_187: $i)). % 119.26/119.54 tff(tptp_fun__i_val_195_type, type, ( % 119.26/119.54 tptp_fun__i_val_195: $i)). % 119.26/119.54 tff(tptp_fun__i_val_129_type, type, ( % 119.26/119.54 tptp_fun__i_val_129: $i)). % 119.26/119.54 tff(tptp_fun__i_val_69_type, type, ( % 119.26/119.54 tptp_fun__i_val_69: $i)). % 119.26/119.54 tff(tptp_fun__i_val_199_type, type, ( % 119.26/119.54 tptp_fun__i_val_199: $i)). % 119.26/119.54 tff(tptp_fun__i_val_204_type, type, ( % 119.26/119.54 tptp_fun__i_val_204: $i)). % 119.26/119.54 tff(tptp_fun__i_val_224_type, type, ( % 119.26/119.55 tptp_fun__i_val_224: $i)). % 119.26/119.55 tff(tptp_fun__i_val_44_type, type, ( % 119.26/119.55 tptp_fun__i_val_44: $i)). % 119.26/119.55 tff(tptp_fun__i_val_11_type, type, ( % 119.26/119.55 tptp_fun__i_val_11: $i)). % 119.26/119.55 tff(tptp_fun__i_val_4_type, type, ( % 119.26/119.55 tptp_fun__i_val_4: $i)). % 119.26/119.55 tff(tptp_fun__i_val_238_type, type, ( % 119.26/119.55 tptp_fun__i_val_238: $i)). % 119.26/119.55 tff(tptp_fun__i_val_243_type, type, ( % 119.26/119.55 tptp_fun__i_val_243: $i)). % 119.26/119.55 tff(tptp_fun__i_val_245_type, type, ( % 119.26/119.55 tptp_fun__i_val_245: $i)). % 119.26/119.55 tff(tptp_fun__i_val_253_type, type, ( % 119.26/119.55 tptp_fun__i_val_253: $i)). % 119.26/119.55 tff(tptp_fun__i_val_256_type, type, ( % 119.26/119.55 tptp_fun__i_val_256: $i)). % 119.26/119.55 tff(tptp_fun__i_val_263_type, type, ( % 119.26/119.55 tptp_fun__i_val_263: $i)). % 119.26/119.55 tff(tptp_fun__i_val_271_type, type, ( % 119.26/119.55 tptp_fun__i_val_271: $i)). % 119.26/119.55 tff(tptp_fun__i_val_220_type, type, ( % 119.26/119.55 tptp_fun__i_val_220: $i)). % 119.26/119.55 tff(tptp_fun__i_val_222_type, type, ( % 119.26/119.55 tptp_fun__i_val_222: $i)). % 119.26/119.55 tff(tptp_fun__i_val_8_type, type, ( % 119.26/119.55 tptp_fun__i_val_8: $i)). % 119.26/119.55 tff(tptp_fun__i_val_49_type, type, ( % 119.26/119.55 tptp_fun__i_val_49: $i)). % 119.26/119.55 tff(tptp_fun__i_val_54_type, type, ( % 119.26/119.55 tptp_fun__i_val_54: $i)). % 119.26/119.55 tff(tptp_fun__i_val_23_type, type, ( % 119.26/119.55 tptp_fun__i_val_23: $i)). % 119.26/119.55 tff(tptp_fun__i_val_71_type, type, ( % 119.26/119.55 tptp_fun__i_val_71: $i)). % 119.26/119.55 tff(tptp_fun__i_val_88_type, type, ( % 119.26/119.55 tptp_fun__i_val_88: $i)). % 119.26/119.55 tff(tptp_fun__i_val_90_type, type, ( % 119.26/119.55 tptp_fun__i_val_90: $i)). % 119.26/119.55 tff(tptp_fun__i_val_96_type, type, ( % 119.26/119.55 tptp_fun__i_val_96: $i)). % 119.26/119.55 tff(tptp_fun__i_val_19_type, type, ( % 119.26/119.55 tptp_fun__i_val_19: $i)). % 119.26/119.55 tff(tptp_fun__i_val_103_type, type, ( % 119.26/119.55 tptp_fun__i_val_103: $i)). % 119.26/119.55 tff(tptp_fun__i_val_105_type, type, ( % 119.26/119.55 tptp_fun__i_val_105: $i)). % 119.26/119.55 tff(tptp_fun__i_val_108_type, type, ( % 119.26/119.55 tptp_fun__i_val_108: $i)). % 119.26/119.55 tff(tptp_fun__i_val_110_type, type, ( % 119.26/119.55 tptp_fun__i_val_110: $i)). % 119.26/119.55 tff(tptp_fun__i_val_68_type, type, ( % 119.26/119.55 tptp_fun__i_val_68: $i)). % 119.26/119.55 tff(tptp_fun__i_val_34_type, type, ( % 119.26/119.55 tptp_fun__i_val_34: $i)). % 119.26/119.55 tff(tptp_fun__i_val_6_type, type, ( % 119.26/119.55 tptp_fun__i_val_6: $i)). % 119.26/119.55 tff(tptp_fun__i_val_123_type, type, ( % 119.26/119.55 tptp_fun__i_val_123: $i)). % 119.26/119.55 tff(p2_type, type, ( % 119.26/119.55 p2: $i > $o)). % 119.26/119.55 tff(tptp_fun__i_val_40_type, type, ( % 119.26/119.55 tptp_fun__i_val_40: $i)). % 119.26/119.55 tff(tptp_fun__i_val_28_type, type, ( % 119.26/119.55 tptp_fun__i_val_28: $i)). % 119.26/119.55 tff(tptp_fun__i_val_59_type, type, ( % 119.26/119.55 tptp_fun__i_val_59: $i)). % 119.26/119.55 tff(tptp_fun__i_val_86_type, type, ( % 119.26/119.55 tptp_fun__i_val_86: $i)). % 119.26/119.55 tff(tptp_fun__i_val_10_type, type, ( % 119.26/119.55 tptp_fun__i_val_10: $i)). % 119.26/119.55 tff(tptp_fun__i_val_7_type, type, ( % 119.26/119.55 tptp_fun__i_val_7: $i)). % 119.26/119.55 tff(p4_type, type, ( % 119.26/119.55 p4: $i > $o)). % 119.26/119.55 tff(tptp_fun__i_val_25_type, type, ( % 119.26/119.55 tptp_fun__i_val_25: $i)). % 119.26/119.55 tff(tptp_fun__i_val_140_type, type, ( % 119.26/119.55 tptp_fun__i_val_140: $i)). % 119.26/119.55 tff(tptp_fun__i_val_225_type, type, ( % 119.26/119.55 tptp_fun__i_val_225: $i)). % 119.26/119.55 tff(tptp_fun__i_val_270_type, type, ( % 119.26/119.55 tptp_fun__i_val_270: $i)). % 119.26/119.55 tff(tptp_fun__i_val_57_type, type, ( % 119.26/119.55 tptp_fun__i_val_57: $i)). % 119.26/119.55 tff(tptp_fun__i_val_201_type, type, ( % 119.26/119.55 tptp_fun__i_val_201: $i)). % 119.26/119.55 tff(tptp_fun__i_val_154_type, type, ( % 119.26/119.55 tptp_fun__i_val_154: $i)). % 119.26/119.55 tff(tptp_fun__i_val_131_type, type, ( % 119.26/119.55 tptp_fun__i_val_131: $i)). % 119.26/119.55 tff(tptp_fun__i_val_43_type, type, ( % 119.26/119.55 tptp_fun__i_val_43: $i)). % 119.26/119.55 tff(tptp_fun__i_val_244_type, type, ( % 119.26/119.55 tptp_fun__i_val_244: $i)). % 119.26/119.55 tff(tptp_fun__i_val_70_type, type, ( % 119.26/119.55 tptp_fun__i_val_70: $i)). % 119.26/119.55 tff(tptp_fun__i_val_65_type, type, ( % 119.26/119.55 tptp_fun__i_val_65: $i)). % 119.26/119.55 tff(tptp_fun__i_val_41_type, type, ( % 119.26/119.55 tptp_fun__i_val_41: $i)). % 119.26/119.55 tff(tptp_fun__i_val_226_type, type, ( % 119.26/119.55 tptp_fun__i_val_226: $i)). % 119.26/119.55 tff(tptp_fun__i_val_111_type, type, ( % 119.26/119.55 tptp_fun__i_val_111: $i)). % 119.26/119.55 tff(tptp_fun__i_val_212_type, type, ( % 119.26/119.55 tptp_fun__i_val_212: $i)). % 119.26/119.55 tff(tptp_fun__i_val_115_type, type, ( % 119.26/119.55 tptp_fun__i_val_115: $i)). % 119.26/119.55 tff(tptp_fun__i_val_255_type, type, ( % 119.26/119.55 tptp_fun__i_val_255: $i)). % 119.26/119.55 tff(tptp_fun__i_val_53_type, type, ( % 119.26/119.55 tptp_fun__i_val_53: $i)). % 119.26/119.55 tff(tptp_fun__i_val_166_type, type, ( % 119.26/119.55 tptp_fun__i_val_166: $i)). % 119.26/119.55 tff(tptp_fun__i_val_1_type, type, ( % 119.26/119.55 tptp_fun__i_val_1: $i)). % 119.26/119.55 tff(tptp_fun__i_val_92_type, type, ( % 119.26/119.55 tptp_fun__i_val_92: $i)). % 119.26/119.55 tff(tptp_fun__i_val_193_type, type, ( % 119.26/119.55 tptp_fun__i_val_193: $i)). % 119.26/119.55 tff(tptp_fun__i_val_51_type, type, ( % 119.26/119.55 tptp_fun__i_val_51: $i)). % 119.26/119.55 tff(tptp_fun__i_val_235_type, type, ( % 119.26/119.55 tptp_fun__i_val_235: $i)). % 119.26/119.55 tff(tptp_fun__i_val_31_type, type, ( % 119.26/119.55 tptp_fun__i_val_31: $i)). % 119.26/119.55 tff(tptp_fun__i_val_251_type, type, ( % 119.26/119.55 tptp_fun__i_val_251: $i)). % 119.26/119.55 tff(tptp_fun__i_val_67_type, type, ( % 119.26/119.55 tptp_fun__i_val_67: $i)). % 119.26/119.55 tff(tptp_fun__i_val_164_type, type, ( % 119.26/119.55 tptp_fun__i_val_164: $i)). % 119.26/119.55 tff(tptp_fun__i_val_52_type, type, ( % 119.26/119.55 tptp_fun__i_val_52: $i)). % 119.26/119.55 tff(tptp_fun__i_val_74_type, type, ( % 119.26/119.55 tptp_fun__i_val_74: $i)). % 119.26/119.55 tff(tptp_fun__i_val_186_type, type, ( % 119.26/119.55 tptp_fun__i_val_186: $i)). % 119.26/119.55 tff(tptp_fun__i_val_178_type, type, ( % 119.26/119.55 tptp_fun__i_val_178: $i)). % 119.26/119.55 tff(tptp_fun__i_val_188_type, type, ( % 119.26/119.55 tptp_fun__i_val_188: $i)). % 119.26/119.55 tff(tptp_fun__i_val_261_type, type, ( % 119.26/119.55 tptp_fun__i_val_261: $i)). % 119.26/119.55 tff(tptp_fun__i_val_216_type, type, ( % 119.26/119.55 tptp_fun__i_val_216: $i)). % 119.26/119.55 tff(tptp_fun__i_val_72_type, type, ( % 119.26/119.55 tptp_fun__i_val_72: $i)). % 119.26/119.55 tff(tptp_fun__i_val_124_type, type, ( % 119.26/119.55 tptp_fun__i_val_124: $i)). % 119.26/119.55 tff(tptp_fun__i_val_157_type, type, ( % 119.26/119.55 tptp_fun__i_val_157: $i)). % 119.26/119.55 tff(tptp_fun__i_val_18_type, type, ( % 119.26/119.55 tptp_fun__i_val_18: $i)). % 119.26/119.55 tff(tptp_fun__i_val_132_type, type, ( % 119.26/119.55 tptp_fun__i_val_132: $i)). % 119.26/119.55 tff(tptp_fun__i_val_234_type, type, ( % 119.26/119.55 tptp_fun__i_val_234: $i)). % 119.26/119.55 tff(tptp_fun__i_val_77_type, type, ( % 119.26/119.55 tptp_fun__i_val_77: $i)). % 119.26/119.55 tff(tptp_fun__i_val_260_type, type, ( % 119.26/119.55 tptp_fun__i_val_260: $i)). % 119.26/119.55 tff(tptp_fun__i_val_241_type, type, ( % 119.26/119.55 tptp_fun__i_val_241: $i)). % 119.26/119.55 tff(tptp_fun__i_val_101_type, type, ( % 119.26/119.55 tptp_fun__i_val_101: $i)). % 119.26/119.55 tff(tptp_fun__i_val_116_type, type, ( % 119.26/119.55 tptp_fun__i_val_116: $i)). % 119.26/119.55 tff(tptp_fun__i_val_3_type, type, ( % 119.26/119.55 tptp_fun__i_val_3: $i)). % 119.26/119.55 tff(tptp_fun__i_val_122_type, type, ( % 119.26/119.55 tptp_fun__i_val_122: $i)). % 119.26/119.55 tff(tptp_fun__i_val_97_type, type, ( % 119.26/119.55 tptp_fun__i_val_97: $i)). % 119.26/119.55 tff(tptp_fun__i_val_16_type, type, ( % 119.26/119.55 tptp_fun__i_val_16: $i)). % 119.26/119.55 tff(tptp_fun__i_val_85_type, type, ( % 119.26/119.55 tptp_fun__i_val_85: $i)). % 119.26/119.55 tff(tptp_fun__i_val_165_type, type, ( % 119.26/119.55 tptp_fun__i_val_165: $i)). % 119.26/119.55 tff(tptp_fun__i_val_29_type, type, ( % 119.26/119.55 tptp_fun__i_val_29: $i)). % 119.26/119.55 tff(tptp_fun__i_val_149_type, type, ( % 119.26/119.55 tptp_fun__i_val_149: $i)). % 119.26/119.55 tff(tptp_fun__i_val_168_type, type, ( % 119.26/119.55 tptp_fun__i_val_168: $i)). % 119.26/119.55 tff(tptp_fun__i_val_13_type, type, ( % 119.26/119.55 tptp_fun__i_val_13: $i)). % 119.26/119.55 tff(tptp_fun__i_val_99_type, type, ( % 119.26/119.55 tptp_fun__i_val_99: $i)). % 119.26/119.55 tff(tptp_fun__i_val_117_type, type, ( % 119.26/119.55 tptp_fun__i_val_117: $i)). % 119.26/119.55 tff(tptp_fun__i_val_210_type, type, ( % 119.26/119.55 tptp_fun__i_val_210: $i)). % 119.26/119.55 tff(tptp_fun__i_val_9_type, type, ( % 119.26/119.55 tptp_fun__i_val_9: $i)). % 119.26/119.55 tff(tptp_fun__i_val_217_type, type, ( % 119.26/119.55 tptp_fun__i_val_217: $i)). % 119.26/119.55 tff(tptp_fun__i_val_83_type, type, ( % 119.26/119.55 tptp_fun__i_val_83: $i)). % 119.26/119.55 tff(tptp_fun__i_val_152_type, type, ( % 119.26/119.55 tptp_fun__i_val_152: $i)). % 119.26/119.55 tff(tptp_fun__i_val_14_type, type, ( % 119.26/119.55 tptp_fun__i_val_14: $i)). % 119.26/119.55 tff(tptp_fun__i_val_237_type, type, ( % 119.26/119.55 tptp_fun__i_val_237: $i)). % 119.26/119.55 tff(tptp_fun__i_val_130_type, type, ( % 119.26/119.55 tptp_fun__i_val_130: $i)). % 119.26/119.55 tff(tptp_fun__i_val_73_type, type, ( % 119.26/119.55 tptp_fun__i_val_73: $i)). % 119.26/119.55 tff(tptp_fun__i_val_87_type, type, ( % 119.26/119.55 tptp_fun__i_val_87: $i)). % 119.26/119.55 tff(tptp_fun__i_val_20_type, type, ( % 119.26/119.55 tptp_fun__i_val_20: $i)). % 119.26/119.55 tff(tptp_fun__i_val_148_type, type, ( % 119.26/119.55 tptp_fun__i_val_148: $i)). % 119.26/119.55 tff(tptp_fun__i_val_125_type, type, ( % 119.26/119.55 tptp_fun__i_val_125: $i)). % 119.26/119.55 tff(tptp_fun__i_val_156_type, type, ( % 119.26/119.55 tptp_fun__i_val_156: $i)). % 119.26/119.55 tff(tptp_fun__i_val_202_type, type, ( % 119.26/119.55 tptp_fun__i_val_202: $i)). % 119.26/119.55 tff(tptp_fun__i_val_211_type, type, ( % 119.26/119.55 tptp_fun__i_val_211: $i)). % 119.26/119.55 tff(tptp_fun__i_val_268_type, type, ( % 119.26/119.55 tptp_fun__i_val_268: $i)). % 119.26/119.55 tff(tptp_fun__i_val_266_type, type, ( % 119.26/119.55 tptp_fun__i_val_266: $i)). % 119.26/119.55 tff(tptp_fun__i_val_114_type, type, ( % 119.26/119.55 tptp_fun__i_val_114: $i)). % 119.26/119.55 tff(tptp_fun__i_val_223_type, type, ( % 119.26/119.55 tptp_fun__i_val_223: $i)). % 119.26/119.55 tff(tptp_fun__i_val_259_type, type, ( % 119.26/119.55 tptp_fun__i_val_259: $i)). % 119.26/119.55 tff(tptp_fun__i_val_227_type, type, ( % 119.26/119.55 tptp_fun__i_val_227: $i)). % 119.26/119.55 tff(tptp_fun__i_val_63_type, type, ( % 119.26/119.55 tptp_fun__i_val_63: $i)). % 119.26/119.55 tff(tptp_fun__i_val_214_type, type, ( % 119.26/119.55 tptp_fun__i_val_214: $i)). % 119.26/119.55 tff(tptp_fun__i_val_98_type, type, ( % 119.26/119.55 tptp_fun__i_val_98: $i)). % 119.26/119.55 tff(tptp_fun__i_val_112_type, type, ( % 119.26/119.55 tptp_fun__i_val_112: $i)). % 119.26/119.55 tff(tptp_fun__i_val_89_type, type, ( % 119.26/119.55 tptp_fun__i_val_89: $i)). % 119.26/119.55 tff(tptp_fun__i_val_163_type, type, ( % 119.26/119.55 tptp_fun__i_val_163: $i)). % 119.26/119.55 tff(tptp_fun__i_val_257_type, type, ( % 119.26/119.55 tptp_fun__i_val_257: $i)). % 119.26/119.55 tff(tptp_fun__i_val_24_type, type, ( % 119.26/119.55 tptp_fun__i_val_24: $i)). % 119.26/119.55 tff(tptp_fun__i_val_36_type, type, ( % 119.26/119.55 tptp_fun__i_val_36: $i)). % 119.26/119.55 tff(tptp_fun__i_val_61_type, type, ( % 119.26/119.55 tptp_fun__i_val_61: $i)). % 119.26/119.55 tff(tptp_fun__i_val_109_type, type, ( % 119.26/119.55 tptp_fun__i_val_109: $i)). % 119.26/119.55 tff(tptp_fun__i_val_169_type, type, ( % 119.26/119.55 tptp_fun__i_val_169: $i)). % 119.26/119.55 tff(tptp_fun__i_val_185_type, type, ( % 119.26/119.55 tptp_fun__i_val_185: $i)). % 119.26/119.55 tff(tptp_fun__i_val_240_type, type, ( % 119.26/119.55 tptp_fun__i_val_240: $i)). % 119.26/119.55 tff(tptp_fun__i_val_161_type, type, ( % 119.26/119.55 tptp_fun__i_val_161: $i)). % 119.26/119.55 tff(tptp_fun__i_val_93_type, type, ( % 119.26/119.55 tptp_fun__i_val_93: $i)). % 119.26/119.55 tff(tptp_fun__i_val_62_type, type, ( % 119.26/119.55 tptp_fun__i_val_62: $i)). % 119.26/119.55 tff(tptp_fun__i_val_84_type, type, ( % 119.26/119.55 tptp_fun__i_val_84: $i)). % 119.26/119.55 tff(tptp_fun__i_val_153_type, type, ( % 119.26/119.55 tptp_fun__i_val_153: $i)). % 119.26/119.55 tff(tptp_fun__i_val_159_type, type, ( % 119.26/119.55 tptp_fun__i_val_159: $i)). % 119.26/119.55 tff(tptp_fun__i_val_126_type, type, ( % 119.26/119.55 tptp_fun__i_val_126: $i)). % 119.26/119.55 tff(tptp_fun__i_val_106_type, type, ( % 119.26/119.55 tptp_fun__i_val_106: $i)). % 119.26/119.55 tff(tptp_fun__i_val_203_type, type, ( % 119.26/119.55 tptp_fun__i_val_203: $i)). % 119.26/119.55 tff(tptp_fun__i_val_75_type, type, ( % 119.26/119.55 tptp_fun__i_val_75: $i)). % 119.26/119.55 tff(tptp_fun__i_val_267_type, type, ( % 119.26/119.55 tptp_fun__i_val_267: $i)). % 119.26/119.55 tff(tptp_fun__i_val_192_type, type, ( % 119.26/119.55 tptp_fun__i_val_192: $i)). % 119.26/119.55 tff(tptp_fun__i_val_0_type, type, ( % 119.26/119.55 tptp_fun__i_val_0: $i)). % 119.26/119.55 tff(tptp_fun__i_val_12_type, type, ( % 119.26/119.55 tptp_fun__i_val_12: $i)). % 119.26/119.55 tff(tptp_fun__i_val_134_type, type, ( % 119.26/119.55 tptp_fun__i_val_134: $i)). % 119.26/119.55 tff(tptp_fun__i_val_147_type, type, ( % 119.26/119.55 tptp_fun__i_val_147: $i)). % 119.26/119.55 tff(tptp_fun__i_val_215_type, type, ( % 119.26/119.55 tptp_fun__i_val_215: $i)). % 119.26/119.55 tff(tptp_fun__i_val_113_type, type, ( % 119.26/119.55 tptp_fun__i_val_113: $i)). % 119.26/119.55 tff(tptp_fun__i_val_27_type, type, ( % 119.26/119.55 tptp_fun__i_val_27: $i)). % 119.26/119.55 tff(tptp_fun__i_val_258_type, type, ( % 119.26/119.55 tptp_fun__i_val_258: $i)). % 119.26/119.55 tff(tptp_fun__i_val_37_type, type, ( % 119.26/119.55 tptp_fun__i_val_37: $i)). % 119.26/119.55 tff(tptp_fun__i_val_176_type, type, ( % 119.26/119.55 tptp_fun__i_val_176: $i)). % 119.26/119.55 tff(tptp_fun__i_val_135_type, type, ( % 119.26/119.55 tptp_fun__i_val_135: $i)). % 119.26/119.55 tff(tptp_fun__i_val_145_type, type, ( % 119.26/119.55 tptp_fun__i_val_145: $i)). % 119.26/119.55 tff(tptp_fun__i_val_219_type, type, ( % 119.26/119.55 tptp_fun__i_val_219: $i)). % 119.26/119.55 tff(tptp_fun__i_val_269_type, type, ( % 119.26/119.55 tptp_fun__i_val_269: $i)). % 119.26/119.55 tff(tptp_fun__i_val_162_type, type, ( % 119.26/119.55 tptp_fun__i_val_162: $i)). % 119.26/119.55 tff(tptp_fun__i_val_17_type, type, ( % 119.26/119.55 tptp_fun__i_val_17: $i)). % 119.26/119.55 tff(tptp_fun__i_val_239_type, type, ( % 119.26/119.55 tptp_fun__i_val_239: $i)). % 119.26/119.55 tff(tptp_fun__i_val_94_type, type, ( % 119.26/119.55 tptp_fun__i_val_94: $i)). % 119.26/119.55 tff(tptp_fun__i_val_190_type, type, ( % 119.26/119.55 tptp_fun__i_val_190: $i)). % 119.26/119.55 tff(tptp_fun__i_val_236_type, type, ( % 119.26/119.55 tptp_fun__i_val_236: $i)). % 119.26/119.55 tff(tptp_fun__i_val_167_type, type, ( % 119.26/119.55 tptp_fun__i_val_167: $i)). % 119.26/119.55 tff(tptp_fun__i_val_183_type, type, ( % 119.26/119.55 tptp_fun__i_val_183: $i)). % 119.26/119.55 tff(tptp_fun__i_val_100_type, type, ( % 119.26/119.55 tptp_fun__i_val_100: $i)). % 119.26/119.55 tff(tptp_fun__i_val_76_type, type, ( % 119.26/119.55 tptp_fun__i_val_76: $i)). % 119.26/119.55 tff(tptp_fun__i_val_128_type, type, ( % 119.26/119.55 tptp_fun__i_val_128: $i)). % 119.26/119.55 tff(tptp_fun__i_val_242_type, type, ( % 119.26/119.55 tptp_fun__i_val_242: $i)). % 119.26/119.55 tff(tptp_fun__i_val_50_type, type, ( % 119.26/119.55 tptp_fun__i_val_50: $i)). % 119.26/119.55 tff(tptp_fun__i_val_264_type, type, ( % 119.26/119.55 tptp_fun__i_val_264: $i)). % 119.26/119.55 tff(tptp_fun__i_val_32_type, type, ( % 119.26/119.55 tptp_fun__i_val_32: $i)). % 119.26/119.55 tff(tptp_fun__i_val_209_type, type, ( % 119.26/119.55 tptp_fun__i_val_209: $i)). % 119.26/119.55 tff(tptp_fun__i_val_107_type, type, ( % 119.26/119.55 tptp_fun__i_val_107: $i)). % 119.26/119.55 tff(tptp_fun__i_val_22_type, type, ( % 119.26/119.55 tptp_fun__i_val_22: $i)). % 119.26/119.55 tff(tptp_fun__i_val_136_type, type, ( % 119.26/119.55 tptp_fun__i_val_136: $i)). % 119.26/119.55 tff(tptp_fun__i_val_102_type, type, ( % 119.26/119.55 tptp_fun__i_val_102: $i)). % 119.26/119.55 tff(tptp_fun__i_val_121_type, type, ( % 119.26/119.55 tptp_fun__i_val_121: $i)). % 119.26/119.55 tff(tptp_fun__i_val_265_type, type, ( % 119.26/119.55 tptp_fun__i_val_265: $i)). % 119.26/119.55 tff(tptp_fun__i_val_146_type, type, ( % 119.26/119.55 tptp_fun__i_val_146: $i)). % 119.26/119.55 tff(tptp_fun__i_val_172_type, type, ( % 119.26/119.55 tptp_fun__i_val_172: $i)). % 119.26/119.55 tff(tptp_fun__i_val_33_type, type, ( % 119.26/119.55 tptp_fun__i_val_33: $i)). % 119.26/119.55 tff(tptp_fun__i_val_38_type, type, ( % 119.26/119.55 tptp_fun__i_val_38: $i)). % 119.26/119.55 tff(tptp_fun__i_val_78_type, type, ( % 119.26/119.55 tptp_fun__i_val_78: $i)). % 119.26/119.55 tff(tptp_fun__i_val_246_type, type, ( % 119.26/119.55 tptp_fun__i_val_246: $i)). % 119.26/119.55 tff(tptp_fun__i_val_160_type, type, ( % 119.26/119.55 tptp_fun__i_val_160: $i)). % 119.26/119.55 tff(tptp_fun__i_val_184_type, type, ( % 119.26/119.55 tptp_fun__i_val_184: $i)). % 119.26/119.55 tff(tptp_fun__i_val_170_type, type, ( % 119.26/119.55 tptp_fun__i_val_170: $i)). % 119.26/119.55 tff(tptp_fun__i_val_104_type, type, ( % 119.26/119.55 tptp_fun__i_val_104: $i)). % 119.26/119.55 tff(tptp_fun__i_val_254_type, type, ( % 119.26/119.55 tptp_fun__i_val_254: $i)). % 119.26/119.55 tff(tptp_fun__i_val_179_type, type, ( % 119.26/119.55 tptp_fun__i_val_179: $i)). % 119.26/119.55 tff(tptp_fun__i_val_151_type, type, ( % 119.26/119.55 tptp_fun__i_val_151: $i)). % 119.26/119.55 tff(tptp_fun__i_val_198_type, type, ( % 119.26/119.55 tptp_fun__i_val_198: $i)). % 119.26/119.55 tff(tptp_fun__i_val_95_type, type, ( % 119.26/119.55 tptp_fun__i_val_95: $i)). % 119.26/119.55 tff(tptp_fun__i_val_233_type, type, ( % 119.26/119.55 tptp_fun__i_val_233: $i)). % 119.26/119.55 tff(tptp_fun__i_val_228_type, type, ( % 119.26/119.55 tptp_fun__i_val_228: $i)). % 119.26/119.55 tff(tptp_fun__i_val_48_type, type, ( % 119.26/119.55 tptp_fun__i_val_48: $i)). % 119.26/119.55 tff(tptp_fun__i_val_205_type, type, ( % 119.26/119.55 tptp_fun__i_val_205: $i)). % 119.26/119.55 tff(tptp_fun__i_val_232_type, type, ( % 119.26/119.55 tptp_fun__i_val_232: $i)). % 119.26/119.55 tff(tptp_fun__i_val_5_type, type, ( % 119.26/119.55 tptp_fun__i_val_5: $i)). % 119.26/119.55 tff(tptp_fun__i_val_144_type, type, ( % 119.26/119.55 tptp_fun__i_val_144: $i)). % 119.26/119.55 tff(tptp_fun__i_val_194_type, type, ( % 119.26/119.55 tptp_fun__i_val_194: $i)). % 119.26/119.55 tff(tptp_fun__i_val_230_type, type, ( % 119.26/119.55 tptp_fun__i_val_230: $i)). % 119.26/119.55 tff(tptp_fun__i_val_208_type, type, ( % 119.26/119.55 tptp_fun__i_val_208: $i)). % 119.26/119.55 tff(tptp_fun__i_val_15_type, type, ( % 119.26/119.55 tptp_fun__i_val_15: $i)). % 119.26/119.55 tff(tptp_fun__i_val_42_type, type, ( % 119.26/119.55 tptp_fun__i_val_42: $i)). % 119.26/119.55 tff(tptp_fun__i_val_142_type, type, ( % 119.26/119.55 tptp_fun__i_val_142: $i)). % 119.26/119.55 tff(tptp_fun__i_val_213_type, type, ( % 119.26/119.55 tptp_fun__i_val_213: $i)). % 119.26/119.55 tff(tptp_fun__i_val_82_type, type, ( % 119.26/119.55 tptp_fun__i_val_82: $i)). % 119.26/119.55 tff(tptp_fun__i_val_174_type, type, ( % 119.26/119.55 tptp_fun__i_val_174: $i)). % 119.26/119.55 tff(tptp_fun__i_val_79_type, type, ( % 119.26/119.55 tptp_fun__i_val_79: $i)). % 119.26/119.55 tff(tptp_fun__i_val_171_type, type, ( % 119.26/119.55 tptp_fun__i_val_171: $i)). % 119.26/119.55 tff(tptp_fun__i_val_80_type, type, ( % 119.26/119.55 tptp_fun__i_val_80: $i)). % 119.26/119.55 tff(tptp_fun__i_val_118_type, type, ( % 119.26/119.55 tptp_fun__i_val_118: $i)). % 119.26/119.55 tff(tptp_fun__i_val_127_type, type, ( % 119.26/119.55 tptp_fun__i_val_127: $i)). % 119.26/119.55 tff(tptp_fun__i_val_47_type, type, ( % 119.26/119.55 tptp_fun__i_val_47: $i)). % 119.26/119.55 tff(tptp_fun__i_val_119_type, type, ( % 119.26/119.55 tptp_fun__i_val_119: $i)). % 119.26/119.55 tff(tptp_fun__i_val_206_type, type, ( % 119.26/119.55 tptp_fun__i_val_206: $i)). % 119.26/119.55 tff(tptp_fun__i_val_196_type, type, ( % 119.26/119.55 tptp_fun__i_val_196: $i)). % 119.26/119.55 tff(tptp_fun__i_val_56_type, type, ( % 119.26/119.55 tptp_fun__i_val_56: $i)). % 119.26/119.55 tff(tptp_fun__i_val_45_type, type, ( % 119.26/119.55 tptp_fun__i_val_45: $i)). % 119.26/119.55 tff(tptp_fun__i_val_262_type, type, ( % 119.26/119.55 tptp_fun__i_val_262: $i)). % 119.26/119.55 tff(tptp_fun__i_val_60_type, type, ( % 119.26/119.55 tptp_fun__i_val_60: $i)). % 119.26/119.55 tff(tptp_fun__i_val_231_type, type, ( % 119.26/119.55 tptp_fun__i_val_231: $i)). % 119.26/119.55 tff(tptp_fun__i_val_35_type, type, ( % 119.26/119.55 tptp_fun__i_val_35: $i)). % 119.26/119.55 tff(tptp_fun__i_val_39_type, type, ( % 119.26/119.55 tptp_fun__i_val_39: $i)). % 119.26/119.55 tff(tptp_fun__i_val_46_type, type, ( % 119.26/119.55 tptp_fun__i_val_46: $i)). % 119.26/119.55 tff(tptp_fun__i_val_143_type, type, ( % 119.26/119.55 tptp_fun__i_val_143: $i)). % 119.26/119.55 tff(tptp_fun__i_val_133_type, type, ( % 119.26/119.55 tptp_fun__i_val_133: $i)). % 119.26/119.55 tff(tptp_fun__i_val_58_type, type, ( % 119.26/119.55 tptp_fun__i_val_58: $i)). % 119.26/119.55 tff(tptp_fun__i_val_221_type, type, ( % 119.26/119.55 tptp_fun__i_val_221: $i)). % 119.26/119.55 tff(tptp_fun__i_val_207_type, type, ( % 119.26/119.55 tptp_fun__i_val_207: $i)). % 119.26/119.55 tff(tptp_fun__i_val_182_type, type, ( % 119.26/119.55 tptp_fun__i_val_182: $i)). % 119.26/119.55 tff(tptp_fun__i_val_120_type, type, ( % 119.26/119.55 tptp_fun__i_val_120: $i)). % 119.26/119.55 tff(tptp_fun__i_val_141_type, type, ( % 119.26/119.55 tptp_fun__i_val_141: $i)). % 119.26/119.55 tff(tptp_fun__i_val_81_type, type, ( % 119.26/119.55 tptp_fun__i_val_81: $i)). % 119.26/119.55 tff(tptp_fun__i_val_30_type, type, ( % 119.26/119.55 tptp_fun__i_val_30: $i)). % 119.26/119.55 tff(tptp_fun__i_val_181_type, type, ( % 119.26/119.55 tptp_fun__i_val_181: $i)). % 119.26/119.55 tff(tptp_fun__i_val_197_type, type, ( % 119.26/119.55 tptp_fun__i_val_197: $i)). % 119.26/119.55 tff(tptp_fun__i_val_229_type, type, ( % 119.26/119.55 tptp_fun__i_val_229: $i)). % 119.26/119.55 tff(tptp_fun__i_val_139_type, type, ( % 119.26/119.55 tptp_fun__i_val_139: $i)). % 119.26/119.55 tff(tptp_fun__i_val_248_type, type, ( % 119.26/119.55 tptp_fun__i_val_248: $i)). % 119.26/119.55 tff(tptp_fun__i_val_252_type, type, ( % 119.26/119.55 tptp_fun__i_val_252: $i)). % 119.26/119.55 tff(tptp_fun__i_val_200_type, type, ( % 119.26/119.55 tptp_fun__i_val_200: $i)). % 119.26/119.55 tff(tptp_fun__i_val_55_type, type, ( % 119.26/119.55 tptp_fun__i_val_55: $i)). % 119.26/119.55 tff(tptp_fun__i_val_64_type, type, ( % 119.26/119.55 tptp_fun__i_val_64: $i)). % 119.26/119.55 tff(tptp_fun__i_val_249_type, type, ( % 119.26/119.55 tptp_fun__i_val_249: $i)). % 119.26/119.55 tff(tptp_fun__i_val_91_type, type, ( % 119.26/119.55 tptp_fun__i_val_91: $i)). % 119.26/119.55 tff(tptp_fun__i_val_272_type, type, ( % 119.26/119.55 tptp_fun__i_val_272: $i)). % 119.26/119.55 tff(tptp_fun__i_val_218_type, type, ( % 119.26/119.55 tptp_fun__i_val_218: $i)). % 119.26/119.55 tff(tptp_fun__i_val_250_type, type, ( % 119.26/119.55 tptp_fun__i_val_250: $i)). % 119.26/119.55 tff(tptp_fun__i_val_173_type, type, ( % 119.26/119.55 tptp_fun__i_val_173: $i)). % 119.26/119.55 tff(tptp_fun__i_val_26_type, type, ( % 119.26/119.55 tptp_fun__i_val_26: $i)). % 119.26/119.55 tff(tptp_fun__i_val_66_type, type, ( % 119.26/119.55 tptp_fun__i_val_66: $i)). % 119.26/119.55 tff(tptp_fun__i_val_247_type, type, ( % 119.26/119.55 tptp_fun__i_val_247: $i)). % 119.26/119.55 tff(tptp_fun__i_val_21_type, type, ( % 119.26/119.55 tptp_fun__i_val_21: $i)). % 119.26/119.55 tff(tptp_fun__i_val_150_type, type, ( % 119.26/119.55 tptp_fun__i_val_150: $i)). % 119.26/119.55 tff(tptp_fun__i_val_177_type, type, ( % 119.26/119.55 tptp_fun__i_val_177: $i)). % 119.26/119.55 tff(tptp_fun__i_val_2_type, type, ( % 119.26/119.55 tptp_fun__i_val_2: $i)). % 119.26/119.55 tff(tptp_fun__i_val_138_type, type, ( % 119.26/119.55 tptp_fun__i_val_138: $i)). % 119.26/119.55 tff(r1_type, type, ( % 119.26/119.55 r1: ( $i * $i ) > $o)). % 119.26/119.55 tff(p3_type, type, ( % 119.26/119.55 p3: $i > $o)). % 119.26/119.55 tff(p1_type, type, ( % 119.26/119.55 p1: $i > $o)). % 119.26/119.55 tff(formula1, axiom, % 119.26/119.55 ![X0: $i] : (p2(X0) <=> ((k!3259(X0) = $i!val!123) | (k!3259(X0) = $i!val!6) | (k!3259(X0) = $i!val!34) | (k!3259(X0) = $i!val!68) | (k!3259(X0) = $i!val!110) | (k!3259(X0) = $i!val!108) | (k!3259(X0) = $i!val!105) | (k!3259(X0) = $i!val!103) | (k!3259(X0) = $i!val!19) | (k!3259(X0) = $i!val!96) | (k!3259(X0) = $i!val!90) | (k!3259(X0) = $i!val!88) | (k!3259(X0) = $i!val!71) | (k!3259(X0) = $i!val!23) | (k!3259(X0) = $i!val!54) | (k!3259(X0) = $i!val!49) | (k!3259(X0) = $i!val!8) | (k!3259(X0) = $i!val!222) | (k!3259(X0) = $i!val!220) | (k!3259(X0) = $i!val!271) | (k!3259(X0) = $i!val!263) | (k!3259(X0) = $i!val!256) | (k!3259(X0) = $i!val!253) | (k!3259(X0) = $i!val!245) | (k!3259(X0) = $i!val!243) | (k!3259(X0) = $i!val!238) | (k!3259(X0) = $i!val!4) | (k!3259(X0) = $i!val!11) | (k!3259(X0) = $i!val!44) | (k!3259(X0) = $i!val!224) | (k!3259(X0) = $i!val!204) | (k!3259(X0) = $i!val!199) | (k!3259(X0) = $i!val!69) | (k!3259(X0) = $i!val!129) | (k!3259(X0) = $i!val!195) | (k!3259(X0) = $i!val!187) | (k!3259(X0) = $i!val!191) | (k!3259(X0) = $i!val!189) | (k!3259(X0) = $i!val!180) | (k!3259(X0) = $i!val!175) | (k!3259(X0) = $i!val!158) | (k!3259(X0) = $i!val!155) | (k!3259(X0) = $i!val!137)))). % 119.26/119.55 tff(formula2, axiom, % 119.26/119.55 ![X0: $i] : (p4(X0) <=> ((k!3259(X0) = $i!val!7) | (k!3259(X0) = $i!val!10) | (k!3259(X0) = $i!val!86) | (k!3259(X0) = $i!val!59) | (k!3259(X0) = $i!val!28) | (k!3259(X0) = $i!val!40)))). % 119.26/119.55 tff(formula3, axiom, % 119.26/119.55 k!3259($i!val!25) = $i!val!25). % 119.26/119.55 tff(formula4, axiom, % 119.26/119.55 k!3259($i!val!140) = $i!val!140). % 119.26/119.55 tff(formula5, axiom, % 119.26/119.55 k!3259($i!val!225) = $i!val!225). % 119.26/119.55 tff(formula6, axiom, % 119.26/119.55 k!3259($i!val!270) = $i!val!270). % 119.26/119.55 tff(formula7, axiom, % 119.26/119.55 k!3259($i!val!57) = $i!val!57). % 119.26/119.55 tff(formula8, axiom, % 119.26/119.55 k!3259($i!val!201) = $i!val!201). % 119.26/119.55 tff(formula9, axiom, % 119.26/119.55 k!3259($i!val!10) = $i!val!10). % 119.26/119.55 tff(formula10, axiom, % 119.26/119.55 k!3259($i!val!154) = $i!val!154). % 119.26/119.55 tff(formula11, axiom, % 119.26/119.55 k!3259($i!val!131) = $i!val!131). % 119.26/119.55 tff(formula12, axiom, % 119.26/119.55 k!3259($i!val!43) = $i!val!43). % 119.26/119.55 tff(formula13, axiom, % 119.26/119.55 k!3259($i!val!244) = $i!val!244). % 119.26/119.55 tff(formula14, axiom, % 119.26/119.55 k!3259($i!val!70) = $i!val!70). % 119.26/119.55 tff(formula15, axiom, % 119.26/119.55 k!3259($i!val!65) = $i!val!65). % 119.26/119.55 tff(formula16, axiom, % 119.26/119.55 k!3259($i!val!41) = $i!val!41). % 119.26/119.55 tff(formula17, axiom, % 119.26/119.55 k!3259($i!val!226) = $i!val!226). % 119.26/119.55 tff(formula18, axiom, % 119.26/119.55 k!3259($i!val!111) = $i!val!111). % 119.26/119.55 tff(formula19, axiom, % 119.26/119.55 k!3259($i!val!212) = $i!val!212). % 119.26/119.55 tff(formula20, axiom, % 119.26/119.55 k!3259($i!val!115) = $i!val!115). % 119.26/119.55 tff(formula21, axiom, % 119.26/119.55 k!3259($i!val!255) = $i!val!255). % 119.26/119.55 tff(formula22, axiom, % 119.26/119.55 k!3259($i!val!53) = $i!val!53). % 119.26/119.55 tff(formula23, axiom, % 119.26/119.55 k!3259($i!val!166) = $i!val!166). % 119.26/119.55 tff(formula24, axiom, % 119.26/119.55 k!3259($i!val!1) = $i!val!1). % 119.26/119.55 tff(formula25, axiom, % 119.26/119.55 k!3259($i!val!92) = $i!val!92). % 119.26/119.55 tff(formula26, axiom, % 119.26/119.55 k!3259($i!val!193) = $i!val!193). % 119.26/119.55 tff(formula27, axiom, % 119.26/119.55 k!3259($i!val!51) = $i!val!51). % 119.26/119.55 tff(formula28, axiom, % 119.26/119.55 k!3259($i!val!235) = $i!val!235). % 119.26/119.55 tff(formula29, axiom, % 119.26/119.55 k!3259($i!val!31) = $i!val!31). % 119.26/119.55 tff(formula30, axiom, % 119.26/119.55 k!3259($i!val!251) = $i!val!251). % 119.26/119.55 tff(formula31, axiom, % 119.26/119.55 k!3259($i!val!67) = $i!val!67). % 119.26/119.55 tff(formula32, axiom, % 119.26/119.55 k!3259($i!val!164) = $i!val!164). % 119.26/119.55 tff(formula33, axiom, % 119.26/119.55 k!3259($i!val!52) = $i!val!52). % 119.26/119.55 tff(formula34, axiom, % 119.26/119.55 k!3259($i!val!74) = $i!val!74). % 119.26/119.55 tff(formula35, axiom, % 119.26/119.55 k!3259($i!val!186) = $i!val!186). % 119.26/119.55 tff(formula36, axiom, % 119.26/119.55 k!3259($i!val!178) = $i!val!178). % 119.26/119.55 tff(formula37, axiom, % 119.26/119.55 k!3259($i!val!188) = $i!val!188). % 119.26/119.55 tff(formula38, axiom, % 119.26/119.55 k!3259($i!val!261) = $i!val!261). % 119.26/119.55 tff(formula39, axiom, % 119.26/119.55 k!3259($i!val!88) = $i!val!88). % 119.26/119.55 tff(formula40, axiom, % 119.26/119.55 k!3259($i!val!216) = $i!val!216). % 119.26/119.55 tff(formula41, axiom, % 119.26/119.55 k!3259($i!val!238) = $i!val!238). % 119.26/119.55 tff(formula42, axiom, % 119.26/119.55 k!3259($i!val!72) = $i!val!72). % 119.26/119.55 tff(formula43, axiom, % 119.26/119.55 k!3259($i!val!124) = $i!val!124). % 119.26/119.55 tff(formula44, axiom, % 119.26/119.55 k!3259($i!val!157) = $i!val!157). % 119.26/119.55 tff(formula45, axiom, % 119.26/119.55 k!3259($i!val!18) = $i!val!18). % 119.26/119.55 tff(formula46, axiom, % 119.26/119.55 k!3259($i!val!132) = $i!val!132). % 119.26/119.55 tff(formula47, axiom, % 119.26/119.55 k!3259($i!val!234) = $i!val!234). % 119.26/119.55 tff(formula48, axiom, % 119.26/119.55 k!3259($i!val!77) = $i!val!77). % 119.26/119.55 tff(formula49, axiom, % 119.26/119.55 k!3259($i!val!260) = $i!val!260). % 119.26/119.55 tff(formula50, axiom, % 119.26/119.55 k!3259($i!val!224) = $i!val!224). % 119.26/119.55 tff(formula51, axiom, % 119.26/119.55 k!3259($i!val!241) = $i!val!241). % 119.26/119.55 tff(formula52, axiom, % 119.26/119.55 k!3259($i!val!101) = $i!val!101). % 119.26/119.55 tff(formula53, axiom, % 119.26/119.55 k!3259($i!val!116) = $i!val!116). % 119.26/119.55 tff(formula54, axiom, % 119.26/119.55 k!3259($i!val!3) = $i!val!3). % 119.26/119.55 tff(formula55, axiom, % 119.26/119.55 k!3259($i!val!90) = $i!val!90). % 119.26/119.55 tff(formula56, axiom, % 119.26/119.55 k!3259($i!val!122) = $i!val!122). % 119.26/119.55 tff(formula57, axiom, % 119.26/119.55 k!3259($i!val!97) = $i!val!97). % 119.26/119.55 tff(formula58, axiom, % 119.26/119.55 k!3259($i!val!16) = $i!val!16). % 119.26/119.55 tff(formula59, axiom, % 119.26/119.55 k!3259($i!val!85) = $i!val!85). % 119.26/119.55 tff(formula60, axiom, % 119.26/119.55 k!3259($i!val!165) = $i!val!165). % 119.26/119.55 tff(formula61, axiom, % 119.26/119.55 k!3259($i!val!29) = $i!val!29). % 119.26/119.55 tff(formula62, axiom, % 119.26/119.55 k!3259($i!val!108) = $i!val!108). % 119.26/119.55 tff(formula63, axiom, % 119.26/119.55 k!3259($i!val!149) = $i!val!149). % 119.26/119.55 tff(formula64, axiom, % 119.26/119.55 k!3259($i!val!168) = $i!val!168). % 119.26/119.55 tff(formula65, axiom, % 119.26/119.55 k!3259($i!val!13) = $i!val!13). % 119.26/119.55 tff(formula66, axiom, % 119.26/119.55 k!3259($i!val!99) = $i!val!99). % 119.26/119.55 tff(formula67, axiom, % 119.26/119.55 k!3259($i!val!117) = $i!val!117). % 119.26/119.55 tff(formula68, axiom, % 119.26/119.55 k!3259($i!val!210) = $i!val!210). % 119.26/119.55 tff(formula69, axiom, % 119.26/119.55 k!3259($i!val!9) = $i!val!9). % 119.26/119.55 tff(formula70, axiom, % 119.26/119.55 k!3259($i!val!217) = $i!val!217). % 119.26/119.55 tff(formula71, axiom, % 119.26/119.55 k!3259($i!val!83) = $i!val!83). % 119.26/119.55 tff(formula72, axiom, % 119.26/119.55 k!3259($i!val!152) = $i!val!152). % 119.26/119.55 tff(formula73, axiom, % 119.26/119.55 k!3259($i!val!7) = $i!val!7). % 119.26/119.55 tff(formula74, axiom, % 119.26/119.55 k!3259($i!val!14) = $i!val!14). % 119.26/119.55 tff(formula75, axiom, % 119.26/119.55 k!3259($i!val!237) = $i!val!237). % 119.26/119.55 tff(formula76, axiom, % 119.26/119.55 k!3259($i!val!130) = $i!val!130). % 119.26/119.55 tff(formula77, axiom, % 119.26/119.55 k!3259($i!val!158) = $i!val!158). % 119.26/119.55 tff(formula78, axiom, % 119.26/119.55 k!3259($i!val!73) = $i!val!73). % 119.26/119.55 tff(formula79, axiom, % 119.26/119.55 k!3259($i!val!87) = $i!val!87). % 119.26/119.55 tff(formula80, axiom, % 119.26/119.55 k!3259($i!val!20) = $i!val!20). % 119.26/119.55 tff(formula81, axiom, % 119.26/119.55 k!3259($i!val!148) = $i!val!148). % 119.26/119.55 tff(formula82, axiom, % 119.26/119.55 k!3259($i!val!105) = $i!val!105). % 119.26/119.55 tff(formula83, axiom, % 119.26/119.55 k!3259($i!val!125) = $i!val!125). % 119.26/119.55 tff(formula84, axiom, % 119.26/119.55 k!3259($i!val!204) = $i!val!204). % 119.26/119.55 tff(formula85, axiom, % 119.26/119.55 k!3259($i!val!156) = $i!val!156). % 119.26/119.55 tff(formula86, axiom, % 119.26/119.55 k!3259($i!val!40) = $i!val!40). % 119.26/119.55 tff(formula87, axiom, % 119.26/119.55 k!3259($i!val!202) = $i!val!202). % 119.26/119.55 tff(formula88, axiom, % 119.26/119.55 k!3259($i!val!69) = $i!val!69). % 119.26/119.55 tff(formula89, axiom, % 119.26/119.55 k!3259($i!val!245) = $i!val!245). % 119.26/119.55 tff(formula90, axiom, % 119.26/119.55 k!3259($i!val!211) = $i!val!211). % 119.26/119.55 tff(formula91, axiom, % 119.26/119.55 k!3259($i!val!268) = $i!val!268). % 119.26/119.55 tff(formula92, axiom, % 119.26/119.55 k!3259($i!val!266) = $i!val!266). % 119.26/119.55 tff(formula93, axiom, % 119.26/119.55 k!3259($i!val!114) = $i!val!114). % 119.26/119.55 tff(formula94, axiom, % 119.26/119.55 k!3259($i!val!223) = $i!val!223). % 119.26/119.55 tff(formula95, axiom, % 119.26/119.55 k!3259($i!val!259) = $i!val!259). % 119.26/119.55 tff(formula96, axiom, % 119.26/119.55 k!3259($i!val!227) = $i!val!227). % 119.26/119.55 tff(formula97, axiom, % 119.26/119.55 k!3259($i!val!63) = $i!val!63). % 119.26/119.55 tff(formula98, axiom, % 119.26/119.55 k!3259($i!val!214) = $i!val!214). % 119.26/119.55 tff(formula99, axiom, % 119.26/119.55 k!3259($i!val!98) = $i!val!98). % 119.26/119.55 tff(formula100, axiom, % 119.26/119.55 k!3259($i!val!112) = $i!val!112). % 119.26/119.55 tff(formula101, axiom, % 119.26/119.55 k!3259($i!val!89) = $i!val!89). % 119.26/119.55 tff(formula102, axiom, % 119.26/119.55 k!3259($i!val!163) = $i!val!163). % 119.26/119.55 tff(formula103, axiom, % 119.26/119.55 k!3259($i!val!257) = $i!val!257). % 119.26/119.55 tff(formula104, axiom, % 119.26/119.55 k!3259($i!val!24) = $i!val!24). % 119.26/119.55 tff(formula105, axiom, % 119.26/119.55 k!3259($i!val!36) = $i!val!36). % 119.26/119.55 tff(formula106, axiom, % 119.26/119.55 k!3259($i!val!61) = $i!val!61). % 119.26/119.55 tff(formula107, axiom, % 119.26/119.55 k!3259($i!val!220) = $i!val!220). % 119.26/119.55 tff(formula108, axiom, % 119.26/119.55 k!3259($i!val!109) = $i!val!109). % 119.26/119.55 tff(formula109, axiom, % 119.26/119.55 k!3259($i!val!169) = $i!val!169). % 119.26/119.55 tff(formula110, axiom, % 119.26/119.55 k!3259($i!val!185) = $i!val!185). % 119.26/119.55 tff(formula111, axiom, % 119.26/119.55 k!3259($i!val!240) = $i!val!240). % 119.26/119.55 tff(formula112, axiom, % 119.26/119.55 k!3259($i!val!161) = $i!val!161). % 119.26/119.55 tff(formula113, axiom, % 119.26/119.55 k!3259($i!val!93) = $i!val!93). % 119.26/119.55 tff(formula114, axiom, % 119.26/119.55 k!3259($i!val!62) = $i!val!62). % 119.26/119.55 tff(formula115, axiom, % 119.26/119.55 k!3259($i!val!84) = $i!val!84). % 119.26/119.55 tff(formula116, axiom, % 119.26/119.55 k!3259($i!val!153) = $i!val!153). % 119.26/119.55 tff(formula117, axiom, % 119.26/119.55 k!3259($i!val!191) = $i!val!191). % 119.26/119.55 tff(formula118, axiom, % 119.26/119.55 k!3259($i!val!159) = $i!val!159). % 119.26/119.55 tff(formula119, axiom, % 119.26/119.55 k!3259($i!val!126) = $i!val!126). % 119.26/119.55 tff(formula120, axiom, % 119.26/119.55 k!3259($i!val!106) = $i!val!106). % 119.26/119.55 tff(formula121, axiom, % 119.26/119.55 k!3259($i!val!203) = $i!val!203). % 119.26/119.55 tff(formula122, axiom, % 119.26/119.55 k!3259($i!val!75) = $i!val!75). % 119.26/119.55 tff(formula123, axiom, % 119.26/119.55 k!3259($i!val!129) = $i!val!129). % 119.26/119.55 tff(formula124, axiom, % 119.26/119.55 k!3259($i!val!267) = $i!val!267). % 119.26/119.55 tff(formula125, axiom, % 119.26/119.55 k!3259($i!val!192) = $i!val!192). % 119.26/119.55 tff(formula126, axiom, % 119.26/119.55 k!3259($i!val!0) = $i!val!0). % 119.26/119.55 tff(formula127, axiom, % 119.26/119.55 k!3259($i!val!12) = $i!val!12). % 119.26/119.55 tff(formula128, axiom, % 119.26/119.55 k!3259($i!val!134) = $i!val!134). % 119.26/119.55 tff(formula129, axiom, % 119.26/119.55 k!3259($i!val!147) = $i!val!147). % 119.26/119.55 tff(formula130, axiom, % 119.26/119.55 k!3259($i!val!215) = $i!val!215). % 119.26/119.55 tff(formula131, axiom, % 119.26/119.55 k!3259($i!val!113) = $i!val!113). % 119.26/119.55 tff(formula132, axiom, % 119.26/119.55 k!3259($i!val!27) = $i!val!27). % 119.26/119.55 tff(formula133, axiom, % 119.26/119.55 k!3259($i!val!258) = $i!val!258). % 119.26/119.55 tff(formula134, axiom, % 119.26/119.55 k!3259($i!val!37) = $i!val!37). % 119.26/119.55 tff(formula135, axiom, % 119.26/119.55 k!3259($i!val!176) = $i!val!176). % 119.26/119.55 tff(formula136, axiom, % 119.26/119.55 k!3259($i!val!23) = $i!val!23). % 119.26/119.55 tff(formula137, axiom, % 119.26/119.55 k!3259($i!val!103) = $i!val!103). % 119.26/119.55 tff(formula138, axiom, % 119.26/119.55 k!3259($i!val!135) = $i!val!135). % 119.26/119.55 tff(formula139, axiom, % 119.26/119.55 k!3259($i!val!145) = $i!val!145). % 119.26/119.55 tff(formula140, axiom, % 119.26/119.55 k!3259($i!val!219) = $i!val!219). % 119.26/119.55 tff(formula141, axiom, % 119.26/119.55 k!3259($i!val!269) = $i!val!269). % 119.26/119.55 tff(formula142, axiom, % 119.26/119.55 k!3259($i!val!162) = $i!val!162). % 119.26/119.55 tff(formula143, axiom, % 119.26/119.55 k!3259($i!val!17) = $i!val!17). % 119.26/119.55 tff(formula144, axiom, % 119.26/119.55 k!3259($i!val!86) = $i!val!86). % 119.26/119.55 tff(formula145, axiom, % 119.26/119.55 k!3259($i!val!239) = $i!val!239). % 119.26/119.55 tff(formula146, axiom, % 119.26/119.55 k!3259($i!val!94) = $i!val!94). % 119.26/119.55 tff(formula147, axiom, % 119.26/119.56 k!3259($i!val!190) = $i!val!190). % 119.26/119.56 tff(formula148, axiom, % 119.26/119.56 k!3259($i!val!236) = $i!val!236). % 119.26/119.56 tff(formula149, axiom, % 119.26/119.56 k!3259($i!val!167) = $i!val!167). % 119.26/119.56 tff(formula150, axiom, % 119.26/119.56 k!3259($i!val!183) = $i!val!183). % 119.26/119.56 tff(formula151, axiom, % 119.26/119.56 k!3259($i!val!100) = $i!val!100). % 119.26/119.56 tff(formula152, axiom, % 119.26/119.56 k!3259($i!val!180) = $i!val!180). % 119.26/119.56 tff(formula153, axiom, % 119.26/119.56 k!3259($i!val!76) = $i!val!76). % 119.26/119.56 tff(formula154, axiom, % 119.26/119.56 k!3259($i!val!199) = $i!val!199). % 119.26/119.56 tff(formula155, axiom, % 119.26/119.56 k!3259($i!val!4) = $i!val!4). % 119.26/119.56 tff(formula156, axiom, % 119.26/119.56 k!3259($i!val!96) = $i!val!96). % 119.26/119.56 tff(formula157, axiom, % 119.26/119.56 k!3259($i!val!128) = $i!val!128). % 119.26/119.56 tff(formula158, axiom, % 119.26/119.56 k!3259($i!val!242) = $i!val!242). % 119.26/119.56 tff(formula159, axiom, % 119.26/119.56 k!3259($i!val!49) = $i!val!49). % 119.26/119.56 tff(formula160, axiom, % 119.26/119.56 k!3259($i!val!50) = $i!val!50). % 119.26/119.56 tff(formula161, axiom, % 119.26/119.56 k!3259($i!val!6) = $i!val!6). % 119.26/119.56 tff(formula162, axiom, % 119.26/119.56 k!3259($i!val!195) = $i!val!195). % 119.26/119.56 tff(formula163, axiom, % 119.26/119.56 k!3259($i!val!264) = $i!val!264). % 119.26/119.56 tff(formula164, axiom, % 119.26/119.56 k!3259($i!val!32) = $i!val!32). % 119.26/119.56 tff(formula165, axiom, % 119.26/119.56 k!3259($i!val!209) = $i!val!209). % 119.26/119.56 tff(formula166, axiom, % 119.26/119.56 k!3259($i!val!107) = $i!val!107). % 119.26/119.56 tff(formula167, axiom, % 119.26/119.56 k!3259($i!val!22) = $i!val!22). % 119.26/119.56 tff(formula168, axiom, % 119.26/119.56 k!3259($i!val!136) = $i!val!136). % 119.26/119.56 tff(formula169, axiom, % 119.26/119.56 k!3259($i!val!102) = $i!val!102). % 119.26/119.56 tff(formula170, axiom, % 119.26/119.56 k!3259($i!val!121) = $i!val!121). % 119.26/119.56 tff(formula171, axiom, % 119.26/119.56 k!3259($i!val!265) = $i!val!265). % 119.26/119.56 tff(formula172, axiom, % 119.26/119.56 k!3259($i!val!146) = $i!val!146). % 119.26/119.56 tff(formula173, axiom, % 119.26/119.56 k!3259($i!val!172) = $i!val!172). % 119.26/119.56 tff(formula174, axiom, % 119.26/119.56 k!3259($i!val!33) = $i!val!33). % 119.26/119.56 tff(formula175, axiom, % 119.26/119.56 k!3259($i!val!38) = $i!val!38). % 119.26/119.56 tff(formula176, axiom, % 119.26/119.56 k!3259($i!val!175) = $i!val!175). % 119.26/119.56 tff(formula177, axiom, % 119.26/119.56 k!3259($i!val!78) = $i!val!78). % 119.26/119.56 tff(formula178, axiom, % 119.26/119.56 k!3259($i!val!246) = $i!val!246). % 119.26/119.56 tff(formula179, axiom, % 119.26/119.56 k!3259($i!val!160) = $i!val!160). % 119.26/119.56 tff(formula180, axiom, % 119.26/119.56 k!3259($i!val!184) = $i!val!184). % 119.26/119.56 tff(formula181, axiom, % 119.26/119.56 k!3259($i!val!170) = $i!val!170). % 119.26/119.56 tff(formula182, axiom, % 119.26/119.56 k!3259($i!val!104) = $i!val!104). % 119.26/119.56 tff(formula183, axiom, % 119.26/119.56 k!3259($i!val!254) = $i!val!254). % 119.26/119.56 tff(formula184, axiom, % 119.26/119.56 k!3259($i!val!179) = $i!val!179). % 119.26/119.56 tff(formula185, axiom, % 119.26/119.56 k!3259($i!val!151) = $i!val!151). % 119.26/119.56 tff(formula186, axiom, % 119.26/119.56 k!3259($i!val!198) = $i!val!198). % 119.26/119.56 tff(formula187, axiom, % 119.26/119.56 k!3259($i!val!95) = $i!val!95). % 119.26/119.56 tff(formula188, axiom, % 119.26/119.56 k!3259($i!val!233) = $i!val!233). % 119.26/119.56 tff(formula189, axiom, % 119.26/119.56 k!3259($i!val!228) = $i!val!228). % 119.26/119.56 tff(formula190, axiom, % 119.26/119.56 k!3259($i!val!48) = $i!val!48). % 119.26/119.56 tff(formula191, axiom, % 119.26/119.56 k!3259($i!val!205) = $i!val!205). % 119.26/119.56 tff(formula192, axiom, % 119.26/119.56 k!3259($i!val!232) = $i!val!232). % 119.26/119.56 tff(formula193, axiom, % 119.26/119.56 k!3259($i!val!5) = $i!val!5). % 119.26/119.56 tff(formula194, axiom, % 119.26/119.56 k!3259($i!val!263) = $i!val!263). % 119.26/119.56 tff(formula195, axiom, % 119.26/119.56 k!3259($i!val!144) = $i!val!144). % 119.26/119.56 tff(formula196, axiom, % 119.26/119.56 k!3259($i!val!194) = $i!val!194). % 119.26/119.56 tff(formula197, axiom, % 119.26/119.56 k!3259($i!val!230) = $i!val!230). % 119.26/119.56 tff(formula198, axiom, % 119.26/119.56 k!3259($i!val!208) = $i!val!208). % 119.26/119.56 tff(formula199, axiom, % 119.26/119.56 k!3259($i!val!15) = $i!val!15). % 119.26/119.56 tff(formula200, axiom, % 119.26/119.56 k!3259($i!val!42) = $i!val!42). % 119.26/119.56 tff(formula201, axiom, % 119.26/119.56 k!3259($i!val!142) = $i!val!142). % 119.26/119.56 tff(formula202, axiom, % 119.26/119.56 k!3259($i!val!213) = $i!val!213). % 119.26/119.56 tff(formula203, axiom, % 119.26/119.56 k!3259($i!val!222) = $i!val!222). % 119.26/119.56 tff(formula204, axiom, % 119.26/119.56 k!3259($i!val!82) = $i!val!82). % 119.26/119.56 tff(formula205, axiom, % 119.26/119.56 k!3259($i!val!174) = $i!val!174). % 119.26/119.56 tff(formula206, axiom, % 119.26/119.56 k!3259($i!val!79) = $i!val!79). % 119.26/119.56 tff(formula207, axiom, % 119.26/119.56 k!3259($i!val!171) = $i!val!171). % 119.26/119.56 tff(formula208, axiom, % 119.26/119.56 k!3259($i!val!80) = $i!val!80). % 119.26/119.56 tff(formula209, axiom, % 119.26/119.56 k!3259($i!val!118) = $i!val!118). % 119.26/119.56 tff(formula210, axiom, % 119.26/119.56 k!3259($i!val!19) = $i!val!19). % 119.26/119.56 tff(formula211, axiom, % 119.26/119.56 k!3259($i!val!127) = $i!val!127). % 119.26/119.56 tff(formula212, axiom, % 119.26/119.56 k!3259($i!val!47) = $i!val!47). % 119.26/119.56 tff(formula213, axiom, % 119.26/119.56 k!3259($i!val!11) = $i!val!11). % 119.26/119.56 tff(formula214, axiom, % 119.26/119.56 k!3259($i!val!119) = $i!val!119). % 119.26/119.56 tff(formula215, axiom, % 119.26/119.56 k!3259($i!val!206) = $i!val!206). % 119.26/119.56 tff(formula216, axiom, % 119.26/119.56 k!3259($i!val!253) = $i!val!253). % 119.26/119.56 tff(formula217, axiom, % 119.26/119.56 k!3259($i!val!196) = $i!val!196). % 119.26/119.56 tff(formula218, axiom, % 119.26/119.56 k!3259($i!val!56) = $i!val!56). % 119.26/119.56 tff(formula219, axiom, % 119.26/119.56 k!3259($i!val!45) = $i!val!45). % 119.26/119.56 tff(formula220, axiom, % 119.26/119.56 k!3259($i!val!262) = $i!val!262). % 119.26/119.56 tff(formula221, axiom, % 119.26/119.56 k!3259($i!val!60) = $i!val!60). % 119.26/119.56 tff(formula222, axiom, % 119.26/119.56 k!3259($i!val!231) = $i!val!231). % 119.26/119.56 tff(formula223, axiom, % 119.26/119.56 k!3259($i!val!35) = $i!val!35). % 119.26/119.56 tff(formula224, axiom, % 119.26/119.56 k!3259($i!val!39) = $i!val!39). % 119.26/119.56 tff(formula225, axiom, % 119.26/119.56 k!3259($i!val!46) = $i!val!46). % 119.26/119.56 tff(formula226, axiom, % 119.26/119.56 k!3259($i!val!143) = $i!val!143). % 119.26/119.56 tff(formula227, axiom, % 119.26/119.56 k!3259($i!val!133) = $i!val!133). % 119.26/119.56 tff(formula228, axiom, % 119.26/119.56 k!3259($i!val!58) = $i!val!58). % 119.26/119.56 tff(formula229, axiom, % 119.26/119.56 k!3259($i!val!221) = $i!val!221). % 119.26/119.56 tff(formula230, axiom, % 119.26/119.56 k!3259($i!val!34) = $i!val!34). % 119.26/119.56 tff(formula231, axiom, % 119.26/119.56 k!3259($i!val!207) = $i!val!207). % 119.26/119.56 tff(formula232, axiom, % 119.26/119.56 k!3259($i!val!182) = $i!val!182). % 119.26/119.56 tff(formula233, axiom, % 119.26/119.56 k!3259($i!val!120) = $i!val!120). % 119.26/119.56 tff(formula234, axiom, % 119.26/119.56 k!3259($i!val!141) = $i!val!141). % 119.26/119.56 tff(formula235, axiom, % 119.26/119.56 k!3259($i!val!81) = $i!val!81). % 119.26/119.56 tff(formula236, axiom, % 119.26/119.56 k!3259($i!val!137) = $i!val!137). % 119.26/119.56 tff(formula237, axiom, % 119.26/119.56 k!3259($i!val!30) = $i!val!30). % 119.26/119.56 tff(formula238, axiom, % 119.26/119.56 k!3259($i!val!181) = $i!val!181). % 119.26/119.56 tff(formula239, axiom, % 119.26/119.56 k!3259($i!val!197) = $i!val!197). % 119.26/119.56 tff(formula240, axiom, % 119.26/119.56 k!3259($i!val!229) = $i!val!229). % 119.26/119.56 tff(formula241, axiom, % 119.26/119.56 k!3259($i!val!139) = $i!val!139). % 119.26/119.56 tff(formula242, axiom, % 119.26/119.56 k!3259($i!val!271) = $i!val!271). % 119.26/119.56 tff(formula243, axiom, % 119.26/119.56 k!3259($i!val!248) = $i!val!248). % 119.26/119.56 tff(formula244, axiom, % 119.26/119.56 k!3259($i!val!8) = $i!val!8). % 119.26/119.56 tff(formula245, axiom, % 119.26/119.56 k!3259($i!val!155) = $i!val!155). % 119.26/119.56 tff(formula246, axiom, % 119.26/119.56 k!3259($i!val!252) = $i!val!252). % 119.26/119.56 tff(formula247, axiom, % 119.26/119.56 k!3259($i!val!200) = $i!val!200). % 119.26/119.56 tff(formula248, axiom, % 119.26/119.56 k!3259($i!val!44) = $i!val!44). % 119.26/119.56 tff(formula249, axiom, % 119.26/119.56 k!3259($i!val!243) = $i!val!243). % 119.26/119.56 tff(formula250, axiom, % 119.26/119.56 k!3259($i!val!71) = $i!val!71). % 119.26/119.56 tff(formula251, axiom, % 119.26/119.56 k!3259($i!val!55) = $i!val!55). % 119.26/119.56 tff(formula252, axiom, % 119.26/119.56 k!3259($i!val!64) = $i!val!64). % 119.26/119.56 tff(formula253, axiom, % 119.26/119.56 k!3259($i!val!110) = $i!val!110). % 119.26/119.56 tff(formula254, axiom, % 119.26/119.56 k!3259($i!val!249) = $i!val!249). % 119.26/119.56 tff(formula255, axiom, % 119.26/119.56 k!3259($i!val!28) = $i!val!28). % 119.26/119.56 tff(formula256, axiom, % 119.26/119.56 k!3259($i!val!256) = $i!val!256). % 119.26/119.56 tff(formula257, axiom, % 119.26/119.56 k!3259($i!val!54) = $i!val!54). % 119.26/119.56 tff(formula258, axiom, % 119.26/119.56 k!3259($i!val!68) = $i!val!68). % 119.26/119.56 tff(formula259, axiom, % 119.26/119.56 k!3259($i!val!91) = $i!val!91). % 119.26/119.56 tff(formula260, axiom, % 119.26/119.56 k!3259($i!val!272) = $i!val!272). % 119.26/119.56 tff(formula261, axiom, % 119.26/119.56 k!3259($i!val!218) = $i!val!218). % 119.26/119.56 tff(formula262, axiom, % 119.26/119.56 k!3259($i!val!250) = $i!val!250). % 119.26/119.56 tff(formula263, axiom, % 119.26/119.56 k!3259($i!val!59) = $i!val!59). % 119.26/119.56 tff(formula264, axiom, % 119.26/119.56 k!3259($i!val!173) = $i!val!173). % 119.26/119.56 tff(formula265, axiom, % 119.26/119.56 k!3259($i!val!26) = $i!val!26). % 119.26/119.56 tff(formula266, axiom, % 119.26/119.56 k!3259($i!val!66) = $i!val!66). % 119.26/119.56 tff(formula267, axiom, % 119.26/119.56 k!3259($i!val!247) = $i!val!247). % 119.26/119.56 tff(formula268, axiom, % 119.26/119.56 k!3259($i!val!187) = $i!val!187). % 119.26/119.56 tff(formula269, axiom, % 119.26/119.56 k!3259($i!val!189) = $i!val!189). % 119.26/119.56 tff(formula270, axiom, % 119.26/119.56 k!3259($i!val!21) = $i!val!21). % 119.26/119.56 tff(formula271, axiom, % 119.26/119.56 k!3259($i!val!150) = $i!val!150). % 119.26/119.56 tff(formula272, axiom, % 119.26/119.56 k!3259($i!val!177) = $i!val!177). % 119.26/119.56 tff(formula273, axiom, % 119.26/119.56 k!3259($i!val!2) = $i!val!2). % 119.26/119.56 tff(formula274, axiom, % 119.26/119.56 k!3259($i!val!138) = $i!val!138). % 119.26/119.56 tff(formula275, axiom, % 119.26/119.56 ![X0: $i] : ((~((($i!val!25 = X0)) | (($i!val!140 = X0)) | (($i!val!225 = X0)) | (($i!val!270 = X0)) | (($i!val!57 = X0)) | (($i!val!201 = X0)) | (($i!val!10 = X0)) | (($i!val!154 = X0)) | (($i!val!131 = X0)) | (($i!val!43 = X0)) | (($i!val!244 = X0)) | (($i!val!70 = X0)) | (($i!val!65 = X0)) | (($i!val!41 = X0)) | (($i!val!226 = X0)) | (($i!val!111 = X0)) | (($i!val!212 = X0)) | (($i!val!115 = X0)) | (($i!val!255 = X0)) | (($i!val!53 = X0)) | (($i!val!166 = X0)) | (($i!val!1 = X0)) | (($i!val!92 = X0)) | (($i!val!193 = X0)) | (($i!val!51 = X0)) | (($i!val!235 = X0)) | (($i!val!31 = X0)) | (($i!val!251 = X0)) | (($i!val!67 = X0)) | (($i!val!164 = X0)) | (($i!val!52 = X0)) | (($i!val!74 = X0)) | (($i!val!186 = X0)) | (($i!val!178 = X0)) | (($i!val!188 = X0)) | (($i!val!261 = X0)) | (($i!val!88 = X0)) | (($i!val!216 = X0)) | (($i!val!238 = X0)) | (($i!val!72 = X0)) | (($i!val!124 = X0)) | (($i!val!157 = X0)) | (($i!val!18 = X0)) | (($i!val!132 = X0)) | (($i!val!234 = X0)) | (($i!val!77 = X0)) | (($i!val!260 = X0)) | (($i!val!224 = X0)) | (($i!val!241 = X0)) | (($i!val!101 = X0)) | (($i!val!116 = X0)) | (($i!val!3 = X0)) | (($i!val!90 = X0)) | (($i!val!122 = X0)) | (($i!val!97 = X0)) | (($i!val!16 = X0)) | (($i!val!85 = X0)) | (($i!val!165 = X0)) | (($i!val!29 = X0)) | (($i!val!108 = X0)) | (($i!val!149 = X0)) | (($i!val!168 = X0)) | (($i!val!13 = X0)) | (($i!val!99 = X0)) | (($i!val!117 = X0)) | (($i!val!210 = X0)) | (($i!val!9 = X0)) | (($i!val!217 = X0)) | (($i!val!83 = X0)) | (($i!val!152 = X0)) | (($i!val!7 = X0)) | (($i!val!14 = X0)) | (($i!val!237 = X0)) | (($i!val!130 = X0)) | (($i!val!158 = X0)) | (($i!val!73 = X0)) | (($i!val!87 = X0)) | (($i!val!20 = X0)) | (($i!val!148 = X0)) | (($i!val!105 = X0)) | (($i!val!125 = X0)) | (($i!val!204 = X0)) | (($i!val!156 = X0)) | (($i!val!40 = X0)) | (($i!val!202 = X0)) | (($i!val!69 = X0)) | (($i!val!245 = X0)) | (($i!val!211 = X0)) | (($i!val!268 = X0)) | (($i!val!266 = X0)) | (($i!val!114 = X0)) | (($i!val!223 = X0)) | (($i!val!259 = X0)) | (($i!val!227 = X0)) | (($i!val!63 = X0)) | (($i!val!214 = X0)) | (($i!val!98 = X0)) | (($i!val!112 = X0)) | (($i!val!89 = X0)) | (($i!val!163 = X0)) | (($i!val!257 = X0)) | (($i!val!24 = X0)) | (($i!val!36 = X0)) | (($i!val!61 = X0)) | (($i!val!220 = X0)) | (($i!val!109 = X0)) | (($i!val!169 = X0)) | (($i!val!185 = X0)) | (($i!val!240 = X0)) | (($i!val!161 = X0)) | (($i!val!93 = X0)) | (($i!val!62 = X0)) | (($i!val!84 = X0)) | (($i!val!153 = X0)) | (($i!val!191 = X0)) | (($i!val!159 = X0)) | (($i!val!126 = X0)) | (($i!val!106 = X0)) | (($i!val!203 = X0)) | (($i!val!75 = X0)) | (($i!val!129 = X0)) | (($i!val!267 = X0)) | (($i!val!192 = X0)) | (($i!val!0 = X0)) | (($i!val!12 = X0)) | (($i!val!134 = X0)) | (($i!val!147 = X0)) | (($i!val!215 = X0)) | (($i!val!113 = X0)) | (($i!val!27 = X0)) | (($i!val!258 = X0)) | (($i!val!37 = X0)) | (($i!val!176 = X0)) | (($i!val!23 = X0)) | (($i!val!103 = X0)) | (($i!val!135 = X0)) | (($i!val!145 = X0)) | (($i!val!219 = X0)) | (($i!val!269 = X0)) | (($i!val!162 = X0)) | (($i!val!17 = X0)) | (($i!val!86 = X0)) | (($i!val!239 = X0)) | (($i!val!94 = X0)) | (($i!val!190 = X0)) | (($i!val!236 = X0)) | (($i!val!167 = X0)) | (($i!val!183 = X0)) | (($i!val!100 = X0)) | (($i!val!180 = X0)) | (($i!val!76 = X0)) | (($i!val!199 = X0)) | (($i!val!4 = X0)) | (($i!val!96 = X0)) | (($i!val!128 = X0)) | (($i!val!242 = X0)) | (($i!val!49 = X0)) | (($i!val!50 = X0)) | (($i!val!6 = X0)) | (($i!val!195 = X0)) | (($i!val!264 = X0)) | (($i!val!32 = X0)) | (($i!val!209 = X0)) | (($i!val!107 = X0)) | (($i!val!22 = X0)) | (($i!val!136 = X0)) | (($i!val!102 = X0)) | (($i!val!121 = X0)) | (($i!val!265 = X0)) | (($i!val!146 = X0)) | (($i!val!172 = X0)) | (($i!val!33 = X0)) | (($i!val!38 = X0)) | (($i!val!175 = X0)) | (($i!val!78 = X0)) | (($i!val!246 = X0)) | (($i!val!160 = X0)) | (($i!val!184 = X0)) | (($i!val!170 = X0)) | (($i!val!104 = X0)) | (($i!val!254 = X0)) | (($i!val!179 = X0)) | (($i!val!151 = X0)) | (($i!val!198 = X0)) | (($i!val!95 = X0)) | (($i!val!233 = X0)) | (($i!val!228 = X0)) | (($i!val!48 = X0)) | (($i!val!205 = X0)) | (($i!val!232 = X0)) | (($i!val!5 = X0)) | (($i!val!263 = X0)) | (($i!val!144 = X0)) | (($i!val!194 = X0)) | (($i!val!230 = X0)) | (($i!val!208 = X0)) | (($i!val!15 = X0)) | (($i!val!42 = X0)) | (($i!val!142 = X0)) | (($i!val!213 = X0)) | (($i!val!222 = X0)) | (($i!val!82 = X0)) | (($i!val!174 = X0)) | (($i!val!79 = X0)) | (($i!val!171 = X0)) | (($i!val!80 = X0)) | (($i!val!118 = X0)) | (($i!val!19 = X0)) | (($i!val!127 = X0)) | (($i!val!47 = X0)) | (($i!val!11 = X0)) | (($i!val!119 = X0)) | (($i!val!206 = X0)) | (($i!val!253 = X0)) | (($i!val!196 = X0)) | (($i!val!56 = X0)) | (($i!val!45 = X0)) | (($i!val!262 = X0)) | (($i!val!60 = X0)) | (($i!val!231 = X0)) | (($i!val!35 = X0)) | (($i!val!39 = X0)) | (($i!val!46 = X0)) | (($i!val!143 = X0)) | (($i!val!133 = X0)) | (($i!val!58 = X0)) | (($i!val!221 = X0)) | (($i!val!34 = X0)) | (($i!val!207 = X0)) | (($i!val!182 = X0)) | (($i!val!120 = X0)) | (($i!val!141 = X0)) | (($i!val!81 = X0)) | (($i!val!137 = X0)) | (($i!val!30 = X0)) | (($i!val!181 = X0)) | (($i!val!197 = X0)) | (($i!val!229 = X0)) | (($i!val!139 = X0)) | (($i!val!271 = X0)) | (($i!val!248 = X0)) | (($i!val!8 = X0)) | (($i!val!155 = X0)) | (($i!val!252 = X0)) | (($i!val!200 = X0)) | (($i!val!44 = X0)) | (($i!val!243 = X0)) | (($i!val!71 = X0)) | (($i!val!55 = X0)) | (($i!val!64 = X0)) | (($i!val!110 = X0)) | (($i!val!249 = X0)) | (($i!val!28 = X0)) | (($i!val!256 = X0)) | (($i!val!54 = X0)) | (($i!val!68 = X0)) | (($i!val!91 = X0)) | (($i!val!272 = X0)) | (($i!val!218 = X0)) | (($i!val!250 = X0)) | (($i!val!59 = X0)) | (($i!val!173 = X0)) | (($i!val!26 = X0)) | (($i!val!66 = X0)) | (($i!val!247 = X0)) | (($i!val!187 = X0)) | (($i!val!189 = X0)) | (($i!val!21 = X0)) | (($i!val!150 = X0)) | (($i!val!177 = X0)) | (($i!val!2 = X0)) | (($i!val!138 = X0)))) => (k!3259(X0) = $i!val!123))). % 119.26/119.56 tff(formula276, axiom, % 119.26/119.56 ![X0: $i, X1: $i] : (r1(X0, X1) <=> (((k!3259(X1) = $i!val!33) & (k!3259(X0) = $i!val!117)) | ((k!3259(X1) = $i!val!96) & (k!3259(X0) = $i!val!95)) | ((k!3259(X1) = $i!val!70) & (k!3259(X0) = $i!val!96)) | ((k!3259(X1) = $i!val!88) & (k!3259(X0) = $i!val!87)) | ((k!3259(X1) = $i!val!60) & (k!3259(X0) = $i!val!108)) | ((k!3259(X1) = $i!val!105) & (k!3259(X0) = $i!val!106)) | ((k!3259(X1) = $i!val!60) & (k!3259(X0) = $i!val!107)) | ((k!3259(X1) = $i!val!58) & (k!3259(X0) = $i!val!86)) | ((k!3259(X1) = $i!val!80) & (k!3259(X0) = $i!val!81)) | ((k!3259(X1) = $i!val!97) & (k!3259(X0) = $i!val!98)) | ((k!3259(X1) = $i!val!28) & (k!3259(X0) = $i!val!85)) | ((k!3259(X1) = $i!val!83) & (k!3259(X0) = $i!val!84)) | ((k!3259(X1) = $i!val!52) & (k!3259(X0) = $i!val!80)) | ((k!3259(X1) = $i!val!72) & (k!3259(X0) = $i!val!104)) | ((k!3259(X1) = $i!val!64) & (k!3259(X0) = $i!val!125)) | ((k!3259(X1) = $i!val!91) & (k!3259(X0) = $i!val!92)) | ((k!3259(X1) = $i!val!10) & (k!3259(X0) = $i!val!91)) | ((k!3259(X1) = $i!val!29) & (k!3259(X0) = $i!val!123)) | ((k!3259(X1) = $i!val!125) & (k!3259(X0) = $i!val!126)) | ((k!3259(X1) = $i!val!119) & (k!3259(X0) = $i!val!144)) | ((k!3259(X1) = $i!val!119) & (k!3259(X0) = $i!val!142)) | ((k!3259(X1) = $i!val!142) & (k!3259(X0) = $i!val!143)) | ((k!3259(X1) = $i!val!123) & (k!3259(X0) = $i!val!124)) | ((k!3259(X1) = $i!val!40) & (k!3259(X0) = $i!val!122)) | ((k!3259(X1) = $i!val!17) & (k!3259(X0) = $i!val!121)) | ((k!3259(X1) = $i!val!111) & (k!3259(X0) = $i!val!141)) | ((k!3259(X1) = $i!val!111) & (k!3259(X0) = $i!val!139)) | ((k!3259(X1) = $i!val!48) & (k!3259(X0) = $i!val!131)) | ((k!3259(X1) = $i!val!129) & (k!3259(X0) = $i!val!128)) | ((k!3259(X1) = $i!val!80) & (k!3259(X0) = $i!val!127)) | ((k!3259(X1) = $i!val!80) & (k!3259(X0) = $i!val!130)) | ((k!3259(X1) = $i!val!150) & (k!3259(X0) = $i!val!151)) | ((k!3259(X1) = $i!val!101) & (k!3259(X0) = $i!val!167)) | ((k!3259(X1) = $i!val!112) & (k!3259(X0) = $i!val!166)) | ((k!3259(X1) = $i!val!112) & (k!3259(X0) = $i!val!164)) | ((k!3259(X1) = $i!val!164) & (k!3259(X0) = $i!val!165)) | ((k!3259(X1) = $i!val!99) & (k!3259(X0) = $i!val!163)) | ((k!3259(X1) = $i!val!99) & (k!3259(X0) = $i!val!161)) | ((k!3259(X1) = $i!val!161) & (k!3259(X0) = $i!val!162)) | ((k!3259(X1) = $i!val!158) & (k!3259(X0) = $i!val!159)) | ((k!3259(X1) = $i!val!124) & (k!3259(X0) = $i!val!158)) | ((k!3259(X1) = $i!val!103) & (k!3259(X0) = $i!val!157)) | ((k!3259(X1) = $i!val!102) & (k!3259(X0) = $i!val!156)) | ((k!3259(X1) = $i!val!102) & (k!3259(X0) = $i!val!155)) | ((k!3259(X1) = $i!val!155) & (k!3259(X0) = $i!val!154)) | ((k!3259(X1) = $i!val!125) & (k!3259(X0) = $i!val!152)) | ((k!3259(X1) = $i!val!139) & (k!3259(X0) = $i!val!187)) | ((k!3259(X1) = $i!val!139) & (k!3259(X0) = $i!val!185)) | ((k!3259(X1) = $i!val!157) & (k!3259(X0) = $i!val!184)) | ((k!3259(X1) = $i!val!182) & (k!3259(X0) = $i!val!183)) | ((k!3259(X1) = $i!val!159) & (k!3259(X0) = $i!val!181)) | ((k!3259(X1) = $i!val!159) & (k!3259(X0) = $i!val!180)) | ((k!3259(X1) = $i!val!180) & (k!3259(X0) = $i!val!179)) | ((k!3259(X1) = $i!val!161) & (k!3259(X0) = $i!val!177)) | ((k!3259(X1) = $i!val!177) & (k!3259(X0) = $i!val!178)) | ((k!3259(X1) = $i!val!161) & (k!3259(X0) = $i!val!176)) | ((k!3259(X1) = $i!val!145) & (k!3259(X0) = $i!val!204)) | ((k!3259(X1) = $i!val!189) & (k!3259(X0) = $i!val!188)) | ((k!3259(X1) = $i!val!204) & (k!3259(X0) = $i!val!203)) | ((k!3259(X1) = $i!val!152) & (k!3259(X0) = $i!val!202)) | ((k!3259(X1) = $i!val!142) & (k!3259(X0) = $i!val!200)) | ((k!3259(X1) = $i!val!200) & (k!3259(X0) = $i!val!201)) | ((k!3259(X1) = $i!val!199) & (k!3259(X0) = $i!val!198)) | ((k!3259(X1) = $i!val!142) & (k!3259(X0) = $i!val!197)) | ((k!3259(X1) = $i!val!155) & (k!3259(X0) = $i!val!196)) | ((k!3259(X1) = $i!val!154) & (k!3259(X0) = $i!val!195)) | ((k!3259(X1) = $i!val!195) & (k!3259(X0) = $i!val!194)) | ((k!3259(X1) = $i!val!192) & (k!3259(X0) = $i!val!193)) | ((k!3259(X1) = $i!val!135) & (k!3259(X0) = $i!val!192)) | ((k!3259(X1) = $i!val!164) & (k!3259(X0) = $i!val!191)) | ((k!3259(X1) = $i!val!191) & (k!3259(X0) = $i!val!190)) | ((k!3259(X1) = $i!val!212) & (k!3259(X0) = $i!val!213)) | ((k!3259(X1) = $i!val!177) & (k!3259(X0) = $i!val!226)) | ((k!3259(X1) = $i!val!190) & (k!3259(X0) = $i!val!225)) | ((k!3259(X1) = $i!val!190) & (k!3259(X0) = $i!val!224)) | ((k!3259(X1) = $i!val!224) & (k!3259(X0) = $i!val!223)) | ((k!3259(X1) = $i!val!198) & (k!3259(X0) = $i!val!222)) | ((k!3259(X1) = $i!val!222) & (k!3259(X0) = $i!val!221)) | ((k!3259(X1) = $i!val!220) & (k!3259(X0) = $i!val!219)) | ((k!3259(X1) = $i!val!180) & (k!3259(X0) = $i!val!218)) | ((k!3259(X1) = $i!val!179) & (k!3259(X0) = $i!val!216)) | ((k!3259(X1) = $i!val!216) & (k!3259(X0) = $i!val!217)) | ((k!3259(X1) = $i!val!200) & (k!3259(X0) = $i!val!214)) | ((k!3259(X1) = $i!val!214) & (k!3259(X0) = $i!val!215)) | ((k!3259(X1) = $i!val!214) & (k!3259(X0) = $i!val!235)) | ((k!3259(X1) = $i!val!218) & (k!3259(X0) = $i!val!234)) | ((k!3259(X1) = $i!val!230) & (k!3259(X0) = $i!val!249)) | ((k!3259(X1) = $i!val!244) & (k!3259(X0) = $i!val!248)) | ((k!3259(X1) = $i!val!240) & (k!3259(X0) = $i!val!247)) | ((k!3259(X1) = $i!val!237) & (k!3259(X0) = $i!val!245)) | ((k!3259(X1) = $i!val!237) & (k!3259(X0) = $i!val!243)) | ((k!3259(X1) = $i!val!243) & (k!3259(X0) = $i!val!244)) | ((k!3259(X1) = $i!val!236) & (k!3259(X0) = $i!val!242)) | ((k!3259(X1) = $i!val!222) & (k!3259(X0) = $i!val!240)) | ((k!3259(X1) = $i!val!221) & (k!3259(X0) = $i!val!238)) | ((k!3259(X1) = $i!val!238) & (k!3259(X0) = $i!val!237)) | ((k!3259(X1) = $i!val!220) & (k!3259(X0) = $i!val!236)) | ((k!3259(X1) = $i!val!252) & (k!3259(X0) = $i!val!257)) | ((k!3259(X1) = $i!val!263) & (k!3259(X0) = $i!val!269)) | ((k!3259(X1) = $i!val!265) & (k!3259(X0) = $i!val!268)) | ((k!3259(X1) = $i!val!266) & (k!3259(X0) = $i!val!267)) | ((k!3259(X1) = $i!val!264) & (k!3259(X0) = $i!val!265)) | ((k!3259(X1) = $i!val!257) & (k!3259(X0) = $i!val!264)) | ((k!3259(X1) = $i!val!257) & (k!3259(X0) = $i!val!263)) | ((k!3259(X1) = $i!val!263) & (k!3259(X0) = $i!val!262)) | ((k!3259(X1) = $i!val!254) & (k!3259(X0) = $i!val!261)) | ((k!3259(X1) = $i!val!253) & (k!3259(X0) = $i!val!260)) | ((k!3259(X1) = $i!val!187) & (k!3259(X0) = $i!val!186)) | ((k!3259(X1) = $i!val!151) & (k!3259(X0) = $i!val!182)) | ((k!3259(X1) = $i!val!252) & (k!3259(X0) = $i!val!259)) | ((k!3259(X1) = $i!val!250) & (k!3259(X0) = $i!val!251)) | ((k!3259(X1) = $i!val!221) & (k!3259(X0) = $i!val!239)) | ((k!3259(X1) = $i!val!230) & (k!3259(X0) = $i!val!231)) | ((k!3259(X1) = $i!val!186) & (k!3259(X0) = $i!val!220)) | ((k!3259(X1) = $i!val!142) & (k!3259(X0) = $i!val!199)) | ((k!3259(X1) = $i!val!152) & (k!3259(X0) = $i!val!153)) | ((k!3259(X1) = $i!val!216) & (k!3259(X0) = $i!val!233)) | ((k!3259(X1) = $i!val!200) & (k!3259(X0) = $i!val!212)) | ((k!3259(X1) = $i!val!168) & (k!3259(X0) = $i!val!189)) | ((k!3259(X1) = $i!val!161) & (k!3259(X0) = $i!val!175)) | ((k!3259(X1) = $i!val!125) & (k!3259(X0) = $i!val!150)) | ((k!3259(X1) = $i!val!52) & (k!3259(X0) = $i!val!82)) | ((k!3259(X1) = $i!val!161) & (k!3259(X0) = $i!val!173)) | ((k!3259(X1) = $i!val!28) & (k!3259(X0) = $i!val!83)) | ((k!3259(X1) = $i!val!139) & (k!3259(X0) = $i!val!140)) | ((k!3259(X1) = $i!val!46) & (k!3259(X0) = $i!val!90)) | ((k!3259(X1) = $i!val!257) & (k!3259(X0) = $i!val!258)) | ((k!3259(X1) = $i!val!175) & (k!3259(X0) = $i!val!174)) | ((k!3259(X1) = $i!val!33) & (k!3259(X0) = $i!val!137)) | ((k!3259(X1) = $i!val!58) & (k!3259(X0) = $i!val!88)) | ((k!3259(X1) = $i!val!90) & (k!3259(X0) = $i!val!89)) | ((k!3259(X1) = $i!val!22) & (k!3259(X0) = $i!val!71)) | ((k!3259(X1) = $i!val!71) & (k!3259(X0) = $i!val!70)) | ((k!3259(X1) = $i!val!72) & (k!3259(X0) = $i!val!73)) | ((k!3259(X1) = $i!val!108) & (k!3259(X0) = $i!val!120)) | ((k!3259(X1) = $i!val!54) & (k!3259(X0) = $i!val!53)) | ((k!3259(X1) = $i!val!51) & (k!3259(X0) = $i!val!52)) | ((k!3259(X1) = $i!val!135) & (k!3259(X0) = $i!val!136)) | ((k!3259(X1) = $i!val!22) & (k!3259(X0) = $i!val!69)) | ((k!3259(X1) = $i!val!62) & (k!3259(X0) = $i!val!68)) | ((k!3259(X1) = $i!val!9) & (k!3259(X0) = $i!val!35)) | ((k!3259(X1) = $i!val!2) & (k!3259(X0) = $i!val!57)) | ((k!3259(X1) = $i!val!1) & (k!3259(X0) = $i!val!58)) | ((k!3259(X1) = $i!val!43) & (k!3259(X0) = $i!val!49)) | ((k!3259(X1) = $i!val!110) & (k!3259(X0) = $i!val!111)) | ((k!3259(X1) = $i!val!108) & (k!3259(X0) = $i!val!109)) | ((k!3259(X1) = $i!val!83) & (k!3259(X0) = $i!val!110)) | ((k!3259(X1) = $i!val!168) & (k!3259(X0) = $i!val!169)) | ((k!3259(X1) = $i!val!45) & (k!3259(X0) = $i!val!46)) | ((k!3259(X1) = $i!val!72) & (k!3259(X0) = $i!val!105)) | ((k!3259(X1) = $i!val!63) & (k!3259(X0) = $i!val!72)) | ((k!3259(X1) = $i!val!63) & (k!3259(X0) = $i!val!74)) | ((k!3259(X1) = $i!val!40) & (k!3259(X0) = $i!val!168)) | ((k!3259(X1) = $i!val!64) & (k!3259(X0) = $i!val!65)) | ((k!3259(X1) = $i!val!130) & (k!3259(X0) = $i!val!148)) | ((k!3259(X1) = $i!val!43) & (k!3259(X0) = $i!val!64)) | ((k!3259(X1) = $i!val!125) & (k!3259(X0) = $i!val!149)) | ((k!3259(X1) = $i!val!205) & (k!3259(X0) = $i!val!206)) | ((k!3259(X1) = $i!val!5) & (k!3259(X0) = $i!val!25)) | ((k!3259(X1) = $i!val!4) & (k!3259(X0) = $i!val!26)) | ((k!3259(X1) = $i!val!17) & (k!3259(X0) = $i!val!18)) | ((k!3259(X1) = $i!val!200) & (k!3259(X0) = $i!val!211)) | ((k!3259(X1) = $i!val!209) & (k!3259(X0) = $i!val!210)) | ((k!3259(X1) = $i!val!4) & (k!3259(X0) = $i!val!28)) | ((k!3259(X1) = $i!val!44) & (k!3259(X0) = $i!val!43)) | ((k!3259(X1) = $i!val!230) & (k!3259(X0) = $i!val!250)) | ((k!3259(X1) = $i!val!7) & (k!3259(X0) = $i!val!40)) | ((k!3259(X1) = $i!val!176) & (k!3259(X0) = $i!val!232)) | ((k!3259(X1) = $i!val!176) & (k!3259(X0) = $i!val!230)) | ((k!3259(X1) = $i!val!41) & (k!3259(X0) = $i!val!42)) | ((k!3259(X1) = $i!val!1) & (k!3259(X0) = $i!val!23)) | ((k!3259(X1) = $i!val!271) & (k!3259(X0) = $i!val!270)) | ((k!3259(X1) = $i!val!252) & (k!3259(X0) = $i!val!256)) | ((k!3259(X1) = $i!val!1) & (k!3259(X0) = $i!val!61)) | ((k!3259(X1) = $i!val!250) & (k!3259(X0) = $i!val!254)) | ((k!3259(X1) = $i!val!29) & (k!3259(X0) = $i!val!75)) | ((k!3259(X1) = $i!val!60) & (k!3259(X0) = $i!val!78)) | ((k!3259(X1) = $i!val!11) & (k!3259(X0) = $i!val!16)) | ((k!3259(X1) = $i!val!11) & (k!3259(X0) = $i!val!13)) | ((k!3259(X1) = $i!val!0) & (k!3259(X0) = $i!val!4)) | ((k!3259(X1) = $i!val!7) & (k!3259(X0) = $i!val!47)) | ((k!3259(X1) = $i!val!0) & (k!3259(X0) = $i!val!1)) | ((k!3259(X1) = $i!val!0) & (k!3259(X0) = $i!val!11)) | ((k!3259(X1) = $i!val!5) & (k!3259(X0) = $i!val!6)) | ((k!3259(X1) = $i!val!7) & (k!3259(X0) = $i!val!8)) | ((k!3259(X1) = $i!val!9) & (k!3259(X0) = $i!val!10)) | ((k!3259(X1) = $i!val!29) & (k!3259(X0) = $i!val!30)) | ((k!3259(X1) = $i!val!35) & (k!3259(X0) = $i!val!34)) | ((k!3259(X1) = $i!val!49) & (k!3259(X0) = $i!val!48)) | ((k!3259(X1) = $i!val!9) & (k!3259(X0) = $i!val!56)) | ((k!3259(X1) = $i!val!58) & (k!3259(X0) = $i!val!59)) | ((k!3259(X1) = $i!val!46) & (k!3259(X0) = $i!val!50)) | ((k!3259(X1) = $i!val!9) & (k!3259(X0) = $i!val!54)) | ((k!3259(X1) = $i!val!10) & (k!3259(X0) = $i!val!55)) | ((k!3259(X1) = $i!val!46) & (k!3259(X0) = $i!val!51)) | ((k!3259(X1) = $i!val!0) & (k!3259(X0) = $i!val!19)) | ((k!3259(X1) = $i!val!23) & (k!3259(X0) = $i!val!22)) | ((k!3259(X1) = $i!val!7) & (k!3259(X0) = $i!val!44)) | ((k!3259(X1) = $i!val!7) & (k!3259(X0) = $i!val!45)) | ((k!3259(X1) = $i!val!7) & (k!3259(X0) = $i!val!41)) | ((k!3259(X1) = $i!val!9) & (k!3259(X0) = $i!val!36)) | ((k!3259(X1) = $i!val!1) & (k!3259(X0) = $i!val!63)) | ((k!3259(X1) = $i!val!11) & (k!3259(X0) = $i!val!17)) | ((k!3259(X1) = $i!val!4) & (k!3259(X0) = $i!val!27)) | ((k!3259(X1) = $i!val!26) & (k!3259(X0) = $i!val!21)) | ((k!3259(X1) = $i!val!36) & (k!3259(X0) = $i!val!37)) | ((k!3259(X1) = $i!val!61) & (k!3259(X0) = $i!val!62)) | ((k!3259(X1) = $i!val!1) & (k!3259(X0) = $i!val!60)) | ((k!3259(X1) = $i!val!23) & (k!3259(X0) = $i!val!77)) | ((k!3259(X1) = $i!val!78) & (k!3259(X0) = $i!val!79)) | ((k!3259(X1) = $i!val!75) & (k!3259(X0) = $i!val!76)) | ((k!3259(X1) = $i!val!11) & (k!3259(X0) = $i!val!15)) | ((k!3259(X1) = $i!val!13) & (k!3259(X0) = $i!val!14)) | ((k!3259(X1) = $i!val!11) & (k!3259(X0) = $i!val!12)) | ((k!3259(X1) = $i!val!1) & (k!3259(X0) = $i!val!2)) | ((k!3259(X1) = $i!val!2) & (k!3259(X0) = $i!val!3)) | ((k!3259(X1) = $i!val!0) & (k!3259(X0) = $i!val!9)) | ((k!3259(X1) = $i!val!0) & (k!3259(X0) = $i!val!7)) | ((k!3259(X1) = $i!val!4) & (k!3259(X0) = $i!val!5)) | ((k!3259(X1) = $i!val!21) & (k!3259(X0) = $i!val!32)) | ((k!3259(X1) = $i!val!32) & (k!3259(X0) = $i!val!33)) | ((k!3259(X1) = $i!val!4) & (k!3259(X0) = $i!val!29)) | ((k!3259(X1) = $i!val!97) & (k!3259(X0) = $i!val!135)) | ((k!3259(X1) = $i!val!118) & (k!3259(X0) = $i!val!119)) | ((k!3259(X1) = $i!val!88) & (k!3259(X0) = $i!val!132)) | ((k!3259(X1) = $i!val!97) & (k!3259(X0) = $i!val!134)) | ((k!3259(X1) = $i!val!33) & (k!3259(X0) = $i!val!118)) | ((k!3259(X1) = $i!val!106) & (k!3259(X0) = $i!val!133)) | ((k!3259(X1) = $i!val!83) & (k!3259(X0) = $i!val!114)) | ((k!3259(X1) = $i!val!112) & (k!3259(X0) = $i!val!113)) | ((k!3259(X1) = $i!val!83) & (k!3259(X0) = $i!val!112)) | ((k!3259(X1) = $i!val!91) & (k!3259(X0) = $i!val!97)) | ((k!3259(X1) = $i!val!103) & (k!3259(X0) = $i!val!102)) | ((k!3259(X1) = $i!val!100) & (k!3259(X0) = $i!val!101)) | ((k!3259(X1) = $i!val!75) & (k!3259(X0) = $i!val!103)) | ((k!3259(X1) = $i!val!19) & (k!3259(X0) = $i!val!100)) | ((k!3259(X1) = $i!val!19) & (k!3259(X0) = $i!val!99)) | ((k!3259(X1) = $i!val!128) & (k!3259(X0) = $i!val!145)) | ((k!3259(X1) = $i!val!145) & (k!3259(X0) = $i!val!146)) | ((k!3259(X1) = $i!val!132) & (k!3259(X0) = $i!val!172)) | ((k!3259(X1) = $i!val!132) & (k!3259(X0) = $i!val!170)) | ((k!3259(X1) = $i!val!170) & (k!3259(X0) = $i!val!171)) | ((k!3259(X1) = $i!val!193) & (k!3259(X0) = $i!val!209)) | ((k!3259(X1) = $i!val!204) & (k!3259(X0) = $i!val!208)) | ((k!3259(X1) = $i!val!174) & (k!3259(X0) = $i!val!207)) | ((k!3259(X1) = $i!val!145) & (k!3259(X0) = $i!val!205)) | ((k!3259(X1) = $i!val!213) & (k!3259(X0) = $i!val!229)) | ((k!3259(X1) = $i!val!196) & (k!3259(X0) = $i!val!228)) | ((k!3259(X1) = $i!val!256) & (k!3259(X0) = $i!val!255)) | ((k!3259(X1) = $i!val!250) & (k!3259(X0) = $i!val!253)) | ((k!3259(X1) = $i!val!253) & (k!3259(X0) = $i!val!252)) | ((k!3259(X1) = $i!val!270) & (k!3259(X0) = $i!val!272)) | ((k!3259(X1) = $i!val!265) & (k!3259(X0) = $i!val!271)) | ((k!3259(X1) = $i!val!124) & (k!3259(X0) = $i!val!160)) | ((k!3259(X1) = $i!val!128) & (k!3259(X0) = $i!val!147)) | ((k!3259(X1) = $i!val!137) & (k!3259(X0) = $i!val!138)) | ((k!3259(X1) = $i!val!80) & (k!3259(X0) = $i!val!129)) | ((k!3259(X1) = $i!val!265) & (k!3259(X0) = $i!val!266))))). % 119.26/119.57 tff(formula277, axiom, % 119.26/119.57 ![X0: $i] : (p3(X0) <=> ((k!3259(X0) = $i!val!150) | (k!3259(X0) = $i!val!182) | (k!3259(X0) = $i!val!192) | (k!3259(X0) = $i!val!29) | (k!3259(X0) = $i!val!47) | (k!3259(X0) = $i!val!9) | (k!3259(X0) = $i!val!43) | (k!3259(X0) = $i!val!1) | (k!3259(X0) = $i!val!63) | (k!3259(X0) = $i!val!37) | (k!3259(X0) = $i!val!212) | (k!3259(X0) = $i!val!46) | (k!3259(X0) = $i!val!56) | (k!3259(X0) = $i!val!209) | (k!3259(X0) = $i!val!41) | (k!3259(X0) = $i!val!27) | (k!3259(X0) = $i!val!100) | (k!3259(X0) = $i!val!17) | (k!3259(X0) = $i!val!60)))). % 119.35/119.63 tff(formula278, axiom, % 119.35/119.63 ![X0: $i] : (p1(X0) <=> ((k!3259(X0) = $i!val!264) | (k!3259(X0) = $i!val!19) | (k!3259(X0) = $i!val!15) | (k!3259(X0) = $i!val!25) | (k!3259(X0) = $i!val!16) | (k!3259(X0) = $i!val!77) | (k!3259(X0) = $i!val!3) | (k!3259(X0) = $i!val!12) | (k!3259(X0) = $i!val!45) | (k!3259(X0) = $i!val!61) | (k!3259(X0) = $i!val!32) | (k!3259(X0) = $i!val!51) | (k!3259(X0) = $i!val!26) | (k!3259(X0) = $i!val!35) | (k!3259(X0) = $i!val!57) | (k!3259(X0) = $i!val!13) | (k!3259(X0) = $i!val!118)))). % 119.35/119.63 % SZS output end Model % 119.35/119.69 % E exiting %------------------------------------------------------------------------------