%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : LCL649+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n029.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 11:25:26 AM UTC 2026 % Result : CounterSatisfiable 207.90s 210.12s % Output : Model 199.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL649+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.36 % Computer : n029.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 5 23:13:55 UTC 2026 % 0.11/0.37 % CPUTime : % 0.95/1.20 %----Disproving FOF, CNF % 207.90/210.12 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 12... % 207.90/210.12 --- Run --no-e-matching --full-saturate-quant at 12... % 207.90/210.12 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 12... % 207.90/210.12 --- Run --finite-model-find --uf-ss=no-minimal at 54... % 207.90/210.12 --- Run --multi-trigger-when-single --full-saturate-quant at 12... % 207.90/210.12 --- Run --trigger-sel=max --full-saturate-quant at 12... % 207.90/210.12 --- Run --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant at 12... % 207.90/210.12 --- Run --multi-trigger-cache --full-saturate-quant at 12... % 207.90/210.12 --- Run --prenex-quant=none --full-saturate-quant at 12... % 207.90/210.12 --- Run --enum-inst-interleave --decision=internal --full-saturate-quant at 12... % 207.90/210.12 --- Run --relevant-triggers --full-saturate-quant at 12... % 207.90/210.12 --- Run --finite-model-find --e-matching --sort-inference --uf-ss-fair at 66... % 207.90/210.12 --- Run --pre-skolem-quant=on --full-saturate-quant at 12... % 207.90/210.12 --- Run --macros-quant --macros-quant-mode=all --full-saturate-quant at 12... % 207.90/210.12 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 36... % 207.90/210.12 % SZS status CounterSatisfiable % 207.90/210.12 % SZS output start Model % 207.90/210.12 ( % 207.90/210.12 ; cardinality of $$unsorted is 192 % 207.90/210.12 ; rep: (as @$$unsorted_0 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_1 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_2 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_3 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_4 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_5 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_6 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_7 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_8 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_9 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_10 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_11 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_12 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_13 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_14 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_15 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_16 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_17 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_18 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_19 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_20 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_21 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_22 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_23 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_24 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_25 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_26 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_27 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_28 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_29 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_30 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_31 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_32 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_33 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_34 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_35 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_36 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_37 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_38 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_39 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_40 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_41 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_42 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_43 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_44 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_45 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_46 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_47 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_48 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_49 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_50 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_51 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_52 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_53 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_54 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_55 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_56 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_57 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_58 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_59 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_60 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_61 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_62 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_63 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_64 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_65 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_66 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_67 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_68 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_69 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_70 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_71 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_72 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_73 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_74 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_75 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_76 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_77 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_78 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_79 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_80 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_81 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_82 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_83 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_84 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_85 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_86 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_87 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_88 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_89 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_90 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_91 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_92 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_93 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_94 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_95 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_96 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_97 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_98 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_99 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_100 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_101 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_102 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_103 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_104 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_105 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_106 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_107 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_108 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_109 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_110 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_111 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_112 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_113 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_114 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_115 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_116 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_117 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_118 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_119 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_120 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_121 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_122 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_123 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_124 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_125 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_126 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_127 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_128 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_129 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_130 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_131 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_132 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_133 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_134 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_135 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_136 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_137 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_138 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_139 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_140 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_141 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_142 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_143 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_144 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_145 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_146 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_147 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_148 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_149 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_150 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_151 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_152 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_153 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_154 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_155 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_156 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_157 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_158 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_159 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_160 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_161 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_162 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_163 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_164 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_165 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_166 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_167 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_168 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_169 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_170 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_171 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_172 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_173 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_174 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_175 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_176 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_177 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_178 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_179 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_180 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_181 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_182 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_183 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_184 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_185 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_186 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_187 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_188 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_189 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_190 $$unsorted) % 207.90/210.12 ; rep: (as @$$unsorted_191 $$unsorted) % 207.90/210.12 (define-fun tptp.r1 ((_arg_1 $$unsorted) (_arg_2 $$unsorted)) Bool true) % 207.90/210.12 (define-fun tptp.p2120 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.12 (define-fun tptp.p2020 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1920 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1820 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1720 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1620 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1520 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1420 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1320 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1220 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1120 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1020 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p920 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p820 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p720 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p620 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p520 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p420 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p320 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p220 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p120 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p2119 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p2019 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.12 (define-fun tptp.p1919 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1819 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1719 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1619 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1519 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1419 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1319 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1219 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1119 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1019 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p919 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p819 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p719 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p619 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p519 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p419 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p319 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p219 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p119 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p2118 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p2018 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1918 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.12 (define-fun tptp.p1818 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1718 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1618 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1518 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1418 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1318 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1218 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1118 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1018 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p918 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p818 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p718 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p618 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p518 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p418 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p318 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p218 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p118 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p2117 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p2017 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1917 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1817 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.12 (define-fun tptp.p1717 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1617 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1517 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1417 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1317 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1217 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1117 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p1017 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p917 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p817 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p717 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p617 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p517 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p417 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p317 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.12 (define-fun tptp.p217 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p117 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2116 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2016 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1916 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1816 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1716 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1616 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1516 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1416 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1316 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1216 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1116 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1016 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p916 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p816 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p716 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p616 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p516 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p416 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p316 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p216 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p116 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2115 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2015 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1915 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1815 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1715 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1615 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1515 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1415 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1315 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1215 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1115 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1015 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p915 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p815 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p715 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p615 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p515 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p415 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p315 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p215 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p115 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2114 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2014 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1914 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1814 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1714 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1614 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1514 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1414 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1314 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1214 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1114 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1014 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p914 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p814 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p714 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p614 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p514 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p414 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p314 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p214 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p114 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2113 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2013 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1913 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1813 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1713 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1613 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1513 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1413 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1313 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1213 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1113 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1013 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p913 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p813 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p713 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p613 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p513 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p413 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p313 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p213 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p113 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2112 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2012 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1912 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1812 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1712 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1612 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1512 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1412 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1312 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1212 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1112 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1012 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p912 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p812 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p712 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p612 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p512 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p412 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p312 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p212 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p112 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2111 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2011 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1911 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1811 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1711 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1611 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1511 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1411 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1311 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1211 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1111 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p1011 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p911 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p811 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p711 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p611 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p511 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p411 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p311 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p211 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p111 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2110 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2010 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1910 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1810 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1710 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1610 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1510 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1410 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1310 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1210 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1110 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1010 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p910 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p810 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p710 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p610 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p510 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p410 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p310 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p210 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p110 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2109 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2009 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1909 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1809 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1709 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1609 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1509 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1409 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1309 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1209 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1109 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1009 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p909 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p809 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p709 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p609 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p509 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p409 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p309 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p209 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p109 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2108 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2008 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1908 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1808 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1708 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1608 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1508 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1408 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1308 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1208 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1108 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1008 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p908 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p808 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p708 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p608 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p508 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p408 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p308 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p208 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p108 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2107 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2007 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1907 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1807 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1707 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1607 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1507 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1407 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1307 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1207 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1107 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1007 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p907 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p807 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p707 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p607 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p507 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p407 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p307 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p207 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p107 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2106 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2006 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1906 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1806 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1706 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1606 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1506 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1406 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1306 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1206 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1106 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1006 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p906 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p806 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p706 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p606 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p506 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p406 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p306 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p206 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p106 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2105 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2005 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1905 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1805 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1705 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1605 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1505 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1405 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1305 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1205 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1105 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1005 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p905 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p805 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p705 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p605 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p505 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p405 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p305 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p205 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p105 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2104 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p2004 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1904 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1804 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1704 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1604 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1504 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1404 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1304 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1204 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1104 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p1004 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p904 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p804 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p704 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p604 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p504 ((_arg_1 $$unsorted)) Bool false) % 207.90/210.13 (define-fun tptp.p404 ((_arg_1 $$unsorted)) Bool true) % 207.90/210.13 (define-fun tptp.p304 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p204 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p104 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p2103 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p2003 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1903 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1803 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1703 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1603 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1503 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1403 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1303 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1203 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1103 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1003 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p903 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p803 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p703 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p603 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p503 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p403 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p303 ((_arg_1 $$unsorted)) Bool true) % 199.94/210.13 (define-fun tptp.p203 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p103 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p2102 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p2002 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1902 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1802 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1702 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1602 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1502 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1402 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1302 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1202 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1102 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1002 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p902 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p802 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p702 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p602 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p502 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p402 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p302 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p202 ((_arg_1 $$unsorted)) Bool true) % 199.94/210.13 (define-fun tptp.p102 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p2101 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p2001 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1901 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1801 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1701 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1601 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1501 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1401 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1301 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.13 (define-fun tptp.p1201 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p1101 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p1001 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p901 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p801 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p701 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p601 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p501 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p401 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p301 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p201 ((_arg_1 $$unsorted)) Bool false) % 199.94/210.14 (define-fun tptp.p101 ((_arg_1 $$unsorted)) Bool true) % 199.94/210.14 ) % 199.94/210.14 % SZS output end Model % 199.94/210.14 % cvc5 exiting %------------------------------------------------------------------------------