%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP369_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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 : Fri Sep 25 01:49:30 PM UTC 2026
% Result : Theorem 99.99s 15.34s
% Output : CNFRefutation 99.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP369_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 18:29:28 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41
% 0.15/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.41
% 0.15/0.41 % Detected problem language: tptp
% 0.15/0.42 % Proving...
% 99.99/15.34 % SZS status Started for theBenchmark.p
% 99.99/15.34 % SZS status Theorem for theBenchmark.p
% 99.99/15.34
% 99.99/15.34 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 99.99/15.34
% 99.99/15.34 % ------ iProver source info
% 99.99/15.34
% 99.99/15.34 % git: date: 2026-07-19 20:42:38 +0200
% 99.99/15.34 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 99.99/15.34 % git: non_committed_changes: false
% 99.99/15.34
% 99.99/15.34 % ------ Parsing...
% 99.99/15.34 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 99.99/15.34
% 99.99/15.34 % ------ Preprocessing... sf_s rm: 2 0s sf_e sf_s rm: 1 0s sf_e %
% 99.99/15.34
% 99.99/15.34 % ------ Preprocessing...%
% 99.99/15.34
% 99.99/15.34 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 99.99/15.34 % ------ Proving...
% 99.99/15.34 % ------ Problem Properties
% 99.99/15.34
% 99.99/15.34 %
% 99.99/15.34 % clauses 1368
% 99.99/15.34 % conjectures 1
% 99.99/15.34 % EPR 126
% 99.99/15.34 % Horn 1147
% 99.99/15.34 % unary 256
% 99.99/15.34 % binary 818
% 99.99/15.34 % lits 3897
% 99.99/15.34 % lits eq 1127
% 99.99/15.34 % fd_pure 1
% 99.99/15.34 % fd_pseudo 0
% 99.99/15.34 % fd_cond 138
% 99.99/15.34 % fd_pseudo_cond 38
% 99.99/15.34 % AC symbols 0
% 99.99/15.34
% 99.99/15.34 % ------ Input Options Time Limit: Unbounded
% 99.99/15.34
% 99.99/15.34
% 99.99/15.34 % ------
% 99.99/15.34 % Current options:
% 99.99/15.34 % ------
% 99.99/15.34
% 99.99/15.34
% 99.99/15.34 %
% 99.99/15.34
% 99.99/15.34 % ------ Proving...
% 99.99/15.34 %
% 99.99/15.34
% 99.99/15.34 % SZS status Theorem for theBenchmark.p
% 99.99/15.34
% 99.99/15.34 % SZS output start CNFRefutation for theBenchmark.p
% 99.99/15.34
% 99.99/15.34 tff(func_def_0, type, 'fun_app$d': ('Bool_bool_a_ltln_set_fun_fun_bool_bool_a_ltln_set_fun_fun_bool_bool_a_ltln_set_fun_fun_fun_fun$' * 'Bool_bool_a_ltln_set_fun_fun$') > 'Bool_bool_a_ltln_set_fun_fun_bool_bool_a_ltln_set_fun_fun_fun$').
% 99.99/15.34 tff(pred_def_1, type, 'less_eq$': ('A_ltln_set$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_2, type, 'less_eq$a': ('Bool_bool_a_ltln_set_fun_fun$' * 'Bool_bool_a_ltln_set_fun_fun$') > $o).
% 99.99/15.34 tff(pred_def_3, type, 'fun_app$': ('A_ltln_bool_fun$' * 'A_ltln$') > $o).
% 99.99/15.34 tff(pred_def_4, type, 'less_eq$c': ('Bool_a_ltln_set_fun$' * 'Bool_a_ltln_set_fun$') > $o).
% 99.99/15.34 tff(pred_def_5, type, 'member$': ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_6, type, 'less_eq$b': ('A_ltln_bool_fun$' * 'A_ltln_bool_fun$') > $o).
% 99.99/15.34 tff(func_def_7, type, 'g_F$': ('A_ltln$' * 'Nat_a_set_fun$') > 'A_ltln_set$').
% 99.99/15.34 tff(pred_def_8, type, 'is_singleton$': 'A_ltln_set$' > $o).
% 99.99/15.34 tff(pred_def_9, type, 'is_empty$': 'A_ltln_set$' > $o).
% 99.99/15.34 tff(pred_def_10, type, 'sup$d': (tlbool * tlbool) > $o).
% 99.99/15.34 tff(pred_def_11, type, sP0: ('A_ltln_set$' * 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$') > $o).
% 99.99/15.34 tff(pred_def_12, type, sP1: ('A_ltln$' * 'A_ltln$' * 'A_ltln_set$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_13, type, sP2: ('A_ltln_set$' * 'A_ltln_set$' * 'A_ltln$') > $o).
% 99.99/15.34 tff(pred_def_14, type, sP3: ('A_ltln_set$' * 'A_ltln_set$' * 'A_ltln$') > $o).
% 99.99/15.34 tff(pred_def_15, type, sP4: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_16, type, sP5: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_17, type, sP6: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_18, type, sP7: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_19, type, sP8: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_20, type, sP9: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_21, type, sP10: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_22, type, sP11: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_23, type, sP12: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_24, type, sP13: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_25, type, sP14: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_26, type, sP15: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_27, type, sP16: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_28, type, sP17: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_29, type, sP18: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_30, type, sP19: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_31, type, sP20: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_32, type, sP21: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_33, type, sP22: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_34, type, sP23: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_35, type, sP24: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_36, type, sP25: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_37, type, sP26: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_38, type, sP27: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_39, type, sP28: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_40, type, sP29: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_41, type, sP30: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_42, type, sP31: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_43, type, sP32: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_44, type, sP33: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_45, type, sP34: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_46, type, sP35: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_47, type, sP36: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_48, type, sP37: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_49, type, sP38: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_50, type, sP39: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_51, type, sP40: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_52, type, sP41: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_53, type, sP42: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_54, type, sP43: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_55, type, sP44: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_56, type, sP45: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_57, type, sP46: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_58, type, sP47: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_59, type, sP48: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_60, type, sP49: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_61, type, sP50: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_62, type, sP51: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_63, type, sP52: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_64, type, sP53: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_65, type, sP54: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_66, type, sP55: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_67, type, sP56: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_68, type, sP57: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_69, type, sP58: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_70, type, sP59: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_71, type, sP60: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_72, type, sP61: 'A_ltln$' > $o).
% 99.99/15.34 tff(pred_def_73, type, sP62: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_74, type, sP63: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_75, type, sP64: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_76, type, sP65: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_77, type, sP66: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_78, type, sP67: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_79, type, sP68: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_80, type, sP69: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_81, type, sP70: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_82, type, sP71: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_83, type, sP72: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_84, type, sP73: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_85, type, sP74: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_86, type, sP75: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_87, type, sP76: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_88, type, sP77: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_89, type, sP78: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_90, type, sP79: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_91, type, sP80: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_92, type, sP81: ('A_ltln$' * tlbool) > $o).
% 99.99/15.34 tff(pred_def_93, type, sP82: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_94, type, sP83: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_95, type, sP84: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_96, type, sP85: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_97, type, sP86: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_98, type, sP87: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_99, type, sP88: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_100, type, sP89: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_101, type, sP90: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_102, type, sP91: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_103, type, sP92: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_104, type, sP93: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_105, type, sP94: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_106, type, sP95: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_107, type, sP96: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_108, type, sP97: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_109, type, sP98: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_110, type, sP99: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_111, type, sP100: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_112, type, sP101: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_113, type, sP102: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_114, type, sP103: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_115, type, sP104: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_116, type, sP105: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_117, type, sP106: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_118, type, sP107: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_119, type, sP108: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_120, type, sP109: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_121, type, sP110: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_122, type, sP111: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_123, type, sP112: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_124, type, sP113: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_125, type, sP114: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_126, type, sP115: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_127, type, sP116: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_128, type, sP117: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_129, type, sP118: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_130, type, sP119: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_131, type, sP120: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_132, type, sP121: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_133, type, sP122: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_134, type, sP123: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_135, type, sP124: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_136, type, sP125: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_137, type, sP126: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_138, type, sP127: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_139, type, sP128: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_140, type, sP129: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_141, type, sP130: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_142, type, sP131: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_143, type, sP132: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_144, type, sP133: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_145, type, sP134: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_146, type, sP135: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_147, type, sP136: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_148, type, sP137: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_149, type, sP138: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_150, type, sP139: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_151, type, sP140: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_152, type, sP141: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_153, type, sP142: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_154, type, sP143: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_155, type, sP144: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_156, type, sP145: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_157, type, sP146: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_158, type, sP147: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_159, type, sP148: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_160, type, sP149: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_161, type, sP150: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_162, type, sP151: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_163, type, sP152: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_164, type, sP153: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_165, type, sP154: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_166, type, sP155: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_167, type, sP156: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_168, type, sP157: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_169, type, sP158: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_170, type, sP159: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_171, type, sP160: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_172, type, sP161: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_173, type, sP162: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_174, type, sP163: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_175, type, sP164: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_176, type, sP165: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_177, type, sP166: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_178, type, sP167: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_179, type, sP168: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_180, type, sP169: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_181, type, sP170: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_182, type, sP171: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_183, type, sP172: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_184, type, sP173: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_185, type, sP174: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_186, type, sP175: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_187, type, sP176: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_188, type, sP177: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_189, type, sP178: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_190, type, sP179: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_191, type, sP180: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_192, type, sP181: ('A_ltln$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_193, type, sP182: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_194, type, sP183: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_195, type, sP184: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_196, type, sP185: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_197, type, sP186: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_198, type, sP187: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_199, type, sP188: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_200, type, sP189: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_201, type, sP190: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_202, type, sP191: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_203, type, sP192: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_204, type, sP193: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_205, type, sP194: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_206, type, sP195: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_207, type, sP196: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_208, type, sP197: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_209, type, sP198: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_210, type, sP199: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_211, type, sP200: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_212, type, sP201: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_213, type, sP202: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_214, type, sP203: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_215, type, sP204: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_216, type, sP205: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_217, type, sP206: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_218, type, sP207: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_219, type, sP208: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_220, type, sP209: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_221, type, sP210: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(pred_def_222, type, sP211: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > $o).
% 99.99/15.34 tff(func_def_223, type, sK361: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_224, type, sK362: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_225, type, sK363: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_226, type, sK364: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_227, type, sK365: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_228, type, sK366: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_229, type, sK367: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_230, type, sK368: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_231, type, sK369: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_232, type, sK370: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_233, type, sK371: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_234, type, sK372: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_235, type, sK373: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_236, type, sK374: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_237, type, sK375: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_238, type, sK376: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_239, type, sK377: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_240, type, sK378: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_241, type, sK379: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_242, type, sK380: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_243, type, sK381: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_244, type, sK382: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_245, type, sK383: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_246, type, sK384: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_247, type, sK385: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_248, type, sK386: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_249, type, sK387: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_250, type, sK388: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_251, type, sK389: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_252, type, sK390: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_253, type, sK391: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_254, type, sK392: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_255, type, sK393: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_256, type, sK394: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_257, type, sK395: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_258, type, sK396: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_259, type, sK397: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_260, type, sK398: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_261, type, sK399: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_262, type, sK400: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_263, type, sK401: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_264, type, sK402: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_265, type, sK403: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_266, type, sK404: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_267, type, sK405: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_268, type, sK406: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_269, type, sK407: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_270, type, sK408: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_271, type, sK409: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_272, type, sK410: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_273, type, sK411: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_274, type, sK412: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_275, type, sK413: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_276, type, sK414: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_277, type, sK415: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_278, type, sK416: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_279, type, sK417: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_280, type, sK418: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_281, type, sK419: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_282, type, sK420: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_283, type, sK421: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_284, type, sK422: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_285, type, sK423: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_286, type, sK424: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_287, type, sK425: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_288, type, sK426: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_289, type, sK427: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_290, type, sK428: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_291, type, sK429: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_292, type, sK430: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_293, type, sK431: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_294, type, sK432: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_295, type, sK433: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_296, type, sK434: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_297, type, sK435: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_298, type, sK436: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_299, type, sK437: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_300, type, sK438: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_301, type, sK439: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_302, type, sK440: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_303, type, sK441: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_304, type, sK442: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_305, type, sK443: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_306, type, sK444: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_307, type, sK445: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_308, type, sK446: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_309, type, sK447: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_310, type, sK448: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_311, type, sK449: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_312, type, sK450: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_313, type, sK451: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_314, type, sK452: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_315, type, sK453: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_316, type, sK454: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_317, type, sK455: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_318, type, sK456: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_319, type, sK457: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_320, type, sK458: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_321, type, sK459: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_322, type, sK460: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_323, type, sK461: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_324, type, sK462: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_325, type, sK463: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_326, type, sK464: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_327, type, sK465: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_328, type, sK466: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_329, type, sK467: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_330, type, sK468: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_331, type, sK469: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_332, type, sK470: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_333, type, sK471: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_334, type, sK472: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_335, type, sK473: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_336, type, sK474: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_337, type, sK475: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_338, type, sK476: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_339, type, sK477: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_340, type, sK478: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_341, type, sK479: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_342, type, sK480: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_343, type, sK481: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_344, type, sK482: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_345, type, sK483: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_346, type, sK484: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_347, type, sK485: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_348, type, sK486: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_349, type, sK487: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_350, type, sK488: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_351, type, sK489: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_352, type, sK490: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_353, type, sK491: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_354, type, sK492: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_355, type, sK493: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_356, type, sK494: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_357, type, sK495: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_358, type, sK496: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_359, type, sK497: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_360, type, sK498: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_361, type, sK499: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_362, type, sK500: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_363, type, sK501: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_364, type, sK502: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_365, type, sK503: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_366, type, sK504: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_367, type, sK505: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_368, type, sK506: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_369, type, sK507: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_370, type, sK508: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_371, type, sK509: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_372, type, sK510: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_373, type, sK511: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_374, type, sK512: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_375, type, sK513: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_376, type, sK514: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_377, type, sK515: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_378, type, sK516: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_379, type, sK517: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_380, type, sK518: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_381, type, sK519: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_382, type, sK520: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_383, type, sK521: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_384, type, sK522: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_385, type, sK523: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_386, type, sK524: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_387, type, sK525: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_388, type, sK526: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_389, type, sK527: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_390, type, sK528: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_391, type, sK529: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_392, type, sK530: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_393, type, sK531: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_394, type, sK532: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_395, type, sK533: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_396, type, sK534: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_397, type, sK535: ('A_ltln$' * tlbool) > 'A$').
% 99.99/15.34 tff(func_def_398, type, sK536: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_399, type, sK537: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_400, type, sK538: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_401, type, sK539: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_402, type, sK540: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_403, type, sK541: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_404, type, sK542: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_405, type, sK543: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_406, type, sK544: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_407, type, sK545: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_408, type, sK546: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_409, type, sK547: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_410, type, sK548: ('A_ltln$' * tlbool) > 'A_ltln$').
% 99.99/15.34 tff(func_def_411, type, sK549: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_412, type, sK550: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_413, type, sK551: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_414, type, sK552: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_415, type, sK553: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_416, type, sK554: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_417, type, sK555: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_418, type, sK556: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_419, type, sK557: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_420, type, sK558: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_421, type, sK559: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_422, type, sK560: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_423, type, sK561: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_424, type, sK562: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_425, type, sK563: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_426, type, sK564: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_427, type, sK565: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_428, type, sK566: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_429, type, sK567: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_430, type, sK568: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_431, type, sK569: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_432, type, sK570: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_433, type, sK571: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_434, type, sK572: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_435, type, sK573: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_436, type, sK574: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_437, type, sK575: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_438, type, sK576: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_439, type, sK577: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_440, type, sK578: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_441, type, sK579: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_442, type, sK580: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_443, type, sK581: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_444, type, sK582: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_445, type, sK583: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_446, type, sK584: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_447, type, sK585: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_448, type, sK586: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_449, type, sK587: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_450, type, sK588: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_451, type, sK589: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_452, type, sK590: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_453, type, sK591: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_454, type, sK592: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_455, type, sK593: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_456, type, sK594: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_457, type, sK595: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_458, type, sK596: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_459, type, sK597: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_460, type, sK598: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_461, type, sK599: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_462, type, sK600: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_463, type, sK601: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_464, type, sK602: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_465, type, sK603: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_466, type, sK604: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_467, type, sK605: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_468, type, sK606: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_469, type, sK607: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_470, type, sK608: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_471, type, sK609: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_472, type, sK610: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_473, type, sK611: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_474, type, sK612: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_475, type, sK613: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_476, type, sK614: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_477, type, sK615: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_478, type, sK616: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_479, type, sK617: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_480, type, sK618: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_481, type, sK619: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_482, type, sK620: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_483, type, sK621: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_484, type, sK622: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_485, type, sK623: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_486, type, sK624: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_487, type, sK625: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_488, type, sK626: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_489, type, sK627: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_490, type, sK628: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_491, type, sK629: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_492, type, sK630: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_493, type, sK631: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_494, type, sK632: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_495, type, sK633: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_496, type, sK634: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_497, type, sK635: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_498, type, sK636: 'A_ltln$' > 'A_ltln$').
% 99.99/15.34 tff(func_def_499, type, sK637: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_500, type, sK638: 'A_ltln$' > 'A$').
% 99.99/15.34 tff(func_def_501, type, sK639: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_502, type, sK640: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_503, type, sK641: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_504, type, sK642: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_505, type, sK643: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_506, type, sK644: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_507, type, sK645: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_508, type, sK646: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_509, type, sK647: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_510, type, sK648: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_511, type, sK649: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_512, type, sK650: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_513, type, sK651: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_514, type, sK652: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_515, type, sK653: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_516, type, sK654: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_517, type, sK655: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_518, type, sK656: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_519, type, sK657: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_520, type, sK658: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_521, type, sK659: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_522, type, sK660: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_523, type, sK661: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_524, type, sK662: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_525, type, sK663: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_526, type, sK664: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_527, type, sK665: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_528, type, sK666: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_529, type, sK667: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_530, type, sK668: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_531, type, sK669: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_532, type, sK670: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_533, type, sK671: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_534, type, sK672: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_535, type, sK673: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_536, type, sK674: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_537, type, sK675: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_538, type, sK676: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_539, type, sK677: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_540, type, sK678: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_541, type, sK679: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_542, type, sK680: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_543, type, sK681: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_544, type, sK682: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_545, type, sK683: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_546, type, sK684: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_547, type, sK685: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_548, type, sK686: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_549, type, sK687: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_550, type, sK688: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_551, type, sK689: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_552, type, sK690: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_553, type, sK691: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_554, type, sK692: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_555, type, sK693: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_556, type, sK694: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_557, type, sK695: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_558, type, sK696: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_559, type, sK697: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_560, type, sK698: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_561, type, sK699: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_562, type, sK700: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_563, type, sK701: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_564, type, sK702: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_565, type, sK703: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_566, type, sK704: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_567, type, sK705: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_568, type, sK706: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_569, type, sK707: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_570, type, sK708: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_571, type, sK709: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_572, type, sK710: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_573, type, sK711: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_574, type, sK712: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_575, type, sK713: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_576, type, sK714: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_577, type, sK715: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_578, type, sK716: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_579, type, sK717: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_580, type, sK718: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_581, type, sK719: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_582, type, sK720: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_583, type, sK721: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_584, type, sK722: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_585, type, sK723: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_586, type, sK724: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_587, type, sK725: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_588, type, sK726: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_589, type, sK727: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_590, type, sK728: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_591, type, sK729: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_592, type, sK730: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_593, type, sK731: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_594, type, sK732: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_595, type, sK733: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_596, type, sK734: ('A_ltln$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_597, type, sK735: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_598, type, sK736: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_599, type, sK737: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_600, type, sK738: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_601, type, sK739: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_602, type, sK740: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_603, type, sK741: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_604, type, sK742: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_605, type, sK743: ('A_ltln$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_606, type, sK744: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_607, type, sK745: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_608, type, sK746: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_609, type, sK747: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_610, type, sK748: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_611, type, sK749: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_612, type, sK750: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_613, type, sK751: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_614, type, sK752: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_615, type, sK753: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_616, type, sK754: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_617, type, sK755: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_618, type, sK756: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_619, type, sK757: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_620, type, sK758: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_621, type, sK759: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_622, type, sK760: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_623, type, sK761: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_624, type, sK762: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_625, type, sK763: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_626, type, sK764: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_627, type, sK765: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_628, type, sK766: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_629, type, sK767: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_630, type, sK768: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_631, type, sK769: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_632, type, sK770: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_633, type, sK771: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_634, type, sK772: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_635, type, sK773: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_636, type, sK774: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_637, type, sK775: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_638, type, sK776: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_639, type, sK777: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_640, type, sK778: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_641, type, sK779: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_642, type, sK780: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_643, type, sK781: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_644, type, sK782: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_645, type, sK783: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_646, type, sK784: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_647, type, sK785: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_648, type, sK786: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_649, type, sK787: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_650, type, sK788: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_651, type, sK789: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_652, type, sK790: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_653, type, sK791: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_654, type, sK792: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_655, type, sK793: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_656, type, sK794: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_657, type, sK795: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_658, type, sK796: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_659, type, sK797: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_660, type, sK798: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_661, type, sK799: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_662, type, sK800: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_663, type, sK801: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_664, type, sK802: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_665, type, sK803: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_666, type, sK804: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_667, type, sK805: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_668, type, sK806: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_669, type, sK807: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_670, type, sK808: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_671, type, sK809: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_672, type, sK810: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_673, type, sK811: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_674, type, sK812: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_675, type, sK813: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_676, type, sK814: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_677, type, sK815: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_678, type, sK816: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_679, type, sK817: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A$').
% 99.99/15.34 tff(func_def_680, type, sK818: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(func_def_681, type, sK819: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_682, type, sK820: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'A_ltln$').
% 99.99/15.34 tff(func_def_683, type, sK821: ('A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$') > 'Nat_a_set_fun$').
% 99.99/15.34 tff(f2,conjecture,(
% 99.99/15.34 'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))) & 'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture1)).
% 99.99/15.34
% 99.99/15.34 tff(f3,negated_conjecture,(
% 99.99/15.34 ~('less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))) & 'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))))),
% 99.99/15.34 inference(negated_conjecture,[status(cth)],[f2])).
% 99.99/15.34
% 99.99/15.34 tff(f6,axiom,(
% 99.99/15.34 'member$'('psi$','subformulas_nu$'('chi_1$')) | 'member$'('psi$','subformulas_nu$'('chi_2$')) | 'member$'('psi$','subformulas_mu$'('chi_1$')) | 'member$'('psi$','subformulas_mu$'('chi_2$'))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis4)).
% 99.99/15.34
% 99.99/15.34 tff(f8,axiom,(
% 99.99/15.34 ~'member$'('psi$','subformulas_nu$'('chi_1$'))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis6)).
% 99.99/15.34
% 99.99/15.34 tff(f9,axiom,(
% 99.99/15.34 ~'member$'('psi$','subformulas_nu$'('chi_2$'))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis7)).
% 99.99/15.34
% 99.99/15.34 tff(f100,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln$'] : (('less_eq$'(X0,X1) & 'member$'(X2,X0)) => 'member$'(X2,X1))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom98)).
% 99.99/15.34
% 99.99/15.34 tff(f193,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln_set$'] : ('less_eq$'(X0,X1) => 'less_eq$'(X0,'fun_app$a'('fun_app$b'('sup$',X2),X1)))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom191)).
% 99.99/15.34
% 99.99/15.34 tff(f195,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln_set$'] : ('less_eq$'(X0,X1) => 'less_eq$'(X0,'fun_app$a'('fun_app$b'('sup$',X1),X2)))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom193)).
% 99.99/15.34
% 99.99/15.34 tff(f208,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln$'] : ('less_eq$'(X0,X1) => 'less_eq$'(X0,'fun_app$a'('insert$'(X2),X1)))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom206)).
% 99.99/15.34
% 99.99/15.34 tff(f294,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln$',X1 : 'A_ltln$'] : ('member$'(X0,'subfrmlsn$'(X1)) => 'less_eq$'('subformulas_nu$'(X0),'subformulas_nu$'(X1)))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom292)).
% 99.99/15.34
% 99.99/15.34 tff(f296,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln$',X1 : 'A_ltln$'] : ('member$'(X0,'subfrmlsn$'(X1)) => 'less_eq$'('subformulas_mu$'(X0),'subformulas_mu$'(X1)))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom294)).
% 99.99/15.34
% 99.99/15.34 tff(f297,axiom,(
% 99.99/15.34 ! [X0 : 'A_ltln$'] : 'less_eq$'('subformulas_mu$'(X0),'subfrmlsn$'(X0))),
% 99.99/15.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom295)).
% 99.99/15.34
% 99.99/15.34 tff(f789,plain,(
% 99.99/15.34 ~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))) | ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))),
% 99.99/15.34 inference(ennf_transformation,[],[f3])).
% 99.99/15.34
% 99.99/15.34 tff(f811,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln$'] : ('member$'(X2,X1) | (~'less_eq$'(X0,X1) | ~'member$'(X2,X0)))),
% 99.99/15.34 inference(ennf_transformation,[],[f100])).
% 99.99/15.34
% 99.99/15.34 tff(f812,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln$'] : ('member$'(X2,X1) | ~'less_eq$'(X0,X1) | ~'member$'(X2,X0))),
% 99.99/15.34 inference(flattening,[],[f811])).
% 99.99/15.34
% 99.99/15.34 tff(f891,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln_set$'] : ('less_eq$'(X0,'fun_app$a'('fun_app$b'('sup$',X2),X1)) | ~'less_eq$'(X0,X1))),
% 99.99/15.34 inference(ennf_transformation,[],[f193])).
% 99.99/15.34
% 99.99/15.34 tff(f893,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln_set$'] : ('less_eq$'(X0,'fun_app$a'('fun_app$b'('sup$',X1),X2)) | ~'less_eq$'(X0,X1))),
% 99.99/15.34 inference(ennf_transformation,[],[f195])).
% 99.99/15.34
% 99.99/15.34 tff(f900,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln_set$',X1 : 'A_ltln_set$',X2 : 'A_ltln$'] : ('less_eq$'(X0,'fun_app$a'('insert$'(X2),X1)) | ~'less_eq$'(X0,X1))),
% 99.99/15.34 inference(ennf_transformation,[],[f208])).
% 99.99/15.34
% 99.99/15.34 tff(f923,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln$',X1 : 'A_ltln$'] : ('less_eq$'('subformulas_nu$'(X0),'subformulas_nu$'(X1)) | ~'member$'(X0,'subfrmlsn$'(X1)))),
% 99.99/15.34 inference(ennf_transformation,[],[f294])).
% 99.99/15.34
% 99.99/15.34 tff(f924,plain,(
% 99.99/15.34 ! [X0 : 'A_ltln$',X1 : 'A_ltln$'] : ('less_eq$'('subformulas_mu$'(X0),'subformulas_mu$'(X1)) | ~'member$'(X0,'subfrmlsn$'(X1)))),
% 99.99/15.34 inference(ennf_transformation,[],[f296])).
% 99.99/15.34
% 99.99/15.34 tff(f2210,plain,(
% 99.99/15.34 ~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))) | ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))),
% 99.99/15.34 inference(cnf_transformation,[],[f789])).
% 99.99/15.34
% 99.99/15.34 tff(f2215,plain,(
% 99.99/15.34 'member$'('psi$','subformulas_nu$'('chi_1$')) | 'member$'('psi$','subformulas_nu$'('chi_2$')) | 'member$'('psi$','subformulas_mu$'('chi_1$')) | 'member$'('psi$','subformulas_mu$'('chi_2$'))),
% 99.99/15.34 inference(cnf_transformation,[],[f6])).
% 99.99/15.34
% 99.99/15.34 tff(f2217,plain,(
% 99.99/15.34 ~'member$'('psi$','subformulas_nu$'('chi_1$'))),
% 99.99/15.34 inference(cnf_transformation,[],[f8])).
% 99.99/15.34
% 99.99/15.34 tff(f2218,plain,(
% 99.99/15.34 ~'member$'('psi$','subformulas_nu$'('chi_2$'))),
% 99.99/15.34 inference(cnf_transformation,[],[f9])).
% 99.99/15.34
% 99.99/15.34 tff(f2352,plain,(
% 99.99/15.34 ( ! [X2 : 'A_ltln$',X0 : 'A_ltln_set$',X1 : 'A_ltln_set$'] : ('member$'(X2,X1) | ~'less_eq$'(X0,X1) | ~'member$'(X2,X0)) )),
% 99.99/15.34 inference(cnf_transformation,[],[f812])).
% 99.99/15.34
% 99.99/15.34 tff(f2499,plain,(
% 99.99/15.34 ( ! [X2 : 'A_ltln_set$',X0 : 'A_ltln_set$',X1 : 'A_ltln_set$'] : ('less_eq$'(X0,'fun_app$a'('fun_app$b'('sup$',X2),X1)) | ~'less_eq$'(X0,X1)) )),
% 99.99/15.34 inference(cnf_transformation,[],[f891])).
% 99.99/15.34
% 99.99/15.34 tff(f2501,plain,(
% 99.99/15.34 ( ! [X2 : 'A_ltln_set$',X0 : 'A_ltln_set$',X1 : 'A_ltln_set$'] : ('less_eq$'(X0,'fun_app$a'('fun_app$b'('sup$',X1),X2)) | ~'less_eq$'(X0,X1)) )),
% 99.99/15.34 inference(cnf_transformation,[],[f893])).
% 99.99/15.34
% 99.99/15.34 tff(f2516,plain,(
% 99.99/15.34 ( ! [X2 : 'A_ltln$',X0 : 'A_ltln_set$',X1 : 'A_ltln_set$'] : ('less_eq$'(X0,'fun_app$a'('insert$'(X2),X1)) | ~'less_eq$'(X0,X1)) )),
% 99.99/15.34 inference(cnf_transformation,[],[f900])).
% 99.99/15.34
% 99.99/15.34 tff(f2650,plain,(
% 99.99/15.34 ( ! [X0 : 'A_ltln$',X1 : 'A_ltln$'] : ('less_eq$'('subformulas_nu$'(X0),'subformulas_nu$'(X1)) | ~'member$'(X0,'subfrmlsn$'(X1))) )),
% 99.99/15.34 inference(cnf_transformation,[],[f923])).
% 99.99/15.34
% 99.99/15.34 tff(f2652,plain,(
% 99.99/15.34 ( ! [X0 : 'A_ltln$',X1 : 'A_ltln$'] : ('less_eq$'('subformulas_mu$'(X0),'subformulas_mu$'(X1)) | ~'member$'(X0,'subfrmlsn$'(X1))) )),
% 99.99/15.34 inference(cnf_transformation,[],[f924])).
% 99.99/15.34
% 99.99/15.34 tff(f2653,plain,(
% 99.99/15.34 ( ! [X0 : 'A_ltln$'] : ('less_eq$'('subformulas_mu$'(X0),'subfrmlsn$'(X0))) )),
% 99.99/15.34 inference(cnf_transformation,[],[f297])).
% 99.99/15.34
% 99.99/15.34 tcf(c_51,negated_conjecture,
% 99.99/15.34 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))),
% 99.99/15.35 inference(cnf_transformation,[],[f2210])).
% 99.99/15.35
% 99.99/15.35 tcf(c_56,plain,
% 99.99/15.35 ('member$'('psi$','subformulas_nu$'('chi_1$'))|'member$'('psi$','subformulas_nu$'('chi_2$'))|
% 99.99/15.35 'member$'('psi$','subformulas_mu$'('chi_1$'))|'member$'('psi$','subformulas_mu$'('chi_2$'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2215])).
% 99.99/15.35
% 99.99/15.35 tcf(c_58,plain,
% 99.99/15.35 (~'member$'('psi$','subformulas_nu$'('chi_1$'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2217])).
% 99.99/15.35
% 99.99/15.35 tcf(c_59,plain,
% 99.99/15.35 (~'member$'('psi$','subformulas_nu$'('chi_2$'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2218])).
% 99.99/15.35
% 99.99/15.35 tcf(c_192,plain,![X0_'A_ltln_set':'A_ltln_set$',X0_'A_ltln':'A_ltln$',X1_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|~'member$'(X0_'A_ltln',X0_'A_ltln_set')|
% 99.99/15.35 'member$'(X0_'A_ltln',X1_'A_ltln_set')),
% 99.99/15.35 inference(cnf_transformation,[],[f2352])).
% 99.99/15.35
% 99.99/15.35 tcf(c_338,plain,![X0_'A_ltln_set':'A_ltln_set$',X1_'A_ltln_set':'A_ltln_set$',X2_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|'less_eq$'(X0_'A_ltln_set','fun_app$a'('fun_app$b'('sup$',X2_'A_ltln_set'),X1_'A_ltln_set'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2499])).
% 99.99/15.35
% 99.99/15.35 tcf(c_340,plain,![X0_'A_ltln_set':'A_ltln_set$',X1_'A_ltln_set':'A_ltln_set$',X2_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|'less_eq$'(X0_'A_ltln_set','fun_app$a'('fun_app$b'('sup$',X1_'A_ltln_set'),X2_'A_ltln_set'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2501])).
% 99.99/15.35
% 99.99/15.35 tcf(c_355,plain,![X0_'A_ltln_set':'A_ltln_set$',X0_'A_ltln':'A_ltln$',X1_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|'less_eq$'(X0_'A_ltln_set','fun_app$a'('insert$'(X0_'A_ltln'),X1_'A_ltln_set'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2516])).
% 99.99/15.35
% 99.99/15.35 tcf(c_487,plain,![X0_'A_ltln':'A_ltln$',X1_'A_ltln':'A_ltln$']:
% 99.99/15.35 (~'member$'(X0_'A_ltln','subfrmlsn$'(X1_'A_ltln'))|'less_eq$'('subformulas_nu$'(X0_'A_ltln'),'subformulas_nu$'(X1_'A_ltln'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2650])).
% 99.99/15.35
% 99.99/15.35 tcf(c_489,plain,![X0_'A_ltln':'A_ltln$',X1_'A_ltln':'A_ltln$']:
% 99.99/15.35 (~'member$'(X0_'A_ltln','subfrmlsn$'(X1_'A_ltln'))|'less_eq$'('subformulas_mu$'(X0_'A_ltln'),'subformulas_mu$'(X1_'A_ltln'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2652])).
% 99.99/15.35
% 99.99/15.35 tcf(c_490,plain,![X0_'A_ltln':'A_ltln$']:
% 99.99/15.35 ('less_eq$'('subformulas_mu$'(X0_'A_ltln'),'subfrmlsn$'(X0_'A_ltln'))),
% 99.99/15.35 inference(cnf_transformation,[],[f2653])).
% 99.99/15.35
% 99.99/15.35 tcf(c_2767,plain,
% 99.99/15.35 ('member$'('psi$','subformulas_mu$'('chi_1$'))|'member$'('psi$','subformulas_mu$'('chi_2$'))),
% 99.99/15.35 inference(global_subsumption_just,[status(thm)],[c_56,c_59,c_58,c_56])).
% 99.99/15.35
% 99.99/15.35 tcf(c_3499,plain,
% 99.99/15.35 ('member$'('psi$','subformulas_mu$'('chi_1$'))|'member$'('psi$','subformulas_mu$'('chi_2$'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_2767])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4615,plain,![X0_'A_ltln':'A_ltln$']:
% 99.99/15.35 ('less_eq$'('subformulas_mu$'(X0_'A_ltln'),'subfrmlsn$'(X0_'A_ltln'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_490])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4616,plain,![X0_'A_ltln':'A_ltln$',X1_'A_ltln':'A_ltln$']:
% 99.99/15.35 (~'member$'(X0_'A_ltln','subfrmlsn$'(X1_'A_ltln'))|'less_eq$'('subformulas_mu$'(X0_'A_ltln'),'subformulas_mu$'(X1_'A_ltln'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_489])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4618,plain,![X0_'A_ltln':'A_ltln$',X1_'A_ltln':'A_ltln$']:
% 99.99/15.35 (~'member$'(X0_'A_ltln','subfrmlsn$'(X1_'A_ltln'))|'less_eq$'('subformulas_nu$'(X0_'A_ltln'),'subformulas_nu$'(X1_'A_ltln'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_487])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4686,plain,![X0_'A_ltln_set':'A_ltln_set$',X0_'A_ltln':'A_ltln$',X1_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|'less_eq$'(X0_'A_ltln_set','fun_app$a'('insert$'(X0_'A_ltln'),X1_'A_ltln_set'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_355])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4729,plain,![X0_'A_ltln_set':'A_ltln_set$',X1_'A_ltln_set':'A_ltln_set$',X2_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|'less_eq$'(X0_'A_ltln_set','fun_app$a'('fun_app$b'('sup$',X1_'A_ltln_set'),X2_'A_ltln_set'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_340])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4733,plain,![X0_'A_ltln_set':'A_ltln_set$',X1_'A_ltln_set':'A_ltln_set$',X2_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|'less_eq$'(X0_'A_ltln_set','fun_app$a'('fun_app$b'('sup$',X2_'A_ltln_set'),X1_'A_ltln_set'))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_338])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4778,plain,![X0_'A_ltln_set':'A_ltln_set$',X0_'A_ltln':'A_ltln$',X1_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'(X0_'A_ltln_set',X1_'A_ltln_set')|~'member$'(X0_'A_ltln',X0_'A_ltln_set')|
% 99.99/15.35 'member$'(X0_'A_ltln',X1_'A_ltln_set')),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_192])).
% 99.99/15.35
% 99.99/15.35 tcf(c_4854,negated_conjecture,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))),
% 99.99/15.35 inference(subtyping,[status(esa)],[c_51])).
% 99.99/15.35
% 99.99/15.35 tcf(c_5841,plain,![X0_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'('subformulas_mu$'('chi_1$'),X0_'A_ltln_set')|~'member$'('psi$','subformulas_mu$'('chi_1$'))|
% 99.99/15.35 'member$'('psi$',X0_'A_ltln_set')),
% 99.99/15.35 inference(instantiation,[status(thm)],[c_4778])).
% 99.99/15.35
% 99.99/15.35 tcf(c_8708,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('insert$'('strongRelease_ltln$'('chi_1$','chi_2$')),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_4686,c_4854])).
% 99.99/15.35
% 99.99/15.35 tcf(c_8756,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_8708,c_4686])).
% 99.99/15.35
% 99.99/15.35 tcf(c_11955,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$'))),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$'))))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_4733,c_8756])).
% 99.99/15.35
% 99.99/15.35 tcf(c_12035,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$')))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','subformulas_mu$'('chi_1$')),'subformulas_mu$'('chi_2$')))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_11955,c_4729])).
% 99.99/15.35
% 99.99/15.35 tcf(c_12166,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$')))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'subformulas_mu$'('chi_2$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_12035,c_4733])).
% 99.99/15.35
% 99.99/15.35 tcf(c_12167,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'fun_app$a'('fun_app$b'('sup$','subformulas_nu$'('chi_1$')),'subformulas_nu$'('chi_2$')))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'subformulas_mu$'('chi_1$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_12035,c_4729])).
% 99.99/15.35
% 99.99/15.35 tcf(c_12758,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'subformulas_nu$'('chi_2$'))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'subformulas_mu$'('chi_2$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_12166,c_4733])).
% 99.99/15.35
% 99.99/15.35 tcf(c_12803,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'subformulas_nu$'('chi_1$'))|
% 99.99/15.35 ~'less_eq$'('subformulas_mu$'('psi$'),'subformulas_mu$'('chi_1$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_12167,c_4729])).
% 99.99/15.35
% 99.99/15.35 tcf(c_13181,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'subformulas_nu$'('chi_2$'))|
% 99.99/15.35 ~'member$'('psi$','subfrmlsn$'('chi_2$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_12758,c_4616])).
% 99.99/15.35
% 99.99/15.35 tcf(c_13298,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_nu$'('psi$'),'subformulas_nu$'('chi_1$'))|
% 99.99/15.35 ~'member$'('psi$','subfrmlsn$'('chi_1$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_12803,c_4616])).
% 99.99/15.35
% 99.99/15.35 tcf(c_13551,plain,
% 99.99/15.35 (~'member$'('psi$','subfrmlsn$'('chi_2$'))),
% 99.99/15.35 inference(forward_subsumption_resolution,[status(thm)],[c_13181,c_4618])).
% 99.99/15.35
% 99.99/15.35 tcf(c_13578,plain,
% 99.99/15.35 (~'member$'('psi$','subfrmlsn$'('chi_1$'))),
% 99.99/15.35 inference(forward_subsumption_resolution,[status(thm)],[c_13298,c_4618])).
% 99.99/15.35
% 99.99/15.35 tcf(c_13750,plain,
% 99.99/15.35 (~'less_eq$'('subformulas_mu$'('chi_1$'),'subfrmlsn$'('chi_1$'))|
% 99.99/15.35 ~'member$'('psi$','subformulas_mu$'('chi_1$'))|'member$'('psi$','subfrmlsn$'('chi_1$'))),
% 99.99/15.35 inference(instantiation,[status(thm)],[c_5841])).
% 99.99/15.35
% 99.99/15.35 tcf(c_13751,plain,
% 99.99/15.35 ('less_eq$'('subformulas_mu$'('chi_1$'),'subfrmlsn$'('chi_1$'))),
% 99.99/15.35 inference(instantiation,[status(thm)],[c_4615])).
% 99.99/15.35
% 99.99/15.35 tcf(c_14283,plain,![X0_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'('subformulas_mu$'('chi_2$'),X0_'A_ltln_set')|'member$'('psi$','subformulas_mu$'('chi_1$'))|
% 99.99/15.35 'member$'('psi$',X0_'A_ltln_set')),
% 99.99/15.35 inference(resolution,[status(thm)],[c_4778,c_3499])).
% 99.99/15.35
% 99.99/15.35 tcf(c_37933,plain,![X0_'A_ltln_set':'A_ltln_set$']:
% 99.99/15.35 (~'less_eq$'('subformulas_mu$'('chi_2$'),X0_'A_ltln_set')|'member$'('psi$',X0_'A_ltln_set')),
% 99.99/15.35 inference(global_subsumption_just,
% 99.99/15.35 [status(thm)],
% 99.99/15.35 [c_14283,c_13578,c_13750,c_13751,c_14283])).
% 99.99/15.35
% 99.99/15.35 tcf(c_37980,plain,
% 99.99/15.35 ('member$'('psi$','subfrmlsn$'('chi_2$'))),
% 99.99/15.35 inference(resolution,[status(thm)],[c_37933,c_4615])).
% 99.99/15.35
% 99.99/15.35 tcf(c_37981,plain,
% 99.99/15.35 ($false),
% 99.99/15.35 inference(prop_impl_just,[status(thm)],[c_37980,c_13551])).
% 99.99/15.35
% 99.99/15.35
% 99.99/15.35 % SZS output end CNFRefutation for theBenchmark.p
% 99.99/15.35
% 99.99/15.35
%------------------------------------------------------------------------------