%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN519+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Thu Jul 21 03:51:01 EDT 2022 % Result : CounterSatisfiable 1.36s 1.56s % Output : Model 1.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN519+1 : TPTP v8.1.0. Released v2.1.0. % 0.11/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.33 % Computer : n003.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Tue Jul 12 01:41:30 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 Defaulting to tptp format. % 1.36/1.56 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.36/1.56 % 1.36/1.56 MODEL (CONTEXT): % 1.36/1.56 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.36/1.56 -__-v__(=0) % 1.36/1.56 -__con207 % 1.36/1.56 +__con208 % 1.36/1.56 -__con209 % 1.36/1.56 -__con210 % 1.36/1.56 -__con211 % 1.36/1.56 -__con212 % 1.36/1.56 -__con213 % 1.36/1.56 -__con214 % 1.36/1.56 -__con216 % 1.36/1.56 -__con217 % 1.36/1.56 +__con218 % 1.36/1.56 +__con219 % 1.36/1.56 -__con220 % 1.36/1.56 +__con221 % 1.36/1.56 +__con222 % 1.36/1.56 +__con223 % 1.36/1.56 -__con224 % 1.36/1.56 -__con225 % 1.36/1.56 +__con226 % 1.36/1.56 +__con227 % 1.36/1.56 +__con228 % 1.36/1.56 +__con229 % 1.36/1.56 +__con230 % 1.36/1.56 +__con231 % 1.36/1.56 +__con232 % 1.36/1.56 +__con233 % 1.36/1.56 +__con235 % 1.36/1.56 +__con239 % 1.36/1.56 -__con240 % 1.36/1.56 +__con243 % 1.36/1.56 +__con244 % 1.36/1.56 -__con245 % 1.36/1.56 +__con246 % 1.36/1.56 -__con248 % 1.36/1.56 -__con249 % 1.36/1.56 -__con251 % 1.36/1.56 -__con252 % 1.36/1.56 +__con253 % 1.36/1.56 +__con254 % 1.36/1.56 +__con255 % 1.36/1.56 +__con256 % 1.36/1.56 +__con257 % 1.36/1.56 -__con258 % 1.36/1.56 -__con259 % 1.36/1.56 +__con260 % 1.36/1.56 +__con261 % 1.36/1.56 +__con262 % 1.36/1.56 +__con263 % 1.36/1.56 -__con265 % 1.36/1.56 -__con266 % 1.36/1.56 -__con267 % 1.36/1.56 +__con268 % 1.36/1.56 +__con269 % 1.36/1.56 +__con270 % 1.36/1.56 +__con271 % 1.36/1.56 -__con272 % 1.36/1.56 +__con273 % 1.36/1.56 +__con278 % 1.36/1.56 +__con279 % 1.36/1.56 +__con281 % 1.36/1.56 -__con282 % 1.36/1.56 +__con283 % 1.36/1.56 +__con284 % 1.36/1.56 -__con285 % 1.36/1.56 -__con286 % 1.36/1.56 +__con287 % 1.36/1.56 +__con288 % 1.36/1.56 -__con289 % 1.36/1.56 -__con290 % 1.36/1.56 -__con291 % 1.36/1.56 -__con292 % 1.36/1.56 -__con293 % 1.36/1.56 +__con295 % 1.36/1.56 -__con296 % 1.36/1.56 +__con297 % 1.36/1.56 +__con298 % 1.36/1.56 +__con299 % 1.36/1.56 -__con300 % 1.36/1.56 +__con301 % 1.36/1.56 +__con302 % 1.36/1.56 +__con303 % 1.36/1.56 -__con304 % 1.36/1.56 -__con305 % 1.36/1.56 -__con306 % 1.36/1.56 +__con307 % 1.36/1.56 -__con311 % 1.36/1.56 +__con312 % 1.36/1.56 -__con313 % 1.36/1.56 +__con314 % 1.36/1.56 +__con315 % 1.36/1.56 -__con317 % 1.36/1.56 -__con318 % 1.36/1.56 +__con319 % 1.36/1.56 +__con322 % 1.36/1.56 +__con323 % 1.36/1.56 +__con324 % 1.36/1.56 +__con325 % 1.36/1.56 -__con326 % 1.36/1.56 +__con327 % 1.36/1.56 +__con328 % 1.36/1.56 -__con329 % 1.36/1.56 -__con330 % 1.36/1.56 +__con331 % 1.36/1.56 +__con332 % 1.36/1.56 -__con333 % 1.36/1.56 +__con334 % 1.36/1.56 +__con335 % 1.36/1.56 +__con336 % 1.36/1.56 +__con337 % 1.36/1.56 +__con338 % 1.36/1.56 +__con339 % 1.36/1.56 +__con340 % 1.36/1.56 +__con341 % 1.36/1.56 -__con342 % 1.36/1.56 +__con343 % 1.36/1.56 +__con345 % 1.36/1.56 +__con346 % 1.36/1.56 +__con347 % 1.36/1.56 +__con348 % 1.36/1.56 +c0_1(_0) % 1.36/1.56 +c1_0 % 1.36/1.56 +c1_1(=0) % 1.36/1.56 +c1_1(a27) % 1.36/1.56 +c1_1(a34) % 1.36/1.56 +c1_1(a43) % 1.36/1.56 +c1_1(a46) % 1.36/1.56 +c1_1(a58) % 1.36/1.56 +c1_1(a66) % 1.36/1.56 +c1_1(a71) % 1.36/1.56 +c1_1(a85) % 1.36/1.56 +c1_1(a86) % 1.36/1.56 +c1_1(a91) % 1.36/1.56 +c1_1(a96) % 1.36/1.56 +c1_1(a102) % 1.36/1.56 +c1_1(a103) % 1.36/1.56 +c1_1(a109) % 1.36/1.56 +c1_1(a110) % 1.36/1.56 +c1_1(a123) % 1.36/1.56 +c1_1(a127) % 1.36/1.56 +c1_1(a128) % 1.36/1.56 +c1_1(a146) % 1.36/1.56 +c1_1(a153) % 1.36/1.56 +c1_1(a154) % 1.36/1.56 +c1_1(a158) % 1.36/1.56 +c1_1(a159) % 1.36/1.56 +c1_1(a172) % 1.36/1.56 +c1_1(a173) % 1.36/1.56 -c1_1(a29) % 1.36/1.56 -c1_1(a33) % 1.36/1.56 -c1_1(a38) % 1.36/1.56 -c1_1(a41) % 1.36/1.56 -c1_1(a47) % 1.36/1.56 -c1_1(a48) % 1.36/1.56 -c1_1(a70) % 1.36/1.56 -c1_1(a72) % 1.36/1.56 -c1_1(a74) % 1.36/1.56 -c1_1(a83) % 1.36/1.56 -c1_1(a87) % 1.36/1.56 -c1_1(a90) % 1.36/1.56 -c1_1(a99) % 1.36/1.56 -c1_1(a107) % 1.36/1.56 -c1_1(a122) % 1.36/1.56 -c1_1(a140) % 1.36/1.56 -c1_1(a145) % 1.36/1.56 -c1_1(a156) % 1.36/1.56 -c1_1(a160) % 1.36/1.56 -c1_1(a164) % 1.36/1.56 -c1_1(a167) % 1.36/1.56 +c1_2(=0, a68) % 1.36/1.56 +c1_2(=0, a100) % 1.36/1.56 +c1_2(=0, a136) % 1.36/1.56 +c1_2(a27, a31) % 1.36/1.56 +c1_2(a27, a45) % 1.36/1.56 +c1_2(a27, a65) % 1.36/1.56 +c1_2(a27, a68) % 1.36/1.56 +c1_2(a27, a81) % 1.36/1.56 +c1_2(a27, a100) % 1.36/1.56 +c1_2(a27, a101) % 1.36/1.56 +c1_2(a27, a134) % 1.36/1.56 +c1_2(a27, a136) % 1.36/1.56 +c1_2(a27, a141) % 1.36/1.56 +c1_2(a29, a65) % 1.36/1.56 +c1_2(a29, a68) % 1.36/1.56 +c1_2(a29, a100) % 1.36/1.56 +c1_2(a33, a65) % 1.36/1.56 +c1_2(a33, a68) % 1.36/1.56 +c1_2(a33, a78) % 1.36/1.56 +c1_2(a33, a100) % 1.36/1.56 +c1_2(a33, a138) % 1.36/1.56 +c1_2(a34, a31) % 1.36/1.56 +c1_2(a34, a45) % 1.36/1.56 +c1_2(a34, a65) % 1.36/1.56 +c1_2(a34, a68) % 1.36/1.56 +c1_2(a34, a81) % 1.36/1.56 +c1_2(a34, a100) % 1.36/1.56 +c1_2(a34, a101) % 1.36/1.56 +c1_2(a34, a134) % 1.36/1.56 +c1_2(a34, a136) % 1.36/1.56 +c1_2(a34, a141) % 1.36/1.56 +c1_2(a38, a65) % 1.36/1.56 +c1_2(a38, a68) % 1.36/1.56 +c1_2(a38, a100) % 1.36/1.56 +c1_2(a41, a65) % 1.36/1.56 +c1_2(a41, a68) % 1.36/1.56 +c1_2(a41, a100) % 1.36/1.56 +c1_2(a43, a65) % 1.36/1.56 +c1_2(a43, a68) % 1.36/1.56 +c1_2(a43, a78) % 1.36/1.56 +c1_2(a43, a100) % 1.36/1.56 +c1_2(a43, a136) % 1.36/1.56 +c1_2(a43, a138) % 1.36/1.56 +c1_2(a46, a65) % 1.36/1.56 +c1_2(a46, a68) % 1.36/1.56 +c1_2(a46, a78) % 1.36/1.56 +c1_2(a46, a100) % 1.36/1.56 +c1_2(a46, a136) % 1.36/1.56 +c1_2(a46, a138) % 1.36/1.56 +c1_2(a46, a141) % 1.36/1.56 +c1_2(a47, =0) % 1.36/1.56 +c1_2(a47, a65) % 1.36/1.56 +c1_2(a47, a78) % 1.36/1.56 +c1_2(a47, a100) % 1.36/1.56 +c1_2(a47, a138) % 1.36/1.56 +c1_2(a48, a28) % 1.36/1.56 +c1_2(a48, a32) % 1.36/1.56 +c1_2(a48, a44) % 1.36/1.56 +c1_2(a48, a68) % 1.36/1.56 +c1_2(a48, a82) % 1.36/1.56 +c1_2(a48, a137) % 1.36/1.56 +c1_2(a58, a65) % 1.36/1.56 +c1_2(a58, a68) % 1.36/1.56 +c1_2(a58, a78) % 1.36/1.56 +c1_2(a58, a100) % 1.36/1.56 +c1_2(a58, a136) % 1.36/1.56 +c1_2(a58, a138) % 1.36/1.56 +c1_2(a61, a28) % 1.36/1.56 +c1_2(a61, a62) % 1.36/1.56 +c1_2(a61, a63) % 1.36/1.56 +c1_2(a61, a115) % 1.36/1.56 +c1_2(a66, a65) % 1.36/1.56 +c1_2(a66, a67) % 1.36/1.56 +c1_2(a66, a68) % 1.36/1.56 +c1_2(a66, a78) % 1.36/1.56 +c1_2(a66, a100) % 1.36/1.56 +c1_2(a66, a136) % 1.36/1.56 +c1_2(a66, a138) % 1.36/1.56 +c1_2(a70, a65) % 1.36/1.56 +c1_2(a70, a68) % 1.36/1.56 +c1_2(a70, a100) % 1.36/1.56 +c1_2(a71, a65) % 1.36/1.56 +c1_2(a71, a68) % 1.36/1.56 +c1_2(a71, a78) % 1.36/1.56 +c1_2(a71, a100) % 1.36/1.56 +c1_2(a71, a136) % 1.36/1.56 +c1_2(a71, a138) % 1.36/1.56 +c1_2(a72, a28) % 1.36/1.56 +c1_2(a72, a31) % 1.36/1.56 +c1_2(a72, a73) % 1.36/1.56 +c1_2(a72, a77) % 1.36/1.56 +c1_2(a72, a78) % 1.36/1.56 +c1_2(a72, a81) % 1.36/1.56 +c1_2(a72, a101) % 1.36/1.56 +c1_2(a72, a115) % 1.36/1.56 +c1_2(a72, a134) % 1.36/1.56 +c1_2(a72, a138) % 1.36/1.56 +c1_2(a74, a65) % 1.36/1.56 +c1_2(a74, a68) % 1.36/1.56 +c1_2(a74, a75) % 1.36/1.56 +c1_2(a74, a100) % 1.36/1.56 +c1_2(a83, a65) % 1.36/1.56 +c1_2(a83, a68) % 1.36/1.56 +c1_2(a83, a78) % 1.36/1.56 +c1_2(a83, a84) % 1.36/1.56 +c1_2(a83, a100) % 1.36/1.56 +c1_2(a83, a138) % 1.36/1.56 +c1_2(a85, a65) % 1.36/1.56 +c1_2(a85, a68) % 1.36/1.56 +c1_2(a85, a78) % 1.36/1.56 +c1_2(a85, a100) % 1.36/1.56 +c1_2(a85, a136) % 1.36/1.56 +c1_2(a85, a138) % 1.36/1.56 +c1_2(a86, a65) % 1.36/1.56 +c1_2(a86, a68) % 1.36/1.56 +c1_2(a86, a78) % 1.36/1.56 +c1_2(a86, a100) % 1.36/1.56 +c1_2(a86, a136) % 1.36/1.56 +c1_2(a86, a138) % 1.36/1.56 +c1_2(a87, a45) % 1.36/1.56 +c1_2(a87, a78) % 1.36/1.56 +c1_2(a87, a88) % 1.36/1.56 +c1_2(a87, a100) % 1.36/1.56 +c1_2(a87, a115) % 1.36/1.56 +c1_2(a87, a124) % 1.36/1.56 +c1_2(a87, a138) % 1.36/1.56 +c1_2(a90, a28) % 1.36/1.56 +c1_2(a90, a31) % 1.36/1.56 +c1_2(a90, a44) % 1.36/1.56 +c1_2(a90, a78) % 1.36/1.56 +c1_2(a90, a81) % 1.36/1.56 +c1_2(a90, a101) % 1.36/1.56 +c1_2(a90, a115) % 1.36/1.56 +c1_2(a90, a134) % 1.36/1.56 +c1_2(a90, a138) % 1.36/1.56 +c1_2(a91, a28) % 1.36/1.56 +c1_2(a91, a44) % 1.36/1.56 +c1_2(a91, a68) % 1.36/1.56 +c1_2(a91, a136) % 1.36/1.56 +c1_2(a93, a28) % 1.36/1.56 +c1_2(a93, a115) % 1.36/1.56 +c1_2(a94, a65) % 1.36/1.56 +c1_2(a94, a68) % 1.36/1.56 +c1_2(a94, a100) % 1.36/1.56 +c1_2(a96, a28) % 1.36/1.56 +c1_2(a96, a31) % 1.36/1.56 +c1_2(a96, a77) % 1.36/1.56 +c1_2(a96, a78) % 1.36/1.56 +c1_2(a96, a81) % 1.36/1.56 +c1_2(a96, a101) % 1.36/1.56 +c1_2(a96, a115) % 1.36/1.56 +c1_2(a96, a134) % 1.36/1.56 +c1_2(a96, a136) % 1.36/1.56 +c1_2(a96, a138) % 1.36/1.56 +c1_2(a99, a65) % 1.36/1.56 +c1_2(a99, a68) % 1.36/1.56 +c1_2(a99, a100) % 1.36/1.56 +c1_2(a102, a65) % 1.36/1.56 +c1_2(a102, a68) % 1.36/1.56 +c1_2(a102, a78) % 1.36/1.56 +c1_2(a102, a100) % 1.36/1.56 +c1_2(a102, a136) % 1.36/1.56 +c1_2(a102, a138) % 1.36/1.56 +c1_2(a103, a65) % 1.36/1.56 +c1_2(a103, a68) % 1.36/1.56 +c1_2(a103, a78) % 1.36/1.56 +c1_2(a103, a100) % 1.36/1.56 +c1_2(a103, a136) % 1.36/1.56 +c1_2(a103, a138) % 1.36/1.56 +c1_2(a107, =0) % 1.36/1.56 +c1_2(a109, a65) % 1.36/1.56 +c1_2(a109, a68) % 1.36/1.56 +c1_2(a109, a78) % 1.36/1.56 +c1_2(a109, a100) % 1.36/1.56 +c1_2(a109, a136) % 1.36/1.56 +c1_2(a109, a138) % 1.36/1.56 +c1_2(a110, a56) % 1.36/1.56 +c1_2(a110, a65) % 1.36/1.56 +c1_2(a110, a100) % 1.36/1.56 +c1_2(a110, a115) % 1.36/1.56 +c1_2(a110, a136) % 1.36/1.56 +c1_2(a114, a28) % 1.36/1.56 +c1_2(a114, a115) % 1.36/1.56 +c1_2(a122, a65) % 1.36/1.56 +c1_2(a122, a68) % 1.36/1.56 +c1_2(a122, a100) % 1.36/1.56 +c1_2(a123, a65) % 1.36/1.56 +c1_2(a123, a68) % 1.36/1.56 +c1_2(a123, a78) % 1.36/1.56 +c1_2(a123, a100) % 1.36/1.56 +c1_2(a123, a136) % 1.36/1.56 +c1_2(a123, a138) % 1.36/1.56 +c1_2(a125, a65) % 1.36/1.56 +c1_2(a125, a68) % 1.36/1.56 +c1_2(a125, a100) % 1.36/1.56 +c1_2(a127, a65) % 1.36/1.56 +c1_2(a127, a68) % 1.36/1.56 +c1_2(a127, a78) % 1.36/1.56 +c1_2(a127, a100) % 1.36/1.56 +c1_2(a127, a136) % 1.36/1.56 +c1_2(a127, a138) % 1.36/1.56 +c1_2(a128, a65) % 1.36/1.56 +c1_2(a128, a78) % 1.36/1.56 +c1_2(a128, a100) % 1.36/1.56 +c1_2(a128, a136) % 1.36/1.56 +c1_2(a128, a138) % 1.36/1.56 +c1_2(a131, a44) % 1.36/1.56 +c1_2(a135, a28) % 1.36/1.56 +c1_2(a135, a115) % 1.36/1.56 +c1_2(a140, a28) % 1.36/1.56 +c1_2(a140, a31) % 1.36/1.56 +c1_2(a140, a78) % 1.36/1.56 +c1_2(a140, a81) % 1.36/1.56 +c1_2(a140, a101) % 1.36/1.56 +c1_2(a140, a115) % 1.36/1.56 +c1_2(a140, a134) % 1.36/1.56 +c1_2(a140, a138) % 1.36/1.56 +c1_2(a145, a65) % 1.36/1.56 +c1_2(a145, a68) % 1.36/1.56 +c1_2(a145, a78) % 1.36/1.56 +c1_2(a145, a100) % 1.36/1.56 +c1_2(a145, a138) % 1.36/1.56 +c1_2(a146, a65) % 1.36/1.56 +c1_2(a146, a68) % 1.36/1.56 +c1_2(a146, a78) % 1.36/1.56 +c1_2(a146, a100) % 1.36/1.56 +c1_2(a146, a136) % 1.36/1.56 +c1_2(a146, a138) % 1.36/1.56 +c1_2(a153, a65) % 1.36/1.56 +c1_2(a153, a68) % 1.36/1.56 +c1_2(a153, a78) % 1.36/1.56 +c1_2(a153, a100) % 1.36/1.56 +c1_2(a153, a136) % 1.36/1.56 +c1_2(a153, a138) % 1.36/1.56 +c1_2(a154, a65) % 1.36/1.56 +c1_2(a154, a68) % 1.36/1.56 +c1_2(a154, a78) % 1.36/1.56 +c1_2(a154, a100) % 1.36/1.56 +c1_2(a154, a136) % 1.36/1.56 +c1_2(a154, a138) % 1.36/1.56 +c1_2(a156, a65) % 1.36/1.56 +c1_2(a156, a68) % 1.36/1.56 +c1_2(a156, a100) % 1.36/1.56 +c1_2(a158, a65) % 1.36/1.56 +c1_2(a158, a68) % 1.36/1.56 +c1_2(a158, a78) % 1.36/1.56 +c1_2(a158, a100) % 1.36/1.56 +c1_2(a158, a136) % 1.36/1.56 +c1_2(a158, a138) % 1.36/1.56 +c1_2(a159, a65) % 1.36/1.56 +c1_2(a159, a68) % 1.36/1.56 +c1_2(a159, a78) % 1.36/1.56 +c1_2(a159, a100) % 1.36/1.56 +c1_2(a159, a136) % 1.36/1.56 +c1_2(a159, a138) % 1.36/1.56 +c1_2(a160, a65) % 1.36/1.56 +c1_2(a160, a68) % 1.36/1.56 +c1_2(a160, a100) % 1.36/1.56 +c1_2(a164, a65) % 1.36/1.56 +c1_2(a164, a68) % 1.36/1.56 +c1_2(a164, a100) % 1.36/1.56 +c1_2(a164, a165) % 1.36/1.56 +c1_2(a167, a65) % 1.36/1.56 +c1_2(a167, a68) % 1.36/1.56 +c1_2(a167, a100) % 1.36/1.56 +c1_2(a172, =0) % 1.36/1.56 +c1_2(a172, a31) % 1.36/1.56 +c1_2(a172, a44) % 1.36/1.56 +c1_2(a172, a65) % 1.36/1.56 +c1_2(a172, a68) % 1.36/1.56 +c1_2(a172, a78) % 1.36/1.56 +c1_2(a172, a81) % 1.36/1.56 +c1_2(a172, a100) % 1.36/1.56 +c1_2(a172, a101) % 1.36/1.56 +c1_2(a172, a138) % 1.36/1.56 +c1_2(a173, a31) % 1.36/1.56 +c1_2(a173, a45) % 1.36/1.56 +c1_2(a173, a65) % 1.36/1.56 +c1_2(a173, a68) % 1.36/1.56 +c1_2(a173, a78) % 1.36/1.56 +c1_2(a173, a81) % 1.36/1.56 +c1_2(a173, a100) % 1.36/1.56 +c1_2(a173, a101) % 1.36/1.56 +c1_2(a173, a134) % 1.36/1.56 +c1_2(a173, a138) % 1.36/1.56 -c1_2(a33, a136) % 1.36/1.56 -c1_2(a34, a35) % 1.36/1.56 -c1_2(a34, a82) % 1.36/1.56 -c1_2(a34, a137) % 1.36/1.56 -c1_2(a47, a82) % 1.36/1.56 -c1_2(a61, a68) % 1.36/1.56 -c1_2(a61, a100) % 1.36/1.56 -c1_2(a61, a136) % 1.36/1.56 -c1_2(a91, a92) % 1.36/1.56 -c1_2(a93, a68) % 1.36/1.56 -c1_2(a93, a100) % 1.36/1.56 -c1_2(a93, a136) % 1.36/1.56 -c1_2(a96, a68) % 1.36/1.56 -c1_2(a96, a100) % 1.36/1.56 -c1_2(a107, a81) % 1.36/1.56 -c1_2(a107, a108) % 1.36/1.56 -c1_2(a114, a68) % 1.36/1.56 -c1_2(a114, a100) % 1.36/1.56 -c1_2(a114, a136) % 1.36/1.56 -c1_2(a135, a68) % 1.36/1.56 -c1_2(a135, a100) % 1.36/1.56 -c1_2(a135, a136) % 1.36/1.56 -c1_2(a140, a82) % 1.36/1.56 -c1_2(a145, a101) % 1.36/1.56 -c1_2(a145, a136) % 1.36/1.56 -c1_2(a172, a82) % 1.36/1.56 -c1_2(a172, a137) % 1.36/1.56 +c2_0 % 1.36/1.56 +c2_1(=0) % 1.36/1.56 +c2_1(a29) % 1.36/1.56 +c2_1(a33) % 1.36/1.56 +c2_1(a38) % 1.36/1.56 +c2_1(a41) % 1.36/1.56 +c2_1(a43) % 1.36/1.56 +c2_1(a46) % 1.36/1.56 +c2_1(a47) % 1.36/1.56 +c2_1(a58) % 1.36/1.56 +c2_1(a66) % 1.36/1.56 +c2_1(a70) % 1.36/1.56 +c2_1(a71) % 1.36/1.56 +c2_1(a72) % 1.36/1.56 +c2_1(a74) % 1.36/1.56 +c2_1(a83) % 1.36/1.56 +c2_1(a85) % 1.36/1.56 +c2_1(a86) % 1.36/1.56 +c2_1(a87) % 1.36/1.56 +c2_1(a90) % 1.36/1.56 +c2_1(a91) % 1.36/1.56 +c2_1(a96) % 1.36/1.56 +c2_1(a99) % 1.36/1.56 +c2_1(a102) % 1.36/1.56 +c2_1(a103) % 1.36/1.56 +c2_1(a107) % 1.36/1.56 +c2_1(a109) % 1.36/1.56 +c2_1(a110) % 1.36/1.56 +c2_1(a122) % 1.36/1.56 +c2_1(a123) % 1.36/1.56 +c2_1(a125) % 1.36/1.56 +c2_1(a127) % 1.36/1.56 +c2_1(a128) % 1.36/1.56 +c2_1(a140) % 1.36/1.56 +c2_1(a145) % 1.36/1.56 +c2_1(a146) % 1.36/1.56 +c2_1(a153) % 1.36/1.56 +c2_1(a154) % 1.36/1.56 +c2_1(a156) % 1.36/1.56 +c2_1(a158) % 1.36/1.56 +c2_1(a159) % 1.36/1.56 +c2_1(a160) % 1.36/1.56 +c2_1(a164) % 1.36/1.56 +c2_1(a167) % 1.36/1.56 -c2_1(a27) % 1.36/1.56 -c2_1(a34) % 1.36/1.56 -c2_1(a61) % 1.36/1.56 -c2_1(a93) % 1.36/1.56 -c2_1(a114) % 1.36/1.56 -c2_1(a135) % 1.36/1.56 -c2_1(a172) % 1.36/1.56 -c2_1(a173) % 1.36/1.56 +c2_2(=0, a31) % 1.36/1.56 +c2_2(=0, a78) % 1.36/1.56 +c2_2(=0, a81) % 1.36/1.56 +c2_2(=0, a101) % 1.36/1.56 +c2_2(=0, a134) % 1.36/1.56 +c2_2(=0, a138) % 1.36/1.56 +c2_2(a27, a45) % 1.36/1.56 +c2_2(a27, a65) % 1.36/1.56 +c2_2(a27, a81) % 1.36/1.56 +c2_2(a27, a101) % 1.36/1.56 +c2_2(a27, a134) % 1.36/1.56 +c2_2(a29, a65) % 1.36/1.56 +c2_2(a29, a78) % 1.36/1.56 +c2_2(a29, a101) % 1.36/1.56 +c2_2(a29, a138) % 1.36/1.56 +c2_2(a33, a65) % 1.36/1.56 +c2_2(a33, a77) % 1.36/1.56 +c2_2(a33, a101) % 1.36/1.56 +c2_2(a34, a35) % 1.36/1.56 +c2_2(a34, a45) % 1.36/1.56 +c2_2(a34, a57) % 1.36/1.56 +c2_2(a34, a65) % 1.36/1.56 +c2_2(a34, a68) % 1.36/1.56 +c2_2(a34, a81) % 1.36/1.56 +c2_2(a34, a100) % 1.36/1.56 +c2_2(a34, a101) % 1.36/1.56 +c2_2(a34, a134) % 1.36/1.56 +c2_2(a34, a136) % 1.36/1.56 +c2_2(a34, a141) % 1.36/1.56 +c2_2(a38, a45) % 1.36/1.56 +c2_2(a38, a65) % 1.36/1.56 +c2_2(a38, a78) % 1.36/1.56 +c2_2(a38, a101) % 1.36/1.56 +c2_2(a38, a138) % 1.36/1.56 +c2_2(a41, a65) % 1.36/1.56 +c2_2(a41, a78) % 1.36/1.56 +c2_2(a41, a101) % 1.36/1.56 +c2_2(a41, a138) % 1.36/1.56 +c2_2(a43, a65) % 1.36/1.56 +c2_2(a43, a77) % 1.36/1.56 +c2_2(a43, a81) % 1.36/1.56 +c2_2(a43, a101) % 1.36/1.56 +c2_2(a43, a134) % 1.36/1.56 +c2_2(a46, a57) % 1.36/1.56 +c2_2(a46, a65) % 1.36/1.56 +c2_2(a46, a77) % 1.36/1.56 +c2_2(a46, a81) % 1.36/1.56 +c2_2(a46, a101) % 1.36/1.56 +c2_2(a46, a134) % 1.36/1.56 +c2_2(a47, a65) % 1.36/1.56 +c2_2(a47, a78) % 1.36/1.56 +c2_2(a47, a101) % 1.36/1.56 +c2_2(a47, a134) % 1.36/1.56 +c2_2(a47, a138) % 1.36/1.56 +c2_2(a58, a65) % 1.36/1.56 +c2_2(a58, a77) % 1.36/1.56 +c2_2(a58, a81) % 1.36/1.56 +c2_2(a58, a101) % 1.36/1.56 +c2_2(a58, a134) % 1.36/1.56 +c2_2(a61, a28) % 1.36/1.56 +c2_2(a61, a45) % 1.36/1.56 +c2_2(a61, a63) % 1.36/1.56 +c2_2(a61, a78) % 1.36/1.56 +c2_2(a61, a115) % 1.36/1.56 +c2_2(a61, a138) % 1.36/1.56 +c2_2(a66, a65) % 1.36/1.56 +c2_2(a66, a77) % 1.36/1.56 +c2_2(a66, a81) % 1.36/1.56 +c2_2(a66, a101) % 1.36/1.56 +c2_2(a66, a134) % 1.36/1.56 +c2_2(a70, a65) % 1.36/1.56 +c2_2(a70, a78) % 1.36/1.56 +c2_2(a70, a101) % 1.36/1.56 +c2_2(a70, a138) % 1.36/1.56 +c2_2(a71, a65) % 1.36/1.56 +c2_2(a71, a77) % 1.36/1.56 +c2_2(a71, a81) % 1.36/1.56 +c2_2(a71, a101) % 1.36/1.56 +c2_2(a71, a134) % 1.36/1.56 +c2_2(a72, a73) % 1.36/1.56 +c2_2(a72, a77) % 1.36/1.56 +c2_2(a72, a115) % 1.36/1.56 +c2_2(a72, a134) % 1.36/1.56 +c2_2(a74, a65) % 1.36/1.56 +c2_2(a74, a76) % 1.36/1.56 +c2_2(a74, a77) % 1.36/1.56 +c2_2(a74, a78) % 1.36/1.56 +c2_2(a74, a101) % 1.36/1.56 +c2_2(a74, a138) % 1.36/1.56 +c2_2(a83, a65) % 1.36/1.56 +c2_2(a83, a77) % 1.36/1.56 +c2_2(a83, a78) % 1.36/1.56 +c2_2(a83, a84) % 1.36/1.56 +c2_2(a83, a101) % 1.36/1.56 +c2_2(a83, a138) % 1.36/1.56 +c2_2(a85, a65) % 1.36/1.56 +c2_2(a85, a77) % 1.36/1.56 +c2_2(a85, a81) % 1.36/1.56 +c2_2(a85, a101) % 1.36/1.56 +c2_2(a85, a134) % 1.36/1.56 +c2_2(a86, a65) % 1.36/1.56 +c2_2(a86, a77) % 1.36/1.56 +c2_2(a86, a81) % 1.36/1.56 +c2_2(a86, a101) % 1.36/1.56 +c2_2(a86, a134) % 1.36/1.56 +c2_2(a87, =0) % 1.36/1.56 +c2_2(a87, a59) % 1.36/1.56 +c2_2(a87, a77) % 1.36/1.56 +c2_2(a87, a88) % 1.36/1.56 +c2_2(a87, a89) % 1.36/1.56 +c2_2(a87, a101) % 1.36/1.56 +c2_2(a87, a113) % 1.36/1.56 +c2_2(a90, a115) % 1.36/1.56 +c2_2(a90, a134) % 1.36/1.56 +c2_2(a93, a28) % 1.36/1.56 +c2_2(a93, a45) % 1.36/1.56 +c2_2(a93, a115) % 1.36/1.56 +c2_2(a94, a65) % 1.36/1.56 +c2_2(a94, a78) % 1.36/1.56 +c2_2(a94, a101) % 1.36/1.56 +c2_2(a94, a138) % 1.36/1.56 +c2_2(a96, a77) % 1.36/1.56 +c2_2(a96, a78) % 1.36/1.56 +c2_2(a96, a81) % 1.36/1.56 +c2_2(a96, a115) % 1.36/1.56 +c2_2(a96, a134) % 1.36/1.56 +c2_2(a96, a138) % 1.36/1.56 +c2_2(a99, a65) % 1.36/1.56 +c2_2(a99, a78) % 1.36/1.56 +c2_2(a99, a101) % 1.36/1.56 +c2_2(a99, a134) % 1.36/1.56 +c2_2(a99, a138) % 1.36/1.56 +c2_2(a102, a65) % 1.36/1.56 +c2_2(a102, a77) % 1.36/1.56 +c2_2(a102, a81) % 1.36/1.56 +c2_2(a102, a101) % 1.36/1.56 +c2_2(a102, a134) % 1.36/1.56 +c2_2(a103, a65) % 1.36/1.56 +c2_2(a103, a77) % 1.36/1.56 +c2_2(a103, a81) % 1.36/1.56 +c2_2(a103, a101) % 1.36/1.56 +c2_2(a103, a134) % 1.36/1.56 +c2_2(a107, a65) % 1.36/1.56 +c2_2(a107, a78) % 1.36/1.56 +c2_2(a107, a81) % 1.36/1.56 +c2_2(a107, a101) % 1.36/1.56 +c2_2(a107, a108) % 1.36/1.56 +c2_2(a107, a134) % 1.36/1.56 +c2_2(a107, a138) % 1.36/1.56 +c2_2(a109, a65) % 1.36/1.56 +c2_2(a109, a77) % 1.36/1.56 +c2_2(a109, a81) % 1.36/1.56 +c2_2(a109, a101) % 1.36/1.56 +c2_2(a109, a134) % 1.36/1.56 +c2_2(a110, a65) % 1.36/1.56 +c2_2(a110, a81) % 1.36/1.56 +c2_2(a110, a101) % 1.36/1.56 +c2_2(a110, a115) % 1.36/1.56 +c2_2(a110, a134) % 1.36/1.56 +c2_2(a114, a28) % 1.36/1.56 +c2_2(a114, a45) % 1.36/1.56 +c2_2(a114, a78) % 1.36/1.56 +c2_2(a114, a115) % 1.36/1.56 +c2_2(a114, a138) % 1.36/1.56 +c2_2(a122, a65) % 1.36/1.56 +c2_2(a122, a78) % 1.36/1.56 +c2_2(a122, a101) % 1.36/1.56 +c2_2(a122, a138) % 1.36/1.56 +c2_2(a123, a65) % 1.36/1.56 +c2_2(a123, a77) % 1.36/1.56 +c2_2(a123, a81) % 1.36/1.56 +c2_2(a123, a101) % 1.36/1.56 +c2_2(a123, a134) % 1.36/1.56 +c2_2(a125, a65) % 1.36/1.56 +c2_2(a125, a78) % 1.36/1.56 +c2_2(a125, a101) % 1.36/1.56 +c2_2(a125, a138) % 1.36/1.56 +c2_2(a127, a65) % 1.36/1.56 +c2_2(a127, a77) % 1.36/1.56 +c2_2(a127, a81) % 1.36/1.56 +c2_2(a127, a101) % 1.36/1.56 +c2_2(a127, a134) % 1.36/1.56 +c2_2(a128, a65) % 1.36/1.56 +c2_2(a128, a77) % 1.36/1.56 +c2_2(a128, a81) % 1.36/1.56 +c2_2(a128, a101) % 1.36/1.56 +c2_2(a128, a134) % 1.36/1.56 +c2_2(a135, a28) % 1.36/1.56 +c2_2(a135, a45) % 1.36/1.56 +c2_2(a135, a115) % 1.36/1.56 +c2_2(a140, a82) % 1.36/1.56 +c2_2(a140, a115) % 1.36/1.56 +c2_2(a140, a134) % 1.36/1.56 +c2_2(a140, a137) % 1.36/1.56 +c2_2(a145, a65) % 1.36/1.56 +c2_2(a145, a77) % 1.36/1.56 +c2_2(a145, a78) % 1.36/1.56 +c2_2(a145, a101) % 1.36/1.56 +c2_2(a145, a138) % 1.36/1.56 +c2_2(a146, a65) % 1.36/1.56 +c2_2(a146, a77) % 1.36/1.56 +c2_2(a146, a81) % 1.36/1.56 +c2_2(a146, a101) % 1.36/1.56 +c2_2(a146, a134) % 1.36/1.56 +c2_2(a153, a65) % 1.36/1.56 +c2_2(a153, a77) % 1.36/1.56 +c2_2(a153, a81) % 1.36/1.56 +c2_2(a153, a101) % 1.36/1.56 +c2_2(a153, a134) % 1.36/1.56 +c2_2(a154, a65) % 1.36/1.56 +c2_2(a154, a77) % 1.36/1.56 +c2_2(a154, a81) % 1.36/1.56 +c2_2(a154, a101) % 1.36/1.56 +c2_2(a154, a134) % 1.36/1.56 +c2_2(a156, a65) % 1.36/1.56 +c2_2(a156, a78) % 1.36/1.56 +c2_2(a156, a101) % 1.36/1.56 +c2_2(a156, a138) % 1.36/1.56 +c2_2(a158, a65) % 1.36/1.56 +c2_2(a158, a77) % 1.36/1.56 +c2_2(a158, a81) % 1.36/1.56 +c2_2(a158, a101) % 1.36/1.56 +c2_2(a158, a134) % 1.36/1.56 +c2_2(a159, a65) % 1.36/1.56 +c2_2(a159, a77) % 1.36/1.56 +c2_2(a159, a81) % 1.36/1.56 +c2_2(a159, a101) % 1.36/1.56 +c2_2(a159, a134) % 1.36/1.56 +c2_2(a160, a65) % 1.36/1.56 +c2_2(a160, a78) % 1.36/1.56 +c2_2(a160, a101) % 1.36/1.56 +c2_2(a160, a138) % 1.36/1.56 +c2_2(a164, a65) % 1.36/1.56 +c2_2(a164, a77) % 1.36/1.56 +c2_2(a164, a78) % 1.36/1.56 +c2_2(a164, a81) % 1.36/1.56 +c2_2(a164, a101) % 1.36/1.56 +c2_2(a164, a134) % 1.36/1.56 +c2_2(a164, a138) % 1.36/1.56 +c2_2(a164, a166) % 1.36/1.56 +c2_2(a167, a65) % 1.36/1.56 +c2_2(a167, a78) % 1.36/1.56 +c2_2(a167, a100) % 1.36/1.56 +c2_2(a167, a101) % 1.36/1.56 +c2_2(a167, a138) % 1.36/1.56 +c2_2(a172, =0) % 1.36/1.56 +c2_2(a172, a65) % 1.36/1.56 +c2_2(a172, a78) % 1.36/1.56 +c2_2(a172, a101) % 1.36/1.56 +c2_2(a172, a137) % 1.36/1.56 +c2_2(a172, a138) % 1.36/1.56 +c2_2(a173, a45) % 1.36/1.56 +c2_2(a173, a65) % 1.36/1.56 +c2_2(a173, a78) % 1.36/1.56 +c2_2(a173, a101) % 1.36/1.56 +c2_2(a173, a134) % 1.36/1.56 +c2_2(a173, a138) % 1.36/1.56 -c2_2(a27, a78) % 1.36/1.56 -c2_2(a27, a138) % 1.36/1.56 -c2_2(a46, a31) % 1.36/1.56 -c2_2(a46, a78) % 1.36/1.56 -c2_2(a46, a138) % 1.36/1.56 -c2_2(a48, a31) % 1.36/1.56 -c2_2(a48, a78) % 1.36/1.56 -c2_2(a48, a81) % 1.36/1.56 -c2_2(a48, a101) % 1.36/1.56 -c2_2(a48, a105) % 1.36/1.56 -c2_2(a48, a134) % 1.36/1.56 -c2_2(a48, a138) % 1.36/1.56 -c2_2(a61, a62) % 1.36/1.56 -c2_2(a72, a105) % 1.36/1.56 -c2_2(a87, a44) % 1.36/1.56 -c2_2(a87, a60) % 1.36/1.56 -c2_2(a90, a105) % 1.36/1.56 -c2_2(a91, _0) % 1.36/1.56 -c2_2(a91, a92) % 1.36/1.56 -c2_2(a96, a82) % 1.36/1.56 -c2_2(a96, a136) % 1.36/1.56 -c2_2(a96, a137) % 1.36/1.56 -c2_2(a99, a31) % 1.36/1.56 -c2_2(a99, a81) % 1.36/1.56 -c2_2(a110, a111) % 1.36/1.56 -c2_2(a140, a105) % 1.36/1.56 -c2_2(a172, a44) % 1.36/1.56 -c2_2(a172, a68) % 1.36/1.56 -c3_0 % 1.36/1.56 +c3_1(=0) % 1.36/1.56 +c3_1(a27) % 1.36/1.56 +c3_1(a29) % 1.36/1.56 +c3_1(a33) % 1.36/1.56 +c3_1(a34) % 1.36/1.56 +c3_1(a38) % 1.36/1.56 +c3_1(a41) % 1.36/1.56 +c3_1(a43) % 1.36/1.56 +c3_1(a46) % 1.36/1.56 +c3_1(a47) % 1.36/1.56 +c3_1(a58) % 1.36/1.56 +c3_1(a66) % 1.36/1.56 +c3_1(a70) % 1.36/1.56 +c3_1(a71) % 1.36/1.56 +c3_1(a74) % 1.36/1.56 +c3_1(a83) % 1.36/1.56 +c3_1(a85) % 1.36/1.56 +c3_1(a86) % 1.36/1.56 +c3_1(a87) % 1.36/1.56 +c3_1(a94) % 1.36/1.56 +c3_1(a99) % 1.36/1.56 +c3_1(a102) % 1.36/1.56 +c3_1(a103) % 1.36/1.56 +c3_1(a107) % 1.36/1.56 +c3_1(a109) % 1.36/1.56 +c3_1(a110) % 1.36/1.56 +c3_1(a122) % 1.36/1.56 +c3_1(a123) % 1.36/1.56 +c3_1(a125) % 1.36/1.56 +c3_1(a127) % 1.36/1.56 +c3_1(a128) % 1.36/1.56 +c3_1(a145) % 1.36/1.56 +c3_1(a146) % 1.36/1.56 +c3_1(a153) % 1.36/1.56 +c3_1(a154) % 1.36/1.56 +c3_1(a156) % 1.36/1.56 +c3_1(a158) % 1.36/1.56 +c3_1(a159) % 1.36/1.56 +c3_1(a160) % 1.36/1.56 +c3_1(a164) % 1.36/1.56 +c3_1(a167) % 1.36/1.56 +c3_1(a172) % 1.36/1.56 +c3_1(a173) % 1.36/1.56 -c3_1(a48) % 1.36/1.56 -c3_1(a61) % 1.36/1.56 -c3_1(a72) % 1.36/1.56 -c3_1(a90) % 1.36/1.56 -c3_1(a91) % 1.36/1.56 -c3_1(a93) % 1.36/1.56 -c3_1(a96) % 1.36/1.56 -c3_1(a114) % 1.36/1.56 -c3_1(a135) % 1.36/1.56 -c3_1(a140) % 1.36/1.56 +c3_2(=0, a44) % 1.36/1.56 +c3_2(a27, a100) % 1.36/1.56 +c3_2(a29, a30) % 1.36/1.56 +c3_2(a33, a65) % 1.36/1.56 +c3_2(a33, a68) % 1.36/1.56 +c3_2(a33, a77) % 1.36/1.56 +c3_2(a33, a78) % 1.36/1.56 +c3_2(a33, a100) % 1.36/1.56 +c3_2(a33, a138) % 1.36/1.56 +c3_2(a34, a100) % 1.36/1.56 +c3_2(a38, a39) % 1.36/1.56 +c3_2(a43, a65) % 1.36/1.56 +c3_2(a43, a68) % 1.36/1.56 +c3_2(a43, a77) % 1.36/1.56 +c3_2(a43, a78) % 1.36/1.56 +c3_2(a43, a100) % 1.36/1.56 +c3_2(a43, a136) % 1.36/1.56 +c3_2(a43, a138) % 1.36/1.56 +c3_2(a46, a65) % 1.36/1.56 +c3_2(a46, a68) % 1.36/1.56 +c3_2(a46, a77) % 1.36/1.56 +c3_2(a46, a78) % 1.36/1.56 +c3_2(a46, a100) % 1.36/1.56 +c3_2(a46, a136) % 1.36/1.56 +c3_2(a46, a138) % 1.36/1.56 +c3_2(a48, a32) % 1.36/1.56 +c3_2(a48, a68) % 1.36/1.56 +c3_2(a48, a82) % 1.36/1.56 +c3_2(a48, a137) % 1.36/1.56 +c3_2(a58, a65) % 1.36/1.56 +c3_2(a58, a68) % 1.36/1.56 +c3_2(a58, a77) % 1.36/1.56 +c3_2(a58, a78) % 1.36/1.56 +c3_2(a58, a100) % 1.36/1.56 +c3_2(a58, a136) % 1.36/1.56 +c3_2(a58, a138) % 1.36/1.56 +c3_2(a61, a62) % 1.36/1.56 +c3_2(a66, a65) % 1.36/1.56 +c3_2(a66, a67) % 1.36/1.56 +c3_2(a66, a68) % 1.36/1.56 +c3_2(a66, a77) % 1.36/1.56 +c3_2(a66, a78) % 1.36/1.56 +c3_2(a66, a100) % 1.36/1.56 +c3_2(a66, a136) % 1.36/1.56 +c3_2(a66, a138) % 1.36/1.56 +c3_2(a71, a65) % 1.36/1.56 +c3_2(a71, a68) % 1.36/1.56 +c3_2(a71, a77) % 1.36/1.56 +c3_2(a71, a78) % 1.36/1.56 +c3_2(a71, a100) % 1.36/1.56 +c3_2(a71, a136) % 1.36/1.56 +c3_2(a71, a138) % 1.36/1.56 +c3_2(a72, a73) % 1.36/1.56 +c3_2(a72, a77) % 1.36/1.56 +c3_2(a74, a76) % 1.36/1.56 +c3_2(a74, a77) % 1.36/1.56 +c3_2(a83, a77) % 1.36/1.56 +c3_2(a83, a84) % 1.36/1.56 +c3_2(a85, a65) % 1.36/1.56 +c3_2(a85, a68) % 1.36/1.56 +c3_2(a85, a77) % 1.36/1.56 +c3_2(a85, a78) % 1.36/1.56 +c3_2(a85, a100) % 1.36/1.56 +c3_2(a85, a136) % 1.36/1.56 +c3_2(a85, a138) % 1.36/1.56 +c3_2(a86, a65) % 1.36/1.56 +c3_2(a86, a68) % 1.36/1.56 +c3_2(a86, a77) % 1.36/1.56 +c3_2(a86, a78) % 1.36/1.56 +c3_2(a86, a100) % 1.36/1.56 +c3_2(a86, a136) % 1.36/1.56 +c3_2(a86, a138) % 1.36/1.56 +c3_2(a87, a59) % 1.36/1.56 +c3_2(a87, a77) % 1.36/1.56 +c3_2(a87, a88) % 1.36/1.56 +c3_2(a87, a89) % 1.36/1.56 +c3_2(a87, a124) % 1.36/1.56 +c3_2(a91, a32) % 1.36/1.56 +c3_2(a91, a68) % 1.36/1.56 +c3_2(a91, a82) % 1.36/1.56 +c3_2(a91, a137) % 1.36/1.56 +c3_2(a96, a28) % 1.36/1.56 +c3_2(a96, a31) % 1.36/1.56 +c3_2(a96, a69) % 1.36/1.56 +c3_2(a96, a77) % 1.36/1.56 +c3_2(a96, a78) % 1.36/1.56 +c3_2(a96, a81) % 1.36/1.56 +c3_2(a96, a82) % 1.36/1.56 +c3_2(a96, a97) % 1.36/1.56 +c3_2(a96, a101) % 1.36/1.56 +c3_2(a96, a115) % 1.36/1.56 +c3_2(a96, a134) % 1.36/1.56 +c3_2(a96, a136) % 1.36/1.56 +c3_2(a96, a137) % 1.36/1.56 +c3_2(a96, a138) % 1.36/1.56 +c3_2(a102, a65) % 1.36/1.56 +c3_2(a102, a68) % 1.36/1.56 +c3_2(a102, a77) % 1.36/1.56 +c3_2(a102, a78) % 1.36/1.56 +c3_2(a102, a100) % 1.36/1.56 +c3_2(a102, a136) % 1.36/1.56 +c3_2(a102, a138) % 1.36/1.56 +c3_2(a103, a65) % 1.36/1.56 +c3_2(a103, a68) % 1.36/1.56 +c3_2(a103, a77) % 1.36/1.56 +c3_2(a103, a78) % 1.36/1.56 +c3_2(a103, a100) % 1.36/1.56 +c3_2(a103, a136) % 1.36/1.56 +c3_2(a103, a138) % 1.36/1.56 +c3_2(a109, a65) % 1.36/1.56 +c3_2(a109, a68) % 1.36/1.56 +c3_2(a109, a77) % 1.36/1.56 +c3_2(a109, a78) % 1.36/1.56 +c3_2(a109, a100) % 1.36/1.56 +c3_2(a109, a136) % 1.36/1.56 +c3_2(a109, a138) % 1.36/1.56 +c3_2(a110, a111) % 1.36/1.56 +c3_2(a123, a65) % 1.36/1.56 +c3_2(a123, a68) % 1.36/1.56 +c3_2(a123, a77) % 1.36/1.56 +c3_2(a123, a78) % 1.36/1.56 +c3_2(a123, a100) % 1.36/1.56 +c3_2(a123, a136) % 1.36/1.56 +c3_2(a123, a138) % 1.36/1.56 +c3_2(a125, a126) % 1.36/1.56 +c3_2(a127, a65) % 1.36/1.56 +c3_2(a127, a68) % 1.36/1.56 +c3_2(a127, a77) % 1.36/1.56 +c3_2(a127, a78) % 1.36/1.56 +c3_2(a127, a100) % 1.36/1.56 +c3_2(a127, a136) % 1.36/1.56 +c3_2(a127, a138) % 1.36/1.56 +c3_2(a128, =0) % 1.36/1.56 +c3_2(a145, a65) % 1.36/1.56 +c3_2(a145, a68) % 1.36/1.56 +c3_2(a145, a77) % 1.36/1.56 +c3_2(a145, a78) % 1.36/1.56 +c3_2(a145, a100) % 1.36/1.56 +c3_2(a145, a138) % 1.36/1.56 +c3_2(a146, a65) % 1.36/1.56 +c3_2(a146, a68) % 1.36/1.56 +c3_2(a146, a77) % 1.36/1.56 +c3_2(a146, a78) % 1.36/1.56 +c3_2(a146, a100) % 1.36/1.56 +c3_2(a146, a136) % 1.36/1.56 +c3_2(a146, a138) % 1.36/1.56 +c3_2(a153, a65) % 1.36/1.56 +c3_2(a153, a68) % 1.36/1.56 +c3_2(a153, a77) % 1.36/1.56 +c3_2(a153, a78) % 1.36/1.56 +c3_2(a153, a100) % 1.36/1.56 +c3_2(a153, a136) % 1.36/1.56 +c3_2(a153, a138) % 1.36/1.56 +c3_2(a154, a65) % 1.36/1.56 +c3_2(a154, a68) % 1.36/1.56 +c3_2(a154, a77) % 1.36/1.56 +c3_2(a154, a78) % 1.36/1.56 +c3_2(a154, a100) % 1.36/1.56 +c3_2(a154, a136) % 1.36/1.56 +c3_2(a154, a138) % 1.36/1.56 +c3_2(a158, a65) % 1.36/1.56 +c3_2(a158, a68) % 1.36/1.56 +c3_2(a158, a77) % 1.36/1.56 +c3_2(a158, a78) % 1.36/1.56 +c3_2(a158, a100) % 1.36/1.56 +c3_2(a158, a136) % 1.36/1.56 +c3_2(a158, a138) % 1.36/1.56 +c3_2(a159, a65) % 1.36/1.56 +c3_2(a159, a68) % 1.36/1.56 +c3_2(a159, a77) % 1.36/1.56 +c3_2(a159, a78) % 1.36/1.56 +c3_2(a159, a100) % 1.36/1.56 +c3_2(a159, a136) % 1.36/1.56 +c3_2(a159, a138) % 1.36/1.56 +c3_2(a164, a77) % 1.36/1.56 +c3_2(a164, a166) % 1.36/1.56 +c3_2(a172, a68) % 1.36/1.56 -c3_2(a27, a44) % 1.36/1.56 -c3_2(a27, a101) % 1.36/1.56 -c3_2(a33, a101) % 1.36/1.56 -c3_2(a34, a44) % 1.36/1.56 -c3_2(a34, a82) % 1.36/1.56 -c3_2(a34, a101) % 1.36/1.56 -c3_2(a34, a134) % 1.36/1.56 -c3_2(a38, a44) % 1.36/1.56 -c3_2(a43, a101) % 1.36/1.56 -c3_2(a46, a101) % 1.36/1.56 -c3_2(a46, a134) % 1.36/1.56 -c3_2(a48, a105) % 1.36/1.56 -c3_2(a58, a101) % 1.36/1.56 -c3_2(a61, a44) % 1.36/1.56 -c3_2(a61, a63) % 1.36/1.56 -c3_2(a61, a64) % 1.36/1.56 -c3_2(a61, a113) % 1.36/1.56 -c3_2(a61, a119) % 1.36/1.56 -c3_2(a66, a101) % 1.36/1.56 -c3_2(a71, a101) % 1.36/1.56 -c3_2(a72, a105) % 1.36/1.56 -c3_2(a85, a101) % 1.36/1.56 -c3_2(a86, a101) % 1.36/1.56 -c3_2(a90, a105) % 1.36/1.56 -c3_2(a93, a44) % 1.36/1.56 -c3_2(a93, a113) % 1.36/1.56 -c3_2(a93, a119) % 1.36/1.56 -c3_2(a102, a101) % 1.36/1.56 -c3_2(a103, a101) % 1.36/1.56 -c3_2(a109, a101) % 1.36/1.56 -c3_2(a110, a56) % 1.36/1.56 -c3_2(a110, a129) % 1.36/1.56 -c3_2(a110, a134) % 1.36/1.56 -c3_2(a114, a44) % 1.36/1.56 -c3_2(a114, a113) % 1.36/1.56 -c3_2(a114, a119) % 1.36/1.56 -c3_2(a123, a101) % 1.36/1.56 -c3_2(a127, a101) % 1.36/1.56 -c3_2(a128, a101) % 1.36/1.56 -c3_2(a128, a134) % 1.36/1.56 -c3_2(a128, a137) % 1.36/1.56 -c3_2(a135, a44) % 1.36/1.56 -c3_2(a135, a113) % 1.36/1.56 -c3_2(a135, a119) % 1.36/1.56 -c3_2(a140, a82) % 1.36/1.56 -c3_2(a140, a105) % 1.36/1.56 -c3_2(a140, a134) % 1.36/1.56 -c3_2(a145, a101) % 1.36/1.56 -c3_2(a146, a101) % 1.36/1.56 -c3_2(a153, a101) % 1.36/1.56 -c3_2(a154, a101) % 1.36/1.56 -c3_2(a158, a101) % 1.36/1.56 -c3_2(a159, a101) % 1.36/1.56 -c3_2(a173, a44) % 1.36/1.56 +c4_0 % 1.36/1.56 +c4_1(=0) % 1.36/1.56 +c4_1(a27) % 1.36/1.56 +c4_1(a29) % 1.36/1.56 +c4_1(a33) % 1.36/1.56 +c4_1(a34) % 1.36/1.56 +c4_1(a38) % 1.36/1.56 +c4_1(a41) % 1.36/1.56 +c4_1(a43) % 1.36/1.56 +c4_1(a46) % 1.36/1.56 +c4_1(a47) % 1.36/1.56 +c4_1(a58) % 1.36/1.56 +c4_1(a66) % 1.36/1.56 +c4_1(a70) % 1.36/1.56 +c4_1(a71) % 1.36/1.56 +c4_1(a74) % 1.36/1.56 +c4_1(a83) % 1.36/1.56 +c4_1(a85) % 1.36/1.56 +c4_1(a86) % 1.36/1.56 +c4_1(a94) % 1.36/1.56 +c4_1(a99) % 1.36/1.56 +c4_1(a102) % 1.36/1.56 +c4_1(a103) % 1.36/1.56 +c4_1(a107) % 1.36/1.56 +c4_1(a109) % 1.36/1.56 +c4_1(a110) % 1.36/1.56 +c4_1(a122) % 1.36/1.56 +c4_1(a123) % 1.36/1.56 +c4_1(a125) % 1.36/1.56 +c4_1(a127) % 1.36/1.56 +c4_1(a128) % 1.36/1.56 +c4_1(a145) % 1.36/1.56 +c4_1(a146) % 1.36/1.56 +c4_1(a153) % 1.36/1.56 +c4_1(a154) % 1.36/1.56 +c4_1(a156) % 1.36/1.56 +c4_1(a158) % 1.36/1.56 +c4_1(a159) % 1.36/1.56 +c4_1(a160) % 1.36/1.56 +c4_1(a164) % 1.36/1.56 +c4_1(a167) % 1.36/1.56 +c4_1(a172) % 1.36/1.56 +c4_1(a173) % 1.36/1.56 -c4_1(a61) % 1.36/1.56 -c4_1(a72) % 1.36/1.56 -c4_1(a87) % 1.36/1.56 -c4_1(a90) % 1.36/1.56 -c4_1(a91) % 1.36/1.56 -c4_1(a93) % 1.36/1.56 -c4_1(a96) % 1.36/1.56 -c4_1(a114) % 1.36/1.56 -c4_1(a135) % 1.36/1.56 -c4_1(a140) % 1.36/1.56 +c4_2(=0, a137) % 1.36/1.56 +c4_2(a27, a78) % 1.36/1.56 +c4_2(a27, a82) % 1.36/1.56 +c4_2(a27, a100) % 1.36/1.56 +c4_2(a27, a137) % 1.36/1.56 +c4_2(a27, a138) % 1.36/1.56 +c4_2(a34, a35) % 1.36/1.56 +c4_2(a34, a57) % 1.36/1.56 +c4_2(a34, a78) % 1.36/1.56 +c4_2(a34, a82) % 1.36/1.56 +c4_2(a34, a100) % 1.36/1.56 +c4_2(a34, a137) % 1.36/1.56 +c4_2(a34, a138) % 1.36/1.56 +c4_2(a34, a141) % 1.36/1.56 +c4_2(a38, a39) % 1.36/1.56 +c4_2(a43, a137) % 1.36/1.56 +c4_2(a46, a32) % 1.36/1.56 +c4_2(a46, a57) % 1.36/1.56 +c4_2(a46, a65) % 1.36/1.56 +c4_2(a46, a77) % 1.36/1.56 +c4_2(a46, a81) % 1.36/1.56 +c4_2(a46, a101) % 1.36/1.56 +c4_2(a46, a134) % 1.36/1.56 +c4_2(a46, a137) % 1.36/1.56 +c4_2(a46, a141) % 1.36/1.56 +c4_2(a47, a82) % 1.36/1.56 +c4_2(a48, a32) % 1.36/1.56 +c4_2(a48, a82) % 1.36/1.56 +c4_2(a58, a137) % 1.36/1.56 +c4_2(a61, a62) % 1.36/1.56 +c4_2(a66, a137) % 1.36/1.56 +c4_2(a71, a137) % 1.36/1.56 +c4_2(a72, a82) % 1.36/1.56 +c4_2(a85, a137) % 1.36/1.56 +c4_2(a86, a137) % 1.36/1.56 +c4_2(a87, a44) % 1.36/1.56 +c4_2(a87, a60) % 1.36/1.56 +c4_2(a90, a82) % 1.36/1.56 +c4_2(a91, a32) % 1.36/1.56 +c4_2(a91, a82) % 1.36/1.56 +c4_2(a91, a137) % 1.36/1.56 +c4_2(a96, a82) % 1.36/1.56 +c4_2(a96, a137) % 1.36/1.56 +c4_2(a99, a32) % 1.36/1.56 +c4_2(a99, a65) % 1.36/1.56 +c4_2(a99, a78) % 1.36/1.56 +c4_2(a99, a82) % 1.36/1.56 +c4_2(a99, a101) % 1.36/1.56 +c4_2(a99, a134) % 1.36/1.56 +c4_2(a99, a138) % 1.36/1.56 +c4_2(a102, a137) % 1.36/1.56 +c4_2(a103, a137) % 1.36/1.56 +c4_2(a107, a108) % 1.36/1.56 +c4_2(a109, a137) % 1.36/1.56 +c4_2(a110, a56) % 1.36/1.56 +c4_2(a110, a78) % 1.36/1.56 +c4_2(a110, a137) % 1.36/1.56 +c4_2(a110, a138) % 1.36/1.56 +c4_2(a123, a137) % 1.36/1.56 +c4_2(a127, a137) % 1.36/1.56 +c4_2(a128, a101) % 1.36/1.56 +c4_2(a128, a134) % 1.36/1.56 +c4_2(a128, a137) % 1.36/1.56 +c4_2(a140, a82) % 1.36/1.56 +c4_2(a146, a137) % 1.36/1.56 +c4_2(a153, a137) % 1.36/1.56 +c4_2(a154, a137) % 1.36/1.56 +c4_2(a158, a137) % 1.36/1.56 +c4_2(a159, a137) % 1.36/1.56 +c4_2(a164, a165) % 1.36/1.56 +c4_2(a172, a68) % 1.36/1.56 +c4_2(a172, a82) % 1.36/1.56 +c4_2(a172, a137) % 1.36/1.56 +c4_2(a173, a82) % 1.36/1.56 -c4_2(a27, a45) % 1.36/1.56 -c4_2(a34, a45) % 1.36/1.56 -c4_2(a38, a45) % 1.36/1.56 -c4_2(a48, a105) % 1.36/1.56 -c4_2(a48, a137) % 1.36/1.56 -c4_2(a61, a45) % 1.36/1.56 -c4_2(a61, a63) % 1.36/1.56 -c4_2(a61, a64) % 1.36/1.56 -c4_2(a61, a113) % 1.36/1.56 -c4_2(a61, a119) % 1.36/1.56 -c4_2(a72, a73) % 1.36/1.56 -c4_2(a72, a113) % 1.36/1.56 -c4_2(a87, a45) % 1.36/1.56 -c4_2(a87, a88) % 1.36/1.56 -c4_2(a87, a89) % 1.36/1.56 -c4_2(a87, a113) % 1.36/1.56 -c4_2(a90, a113) % 1.36/1.56 -c4_2(a91, a60) % 1.36/1.56 -c4_2(a91, a92) % 1.36/1.56 -c4_2(a93, a45) % 1.36/1.56 -c4_2(a93, a113) % 1.36/1.56 -c4_2(a93, a119) % 1.36/1.56 -c4_2(a96, a97) % 1.36/1.56 -c4_2(a96, a113) % 1.36/1.56 -c4_2(a110, a113) % 1.36/1.56 -c4_2(a110, a129) % 1.36/1.56 -c4_2(a114, a45) % 1.36/1.56 -c4_2(a114, a113) % 1.36/1.56 -c4_2(a114, a119) % 1.36/1.56 -c4_2(a135, a45) % 1.36/1.56 -c4_2(a135, a113) % 1.36/1.56 -c4_2(a135, a119) % 1.36/1.56 -c4_2(a140, a105) % 1.36/1.56 -c4_2(a140, a113) % 1.36/1.56 -c4_2(a173, a45) % 1.36/1.56 +c5_0 % 1.36/1.56 +c5_1(=0) % 1.36/1.56 +c5_1(a27) % 1.36/1.56 +c5_1(a29) % 1.36/1.56 +c5_1(a33) % 1.36/1.56 +c5_1(a34) % 1.36/1.56 +c5_1(a38) % 1.36/1.56 +c5_1(a41) % 1.36/1.56 +c5_1(a43) % 1.36/1.56 +c5_1(a46) % 1.36/1.56 +c5_1(a47) % 1.36/1.56 +c5_1(a58) % 1.36/1.56 +c5_1(a66) % 1.36/1.56 +c5_1(a70) % 1.36/1.56 +c5_1(a71) % 1.36/1.56 +c5_1(a74) % 1.36/1.56 +c5_1(a83) % 1.36/1.56 +c5_1(a85) % 1.36/1.56 +c5_1(a86) % 1.36/1.56 +c5_1(a91) % 1.36/1.56 +c5_1(a94) % 1.36/1.56 +c5_1(a99) % 1.36/1.56 +c5_1(a102) % 1.36/1.56 +c5_1(a103) % 1.36/1.56 +c5_1(a107) % 1.36/1.56 +c5_1(a109) % 1.36/1.56 +c5_1(a122) % 1.36/1.56 +c5_1(a123) % 1.36/1.56 +c5_1(a125) % 1.36/1.56 +c5_1(a127) % 1.36/1.56 +c5_1(a128) % 1.36/1.56 +c5_1(a145) % 1.36/1.56 +c5_1(a146) % 1.36/1.56 +c5_1(a153) % 1.36/1.56 +c5_1(a154) % 1.36/1.56 +c5_1(a156) % 1.36/1.56 +c5_1(a158) % 1.36/1.56 +c5_1(a159) % 1.36/1.56 +c5_1(a160) % 1.36/1.56 +c5_1(a164) % 1.36/1.56 +c5_1(a167) % 1.36/1.56 +c5_1(a172) % 1.36/1.56 +c5_1(a173) % 1.36/1.56 -c5_1(a61) % 1.36/1.56 -c5_1(a72) % 1.36/1.56 -c5_1(a87) % 1.36/1.56 -c5_1(a90) % 1.36/1.56 -c5_1(a93) % 1.36/1.56 -c5_1(a96) % 1.36/1.56 -c5_1(a110) % 1.36/1.56 -c5_1(a114) % 1.36/1.56 -c5_1(a135) % 1.36/1.56 -c5_1(a140) % 1.36/1.56 +c5_2(=0, a78) % 1.36/1.56 +c5_2(=0, a138) % 1.36/1.56 +c5_2(a27, a45) % 1.36/1.56 +c5_2(a27, a78) % 1.36/1.56 +c5_2(a27, a138) % 1.36/1.56 +c5_2(a29, a78) % 1.36/1.56 +c5_2(a29, a138) % 1.36/1.56 +c5_2(a33, a78) % 1.36/1.56 +c5_2(a33, a138) % 1.36/1.56 +c5_2(a34, a35) % 1.36/1.56 +c5_2(a34, a45) % 1.36/1.56 +c5_2(a34, a57) % 1.36/1.56 +c5_2(a34, a78) % 1.36/1.56 +c5_2(a34, a138) % 1.36/1.56 +c5_2(a38, a45) % 1.36/1.56 +c5_2(a38, a78) % 1.36/1.56 +c5_2(a38, a138) % 1.36/1.56 +c5_2(a41, a78) % 1.36/1.56 +c5_2(a41, a138) % 1.36/1.56 +c5_2(a43, a78) % 1.36/1.56 +c5_2(a43, a138) % 1.36/1.56 +c5_2(a46, a32) % 1.36/1.56 +c5_2(a46, a57) % 1.36/1.56 +c5_2(a46, a78) % 1.36/1.56 +c5_2(a46, a138) % 1.36/1.56 +c5_2(a47, a78) % 1.36/1.56 +c5_2(a47, a138) % 1.36/1.56 +c5_2(a48, a32) % 1.36/1.56 +c5_2(a48, a82) % 1.36/1.56 +c5_2(a58, a78) % 1.36/1.56 +c5_2(a58, a138) % 1.36/1.56 +c5_2(a61, a45) % 1.36/1.56 +c5_2(a66, a67) % 1.36/1.56 +c5_2(a66, a78) % 1.36/1.56 +c5_2(a66, a138) % 1.36/1.56 +c5_2(a70, a78) % 1.36/1.56 +c5_2(a70, a138) % 1.36/1.56 +c5_2(a71, a78) % 1.36/1.56 +c5_2(a71, a138) % 1.36/1.56 +c5_2(a74, a78) % 1.36/1.56 +c5_2(a74, a138) % 1.36/1.56 +c5_2(a83, a78) % 1.36/1.56 +c5_2(a83, a138) % 1.36/1.56 +c5_2(a85, a78) % 1.36/1.56 +c5_2(a85, a138) % 1.36/1.56 +c5_2(a86, a78) % 1.36/1.56 +c5_2(a86, a138) % 1.36/1.56 +c5_2(a87, a45) % 1.36/1.56 +c5_2(a87, a88) % 1.36/1.56 +c5_2(a87, a138) % 1.36/1.56 +c5_2(a91, a32) % 1.36/1.56 +c5_2(a91, a82) % 1.36/1.56 +c5_2(a91, a136) % 1.36/1.56 +c5_2(a91, a137) % 1.36/1.56 +c5_2(a93, a45) % 1.36/1.56 +c5_2(a94, a78) % 1.36/1.56 +c5_2(a94, a138) % 1.36/1.56 +c5_2(a96, a82) % 1.36/1.56 +c5_2(a96, a136) % 1.36/1.56 +c5_2(a96, a137) % 1.36/1.56 +c5_2(a99, a32) % 1.36/1.56 +c5_2(a99, a78) % 1.36/1.56 +c5_2(a99, a138) % 1.36/1.56 +c5_2(a102, a78) % 1.36/1.56 +c5_2(a102, a138) % 1.36/1.56 +c5_2(a103, a78) % 1.36/1.56 +c5_2(a103, a138) % 1.36/1.56 +c5_2(a107, a78) % 1.36/1.56 +c5_2(a107, a138) % 1.36/1.56 +c5_2(a109, a78) % 1.36/1.56 +c5_2(a109, a138) % 1.36/1.56 +c5_2(a110, a56) % 1.36/1.56 +c5_2(a110, a78) % 1.36/1.56 +c5_2(a110, a138) % 1.36/1.56 +c5_2(a114, a45) % 1.36/1.56 +c5_2(a122, a78) % 1.36/1.56 +c5_2(a122, a138) % 1.36/1.56 +c5_2(a123, a78) % 1.36/1.56 +c5_2(a123, a138) % 1.36/1.56 +c5_2(a125, a78) % 1.36/1.56 +c5_2(a125, a138) % 1.36/1.56 +c5_2(a127, a78) % 1.36/1.56 +c5_2(a127, a138) % 1.36/1.56 +c5_2(a128, a78) % 1.36/1.56 +c5_2(a128, a138) % 1.36/1.56 +c5_2(a135, a45) % 1.36/1.56 +c5_2(a145, a78) % 1.36/1.56 +c5_2(a145, a138) % 1.36/1.56 +c5_2(a146, a78) % 1.36/1.56 +c5_2(a146, a138) % 1.36/1.56 +c5_2(a153, a78) % 1.36/1.57 +c5_2(a153, a138) % 1.36/1.57 +c5_2(a154, a78) % 1.36/1.57 +c5_2(a154, a138) % 1.36/1.57 +c5_2(a156, a78) % 1.36/1.57 +c5_2(a156, a138) % 1.36/1.57 +c5_2(a158, a78) % 1.36/1.57 +c5_2(a158, a138) % 1.36/1.57 +c5_2(a159, a78) % 1.36/1.57 +c5_2(a159, a138) % 1.36/1.57 +c5_2(a160, a78) % 1.36/1.57 +c5_2(a160, a138) % 1.36/1.57 +c5_2(a164, a78) % 1.36/1.57 +c5_2(a164, a138) % 1.36/1.57 +c5_2(a164, a166) % 1.36/1.57 +c5_2(a167, a78) % 1.36/1.57 +c5_2(a167, a138) % 1.36/1.57 +c5_2(a172, a44) % 1.36/1.57 +c5_2(a172, a68) % 1.36/1.57 +c5_2(a172, a78) % 1.36/1.57 +c5_2(a172, a138) % 1.36/1.57 +c5_2(a173, a45) % 1.36/1.57 +c5_2(a173, a78) % 1.36/1.57 +c5_2(a173, a138) % 1.36/1.57 -c5_2(a27, a101) % 1.36/1.57 -c5_2(a29, a30) % 1.36/1.57 -c5_2(a33, a101) % 1.36/1.57 -c5_2(a34, a101) % 1.36/1.57 -c5_2(a34, a137) % 1.36/1.57 -c5_2(a43, a101) % 1.36/1.57 -c5_2(a46, a101) % 1.36/1.57 -c5_2(a47, a82) % 1.36/1.57 -c5_2(a58, a101) % 1.36/1.57 -c5_2(a61, a63) % 1.36/1.57 -c5_2(a61, a113) % 1.36/1.57 -c5_2(a66, a101) % 1.36/1.57 -c5_2(a71, a101) % 1.36/1.57 -c5_2(a72, a113) % 1.36/1.57 -c5_2(a85, a101) % 1.36/1.57 -c5_2(a86, a101) % 1.36/1.57 -c5_2(a87, a113) % 1.36/1.57 -c5_2(a90, a113) % 1.36/1.57 -c5_2(a91, a60) % 1.36/1.57 -c5_2(a93, a113) % 1.36/1.57 -c5_2(a96, a97) % 1.36/1.57 -c5_2(a96, a113) % 1.36/1.57 -c5_2(a102, a101) % 1.36/1.57 -c5_2(a103, a101) % 1.36/1.57 -c5_2(a109, a101) % 1.36/1.57 -c5_2(a110, a111) % 1.36/1.57 -c5_2(a110, a113) % 1.36/1.57 -c5_2(a110, a129) % 1.36/1.57 -c5_2(a114, a113) % 1.36/1.57 -c5_2(a123, a101) % 1.36/1.57 -c5_2(a127, a101) % 1.36/1.57 -c5_2(a135, a113) % 1.36/1.57 -c5_2(a140, a82) % 1.36/1.57 -c5_2(a140, a113) % 1.36/1.57 -c5_2(a145, a101) % 1.36/1.57 -c5_2(a146, a101) % 1.36/1.57 -c5_2(a153, a101) % 1.36/1.57 -c5_2(a154, a101) % 1.36/1.57 -c5_2(a158, a101) % 1.36/1.57 -c5_2(a159, a101) % 1.36/1.57 +epred1_0 % 1.36/1.57 +epred2_0 % 1.36/1.57 +epred3_0 % 1.36/1.57 +ndr1_0 % 1.36/1.57 +ndr1_1(_0) % 1.36/1.57 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------