%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN420+1 : TPTP v9.0.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:03:31 PM UTC 2025 % Result : CounterSatisfiable 27.42s 12.05s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN420+1 : TPTP v9.0.0. Released v2.1.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 07:23:39 EDT 2025 % 0.13/0.34 % CPUTime : % 27.42/12.05 % 27.42/12.05 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.42/12.05 % 27.42/12.05 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.76/12.07 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > a448 > a447 > a446 > a445 > a444 > a443 > a442 > a441 > a440 > a439 > a438 > a437 > a436 > a435 > a434 > a433 > a432 > a431 > a430 > a429 > a428 > a427 > a426 > a425 > a424 > a423 > a422 > a421 > a420 > a419 > a418 > a417 > a416 > a415 > a414 > a413 > a412 > a411 > a410 > a409 > a408 > a407 > a406 > a405 > a404 > a403 > a402 > a401 > a400 > a399 > a398 > a397 > a396 > a395 > a394 > a393 > a392 > a391 > a390 > a389 > a388 > a387 > a386 > a385 > a384 > a383 > a382 > a381 > a380 > a379 > a378 > a377 > a376 > a375 > a374 > a373 > a372 > a371 > a370 > a369 > a368 > a367 > a366 > a365 > a364 > a363 > a362 > a361 > a360 > a359 > a358 > a357 > a356 > a355 > a354 > a353 > a352 > a351 > a350 > a349 > a348 > a347 > a346 > a345 > a344 > a343 > a342 > a341 > a340 > a339 > a338 > a337 > a336 > a335 > a334 > a333 > a332 > a331 > a330 > a329 > a328 > a327 > a326 > a325 > a324 > a323 > a322 > a321 > a320 > a319 > a318 > a317 > a316 > a315 > a314 > a313 > a312 > a311 > a310 > a309 > a308 > a307 > a306 > a305 > a304 > a303 > a302 > a301 > a300 > a299 > a298 > a297 > a296 > a295 > a294 > a293 > a292 > a291 > a290 > a289 > a288 > a287 > a286 > a285 > a284 > a283 > a282 > a281 > a280 > a279 > a278 > a277 > a276 > a275 > a274 > a273 > a272 > a271 > a270 > a269 % 27.76/12.07 % 27.76/12.07 %Foreground sorts: % 27.76/12.07 % 27.76/12.07 % 27.76/12.07 %Background operators: % 27.76/12.07 % 27.76/12.07 % 27.76/12.07 %Foreground operators: % 27.76/12.07 tff(a430, type, a430: $i). % 27.76/12.07 tff(c7_0, type, c7_0: $o). % 27.76/12.07 tff(a323, type, a323: $i). % 27.76/12.07 tff(a421, type, a421: $i). % 27.76/12.07 tff(a316, type, a316: $i). % 27.76/12.07 tff(a389, type, a389: $i). % 27.76/12.07 tff(a347, type, a347: $i). % 27.76/12.07 tff(a281, type, a281: $i). % 27.76/12.07 tff(a433, type, a433: $i). % 27.76/12.07 tff(a322, type, a322: $i). % 27.76/12.07 tff(a313, type, a313: $i). % 27.76/12.07 tff(a292, type, a292: $i). % 27.76/12.07 tff(a435, type, a435: $i). % 27.76/12.07 tff(a336, type, a336: $i). % 27.76/12.07 tff(a422, type, a422: $i). % 27.76/12.07 tff(c4_0, type, c4_0: $o). % 27.76/12.07 tff(a335, type, a335: $i). % 27.76/12.07 tff(a431, type, a431: $i). % 27.76/12.07 tff(a280, type, a280: $i). % 27.76/12.07 tff(a326, type, a326: $i). % 27.76/12.07 tff(a297, type, a297: $i). % 27.76/12.07 tff(a290, type, a290: $i). % 27.76/12.07 tff(a446, type, a446: $i). % 27.76/12.07 tff(a359, type, a359: $i). % 27.76/12.07 tff(c3_0, type, c3_0: $o). % 27.76/12.07 tff(a386, type, a386: $i). % 27.76/12.07 tff(a399, type, a399: $i). % 27.76/12.07 tff(a423, type, a423: $i). % 27.76/12.07 tff(a338, type, a338: $i). % 27.76/12.07 tff(a398, type, a398: $i). % 27.76/12.07 tff(c1_2, type, c1_2: ($i * $i) > $o). % 27.76/12.07 tff(a334, type, a334: $i). % 27.76/12.07 tff(a384, type, a384: $i). % 27.76/12.07 tff(a373, type, a373: $i). % 27.76/12.07 tff(a387, type, a387: $i). % 27.76/12.07 tff(a272, type, a272: $i). % 27.76/12.07 tff(a309, type, a309: $i). % 27.76/12.07 tff(a302, type, a302: $i). % 27.76/12.07 tff(a337, type, a337: $i). % 27.76/12.07 tff(a306, type, a306: $i). % 27.76/12.07 tff(a368, type, a368: $i). % 27.76/12.07 tff(a432, type, a432: $i). % 27.76/12.07 tff(a367, type, a367: $i). % 27.76/12.07 tff(a417, type, a417: $i). % 27.76/12.07 tff(a320, type, a320: $i). % 27.76/12.07 tff(a301, type, a301: $i). % 27.76/12.07 tff(a401, type, a401: $i). % 27.76/12.07 tff(a354, type, a354: $i). % 27.76/12.07 tff(a284, type, a284: $i). % 27.76/12.07 tff(a295, type, a295: $i). % 27.76/12.07 tff(a310, type, a310: $i). % 27.76/12.07 tff(a407, type, a407: $i). % 27.76/12.07 tff(a285, type, a285: $i). % 27.76/12.07 tff(a348, type, a348: $i). % 27.76/12.07 tff(a434, type, a434: $i). % 27.76/12.07 tff(a436, type, a436: $i). % 27.76/12.07 tff(a341, type, a341: $i). % 27.76/12.07 tff(a448, type, a448: $i). % 27.76/12.07 tff(a380, type, a380: $i). % 27.76/12.07 tff(a361, type, a361: $i). % 27.76/12.07 tff(a342, type, a342: $i). % 27.76/12.07 tff(c8_0, type, c8_0: $o). % 27.76/12.07 tff(a311, type, a311: $i). % 27.76/12.07 tff(a391, type, a391: $i). % 27.76/12.07 tff(a355, type, a355: $i). % 27.76/12.07 tff(a269, type, a269: $i). % 27.76/12.07 tff(a286, type, a286: $i). % 27.76/12.07 tff(a330, type, a330: $i). % 27.76/12.07 tff(a418, type, a418: $i). % 27.76/12.07 tff(a291, type, a291: $i). % 27.76/12.07 tff(a314, type, a314: $i). % 27.76/12.07 tff(a413, type, a413: $i). % 27.76/12.07 tff(a405, type, a405: $i). % 27.76/12.07 tff(a283, type, a283: $i). % 27.76/12.07 tff(a397, type, a397: $i). % 27.76/12.07 tff(a439, type, a439: $i). % 27.76/12.07 tff(a402, type, a402: $i). % 27.76/12.07 tff(a437, type, a437: $i). % 27.76/12.07 tff(a370, type, a370: $i). % 27.76/12.07 tff(a293, type, a293: $i). % 27.76/12.07 tff(a294, type, a294: $i). % 27.76/12.07 tff(a321, type, a321: $i). % 27.76/12.07 tff(a318, type, a318: $i). % 27.76/12.07 tff(c5_0, type, c5_0: $o). % 27.76/12.07 tff(a414, type, a414: $i). % 27.76/12.07 tff(a438, type, a438: $i). % 27.76/12.07 tff(a366, type, a366: $i). % 27.76/12.07 tff(a396, type, a396: $i). % 27.76/12.07 tff(a308, type, a308: $i). % 27.76/12.07 tff(a329, type, a329: $i). % 27.76/12.07 tff(c6_0, type, c6_0: $o). % 27.76/12.07 tff(c8_2, type, c8_2: ($i * $i) > $o). % 27.76/12.07 tff(a270, type, a270: $i). % 27.76/12.07 tff(a278, type, a278: $i). % 27.76/12.07 tff(a442, type, a442: $i). % 27.76/12.07 tff(a410, type, a410: $i). % 27.76/12.07 tff(a388, type, a388: $i). % 27.76/12.07 tff(a298, type, a298: $i). % 27.76/12.07 tff(a353, type, a353: $i). % 27.76/12.07 tff(a443, type, a443: $i). % 27.76/12.07 tff(a374, type, a374: $i). % 27.76/12.07 tff(a358, type, a358: $i). % 27.76/12.07 tff(a304, type, a304: $i). % 27.76/12.07 tff(a343, type, a343: $i). % 27.76/12.07 tff(a275, type, a275: $i). % 27.76/12.07 tff(a357, type, a357: $i). % 27.76/12.07 tff(a282, type, a282: $i). % 27.76/12.07 tff(a273, type, a273: $i). % 27.76/12.07 tff(c1_0, type, c1_0: $o). % 27.76/12.07 tff(a331, type, a331: $i). % 27.76/12.07 tff(c8_1, type, c8_1: $i > $o). % 27.76/12.07 tff(a427, type, a427: $i). % 27.76/12.07 tff(a371, type, a371: $i). % 27.76/12.07 tff(a393, type, a393: $i). % 27.76/12.07 tff(c2_1, type, c2_1: $i > $o). % 27.76/12.07 tff(a392, type, a392: $i). % 27.76/12.07 tff(ndr1_1, type, ndr1_1: $i > $o). % 27.76/12.07 tff(c2_0, type, c2_0: $o). % 27.76/12.07 tff(c4_1, type, c4_1: $i > $o). % 27.76/12.07 tff(a277, type, a277: $i). % 27.76/12.07 tff(a333, type, a333: $i). % 27.76/12.07 tff(a382, type, a382: $i). % 27.76/12.07 tff(a274, type, a274: $i). % 27.76/12.07 tff(a420, type, a420: $i). % 27.76/12.07 tff(a383, type, a383: $i). % 27.76/12.07 tff(a345, type, a345: $i). % 27.76/12.07 tff(a408, type, a408: $i). % 27.76/12.07 tff(a363, type, a363: $i). % 27.76/12.07 tff(a416, type, a416: $i). % 27.76/12.07 tff(a271, type, a271: $i). % 27.76/12.07 tff(a352, type, a352: $i). % 27.76/12.07 tff(a327, type, a327: $i). % 27.76/12.07 tff(a390, type, a390: $i). % 27.76/12.07 tff(c9_1, type, c9_1: $i > $o). % 27.76/12.07 tff(c10_1, type, c10_1: $i > $o). % 27.76/12.07 tff(c10_0, type, c10_0: $o). % 27.76/12.07 tff(a425, type, a425: $i). % 27.76/12.07 tff(a447, type, a447: $i). % 27.76/12.07 tff(c6_2, type, c6_2: ($i * $i) > $o). % 27.76/12.07 tff(a400, type, a400: $i). % 27.76/12.07 tff(a364, type, a364: $i). % 27.76/12.07 tff(a381, type, a381: $i). % 27.76/12.07 tff(a429, type, a429: $i). % 27.76/12.07 tff(a289, type, a289: $i). % 27.76/12.07 tff(a411, type, a411: $i). % 27.76/12.07 tff(ndr1_0, type, ndr1_0: $o). % 27.76/12.07 tff(a288, type, a288: $i). % 27.76/12.07 tff(a300, type, a300: $i). % 27.76/12.07 tff(a287, type, a287: $i). % 27.76/12.07 tff(a375, type, a375: $i). % 27.76/12.07 tff(a444, type, a444: $i). % 27.76/12.07 tff(a344, type, a344: $i). % 27.76/12.07 tff(a351, type, a351: $i). % 27.76/12.07 tff(c9_2, type, c9_2: ($i * $i) > $o). % 27.76/12.07 tff(a395, type, a395: $i). % 27.76/12.07 tff(c10_2, type, c10_2: ($i * $i) > $o). % 27.76/12.07 tff(a424, type, a424: $i). % 27.76/12.07 tff(a317, type, a317: $i). % 27.76/12.07 tff(a441, type, a441: $i). % 27.76/12.07 tff(a349, type, a349: $i). % 27.76/12.07 tff(a426, type, a426: $i). % 27.76/12.07 tff(a324, type, a324: $i). % 27.76/12.07 tff(a403, type, a403: $i). % 27.76/12.07 tff(a419, type, a419: $i). % 27.76/12.07 tff(c1_1, type, c1_1: $i > $o). % 27.76/12.07 tff(a369, type, a369: $i). % 27.76/12.07 tff(a378, type, a378: $i). % 27.76/12.07 tff(a415, type, a415: $i). % 27.76/12.07 tff(a409, type, a409: $i). % 27.76/12.07 tff(a385, type, a385: $i). % 27.76/12.07 tff(c5_2, type, c5_2: ($i * $i) > $o). % 27.76/12.07 tff(a340, type, a340: $i). % 27.76/12.07 tff(a299, type, a299: $i). % 27.76/12.07 tff(c9_0, type, c9_0: $o). % 27.76/12.07 tff(a394, type, a394: $i). % 27.76/12.07 tff(c7_1, type, c7_1: $i > $o). % 27.76/12.07 tff(a362, type, a362: $i). % 27.76/12.07 tff(c6_1, type, c6_1: $i > $o). % 27.76/12.07 tff(a315, type, a315: $i). % 27.76/12.07 tff(a445, type, a445: $i). % 27.76/12.07 tff(a440, type, a440: $i). % 27.76/12.07 tff(c4_2, type, c4_2: ($i * $i) > $o). % 27.76/12.07 tff(a276, type, a276: $i). % 27.76/12.07 tff(a406, type, a406: $i). % 27.76/12.07 tff(a319, type, a319: $i). % 27.76/12.07 tff(a376, type, a376: $i). % 27.76/12.07 tff(a328, type, a328: $i). % 27.76/12.07 tff(a332, type, a332: $i). % 27.76/12.07 tff(a428, type, a428: $i). % 27.76/12.07 tff(a279, type, a279: $i). % 27.76/12.07 tff(a296, type, a296: $i). % 27.76/12.07 tff(c5_1, type, c5_1: $i > $o). % 27.76/12.07 tff(a346, type, a346: $i). % 27.76/12.07 tff(c7_2, type, c7_2: ($i * $i) > $o). % 27.76/12.07 tff(c3_2, type, c3_2: ($i * $i) > $o). % 27.76/12.07 tff(a350, type, a350: $i). % 27.76/12.07 tff(a404, type, a404: $i). % 27.76/12.07 tff(a412, type, a412: $i). % 27.76/12.07 tff(c2_2, type, c2_2: ($i * $i) > $o). % 27.76/12.07 tff(a365, type, a365: $i). % 27.76/12.07 tff(a325, type, a325: $i). % 27.76/12.07 tff(a360, type, a360: $i). % 27.76/12.07 tff(a372, type, a372: $i). % 27.76/12.07 tff(a305, type, a305: $i). % 27.76/12.07 tff(a312, type, a312: $i). % 27.76/12.07 tff(a307, type, a307: $i). % 27.76/12.07 tff(a303, type, a303: $i). % 27.76/12.07 tff(a339, type, a339: $i). % 27.76/12.07 tff(a379, type, a379: $i). % 27.76/12.07 tff(a377, type, a377: $i). % 27.76/12.07 tff(a356, type, a356: $i). % 27.76/12.07 tff(c3_1, type, c3_1: $i > $o). % 27.76/12.07 % 27.76/12.07 %Saturated clause set: % 27.76/12.07 tff(c_15410, plain, (~c4_2(a395, a396))). % 27.76/12.07 tff(c_15407, plain, (~c10_2(a416, a418))). % 27.76/12.07 tff(c_15388, plain, (~c4_2(a416, a418))). % 27.76/12.07 tff(c_15385, plain, (~c10_2(a414, a415))). % 27.76/12.07 tff(c_15362, plain, (~c4_2(a414, a415))). % 27.76/12.07 tff(c_15340, plain, (~c4_2(a302, a303))). % 27.76/12.07 tff(c_15305, plain, (![X72_97, X74_101, X73_100]: (~c4_2(X72_97, X74_101) | ~c6_2(X72_97, X74_101) | c8_2(X72_97, X73_100) | c1_2(X72_97, X73_100) | c5_2(X72_97, X73_100) | c9_1(X72_97)))). % 27.76/12.07 tff(c_15284, plain, (![X81_345]: (~c1_2(X81_345, a428) | c6_1(X81_345) | c1_2(X81_345, a388) | ~c9_1(X81_345) | c3_1(X81_345) | c5_1(X81_345) | c2_1(X81_345) | c10_2(X81_345, a388)))). % 27.76/12.07 tff(c_15261, plain, (![X146_359]: (c9_1(X146_359) | c3_1(X146_359) | ~c1_2(X146_359, a428) | c6_1(X146_359) | ~c2_2(X146_359, a399) | c1_2(X146_359, a399)))). % 27.76/12.07 tff(c_15267, plain, (![X146_359]: (~c9_1(X146_359) | c3_1(X146_359) | ~c1_2(X146_359, a428) | c6_1(X146_359) | ~c2_2(X146_359, a388) | c1_2(X146_359, a388)))). % 27.76/12.07 tff(c_15277, plain, (~c1_2(a278, a428))). % 27.76/12.07 tff(c_15276, plain, (~c1_2(a308, a428))). % 27.76/12.07 tff(c_15273, plain, (~c1_2(a403, a428))). % 27.76/12.07 tff(c_15272, plain, (~c1_2(a369, a428))). % 27.76/12.07 tff(c_15221, plain, (![X146_194, X147_196]: (~c1_2(X146_194, a428) | c6_1(X146_194) | ~c2_2(X146_194, X147_196) | c1_2(X146_194, X147_196) | c7_2(X146_194, X147_196)))). % 27.76/12.07 tff(c_15206, plain, (![X81_345]: (~c10_2(X81_345, a428) | c6_1(X81_345) | c1_2(X81_345, a388) | ~c9_1(X81_345) | c3_1(X81_345) | c5_1(X81_345) | c2_1(X81_345) | c10_2(X81_345, a388)))). % 27.76/12.07 tff(c_15185, plain, (![X146_354]: (c9_1(X146_354) | c3_1(X146_354) | ~c10_2(X146_354, a428) | c6_1(X146_354) | ~c2_2(X146_354, a399) | c1_2(X146_354, a399)))). % 27.76/12.07 tff(c_15191, plain, (![X146_354]: (~c9_1(X146_354) | c3_1(X146_354) | ~c10_2(X146_354, a428) | c6_1(X146_354) | ~c2_2(X146_354, a388) | c1_2(X146_354, a388)))). % 27.76/12.07 tff(c_15199, plain, (~c10_2(a278, a428))). % 27.76/12.07 tff(c_15198, plain, (~c10_2(a403, a428))). % 27.76/12.07 tff(c_15197, plain, (~c10_2(a308, a428))). % 27.76/12.07 tff(c_15196, plain, (~c10_2(a369, a428))). % 27.76/12.07 tff(c_15142, plain, (![X146_194, X147_196]: (~c10_2(X146_194, a428) | c6_1(X146_194) | ~c2_2(X146_194, X147_196) | c1_2(X146_194, X147_196) | c7_2(X146_194, X147_196)))). % 27.76/12.07 tff(c_15131, plain, (![X146_194, X147_196]: (~c8_2(X146_194, a428) | c6_1(X146_194) | ~c2_2(X146_194, X147_196) | c1_2(X146_194, X147_196) | c7_2(X146_194, X147_196)))). % 27.76/12.07 tff(c_15126, plain, (~c1_1(a375))). % 27.76/12.07 tff(c_15111, plain, (~c6_2(a375, a377))). % 27.76/12.07 tff(c_15106, plain, (c1_2(a375, a376))). % 27.76/12.07 tff(c_15099, plain, (~c2_2(a375, a376))). % 27.76/12.07 tff(c_15026, plain, (![X81_345, X134_180]: (c4_2(X81_345, X134_180) | c6_2(X81_345, X134_180) | ~c10_2(X81_345, X134_180) | ~c1_1(X81_345) | c5_1(X81_345) | c2_1(X81_345) | c10_2(X81_345, a411) | c2_2(X81_345, a411)))). % 27.76/12.07 tff(c_15070, plain, (![X41_325]: (~c5_1(X41_325) | ~c10_2(X41_325, a413) | ~c2_2(X41_325, a399) | c9_1(X41_325) | c4_2(X41_325, a399) | ~c10_2(X41_325, a412) | c3_1(X41_325)))). % 27.76/12.07 tff(c_14970, plain, (![X41_342]: (~c4_2(X41_342, a412) | ~c5_1(X41_342) | ~c2_2(X41_342, a399) | c9_1(X41_342) | c4_2(X41_342, a399) | ~c10_2(X41_342, a413) | c3_1(X41_342)))). % 27.76/12.07 tff(c_15032, plain, (![X81_345]: (~c9_1(X81_345) | c3_1(X81_345) | c5_1(X81_345) | c2_1(X81_345) | c10_2(X81_345, a388) | c2_2(X81_345, a388)))). % 27.76/12.07 tff(c_15045, plain, (c2_2(a403, a404))). % 27.76/12.08 tff(c_15042, plain, (c2_2(a308, a309))). % 27.76/12.08 tff(c_15038, plain, (c10_2(a320, a322))). % 27.76/12.08 tff(c_15041, plain, (c7_2(a375, a376))). % 27.76/12.08 tff(c_15037, plain, (c2_2(a369, a370))). % 27.76/12.08 tff(c_14987, plain, (![X81_110, X82_112]: (c5_1(X81_110) | c2_1(X81_110) | c10_2(X81_110, X82_112) | c7_2(X81_110, X82_112) | c2_2(X81_110, X82_112)))). % 27.76/12.08 tff(c_14984, plain, (c3_1(a443))). % 27.76/12.08 tff(c_14983, plain, (~c8_2(a375, a377))). % 27.76/12.08 tff(c_14922, plain, (![X41_325]: (~c2_2(X41_325, a399) | c9_1(X41_325) | ~c10_2(X41_325, a399) | c3_1(X41_325) | c4_2(X41_325, a399)))). % 27.76/12.08 tff(c_14979, plain, (~c4_1(a375))). % 27.76/12.08 tff(c_14975, plain, (c8_1(a375))). % 27.76/12.08 tff(c_14644, plain, (![X41_325, X42_326]: (~c2_2(X41_325, a399) | c9_1(X41_325) | c4_2(X41_325, a399) | c4_2(X41_325, X42_326) | ~c10_2(X41_325, X42_326) | c3_1(X41_325)))). % 27.76/12.08 tff(c_14844, plain, (![X41_333]: (c10_1(X41_333) | c6_1(X41_333) | c3_2(X41_333, a440) | ~c9_1(X41_333) | ~c10_2(X41_333, a276) | c3_1(X41_333)))). % 27.76/12.08 tff(c_14893, plain, (![X41_329]: (~c5_1(X41_329) | ~c10_2(X41_329, a413) | ~c9_1(X41_329) | ~c10_2(X41_329, a412) | c3_1(X41_329)))). % 27.76/12.08 tff(c_14837, plain, (![X41_333]: (~c4_2(X41_333, a412) | ~c5_1(X41_333) | ~c9_1(X41_333) | ~c10_2(X41_333, a413) | c3_1(X41_333)))). % 27.76/12.08 tff(c_14868, plain, (![X41_329]: (~c10_2(X41_329, a380) | ~c9_1(X41_329) | ~c10_2(X41_329, a379) | c3_1(X41_329)))). % 27.76/12.08 tff(c_14848, plain, (![X41_333]: (~c2_2(X41_333, a380) | ~c9_1(X41_333) | ~c10_2(X41_333, a379) | c3_1(X41_333)))). % 27.76/12.08 tff(c_14847, plain, (![X41_333]: (~c1_2(X41_333, a380) | ~c9_1(X41_333) | ~c10_2(X41_333, a379) | c3_1(X41_333)))). % 27.89/12.08 tff(c_14846, plain, (![X41_333]: (~c4_2(X41_333, a379) | ~c9_1(X41_333) | ~c10_2(X41_333, a380) | c3_1(X41_333)))). % 27.89/12.08 tff(c_14758, plain, (![X41_329, X42_330]: (~c9_1(X41_329) | c4_2(X41_329, X42_330) | ~c10_2(X41_329, X42_330) | c3_1(X41_329)))). % 27.89/12.08 tff(c_14768, plain, (![X41_331]: (~c9_1(X41_331) | ~c10_2(X41_331, a388) | c3_1(X41_331)))). % 27.89/12.08 tff(c_14703, plain, (~c2_2(a320, a322))). % 27.89/12.08 tff(c_14700, plain, (~c1_1(a320))). % 27.89/12.08 tff(c_14691, plain, (~c6_2(a320, a321))). % 27.89/12.08 tff(c_14592, plain, (![X41_322, X42_324]: (c9_1(X41_322) | c4_2(X41_322, a399) | c7_2(X41_322, a399) | c4_2(X41_322, X42_324) | ~c10_2(X41_322, X42_324) | c3_1(X41_322)))). % 27.89/12.08 tff(c_14604, plain, (c3_1(a369))). % 27.89/12.08 tff(c_14603, plain, (c2_2(a320, a321))). % 27.89/12.08 tff(c_14534, plain, (![X41_57, X43_61, X42_60]: (c4_2(X41_57, X43_61) | c7_2(X41_57, X43_61) | c9_2(X41_57, X43_61) | c4_2(X41_57, X42_60) | ~c10_2(X41_57, X42_60) | c3_1(X41_57)))). % 27.89/12.08 tff(c_14530, plain, (~c7_2(a320, a322))). % 27.89/12.08 tff(c_14493, plain, (![X118_158]: (~c4_1(X118_158) | ~c10_1(X118_158) | ~c2_2(X118_158, a399) | ~c10_2(X118_158, a399) | c3_1(X118_158) | c9_1(X118_158)))). % 27.89/12.08 tff(c_14526, plain, (~c10_1(a280))). % 27.89/12.08 tff(c_14522, plain, (~c10_2(a443, a393))). % 27.89/12.08 tff(c_14525, plain, (c6_1(a320))). % 27.89/12.08 tff(c_14521, plain, (~c10_2(a424, a425))). % 27.89/12.08 tff(c_14518, plain, (~c10_2(a436, a437))). % 27.89/12.08 tff(c_14517, plain, (~c10_2(a395, a396))). % 27.89/12.09 tff(c_14514, plain, (~c10_2(a302, a303))). % 27.89/12.09 tff(c_14513, plain, (~c10_1(a408))). % 27.89/12.09 tff(c_14445, plain, (![X25_36, X26_38]: (~c4_1(X25_36) | ~c10_1(X25_36) | ~c2_2(X25_36, X26_38) | ~c10_2(X25_36, X26_38) | ~c3_2(X25_36, X26_38)))). % 27.89/12.09 tff(c_14403, plain, (~c7_2(a369, a370))). % 27.89/12.09 tff(c_14398, plain, (~c9_2(a369, a370))). % 27.89/12.09 tff(c_14395, plain, (c3_2(a369, a370))). % 27.89/12.09 tff(c_14392, plain, (~c10_2(a369, a370))). % 27.89/12.09 tff(c_14389, plain, (~c1_2(a369, a370))). % 27.89/12.09 tff(c_14378, plain, (~c4_2(a369, a370))). % 27.89/12.09 tff(c_14361, plain, (~c2_2(a358, a359))). % 27.89/12.09 tff(c_14344, plain, (c5_2(a358, a359))). % 27.89/12.09 tff(c_14341, plain, (~c2_1(a356))). % 27.89/12.09 tff(c_14332, plain, (~c10_2(a345, a346))). % 27.89/12.09 tff(c_14325, plain, (c8_2(a345, a346))). % 27.89/12.09 tff(c_14322, plain, (~c1_1(a369))). % 27.89/12.09 tff(c_14314, plain, (![X76_103]: (~c1_2(X76_103, a347) | ~c4_1(X76_103)))). % 27.89/12.09 tff(c_14305, plain, (c2_2(a345, a346))). % 27.89/12.09 tff(c_14290, plain, (c10_2(a358, a359))). % 27.89/12.09 tff(c_14287, plain, (~c2_1(a369))). % 27.89/12.09 tff(c_14280, plain, (~c9_1(a403))). % 27.89/12.09 tff(c_14246, plain, (![X125_168]: (~c4_2(a403, X125_168) | ~c6_2(a403, X125_168) | ~c10_2(a403, X125_168)))). % 27.89/12.09 tff(c_14203, plain, (c1_1(a345))). % 27.89/12.09 tff(c_14193, plain, (~c2_1(a358))). % 27.89/12.09 tff(c_14196, plain, (~c3_1(a358))). % 27.89/12.09 tff(c_14192, plain, (~c1_1(a358))). % 27.89/12.09 tff(c_14183, plain, (~c8_1(a358))). % 27.89/12.09 tff(c_14118, plain, (~c1_1(a280))). % 27.89/12.09 tff(c_14112, plain, (![X133_178, X134_180]: (~c7_2(X133_178, a411) | c4_2(X133_178, X134_180) | c6_2(X133_178, X134_180) | ~c10_2(X133_178, X134_180) | ~c1_1(X133_178)))). % 27.89/12.09 tff(c_14103, plain, (~c2_2(a280, a412))). % 27.89/12.09 tff(c_14061, plain, (![X160_212]: (~c5_1(X160_212) | c9_1(X160_212) | ~c3_2(X160_212, a413) | ~c10_2(X160_212, a413) | ~c4_1(X160_212) | c1_1(X160_212) | ~c10_2(X160_212, a412) | ~c1_2(X160_212, a412)))). % 27.89/12.09 tff(c_14075, plain, (![X66_90]: (~c5_1(X66_90) | ~c4_1(X66_90) | c1_1(X66_90) | ~c10_2(X66_90, a413) | ~c1_2(X66_90, a413) | c9_1(X66_90) | ~c3_2(X66_90, a412) | ~c10_2(X66_90, a412)))). % 27.89/12.09 tff(c_14074, plain, (![X160_212]: (~c5_1(X160_212) | ~c10_2(X160_212, a413) | ~c1_2(X160_212, a413) | ~c4_1(X160_212) | c1_1(X160_212) | ~c10_2(X160_212, a412) | ~c1_2(X160_212, a412)))). % 27.89/12.09 tff(c_14084, plain, (~c2_2(a280, a413))). % 27.89/12.09 tff(c_14062, plain, (![X66_90]: (~c5_1(X66_90) | ~c3_2(X66_90, a413) | ~c10_2(X66_90, a413) | c9_1(X66_90) | ~c3_2(X66_90, a412) | ~c10_2(X66_90, a412)))). % 27.89/12.09 tff(c_14050, plain, (![X160_212]: (~c4_2(X160_212, a412) | ~c5_1(X160_212) | ~c4_1(X160_212) | c1_1(X160_212) | ~c10_2(X160_212, a413) | ~c1_2(X160_212, a413)))). % 27.89/12.09 tff(c_14051, plain, (![X66_90]: (~c4_2(X66_90, a412) | ~c5_1(X66_90) | c9_1(X66_90) | ~c3_2(X66_90, a413) | ~c10_2(X66_90, a413)))). % 27.89/12.09 tff(c_14040, plain, (![X135_181]: (~c4_2(X135_181, a412) | ~c4_2(X135_181, a413) | ~c5_1(X135_181)))). % 27.89/12.09 tff(c_14024, plain, (![X133_178, X134_180]: (~c2_2(X133_178, a411) | c4_2(X133_178, X134_180) | c6_2(X133_178, X134_180) | ~c10_2(X133_178, X134_180) | ~c1_1(X133_178)))). % 27.89/12.09 tff(c_14025, plain, (~c2_1(a427))). % 27.89/12.09 tff(c_14017, plain, (c4_1(a427))). % 27.89/12.09 tff(c_14013, plain, (~c7_1(a427))). % 27.89/12.09 tff(c_14002, plain, (![X133_178, X134_180]: (c3_2(X133_178, a411) | c4_2(X133_178, X134_180) | c6_2(X133_178, X134_180) | ~c10_2(X133_178, X134_180) | ~c1_1(X133_178)))). % 27.89/12.09 tff(c_13987, plain, (~c2_2(a280, a399))). % 27.89/12.10 tff(c_13972, plain, (![X34_48]: (c9_1(X34_48) | c3_1(X34_48) | ~c2_2(X34_48, a399) | ~c7_2(X34_48, a399)))). % 27.89/12.10 tff(c_13976, plain, (~c10_2(a280, a399))). % 27.89/12.10 tff(c_13962, plain, (![X118_158]: (~c9_2(X118_158, a399) | c3_1(X118_158) | c9_1(X118_158)))). % 27.89/12.10 tff(c_13957, plain, (~c10_2(a332, a399))). % 27.89/12.10 tff(c_13945, plain, (![X118_158]: (c3_2(X118_158, a399) | c3_1(X118_158) | c9_1(X118_158)))). % 27.89/12.10 tff(c_13937, plain, (![X118_158]: (c8_2(X118_158, a399) | c3_1(X118_158) | c9_1(X118_158)))). % 27.89/12.10 tff(c_13932, plain, (~c10_1(a362))). % 27.89/12.10 tff(c_13888, plain, (![X160_293]: (~c9_1(X160_293) | c10_1(X160_293) | c6_1(X160_293) | c3_2(X160_293, a440) | ~c4_1(X160_293) | c1_1(X160_293) | ~c10_2(X160_293, a276) | ~c1_2(X160_293, a276)))). % 27.89/12.10 tff(c_13887, plain, (![X160_293]: (c9_1(X160_293) | ~c3_2(X160_293, a380) | ~c10_2(X160_293, a380) | ~c4_1(X160_293) | c1_1(X160_293) | ~c10_2(X160_293, a379) | ~c1_2(X160_293, a379)))). % 27.89/12.10 tff(c_13892, plain, (![X160_293]: (~c2_2(X160_293, a380) | ~c4_1(X160_293) | c1_1(X160_293) | ~c10_2(X160_293, a379) | ~c1_2(X160_293, a379)))). % 27.89/12.10 tff(c_13891, plain, (![X160_293]: (~c1_2(X160_293, a380) | ~c4_1(X160_293) | c1_1(X160_293) | ~c10_2(X160_293, a379) | ~c1_2(X160_293, a379)))). % 27.89/12.10 tff(c_13832, plain, (![X160_212, X161_214]: (~c4_1(X160_212) | c1_1(X160_212) | ~c10_2(X160_212, X161_214) | c4_2(X160_212, X161_214) | ~c1_2(X160_212, X161_214)))). % 27.89/12.10 tff(c_13828, plain, (c5_1(a317))). % 27.89/12.10 tff(c_13817, plain, (~c8_2(a365, a366))). % 27.89/12.10 tff(c_13812, plain, (c1_2(a365, a366))). % 27.89/12.10 tff(c_13807, plain, (~c2_1(a317))). % 27.89/12.10 tff(c_13802, plain, (c4_1(a317))). % 27.89/12.10 tff(c_13794, plain, (c4_2(a365, a366))). % 27.89/12.10 tff(c_13784, plain, (![X128_171]: (c10_2(X128_171, a407) | c9_1(X128_171) | ~c2_1(X128_171)))). % 27.89/12.10 tff(c_13774, plain, (~c2_1(a416))). % 27.89/12.10 tff(c_13771, plain, (~c2_1(a443))). % 27.89/12.10 tff(c_13759, plain, (![X128_171]: (c5_2(X128_171, a407) | c9_1(X128_171) | ~c2_1(X128_171)))). % 27.89/12.10 tff(c_13746, plain, (![X128_171]: (~c2_2(X128_171, a407) | c9_1(X128_171) | ~c2_1(X128_171)))). % 27.89/12.10 tff(c_13740, plain, (c3_1(a365))). % 27.89/12.10 tff(c_13735, plain, (c2_2(a408, a410))). % 27.89/12.10 tff(c_13730, plain, (~c10_2(a302, a276))). % 27.89/12.10 tff(c_13727, plain, (c3_2(a302, a303))). % 27.89/12.10 tff(c_13722, plain, (~c4_2(a302, a276))). % 27.89/12.10 tff(c_13712, plain, (~c5_2(a302, a303))). % 27.89/12.10 tff(c_13701, plain, (~c10_2(a408, a276))). % 27.89/12.10 tff(c_13700, plain, (~c1_1(a365))). % 27.89/12.10 tff(c_13692, plain, (c3_2(a408, a409))). % 27.89/12.10 tff(c_13695, plain, (c7_1(a365))). % 27.89/12.10 tff(c_13684, plain, (~c4_2(a408, a276))). % 27.89/12.10 tff(c_13687, plain, (c2_2(a408, a409))). % 27.89/12.10 tff(c_13683, plain, (~c10_2(a408, a410))). % 27.89/12.10 tff(c_13673, plain, (~c5_2(a408, a409))). % 27.89/12.10 tff(c_13670, plain, (~c1_1(a434))). % 27.89/12.10 tff(c_13669, plain, (c10_2(a408, a409))). % 27.89/12.10 tff(c_13666, plain, (~c1_1(a395))). % 27.89/12.10 tff(c_13599, plain, (![X171_224]: (~c4_1(X171_224) | ~c7_1(X171_224) | ~c1_1(X171_224)))). % 27.89/12.10 tff(c_13648, plain, (~c2_1(a296))). % 27.89/12.10 tff(c_13647, plain, (c6_2(a302, a303))). % 27.89/12.10 tff(c_13644, plain, (~c2_1(a297))). % 27.89/12.10 tff(c_13639, plain, (~c4_2(a408, a410))). % 27.89/12.10 tff(c_13636, plain, (~c2_1(a355))). % 27.89/12.10 tff(c_13635, plain, (~c2_1(a302))). % 27.89/12.10 tff(c_13631, plain, (c3_1(a386))). % 27.89/12.10 tff(c_13602, plain, (![X15_24]: (~c4_1(X15_24) | ~c2_1(X15_24) | c3_1(X15_24)))). % 27.89/12.10 tff(c_13603, plain, (~c4_1(a444))). % 27.89/12.10 tff(c_13601, plain, (~c4_1(a405))). % 27.89/12.10 tff(c_13600, plain, (~c4_1(a442))). % 27.89/12.10 tff(c_13582, plain, (![X31_45]: (~c8_1(X31_45) | ~c4_1(X31_45)))). % 27.89/12.10 tff(c_13528, plain, (c10_1(a302))). % 27.89/12.11 tff(c_13495, plain, (~c2_1(a300))). % 27.89/12.11 tff(c_13494, plain, (~c1_1(a300))). % 27.89/12.11 tff(c_13483, plain, (~c8_1(a300))). % 27.89/12.11 tff(c_13480, plain, (c4_1(a302))). % 27.89/12.11 tff(c_13476, plain, (~c7_1(a302))). % 27.89/12.11 tff(c_13468, plain, (~c7_2(a403, a404))). % 27.89/12.11 tff(c_13465, plain, (c3_2(a403, a404))). % 27.89/12.11 tff(c_13444, plain, (~c1_1(a352))). % 27.89/12.11 tff(c_13442, plain, (~c1_1(a420))). % 27.89/12.11 tff(c_13432, plain, (![X171_224]: (~c7_1(X171_224) | c8_1(X171_224) | ~c1_1(X171_224)))). % 27.89/12.11 tff(c_13424, plain, (c5_2(a403, a404))). % 27.89/12.11 tff(c_13405, plain, (c3_1(a381))). % 27.89/12.11 tff(c_13402, plain, (~c2_2(a443, a380))). % 27.89/12.11 tff(c_13401, plain, (~c1_2(a443, a380))). % 27.89/12.11 tff(c_13398, plain, (~c10_2(a443, a380))). % 27.89/12.11 tff(c_13393, plain, (~c4_2(a443, a380))). % 27.89/12.11 tff(c_13374, plain, (![X35_284]: (~c3_2(a443, X35_284) | ~c2_2(a443, X35_284) | ~c7_2(a443, X35_284)))). % 27.89/12.11 tff(c_13373, plain, (~c2_2(a323, a324))). % 27.89/12.11 tff(c_13344, plain, (![X34_48, X35_50]: (c9_1(X34_48) | c3_1(X34_48) | ~c2_2(X34_48, X35_50) | c9_2(X34_48, X35_50) | ~c7_2(X34_48, X35_50)))). % 27.89/12.11 tff(c_13341, plain, (~c3_2(a283, a284))). % 27.89/12.11 tff(c_13340, plain, (~c8_2(a283, a284))). % 27.89/12.11 tff(c_13261, plain, (![X113_153]: (~c4_2(X113_153, a388) | ~c9_1(X113_153) | c3_1(X113_153)))). % 27.89/12.11 tff(c_13258, plain, (~c2_1(a283))). % 27.89/12.11 tff(c_13251, plain, (![X113_153]: (~c9_2(X113_153, a388) | ~c9_1(X113_153) | c3_1(X113_153)))). % 27.89/12.11 tff(c_13247, plain, (c4_1(a283))). % 27.89/12.11 tff(c_13246, plain, (~c9_1(a280))). % 27.89/12.11 tff(c_13239, plain, (![X113_153]: (~c7_2(X113_153, a388) | ~c9_1(X113_153) | c3_1(X113_153)))). % 27.89/12.11 tff(c_13234, plain, (~c2_2(a280, a379))). % 27.89/12.11 tff(c_13220, plain, (![X66_90]: (~c3_2(X66_90, a380) | ~c10_2(X66_90, a380) | c9_1(X66_90) | ~c3_2(X66_90, a379) | ~c10_2(X66_90, a379)))). % 27.89/12.11 tff(c_13198, plain, (![X66_274]: (~c1_2(X66_274, a380) | c9_1(X66_274) | ~c3_2(X66_274, a379) | ~c10_2(X66_274, a379)))). % 27.89/12.11 tff(c_13197, plain, (![X66_274]: (~c4_2(X66_274, a379) | c9_1(X66_274) | ~c3_2(X66_274, a380) | ~c10_2(X66_274, a380)))). % 27.89/12.11 tff(c_13199, plain, (![X66_274]: (~c2_2(X66_274, a380) | c9_1(X66_274) | ~c3_2(X66_274, a379) | ~c10_2(X66_274, a379)))). % 27.89/12.11 tff(c_13206, plain, (~c10_2(a278, a380))). % 27.89/12.11 tff(c_13205, plain, (~c10_2(a416, a417))). % 27.89/12.11 tff(c_13202, plain, (~c10_2(a325, a326))). % 27.89/12.11 tff(c_13168, plain, (![X66_90, X67_92]: (c9_1(X66_90) | ~c3_2(X66_90, X67_92) | ~c10_2(X66_90, X67_92) | c4_2(X66_90, X67_92)))). % 27.89/12.11 tff(c_13144, plain, (![X1_9, X2_11]: (c8_2(X1_9, a276) | c6_1(X1_9) | c5_2(X1_9, X2_11) | c3_2(X1_9, X2_11)))). % 27.89/12.11 tff(c_13135, plain, (![X1_269]: (~c9_1(X1_269) | c10_1(X1_269) | ~c4_2(X1_269, a276) | c6_1(X1_269) | c3_2(X1_269, a440)))). % 27.89/12.11 tff(c_13106, plain, (![X1_9, X2_11]: (~c4_2(X1_9, a276) | c6_1(X1_9) | c5_2(X1_9, X2_11) | c3_2(X1_9, X2_11)))). % 27.89/12.11 tff(c_13101, plain, (c6_1(a416))). % 27.89/12.11 tff(c_13098, plain, (~c9_1(a332))). % 27.89/12.11 tff(c_13081, plain, (![X1_266]: (~c9_1(X1_266) | c10_1(X1_266) | c2_2(X1_266, a276) | c6_1(X1_266) | c3_2(X1_266, a440)))). % 27.89/12.11 tff(c_13089, plain, (c6_1(a443))). % 27.89/12.11 tff(c_13087, plain, (c3_2(a443, a393))). % 27.89/12.11 tff(c_13085, plain, (c3_2(a424, a425))). % 27.89/12.11 tff(c_13084, plain, (c3_2(a381, a382))). % 27.89/12.11 tff(c_13055, plain, (![X1_9, X2_11]: (c2_2(X1_9, a276) | c6_1(X1_9) | c5_2(X1_9, X2_11) | c3_2(X1_9, X2_11)))). % 27.89/12.11 tff(c_12799, plain, (c6_2(a395, a396))). % 27.89/12.11 tff(c_12793, plain, (~c5_2(a443, a393))). % 27.89/12.11 tff(c_12792, plain, (c3_2(a395, a396))). % 27.89/12.11 tff(c_12785, plain, (![X115_155]: (~c2_2(X115_155, a391) | ~c6_2(X115_155, a392) | ~c8_2(X115_155, a393)))). % 27.89/12.11 tff(c_12783, plain, (c9_2(a395, a396))). % 27.89/12.11 tff(c_12780, plain, (~c4_1(a394))). % 27.89/12.11 tff(c_12773, plain, (![X169_222]: (~c5_2(a443, X169_222) | c6_2(a443, X169_222) | c8_2(a443, X169_222)))). % 27.89/12.11 tff(c_12759, plain, (![X168_221]: (~c5_2(a443, X168_221) | c10_2(a443, X168_221) | c3_2(a443, X168_221)))). % 27.89/12.11 tff(c_12755, plain, (~c10_1(a403))). % 27.89/12.11 tff(c_12754, plain, (~c10_1(a406))). % 27.89/12.11 tff(c_12753, plain, (~c10_1(a350))). % 27.89/12.11 tff(c_12733, plain, (![X52_72]: (~c2_1(X52_72) | ~c10_1(X52_72) | c3_1(X52_72)))). % 27.89/12.11 tff(c_12688, plain, (c8_1(a442))). % 27.89/12.11 tff(c_12665, plain, (~c1_2(a416, a417))). % 27.89/12.11 tff(c_12653, plain, (![X139_186]: (~c5_2(a416, X139_186) | ~c1_2(a416, X139_186) | c4_2(a416, X139_186)))). % 27.89/12.11 tff(c_12641, plain, (~c1_1(a443))). % 27.89/12.11 tff(c_12634, plain, (![X170_223]: (~c9_2(a443, X170_223) | ~c3_2(a443, X170_223)))). % 27.89/12.11 tff(c_12610, plain, (c7_2(a323, a324))). % 27.89/12.12 tff(c_12541, plain, (c4_2(a323, a324))). % 27.89/12.12 tff(c_12531, plain, (~c1_2(a434, a435))). % 27.89/12.12 tff(c_12527, plain, (c7_1(a395))). % 27.89/12.12 tff(c_12520, plain, (~c2_2(a310, a311))). % 27.89/12.12 tff(c_12512, plain, (c9_2(a434, a435))). % 27.89/12.12 tff(c_12508, plain, (c4_2(a310, a311))). % 27.89/12.12 tff(c_12495, plain, (~c2_1(a395))). % 27.89/12.12 tff(c_12488, plain, (~c7_2(a308, a309))). % 27.89/12.12 tff(c_12472, plain, (c4_2(a434, a435))). % 27.89/12.12 tff(c_12455, plain, (~c8_2(a414, a415))). % 27.89/12.12 tff(c_12448, plain, (c6_2(a414, a415))). % 27.89/12.12 tff(c_12444, plain, (c2_2(a414, a415))). % 27.89/12.12 tff(c_12430, plain, (~c3_1(a406))). % 27.89/12.12 tff(c_12414, plain, (c8_1(a405))). % 27.89/12.12 tff(c_12409, plain, (~c10_2(a280, a402))). % 27.89/12.12 tff(c_12402, plain, (![X124_167]: (~c9_2(X124_167, a402) | ~c2_1(X124_167) | ~c10_1(X124_167)))). % 27.89/12.12 tff(c_12397, plain, (~c5_1(a308))). % 27.89/12.12 tff(c_12396, plain, (~c6_2(a310, a311))). % 27.89/12.12 tff(c_12375, plain, (~c10_1(a308))). % 27.89/12.12 tff(c_12369, plain, (![X124_167]: (~c2_2(X124_167, a402) | ~c2_1(X124_167) | ~c10_1(X124_167)))). % 27.89/12.12 tff(c_12368, plain, (~c2_1(a420))). % 27.89/12.12 tff(c_12367, plain, (~c2_1(a352))). % 27.89/12.12 tff(c_12353, plain, (![X15_24]: (c8_1(X15_24) | ~c2_1(X15_24) | c3_1(X15_24)))). % 27.89/12.12 tff(c_12357, plain, (c7_1(a434))). % 27.89/12.12 tff(c_12308, plain, (~c3_1(a403))). % 27.89/12.12 tff(c_12302, plain, (c2_1(a431))). % 27.89/12.12 tff(c_12274, plain, (c6_1(a431))). % 27.89/12.12 tff(c_12248, plain, (c6_1(a296))). % 27.89/12.12 tff(c_12245, plain, (~c4_1(a431))). % 27.89/12.12 tff(c_12235, plain, (![X8_17]: (c4_2(a280, X8_17) | c6_2(a280, X8_17) | c7_2(a280, X8_17)))). % 27.89/12.12 tff(c_12231, plain, (~c2_1(a310))). % 27.89/12.12 tff(c_12209, plain, (~c5_1(a310))). % 27.89/12.12 tff(c_12202, plain, (c4_1(a296))). % 27.89/12.12 tff(c_12198, plain, (~c7_1(a296))). % 27.89/12.12 tff(c_12193, plain, (c10_1(a296))). % 27.89/12.12 tff(c_12183, plain, (c4_1(a297))). % 27.89/12.12 tff(c_12179, plain, (~c7_1(a297))). % 27.89/12.12 tff(c_12169, plain, (~c10_2(a381, a354))). % 27.89/12.12 tff(c_12160, plain, (![X106_144]: (c8_2(a381, X106_144) | ~c10_2(a381, X106_144) | ~c9_2(a381, X106_144)))). % 27.89/12.12 tff(c_12146, plain, (![X7_16]: (c6_2(a280, X7_16) | c9_2(a280, X7_16) | ~c10_2(a280, X7_16)))). % 27.89/12.12 tff(c_12138, plain, (~c2_2(a278, a380))). % 27.89/12.12 tff(c_12137, plain, (~c1_2(a278, a380))). % 27.89/12.12 tff(c_12136, plain, (~c4_2(a278, a380))). % 27.89/12.12 tff(c_12119, plain, (![X5_14]: (~c2_2(a278, X5_14) | c4_2(a278, X5_14) | ~c7_2(a278, X5_14)))). % 27.89/12.12 tff(c_12102, plain, (c4_1(a386))). % 27.89/12.12 tff(c_12105, plain, (![X9_18]: (c3_2(a280, X9_18) | c1_2(a280, X9_18) | ~c2_2(a280, X9_18)))). % 27.89/12.12 tff(c_12098, plain, (~c7_1(a386))). % 27.89/12.12 tff(c_12093, plain, (c9_1(a386))). % 27.89/12.12 tff(c_12089, plain, (![X77_104]: (c5_2(X77_104, a354) | c7_1(X77_104) | ~c1_1(X77_104)))). % 27.89/12.12 tff(c_12082, plain, (~c2_2(a294, a295))). % 27.89/12.12 tff(c_12080, plain, (~c1_2(a294, a295))). % 27.89/12.12 tff(c_12076, plain, (![X77_104]: (c9_2(X77_104, a354) | c7_1(X77_104) | ~c1_1(X77_104)))). % 27.89/12.12 tff(c_12067, plain, (![X77_104]: (c4_2(X77_104, a354) | c7_1(X77_104) | ~c1_1(X77_104)))). % 27.89/12.12 tff(c_12051, plain, (~c6_1(a355))). % 27.89/12.12 tff(c_12048, plain, (c2_1(a386))). % 27.89/12.12 tff(c_12037, plain, (c4_1(a355))). % 27.89/12.12 tff(c_12033, plain, (~c7_1(a355))). % 27.89/12.12 tff(c_12021, plain, (c3_2(a294, a295))). % 27.89/12.12 tff(c_12003, plain, (![X57_78]: (~c1_2(X57_78, a328) | c6_1(X57_78) | c3_1(X57_78)))). % 27.89/12.12 tff(c_12001, plain, (c8_1(a444))). % 27.89/12.12 tff(c_11988, plain, (![X57_78]: (c2_2(X57_78, a328) | c6_1(X57_78) | c3_1(X57_78)))). % 27.89/12.12 tff(c_11983, plain, (![X57_78]: (c8_2(X57_78, a328) | c6_1(X57_78) | c3_1(X57_78)))). % 28.09/12.12 tff(c_11979, plain, (~c4_1(a294))). % 28.09/12.12 tff(c_11973, plain, (![X60_81]: (~c10_2(a332, X60_81) | ~c3_2(a332, X60_81)))). % 28.09/12.12 tff(c_11966, plain, (![X163_216]: (~c5_2(X163_216, a440) | ~c9_1(X163_216) | c10_1(X163_216)))). % 28.09/12.12 tff(c_11963, plain, (![X105_143]: (~c4_2(X105_143, a379) | ~c4_2(X105_143, a380)))). % 28.09/12.12 tff(c_11959, plain, (![X105_143]: (c7_2(X105_143, a379) | ~c4_2(X105_143, a380)))). % 28.09/12.12 tff(c_11955, plain, (![X105_143]: (c7_2(X105_143, a379) | ~c1_2(X105_143, a380)))). % 28.09/12.12 tff(c_11951, plain, (~c1_1(a330))). % 28.09/12.12 tff(c_11947, plain, (![X163_216]: (c1_2(X163_216, a440) | ~c9_1(X163_216) | c10_1(X163_216)))). % 28.09/12.12 tff(c_11944, plain, (![X163_216]: (c6_2(X163_216, a440) | ~c9_1(X163_216) | c10_1(X163_216)))). % 28.09/12.12 tff(c_11941, plain, (![X105_143]: (c6_2(X105_143, a379) | ~c1_2(X105_143, a380)))). % 28.09/12.12 tff(c_11937, plain, (![X105_143]: (c6_2(X105_143, a379) | ~c4_2(X105_143, a380)))). % 28.09/12.12 tff(c_11933, plain, (![X105_143]: (~c4_2(X105_143, a379) | ~c1_2(X105_143, a380)))). % 28.09/12.12 tff(c_11929, plain, (![X105_143]: (~c4_2(X105_143, a379) | ~c2_2(X105_143, a380)))). % 28.09/12.12 tff(c_11925, plain, (![X105_143]: (c6_2(X105_143, a379) | ~c2_2(X105_143, a380)))). % 28.09/12.12 tff(c_11920, plain, (![X105_143]: (c7_2(X105_143, a379) | ~c2_2(X105_143, a380)))). % 28.09/12.12 tff(c_11880, plain, (c6_2(a416, a418))). % 28.09/12.12 tff(c_11869, plain, (c8_2(a416, a418))). % 28.09/12.12 tff(c_11864, plain, (c5_2(a416, a417))). % 28.09/12.12 tff(c_11840, plain, (c7_2(a416, a417))). % 28.09/12.12 tff(c_11831, plain, (c5_2(a325, a326))). % 28.09/12.12 tff(c_11805, plain, (~c9_2(a323, a324))). % 28.09/12.12 tff(c_11800, plain, (c7_2(a325, a326))). % 28.09/12.13 tff(c_11797, plain, (~c4_2(a325, a326))). % 28.09/12.13 tff(c_11774, plain, (c3_2(a436, a437))). % 28.09/12.13 tff(c_11772, plain, (~c5_2(a424, a425))). % 28.09/12.13 tff(c_11734, plain, (~c1_1(a414))). % 28.09/12.13 tff(c_11730, plain, (c7_2(a424, a425))). % 28.09/12.13 tff(c_11723, plain, (~c6_1(a434))). % 28.09/12.13 tff(c_11719, plain, (c8_2(a436, a437))). % 28.09/12.13 tff(c_11710, plain, (~c4_2(a416, a417))). % 28.09/12.13 tff(c_11703, plain, (c4_2(a436, a437))). % 28.09/12.13 tff(c_11664, plain, (~c10_1(a323))). % 28.09/12.13 tff(c_11659, plain, (~c3_1(a323))). % 28.09/12.13 tff(c_11654, plain, (c10_2(a420, a421))). % 28.09/12.13 tff(c_11652, plain, (c8_2(a381, a382))). % 28.09/12.13 tff(c_11650, plain, (~c2_2(a381, a382))). % 28.09/12.13 tff(c_11646, plain, (~c3_2(a420, a421))). % 28.09/12.13 tff(c_11638, plain, (~c5_2(a381, a382))). % 28.09/12.13 tff(c_11608, plain, (~c5_1(a424))). % 28.09/12.13 tff(c_11598, plain, (~c2_1(a436))). % 28.09/12.13 tff(c_11585, plain, (c7_2(a420, a421))). % 28.09/12.13 tff(c_11570, plain, (![X6_15]: (c4_1(X6_15) | c7_1(X6_15)))). % 28.09/12.13 tff(c_11568, plain, (c8_2(a278, a279))). % 28.09/12.13 tff(c_11563, plain, (c3_2(a278, a279))). % 28.09/12.13 tff(c_11554, plain, (c4_2(a278, a279))). % 28.09/12.13 tff(c_11545, plain, (~c1_1(a325))). % 28.09/12.13 tff(c_11537, plain, (~c8_1(a420))). % 28.09/12.13 tff(c_11534, plain, (~c4_1(a278))). % 28.09/12.13 tff(c_11527, plain, (c1_1(a381))). % 28.09/12.13 tff(c_11513, plain, (![X105_143]: (ndr1_1(X105_143)))). % 28.09/12.13 tff(c_11503, plain, (c7_1(a420))). % 28.09/12.13 tff(c_11490, plain, (c2_0)). % 28.09/12.13 tff(c_11476, plain, (~c6_1(a332))). % 28.09/12.13 tff(c_11475, plain, (~c10_1(a332))). % 28.09/12.13 tff(c_11474, plain, (~c1_0)). % 28.09/12.13 tff(c_11464, plain, (c10_0)). % 28.09/12.13 tff(c_11463, plain, (c3_0)). % 28.09/12.13 tff(c_11461, plain, (~c8_1(a352))). % 28.09/12.13 tff(c_11459, plain, (~c8_0)). % 28.09/12.13 tff(c_11455, plain, (c7_0)). % 28.09/12.13 tff(c_11454, plain, (~c3_1(a350))). % 28.09/12.13 tff(c_11453, plain, (~c6_1(a348))). % 28.09/12.13 tff(c_11452, plain, (c5_0)). % 28.09/12.13 tff(c_11451, plain, (c4_0)). % 28.09/12.13 tff(c_11450, plain, (c9_0)). % 28.09/12.13 tff(c_11449, plain, (~c6_0)). % 28.09/12.13 tff(c_5828, plain, (ndr1_0)). % 28.09/12.13 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.09/12.13 %------------------------------------------------------------------------------