%------------------------------------------------------------------------------ % 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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n010.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 : Satisfiable 15.03s 5.00s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN420-1 : TPTP v9.0.0. Released v2.1.0. % 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n010.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:24:03 EDT 2025 % 0.13/0.35 % CPUTime : % 15.03/5.00 % 15.03/5.00 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.03/5.00 % 15.03/5.00 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.03/5.01 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ssSkP7 > ssSkP6 > ssSkP5 > ssSkP4 > ssSkP3 > ssSkP2 > ssSkP1 > ssSkP0 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ssSkC9 > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC38 > ssSkC37 > ssSkC36 > ssSkC35 > ssSkC34 > ssSkC33 > ssSkC32 > ssSkC31 > ssSkC30 > ssSkC3 > ssSkC29 > ssSkC28 > ssSkC27 > ssSkC26 > ssSkC25 > ssSkC24 > ssSkC23 > ssSkC22 > ssSkC21 > ssSkC20 > ssSkC2 > ssSkC19 > ssSkC18 > ssSkC17 > ssSkC16 > ssSkC15 > ssSkC14 > ssSkC13 > ssSkC12 > ssSkC11 > ssSkC10 > ssSkC1 > ssSkC0 > 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 > a396 > a395 > a394 > a393 > a392 > a391 > a390 > a389 > a388 > a387 > a386 > a385 > a384 > a383 > a382 > a381 > a380 > a379 > 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 % 15.03/5.01 % 15.03/5.01 %Foreground sorts: % 15.03/5.01 % 15.03/5.01 % 15.03/5.01 %Background operators: % 15.03/5.01 % 15.03/5.01 % 15.03/5.01 %Foreground operators: % 15.03/5.01 tff(a430, type, a430: $i). % 15.03/5.01 tff(c7_0, type, c7_0: $o). % 15.03/5.01 tff(a323, type, a323: $i). % 15.03/5.01 tff(a421, type, a421: $i). % 15.03/5.01 tff(ssSkC8, type, ssSkC8: $o). % 15.03/5.01 tff(a316, type, a316: $i). % 15.03/5.01 tff(a389, type, a389: $i). % 15.03/5.01 tff(a347, type, a347: $i). % 15.03/5.01 tff(a281, type, a281: $i). % 15.03/5.01 tff(a433, type, a433: $i). % 15.03/5.01 tff(ssSkC7, type, ssSkC7: $o). % 15.03/5.01 tff(a322, type, a322: $i). % 15.03/5.01 tff(ssSkC21, type, ssSkC21: $o). % 15.03/5.01 tff(a313, type, a313: $i). % 15.03/5.01 tff(a292, type, a292: $i). % 15.03/5.01 tff(a435, type, a435: $i). % 15.03/5.01 tff(a336, type, a336: $i). % 15.03/5.01 tff(a422, type, a422: $i). % 15.03/5.01 tff(c4_0, type, c4_0: $o). % 15.03/5.01 tff(a335, type, a335: $i). % 15.03/5.01 tff(a431, type, a431: $i). % 15.03/5.01 tff(a280, type, a280: $i). % 15.03/5.01 tff(a326, type, a326: $i). % 15.03/5.01 tff(ssSkC10, type, ssSkC10: $o). % 15.03/5.01 tff(a297, type, a297: $i). % 15.03/5.01 tff(a290, type, a290: $i). % 15.03/5.01 tff(a446, type, a446: $i). % 15.03/5.01 tff(ssSkP0, type, ssSkP0: $i > $o). % 15.03/5.01 tff(a359, type, a359: $i). % 15.03/5.01 tff(ssSkC6, type, ssSkC6: $o). % 15.03/5.01 tff(c3_0, type, c3_0: $o). % 15.03/5.01 tff(a386, type, a386: $i). % 15.03/5.01 tff(a399, type, a399: $i). % 15.03/5.01 tff(a423, type, a423: $i). % 15.03/5.01 tff(ssSkP7, type, ssSkP7: $i > $o). % 15.03/5.01 tff(a338, type, a338: $i). % 15.03/5.01 tff(a398, type, a398: $i). % 15.03/5.01 tff(c1_2, type, c1_2: ($i * $i) > $o). % 15.03/5.01 tff(a334, type, a334: $i). % 15.03/5.01 tff(a384, type, a384: $i). % 15.03/5.01 tff(a373, type, a373: $i). % 15.03/5.01 tff(a387, type, a387: $i). % 15.03/5.01 tff(a272, type, a272: $i). % 15.03/5.01 tff(a309, type, a309: $i). % 15.03/5.01 tff(a302, type, a302: $i). % 15.03/5.01 tff(a337, type, a337: $i). % 15.03/5.01 tff(ssSkC23, type, ssSkC23: $o). % 15.03/5.01 tff(a306, type, a306: $i). % 15.03/5.01 tff(ssSkC3, type, ssSkC3: $o). % 15.03/5.01 tff(a368, type, a368: $i). % 15.03/5.01 tff(a432, type, a432: $i). % 15.03/5.01 tff(a367, type, a367: $i). % 15.03/5.01 tff(a417, type, a417: $i). % 15.03/5.01 tff(a320, type, a320: $i). % 15.03/5.01 tff(a301, type, a301: $i). % 15.03/5.01 tff(a401, type, a401: $i). % 15.03/5.01 tff(a354, type, a354: $i). % 15.03/5.01 tff(a284, type, a284: $i). % 15.03/5.01 tff(ssSkP2, type, ssSkP2: $i > $o). % 15.03/5.01 tff(ssSkC19, type, ssSkC19: $o). % 15.03/5.01 tff(ssSkC28, type, ssSkC28: $o). % 15.03/5.01 tff(a295, type, a295: $i). % 15.03/5.01 tff(a310, type, a310: $i). % 15.03/5.01 tff(a407, type, a407: $i). % 15.03/5.01 tff(a285, type, a285: $i). % 15.03/5.01 tff(a348, type, a348: $i). % 15.03/5.01 tff(ssSkC38, type, ssSkC38: $o). % 15.03/5.01 tff(ssSkC26, type, ssSkC26: $o). % 15.03/5.01 tff(a434, type, a434: $i). % 15.03/5.01 tff(a436, type, a436: $i). % 15.03/5.01 tff(a341, type, a341: $i). % 15.03/5.01 tff(a448, type, a448: $i). % 15.03/5.01 tff(a380, type, a380: $i). % 15.03/5.01 tff(a361, type, a361: $i). % 15.03/5.01 tff(a342, type, a342: $i). % 15.03/5.01 tff(c8_0, type, c8_0: $o). % 15.03/5.01 tff(a311, type, a311: $i). % 15.03/5.01 tff(a391, type, a391: $i). % 15.03/5.01 tff(a355, type, a355: $i). % 15.03/5.01 tff(a269, type, a269: $i). % 15.03/5.01 tff(a286, type, a286: $i). % 15.03/5.01 tff(a330, type, a330: $i). % 15.03/5.01 tff(a418, type, a418: $i). % 15.03/5.01 tff(ssSkC4, type, ssSkC4: $o). % 15.03/5.01 tff(a291, type, a291: $i). % 15.03/5.01 tff(a314, type, a314: $i). % 15.03/5.01 tff(a413, type, a413: $i). % 15.03/5.01 tff(a405, type, a405: $i). % 15.03/5.01 tff(a283, type, a283: $i). % 15.03/5.01 tff(ssSkC37, type, ssSkC37: $o). % 15.03/5.01 tff(a439, type, a439: $i). % 15.03/5.01 tff(a402, type, a402: $i). % 15.03/5.01 tff(a437, type, a437: $i). % 15.03/5.01 tff(a370, type, a370: $i). % 15.03/5.01 tff(a293, type, a293: $i). % 15.03/5.01 tff(a294, type, a294: $i). % 15.03/5.01 tff(a321, type, a321: $i). % 15.03/5.01 tff(a318, type, a318: $i). % 15.03/5.01 tff(c5_0, type, c5_0: $o). % 15.03/5.01 tff(a414, type, a414: $i). % 15.03/5.01 tff(a438, type, a438: $i). % 15.03/5.01 tff(ssSkC9, type, ssSkC9: $o). % 15.03/5.01 tff(a366, type, a366: $i). % 15.03/5.01 tff(a396, type, a396: $i). % 15.03/5.01 tff(ssSkP6, type, ssSkP6: $i > $o). % 15.03/5.01 tff(a308, type, a308: $i). % 15.03/5.01 tff(a329, type, a329: $i). % 15.03/5.01 tff(c6_0, type, c6_0: $o). % 15.03/5.01 tff(c8_2, type, c8_2: ($i * $i) > $o). % 15.03/5.01 tff(a270, type, a270: $i). % 15.03/5.01 tff(ssSkC30, type, ssSkC30: $o). % 15.03/5.02 tff(a278, type, a278: $i). % 15.03/5.02 tff(ssSkC11, type, ssSkC11: $o). % 15.03/5.02 tff(a442, type, a442: $i). % 15.03/5.02 tff(ssSkC18, type, ssSkC18: $o). % 15.03/5.02 tff(a410, type, a410: $i). % 15.03/5.02 tff(ssSkC16, type, ssSkC16: $o). % 15.03/5.02 tff(a388, type, a388: $i). % 15.03/5.02 tff(a298, type, a298: $i). % 15.03/5.02 tff(a353, type, a353: $i). % 15.03/5.02 tff(a443, type, a443: $i). % 15.03/5.02 tff(a374, type, a374: $i). % 15.03/5.02 tff(ssSkP3, type, ssSkP3: $i > $o). % 15.03/5.02 tff(a358, type, a358: $i). % 15.03/5.02 tff(ssSkC32, type, ssSkC32: $o). % 15.03/5.02 tff(a304, type, a304: $i). % 15.03/5.02 tff(ssSkC24, type, ssSkC24: $o). % 15.03/5.02 tff(a343, type, a343: $i). % 15.03/5.02 tff(a275, type, a275: $i). % 15.03/5.02 tff(ssSkC17, type, ssSkC17: $o). % 15.03/5.02 tff(a357, type, a357: $i). % 15.03/5.02 tff(a282, type, a282: $i). % 15.03/5.02 tff(a273, type, a273: $i). % 15.03/5.02 tff(c1_0, type, c1_0: $o). % 15.03/5.02 tff(a331, type, a331: $i). % 15.03/5.02 tff(c8_1, type, c8_1: $i > $o). % 15.03/5.02 tff(a427, type, a427: $i). % 15.03/5.02 tff(a371, type, a371: $i). % 15.03/5.02 tff(ssSkC29, type, ssSkC29: $o). % 15.03/5.02 tff(ssSkP4, type, ssSkP4: $i > $o). % 15.03/5.02 tff(a393, type, a393: $i). % 15.03/5.02 tff(c2_1, type, c2_1: $i > $o). % 15.03/5.02 tff(a392, type, a392: $i). % 15.03/5.02 tff(ssSkC27, type, ssSkC27: $o). % 15.03/5.02 tff(ndr1_1, type, ndr1_1: $i > $o). % 15.03/5.02 tff(ssSkC15, type, ssSkC15: $o). % 15.03/5.02 tff(c2_0, type, c2_0: $o). % 15.03/5.02 tff(c4_1, type, c4_1: $i > $o). % 15.03/5.02 tff(a277, type, a277: $i). % 15.03/5.02 tff(a333, type, a333: $i). % 15.03/5.02 tff(a382, type, a382: $i). % 15.03/5.02 tff(a274, type, a274: $i). % 15.03/5.02 tff(a420, type, a420: $i). % 15.03/5.02 tff(a383, type, a383: $i). % 15.03/5.02 tff(a345, type, a345: $i). % 15.03/5.02 tff(a408, type, a408: $i). % 15.03/5.02 tff(a363, type, a363: $i). % 15.03/5.02 tff(a416, type, a416: $i). % 15.03/5.02 tff(a271, type, a271: $i). % 15.03/5.02 tff(a352, type, a352: $i). % 15.03/5.02 tff(a327, type, a327: $i). % 15.03/5.02 tff(a390, type, a390: $i). % 15.03/5.02 tff(ssSkC36, type, ssSkC36: $o). % 15.03/5.02 tff(c9_1, type, c9_1: $i > $o). % 15.03/5.02 tff(c10_1, type, c10_1: $i > $o). % 15.03/5.02 tff(c10_0, type, c10_0: $o). % 15.03/5.02 tff(a425, type, a425: $i). % 15.03/5.02 tff(ssSkC12, type, ssSkC12: $o). % 15.03/5.02 tff(a447, type, a447: $i). % 15.03/5.02 tff(c6_2, type, c6_2: ($i * $i) > $o). % 15.03/5.02 tff(a400, type, a400: $i). % 15.03/5.02 tff(a364, type, a364: $i). % 15.03/5.02 tff(ssSkC20, type, ssSkC20: $o). % 15.03/5.02 tff(a381, type, a381: $i). % 15.03/5.02 tff(a429, type, a429: $i). % 15.03/5.02 tff(a289, type, a289: $i). % 15.03/5.02 tff(a411, type, a411: $i). % 15.03/5.02 tff(ndr1_0, type, ndr1_0: $o). % 15.03/5.02 tff(a288, type, a288: $i). % 15.03/5.02 tff(a300, type, a300: $i). % 15.03/5.02 tff(a287, type, a287: $i). % 15.03/5.02 tff(a375, type, a375: $i). % 15.03/5.02 tff(a444, type, a444: $i). % 15.03/5.02 tff(a344, type, a344: $i). % 15.03/5.02 tff(a351, type, a351: $i). % 15.03/5.02 tff(ssSkC14, type, ssSkC14: $o). % 15.03/5.02 tff(c9_2, type, c9_2: ($i * $i) > $o). % 15.03/5.02 tff(ssSkC33, type, ssSkC33: $o). % 15.03/5.02 tff(a395, type, a395: $i). % 15.03/5.02 tff(c10_2, type, c10_2: ($i * $i) > $o). % 15.03/5.02 tff(ssSkC34, type, ssSkC34: $o). % 15.03/5.02 tff(a424, type, a424: $i). % 15.03/5.02 tff(a317, type, a317: $i). % 15.03/5.02 tff(a441, type, a441: $i). % 15.03/5.02 tff(a349, type, a349: $i). % 15.03/5.02 tff(a426, type, a426: $i). % 15.03/5.02 tff(a324, type, a324: $i). % 15.03/5.02 tff(a403, type, a403: $i). % 15.03/5.02 tff(a419, type, a419: $i). % 15.03/5.02 tff(c1_1, type, c1_1: $i > $o). % 15.03/5.02 tff(a369, type, a369: $i). % 15.03/5.02 tff(a415, type, a415: $i). % 15.03/5.02 tff(ssSkC13, type, ssSkC13: $o). % 15.03/5.02 tff(a409, type, a409: $i). % 15.03/5.02 tff(ssSkC25, type, ssSkC25: $o). % 15.03/5.02 tff(ssSkC2, type, ssSkC2: $o). % 15.03/5.02 tff(a385, type, a385: $i). % 15.03/5.02 tff(c5_2, type, c5_2: ($i * $i) > $o). % 15.03/5.02 tff(a340, type, a340: $i). % 15.03/5.02 tff(ssSkC31, type, ssSkC31: $o). % 15.03/5.02 tff(a299, type, a299: $i). % 15.03/5.02 tff(c9_0, type, c9_0: $o). % 15.03/5.02 tff(a394, type, a394: $i). % 15.03/5.02 tff(c7_1, type, c7_1: $i > $o). % 15.03/5.02 tff(a362, type, a362: $i). % 15.03/5.02 tff(c6_1, type, c6_1: $i > $o). % 15.03/5.02 tff(a315, type, a315: $i). % 15.03/5.02 tff(ssSkC22, type, ssSkC22: $o). % 15.03/5.02 tff(a445, type, a445: $i). % 15.03/5.02 tff(a440, type, a440: $i). % 15.03/5.02 tff(c4_2, type, c4_2: ($i * $i) > $o). % 15.03/5.02 tff(a276, type, a276: $i). % 15.03/5.02 tff(a406, type, a406: $i). % 15.03/5.02 tff(ssSkC1, type, ssSkC1: $o). % 15.03/5.02 tff(ssSkP5, type, ssSkP5: $i > $o). % 15.03/5.02 tff(ssSkC0, type, ssSkC0: $o). % 15.03/5.02 tff(ssSkC5, type, ssSkC5: $o). % 15.03/5.02 tff(ssSkP1, type, ssSkP1: $i > $o). % 15.03/5.02 tff(a319, type, a319: $i). % 15.03/5.02 tff(a376, type, a376: $i). % 15.03/5.02 tff(a328, type, a328: $i). % 15.03/5.02 tff(a332, type, a332: $i). % 15.03/5.02 tff(ssSkC35, type, ssSkC35: $o). % 15.03/5.02 tff(a428, type, a428: $i). % 15.03/5.02 tff(a279, type, a279: $i). % 15.03/5.02 tff(a296, type, a296: $i). % 15.03/5.02 tff(c5_1, type, c5_1: $i > $o). % 15.03/5.02 tff(a346, type, a346: $i). % 15.03/5.02 tff(c7_2, type, c7_2: ($i * $i) > $o). % 15.03/5.02 tff(c3_2, type, c3_2: ($i * $i) > $o). % 15.03/5.02 tff(a350, type, a350: $i). % 15.03/5.02 tff(a404, type, a404: $i). % 15.03/5.02 tff(a412, type, a412: $i). % 15.03/5.02 tff(c2_2, type, c2_2: ($i * $i) > $o). % 15.03/5.02 tff(a365, type, a365: $i). % 15.03/5.02 tff(a325, type, a325: $i). % 15.03/5.02 tff(a360, type, a360: $i). % 15.03/5.02 tff(a372, type, a372: $i). % 15.03/5.02 tff(a305, type, a305: $i). % 15.03/5.02 tff(a312, type, a312: $i). % 15.03/5.02 tff(a307, type, a307: $i). % 15.03/5.02 tff(a303, type, a303: $i). % 15.03/5.02 tff(a339, type, a339: $i). % 15.03/5.02 tff(a379, type, a379: $i). % 15.03/5.02 tff(a377, type, a377: $i). % 15.03/5.02 tff(a356, type, a356: $i). % 15.03/5.02 tff(c3_1, type, c3_1: $i > $o). % 15.03/5.02 % 15.03/5.02 %Saturated clause set: % 15.03/5.02 tff(c_3527, plain, (~c4_1(a427))). % 15.03/5.02 tff(c_3526, plain, (~ssSkP4(a427))). % 15.03/5.02 tff(c_3524, plain, (~c10_2(a330, a285))). % 15.03/5.02 tff(c_3009, plain, (![U_323]: (ssSkP0(U_323) | c9_1(U_323) | c1_2(U_323, a274) | ~ssSkP5(U_323) | ~ssSkP4(U_323) | c1_1(U_323) | ~c4_1(U_323) | ~c10_2(U_323, a393) | ~c1_2(U_323, a393)))). % 15.03/5.02 tff(c_3506, plain, (![U_20]: (ssSkP0(U_20) | c9_1(U_20) | c1_2(U_20, a274) | c1_1(U_20) | ~c4_1(U_20) | ~c10_2(U_20, a285) | ssSkP1(U_20)))). % 15.03/5.02 tff(c_2936, plain, (![U_591]: (~c10_1(U_591) | ~c4_1(U_591) | c9_1(U_591) | c1_2(U_591, a338) | c5_2(U_591, a338) | ~c4_2(U_591, a393) | ~ssSkP5(U_591) | ~ssSkP4(U_591)))). % 15.03/5.02 tff(c_3060, plain, (![U_599]: (~ssSkP5(U_599) | ~ssSkP4(U_599) | c9_1(U_599) | c1_2(U_599, a393) | c5_2(U_599, a393) | ~c4_2(U_599, a430) | c5_1(U_599) | ~c4_1(U_599)))). % 15.03/5.02 tff(c_3464, plain, (![U_591]: (~c1_1(U_591) | ~c4_1(U_591) | c9_1(U_591) | c1_2(U_591, a393) | ~c4_2(U_591, a393) | ~ssSkP5(U_591) | ~ssSkP4(U_591)))). % 15.03/5.02 tff(c_3477, plain, (~c1_2(a441, a393))). % 15.03/5.02 tff(c_3476, plain, (~c5_2(a307, a391))). % 15.03/5.02 tff(c_3469, plain, (~c4_2(a441, a393))). % 15.03/5.02 tff(c_3468, plain, (c9_1(a384))). % 15.30/5.02 tff(c_3467, plain, (~c1_1(a448))). % 15.30/5.02 tff(c_3356, plain, (![U_52]: (~c1_1(U_52) | ~c4_1(U_52) | ~c4_2(U_52, a393) | ~c5_2(U_52, a393) | ~ssSkP5(U_52) | ~ssSkP4(U_52)))). % 15.30/5.02 tff(c_3440, plain, (![U_17]: (c10_2(U_17, a379) | ~c1_1(U_17) | ~c10_1(U_17) | ~c2_2(U_17, a379) | ssSkP2(U_17)))). % 15.30/5.02 tff(c_3450, plain, (~c2_2(a348, a349))). % 15.30/5.02 tff(c_3439, plain, (![U_18]: (c10_2(U_18, a285) | ~c1_1(U_18) | ~c10_1(U_18) | ~c2_2(U_18, a285) | ssSkP1(U_18)))). % 15.30/5.02 tff(c_3449, plain, (~c10_1(a350))). % 15.30/5.02 tff(c_3381, plain, (![U_491, V_494]: (c10_2(U_491, V_494) | ~c1_1(U_491) | ~c10_1(U_491) | ~c7_2(U_491, V_494) | ~c2_2(U_491, V_494)))). % 15.30/5.02 tff(c_3393, plain, (ssSkP1(a441))). % 15.30/5.02 tff(c_3389, plain, (~c1_2(a441, a285))). % 15.30/5.02 tff(c_3382, plain, (~c4_2(a441, a285))). % 15.30/5.02 tff(c_3355, plain, (![U_70]: (~c1_1(U_70) | ~c4_2(U_70, a430) | ~c5_2(U_70, a430) | c5_1(U_70) | ~c4_1(U_70)))). % 15.30/5.02 tff(c_3357, plain, (![U_19]: (~c1_1(U_19) | ~c4_1(U_19) | ~c4_2(U_19, a285) | ~c5_2(U_19, a285) | ssSkP1(U_19)))). % 15.30/5.02 tff(c_3318, plain, (![U_486, V_489]: (~c1_1(U_486) | ~c4_1(U_486) | ~c6_2(U_486, V_489) | ~c4_2(U_486, V_489) | ~c5_2(U_486, V_489)))). % 15.30/5.02 tff(c_3314, plain, (ssSkP1(a427))). % 15.30/5.02 tff(c_3310, plain, (~c1_2(a427, a285))). % 15.30/5.02 tff(c_3300, plain, (~c4_2(a427, a285))). % 15.30/5.02 tff(c_3303, plain, (~c6_2(a375, a377))). % 15.30/5.02 tff(c_3299, plain, (c7_2(a375, a376))). % 15.30/5.02 tff(c_3296, plain, (~ssSkP4(a375))). % 15.30/5.02 tff(c_3289, plain, (~c4_2(a375, a285))). % 15.30/5.02 tff(c_3276, plain, (~c8_2(a375, a377))). % 15.30/5.02 tff(c_3273, plain, (~c4_1(a281))). % 15.30/5.02 tff(c_3272, plain, (~c2_2(a375, a376))). % 15.30/5.02 tff(c_3269, plain, (~ssSkP4(a281))). % 15.30/5.02 tff(c_3059, plain, (![U_599]: (~c10_1(U_599) | c9_1(U_599) | c1_2(U_599, a338) | c5_2(U_599, a338) | ~c4_2(U_599, a430) | c5_1(U_599) | ~c4_1(U_599)))). % 15.30/5.02 tff(c_3253, plain, (![U_606]: (ssSkP0(U_606) | c9_1(U_606) | c1_2(U_606, a274) | ~c4_2(U_606, a430) | c5_1(U_606) | ~c4_1(U_606)))). % 15.30/5.02 tff(c_3244, plain, (c1_2(a375, a376))). % 15.30/5.02 tff(c_3166, plain, (![U_601, V_602]: (ssSkP4(U_601) | c3_1(U_601) | c4_2(U_601, V_602) | c4_2(U_601, a391) | c7_2(U_601, a391) | ~c10_2(U_601, V_602)))). % 15.30/5.03 tff(c_3202, plain, (~c4_1(a375))). % 15.30/5.03 tff(c_3198, plain, (c8_1(a375))). % 15.30/5.03 tff(c_3195, plain, (c4_2(a287, a290))). % 15.30/5.03 tff(c_3194, plain, (c4_2(a333, a335))). % 15.30/5.03 tff(c_3191, plain, (c4_2(a371, a373))). % 15.30/5.03 tff(c_3183, plain, (c7_2(a313, a314))). % 15.30/5.03 tff(c_3186, plain, (c2_2(a320, a321))). % 15.30/5.03 tff(c_3182, plain, (c3_1(a369))). % 15.30/5.03 tff(c_3094, plain, (![U_422, V_423, X_425]: (c3_1(U_422) | c4_2(U_422, V_423) | c4_2(U_422, X_425) | c7_2(U_422, X_425) | c9_2(U_422, X_425) | ~c10_2(U_422, V_423)))). % 15.30/5.03 tff(c_3090, plain, (~c4_1(a350))). % 15.30/5.03 tff(c_3089, plain, (~c2_2(a320, a322))). % 15.30/5.03 tff(c_3086, plain, (~c4_1(a422))). % 15.30/5.03 tff(c_3085, plain, (~c1_2(a283, a430))). % 15.30/5.03 tff(c_3075, plain, (~c4_2(a283, a430))). % 15.30/5.03 tff(c_3078, plain, (~c7_2(a320, a322))). % 15.30/5.03 tff(c_3074, plain, (~c6_2(a320, a321))). % 15.30/5.03 tff(c_3071, plain, (~c4_1(a414))). % 15.30/5.03 tff(c_2662, plain, (![U_70, X_583]: (c9_1(U_70) | c8_2(U_70, X_583) | c1_2(U_70, X_583) | c5_2(U_70, X_583) | ~c4_2(U_70, a430) | c5_1(U_70) | ~c4_1(U_70)))). % 15.30/5.03 tff(c_3003, plain, (![U_597]: (ssSkP0(U_597) | c9_1(U_597) | c1_2(U_597, a274) | ~c4_2(U_597, a393) | ~ssSkP5(U_597) | ~ssSkP4(U_597)))). % 15.30/5.03 tff(c_2992, plain, (~ssSkP4(a350))). % 15.30/5.03 tff(c_2988, plain, (~c10_1(a427))). % 15.30/5.03 tff(c_2991, plain, (c6_1(a320))). % 15.30/5.03 tff(c_2984, plain, (![U_11]: (~c4_1(U_11) | ~c10_1(U_11) | ~c2_2(U_11, a412) | ~c10_2(U_11, a412) | ssSkP6(U_11)))). % 15.30/5.03 tff(c_2986, plain, (~c10_2(a369, a370))). % 15.30/5.03 tff(c_2960, plain, (![W_428, X_429]: (~c4_1(W_428) | ~c10_1(W_428) | ~c2_2(W_428, X_429) | ~c10_2(W_428, X_429) | ~c3_2(W_428, X_429)))). % 15.30/5.03 tff(c_2956, plain, (~ssSkP4(a422))). % 15.30/5.03 tff(c_2952, plain, (~ssSkP4(a283))). % 15.30/5.03 tff(c_2937, plain, (![U_591]: (c9_1(U_591) | c1_2(U_591, a393) | c5_2(U_591, a393) | ~c4_2(U_591, a393) | ~ssSkP5(U_591) | ~ssSkP4(U_591)))). % 15.30/5.03 tff(c_2946, plain, (~ssSkP4(a414))). % 15.30/5.03 tff(c_2663, plain, (![U_52, X_583]: (c9_1(U_52) | c8_2(U_52, X_583) | c1_2(U_52, X_583) | c5_2(U_52, X_583) | ~c4_2(U_52, a393) | ~ssSkP5(U_52) | ~ssSkP4(U_52)))). % 15.30/5.03 tff(c_2769, plain, (![U_585]: (~c10_1(U_585) | ~c4_1(U_585) | c9_1(U_585) | c1_2(U_585, a338) | c5_2(U_585, a338) | ~c4_2(U_585, a285) | ssSkP1(U_585)))). % 15.30/5.03 tff(c_2770, plain, (![U_585]: (~ssSkP5(U_585) | ~ssSkP4(U_585) | c9_1(U_585) | c1_2(U_585, a393) | c5_2(U_585, a393) | ~c4_2(U_585, a285) | ssSkP1(U_585)))). % 15.30/5.03 tff(c_2872, plain, (ssSkP1(a281))). % 15.30/5.03 tff(c_2868, plain, (~c1_2(a281, a285))). % 15.30/5.03 tff(c_2863, plain, (~c4_2(a281, a285))). % 15.30/5.03 tff(c_2846, plain, (![U_587]: (ssSkP0(U_587) | c9_1(U_587) | c1_2(U_587, a274) | ~c4_2(U_587, a285) | ssSkP1(U_587)))). % 15.30/5.03 tff(c_2854, plain, (~c7_2(a369, a370))). % 15.30/5.03 tff(c_2849, plain, (~c9_2(a369, a370))). % 15.30/5.03 tff(c_2837, plain, (ssSkP1(a350))). % 15.30/5.03 tff(c_2833, plain, (~c1_2(a350, a285))). % 15.30/5.03 tff(c_2826, plain, (~c4_2(a350, a285))). % 15.30/5.03 tff(c_2820, plain, (~c4_2(a422, a285))). % 15.30/5.03 tff(c_2817, plain, (ssSkP1(a283))). % 15.30/5.03 tff(c_2813, plain, (~c1_2(a283, a285))). % 15.30/5.03 tff(c_2803, plain, (~c4_2(a283, a285))). % 15.30/5.03 tff(c_2806, plain, (c3_2(a369, a370))). % 15.30/5.03 tff(c_2802, plain, (ssSkP1(a414))). % 15.30/5.03 tff(c_2796, plain, (~c1_2(a414, a285))). % 15.30/5.03 tff(c_2795, plain, (~c1_2(a369, a370))). % 15.30/5.03 tff(c_2779, plain, (~c4_2(a414, a285))). % 15.30/5.03 tff(c_2782, plain, (~c4_2(a369, a370))). % 15.30/5.03 tff(c_2664, plain, (![U_19, X_583]: (c9_1(U_19) | c8_2(U_19, X_583) | c1_2(U_19, X_583) | c5_2(U_19, X_583) | ~c4_2(U_19, a285) | ssSkP1(U_19)))). % 15.30/5.03 tff(c_2710, plain, (~c4_2(a330, a331))). % 15.30/5.03 tff(c_2709, plain, (~c1_2(a414, a415))). % 15.30/5.03 tff(c_2702, plain, (~c4_2(a414, a415))). % 15.30/5.03 tff(c_2699, plain, (~c1_2(a302, a303))). % 15.30/5.03 tff(c_2692, plain, (~c4_2(a302, a303))). % 15.30/5.03 tff(c_2691, plain, (~c1_2(a348, a349))). % 15.30/5.03 tff(c_2686, plain, (~c4_2(a348, a349))). % 15.30/5.03 tff(c_2683, plain, (~c1_2(a352, a353))). % 15.30/5.03 tff(c_2674, plain, (~c4_2(a352, a353))). % 15.30/5.03 tff(c_2673, plain, (c9_1(a300))). % 15.30/5.03 tff(c_2636, plain, (![U_357, X_360, V_358]: (c9_1(U_357) | c8_2(U_357, X_360) | c1_2(U_357, X_360) | c5_2(U_357, X_360) | ~c4_2(U_357, V_358) | ~c6_2(U_357, V_358)))). % 15.30/5.03 tff(c_2633, plain, (~c1_1(a369))). % 15.30/5.03 tff(c_2630, plain, (~c2_1(a369))). % 15.30/5.03 tff(c_2624, plain, (![W_384]: (~c4_1(W_384) | ~c1_2(W_384, a347)))). % 15.30/5.03 tff(c_2619, plain, (~ssSkC16)). % 15.30/5.03 tff(c_2590, plain, (![U_577]: (ssSkP6(U_577) | c1_1(U_577) | ~c4_1(U_577) | ~c10_2(U_577, a412) | ~c1_2(U_577, a412)))). % 15.30/5.03 tff(c_2585, plain, (![U_577]: (ssSkP2(U_577) | c1_1(U_577) | ~c4_1(U_577) | ~c10_2(U_577, a379) | ~c1_2(U_577, a379)))). % 15.30/5.03 tff(c_2610, plain, (~c1_2(a448, a338))). % 15.30/5.03 tff(c_2609, plain, (~c1_2(a441, a274))). % 15.30/5.03 tff(c_2608, plain, (ssSkP1(a313))). % 15.30/5.04 tff(c_2602, plain, (~c1_2(a313, a285))). % 15.30/5.04 tff(c_2601, plain, (~c1_2(a313, a314))). % 15.30/5.04 tff(c_2597, plain, (~c10_2(a272, a273))). % 15.30/5.04 tff(c_2596, plain, (~c1_2(a343, a344))). % 15.30/5.04 tff(c_2551, plain, (![U_323, V_324]: (c1_1(U_323) | c4_2(U_323, V_324) | ~c4_1(U_323) | ~c10_2(U_323, V_324) | ~c1_2(U_323, V_324)))). % 15.30/5.04 tff(c_2546, plain, (![V_575]: (~c2_1(V_575) | ~c4_1(V_575) | ~c1_2(V_575, a363) | ~c2_2(V_575, a363) | c6_1(V_575) | ~c10_1(V_575)))). % 15.30/5.04 tff(c_2540, plain, (![V_274]: (c6_1(V_274) | c5_2(V_274, a363) | ~c10_1(V_274)))). % 15.30/5.04 tff(c_2537, plain, (![V_277]: (c6_1(V_277) | c4_2(V_277, a363) | ~c10_1(V_277)))). % 15.30/5.04 tff(c_2526, plain, (c5_1(a317))). % 15.30/5.04 tff(c_2522, plain, (c1_1(a401))). % 15.30/5.04 tff(c_2503, plain, (c4_2(a365, a366))). % 15.30/5.04 tff(c_2507, plain, (~c6_1(a401))). % 15.30/5.04 tff(c_2500, plain, (~c2_1(a317))). % 15.30/5.04 tff(c_2493, plain, (c4_1(a317))). % 15.30/5.04 tff(c_2489, plain, (c1_2(a365, a366))). % 15.30/5.04 tff(c_2483, plain, (~c1_1(a365))). % 15.30/5.04 tff(c_2478, plain, (~c8_2(a365, a366))). % 15.30/5.04 tff(c_2475, plain, (c7_1(a365))). % 15.30/5.04 tff(c_2472, plain, (~c1_1(a434))). % 15.30/5.04 tff(c_2450, plain, (![U_239]: (~c4_1(U_239) | ~c7_1(U_239) | ~c1_1(U_239)))). % 15.30/5.04 tff(c_2451, plain, (![U_164]: (~c4_1(U_164) | c3_1(U_164) | ~c2_1(U_164)))). % 15.30/5.04 tff(c_2456, plain, (~c4_1(a356))). % 15.30/5.04 tff(c_2455, plain, (~c4_1(a333))). % 15.30/5.04 tff(c_2459, plain, (c3_1(a365))). % 15.30/5.04 tff(c_2454, plain, (~c4_1(a442))). % 15.30/5.04 tff(c_2453, plain, (~c4_1(a307))). % 15.30/5.04 tff(c_2452, plain, (~c4_1(a444))). % 15.30/5.04 tff(c_2427, plain, (![U_304]: (~c8_1(U_304) | ~c4_1(U_304)))). % 15.30/5.04 tff(c_2423, plain, (c6_2(a302, a303))). % 15.30/5.04 tff(c_2420, plain, (~c5_2(a302, a303))). % 15.30/5.04 tff(c_2410, plain, (~c7_1(a302))). % 15.30/5.04 tff(c_2404, plain, (c10_1(a302))). % 15.30/5.04 tff(c_2376, plain, (![U_78]: (~c2_1(U_78) | ~c4_1(U_78) | ~c1_2(U_78, a354) | ~c2_2(U_78, a354) | c7_1(U_78) | ~c1_1(U_78)))). % 15.30/5.04 tff(c_2377, plain, (![U_12]: (~c2_1(U_12) | ~c4_1(U_12) | ~c1_2(U_12, a412) | ~c2_2(U_12, a412) | ssSkP6(U_12)))). % 15.30/5.04 tff(c_2388, plain, (~c2_2(a403, a404))). % 15.30/5.04 tff(c_2384, plain, (~c2_2(a333, a335))). % 15.30/5.04 tff(c_2381, plain, (~c2_2(a287, a290))). % 15.30/5.04 tff(c_2346, plain, (![U_289, V_290]: (~c2_1(U_289) | ~c4_1(U_289) | ~c1_2(U_289, V_290) | ~c5_2(U_289, V_290) | ~c2_2(U_289, V_290)))). % 15.30/5.04 tff(c_2351, plain, (~c1_1(a343))). % 15.30/5.04 tff(c_2348, plain, (~c1_1(a300))). % 15.30/5.04 tff(c_2347, plain, (~c1_1(a352))). % 15.30/5.04 tff(c_2329, plain, (![U_239]: (c8_1(U_239) | ~c7_1(U_239) | ~c1_1(U_239)))). % 15.30/5.04 tff(c_2306, plain, (c3_1(a422))). % 15.30/5.04 tff(c_2305, plain, (~c7_2(a339, a341))). % 15.30/5.04 tff(c_2304, plain, (ssSkC30)). % 15.30/5.04 tff(c_2301, plain, (~c7_2(a371, a373))). % 15.30/5.04 tff(c_2300, plain, (ssSkC34)). % 15.30/5.04 tff(c_2297, plain, (~c7_2(a287, a290))). % 15.30/5.04 tff(c_2296, plain, (~c2_2(a323, a324))). % 15.30/5.04 tff(c_2252, plain, (![U_223, V_224]: (c9_1(U_223) | c3_1(U_223) | c9_2(U_223, V_224) | ~c2_2(U_223, V_224) | ~c7_2(U_223, V_224)))). % 15.30/5.04 tff(c_2233, plain, (~ssSkC1)). % 15.30/5.04 tff(c_2226, plain, (~c2_1(a343))). % 15.30/5.04 tff(c_2223, plain, (~c2_1(a300))). % 15.30/5.04 tff(c_2222, plain, (~c2_1(a352))). % 15.30/5.04 tff(c_2205, plain, (![U_164]: (c8_1(U_164) | c3_1(U_164) | ~c2_1(U_164)))). % 15.30/5.04 tff(c_2201, plain, (~c4_2(a448, a338))). % 15.30/5.04 tff(c_2192, plain, (![U_154]: (c6_2(a448, U_154) | c7_2(a448, U_154) | ~c4_2(a448, U_154)))). % 15.30/5.04 tff(c_2180, plain, (~c5_2(a384, a392))). % 15.30/5.04 tff(c_2169, plain, (![U_183]: (c6_2(a384, U_183) | c2_2(a384, U_183) | ~c5_2(a384, U_183)))). % 15.30/5.04 tff(c_2166, plain, (~c4_1(a384))). % 15.30/5.04 tff(c_2163, plain, (~ssSkP4(a384))). % 15.30/5.04 tff(c_2162, plain, (c4_2(a384, a274))). % 15.30/5.04 tff(c_2161, plain, (c4_2(a384, a446))). % 15.30/5.04 tff(c_2137, plain, (![U_159]: (c3_2(a384, U_159) | c8_2(a384, U_159) | c4_2(a384, U_159)))). % 15.30/5.04 tff(c_2119, plain, (~c2_0)). % 15.30/5.04 tff(c_2110, plain, (~c3_0)). % 15.30/5.04 tff(c_2102, plain, (ssSkC14)). % 15.30/5.04 tff(c_2095, plain, (~c7_2(a422, a354))). % 15.30/5.04 tff(c_2086, plain, (![U_172]: (c5_2(a422, U_172) | ~c7_2(a422, U_172) | ~c9_2(a422, U_172)))). % 15.30/5.04 tff(c_2083, plain, (ssSkC38)). % 15.30/5.04 tff(c_2069, plain, (![U_152]: (c9_2(a406, U_152) | c1_2(a406, U_152) | ~c2_2(a406, U_152)))). % 15.30/5.04 tff(c_2066, plain, (ssSkC4)). % 15.30/5.04 tff(c_2063, plain, (~c10_1(a307))). % 15.30/5.04 tff(c_2061, plain, (![U_170]: (c10_2(a427, U_170) | ~c8_2(a427, U_170) | ~c6_2(a427, U_170)))). % 15.30/5.04 tff(c_2042, plain, (![U_161]: (c6_2(a307, U_161) | ~c5_2(a307, U_161) | ~c7_2(a307, U_161)))). % 15.30/5.04 tff(c_2039, plain, (ssSkC19)). % 15.30/5.04 tff(c_2036, plain, (ssSkC18)). % 15.30/5.04 tff(c_2032, plain, (![U_178]: (c1_2(a281, U_178) | ~c2_2(a281, U_178) | ~c8_2(a281, U_178)))). % 15.30/5.04 tff(c_2029, plain, (~ssSkP4(a403))). % 15.30/5.04 tff(c_2026, plain, (~c10_2(a403, a285))). % 15.30/5.04 tff(c_2004, plain, (![U_190]: (~c4_2(a403, U_190) | ~c6_2(a403, U_190) | ~c10_2(a403, U_190)))). % 15.30/5.04 tff(c_1999, plain, (~c1_2(a330, a393))). % 15.30/5.04 tff(c_1998, plain, (~c1_2(a330, a274))). % 15.30/5.04 tff(c_1983, plain, (~c3_2(a414, a338))). % 15.30/5.04 tff(c_1986, plain, (![U_153]: (c2_2(a330, U_153) | c3_2(a330, U_153) | ~c1_2(a330, U_153)))). % 15.30/5.04 tff(c_1982, plain, (~c4_2(a441, a274))). % 15.30/5.04 tff(c_1975, plain, (![U_151]: (c1_2(a414, U_151) | c7_2(a414, U_151) | ~c3_2(a414, U_151)))). % 15.30/5.05 tff(c_1966, plain, (![U_150]: (c2_2(a441, U_150) | c5_2(a441, U_150) | ~c4_2(a441, U_150)))). % 15.30/5.05 tff(c_1963, plain, (~c10_1(a313))). % 15.30/5.05 tff(c_1962, plain, (~c1_2(a427, a393))). % 15.30/5.05 tff(c_1960, plain, (![U_169]: (c7_2(a441, U_169) | ~c8_2(a441, U_169) | ~c5_2(a441, U_169)))). % 15.30/5.05 tff(c_1957, plain, (~c4_2(a313, a285))). % 15.30/5.05 tff(c_1937, plain, (~c1_2(a427, a274))). % 15.30/5.05 tff(c_1940, plain, (![U_191]: (~c3_2(a313, U_191) | ~c4_2(a313, U_191) | ~c7_2(a313, U_191)))). % 15.30/5.05 tff(c_1925, plain, (![U_171]: (c3_2(a427, U_171) | ~c10_2(a427, U_171) | ~c1_2(a427, U_171)))). % 15.30/5.05 tff(c_1922, plain, (c3_2(a294, a295))). % 15.30/5.05 tff(c_1918, plain, (~c1_2(a294, a295))). % 15.30/5.05 tff(c_1914, plain, (~c2_2(a294, a295))). % 15.30/5.05 tff(c_1909, plain, (![U_142]: (~c10_1(U_142) | ~c4_1(U_142) | ~c8_2(U_142, a338)))). % 15.30/5.05 tff(c_1891, plain, (![U_141]: (~c10_1(U_141) | ~c4_1(U_141) | ~c7_2(U_141, a338)))). % 15.30/5.05 tff(c_1881, plain, (c8_1(a444))). % 15.30/5.05 tff(c_1861, plain, (![U_143]: (~c10_1(U_143) | ~c4_1(U_143) | ~c10_2(U_143, a338)))). % 15.30/5.05 tff(c_1850, plain, (~c4_1(a294))). % 15.30/5.05 tff(c_1844, plain, (~ssSkC33)). % 15.30/5.05 tff(c_1839, plain, (~ssSkC5)). % 15.30/5.05 tff(c_1836, plain, (~ssSkC11)). % 15.30/5.05 tff(c_1830, plain, (~ssSkC2)). % 15.30/5.05 tff(c_1824, plain, (~ssSkC37)). % 15.30/5.05 tff(c_1819, plain, (~ssSkC21)). % 15.30/5.05 tff(c_1808, plain, (![U_132]: (~c2_1(U_132) | ~c10_1(U_132) | ~c9_2(U_132, a402)))). % 15.30/5.05 tff(c_1794, plain, (![U_133]: (~c2_1(U_133) | ~c10_1(U_133) | ~c2_2(U_133, a402)))). % 15.30/5.05 tff(c_1773, plain, (c4_2(a287, a288))). % 15.30/5.05 tff(c_1766, plain, (![U_76]: (~c8_2(U_76, a393) | ~ssSkP5(U_76) | ~ssSkP4(U_76)))). % 15.30/5.05 tff(c_1756, plain, (![U_70]: (c5_1(U_70) | c6_2(U_70, a430) | ~c4_1(U_70)))). % 15.30/5.05 tff(c_1752, plain, (![U_108]: (c7_2(U_108, a402) | ~c2_1(U_108) | ~c10_1(U_108)))). % 15.30/5.05 tff(c_1748, plain, (![U_80]: (c7_1(U_80) | c4_2(U_80, a354) | ~c1_1(U_80)))). % 15.30/5.05 tff(c_1744, plain, (![U_106]: (c5_1(U_106) | ~c4_1(U_106) | ~c10_2(U_106, a430)))). % 15.30/5.05 tff(c_1733, plain, (~c6_2(a287, a289))). % 15.30/5.05 tff(c_1730, plain, (~c3_2(a287, a290))). % 15.30/5.05 tff(c_1727, plain, (c5_2(a287, a290))). % 15.30/5.05 tff(c_1722, plain, (c8_2(a287, a289))). % 15.30/5.05 tff(c_1710, plain, (~c9_2(a287, a290))). % 15.30/5.05 tff(c_1713, plain, (![U_79]: (c7_1(U_79) | c9_2(U_79, a354) | ~c1_1(U_79)))). % 15.30/5.05 tff(c_1707, plain, (~ssSkP4(a272))). % 15.30/5.05 tff(c_1704, plain, (ssSkP2(a272))). % 15.30/5.05 tff(c_1687, plain, (![U_69]: (c1_2(a272, U_69) | ~c6_2(a272, U_69)))). % 15.30/5.05 tff(c_1683, plain, (![U_71]: (c5_1(U_71) | c2_2(U_71, a430) | ~c4_1(U_71)))). % 15.30/5.05 tff(c_1676, plain, (~c6_2(a287, a288))). % 15.30/5.05 tff(c_1679, plain, (![U_78]: (c7_1(U_78) | c5_2(U_78, a354) | ~c1_1(U_78)))). % 15.30/5.05 tff(c_1670, plain, (![U_77]: (~c3_2(U_77, a393) | ~ssSkP5(U_77) | ~ssSkP4(U_77)))). % 15.30/5.05 tff(c_1661, plain, (![U_52]: (c6_2(U_52, a393) | ~ssSkP5(U_52) | ~ssSkP4(U_52)))). % 15.30/5.05 tff(c_1608, plain, (![U_4]: (ndr1_1(U_4)))). % 15.30/5.05 tff(c_1593, plain, (ssSkC29)). % 15.30/5.05 tff(c_1586, plain, (ssSkC22)). % 15.30/5.05 tff(c_1579, plain, (ssSkC12)). % 15.30/5.05 tff(c_1569, plain, (ssSkC25)). % 15.30/5.05 tff(c_1561, plain, (~c4_0)). % 15.30/5.05 tff(c_1546, plain, (~ssSkC35)). % 15.30/5.05 tff(c_1541, plain, (ssSkC8)). % 15.30/5.05 tff(c_508, plain, (![U_27]: (ssSkP4(U_27) | ~c2_2(U_27, a391)))). % 15.30/5.05 tff(c_302, plain, (![U_14]: (ssSkP3(U_14) | c4_2(U_14, a389)))). % 15.30/5.05 tff(c_506, plain, (![U_26]: (ssSkP4(U_26) | ~c9_2(U_26, a391)))). % 15.30/5.05 tff(c_502, plain, (![U_24]: (ssSkP5(U_24) | ~c6_2(U_24, a392)))). % 15.30/5.05 tff(c_1533, plain, (c2_2(a343, a344))). % 15.30/5.05 tff(c_484, plain, (![U_21]: (ssSkP7(U_21) | ~c8_2(U_21, a446)))). % 15.30/5.05 tff(c_1530, plain, (c9_2(a384, a385))). % 15.30/5.05 tff(c_572, plain, (![U_31]: (ssSkP0(U_31) | ~c3_2(U_31, a274)))). % 15.30/5.05 tff(c_512, plain, (![U_29]: (ssSkP2(U_29) | ~c4_2(U_29, a379)))). % 15.30/5.05 tff(c_510, plain, (![U_28]: (ssSkP3(U_28) | ~c2_2(U_28, a389)))). % 15.30/5.05 tff(c_1518, plain, (c10_2(a343, a344))). % 15.30/5.05 tff(c_270, plain, (![U_10]: (ssSkP7(U_10) | c1_2(U_10, a446)))). % 15.30/5.05 tff(c_1515, plain, (~c5_2(a384, a385))). % 15.30/5.05 tff(c_1506, plain, (~c6_2(a384, a385))). % 15.30/5.05 tff(c_390, plain, (![U_19]: (ssSkP1(U_19) | c6_2(U_19, a285)))). % 15.30/5.05 tff(c_300, plain, (![U_13]: (ssSkP5(U_13) | c1_2(U_13, a392)))). % 15.30/5.05 tff(c_286, plain, (![U_11]: (ssSkP6(U_11) | c3_2(U_11, a412)))). % 15.30/5.05 tff(c_1499, plain, (~c4_2(a343, a344))). % 15.30/5.05 tff(c_392, plain, (![U_20]: (ssSkP1(U_20) | c1_2(U_20, a285)))). % 15.30/5.05 tff(c_288, plain, (![U_12]: (ssSkP6(U_12) | c5_2(U_12, a412)))). % 15.30/5.05 tff(c_574, plain, (![U_32]: (ssSkP0(U_32) | ~c5_2(U_32, a274)))). % 15.30/5.05 tff(c_388, plain, (![U_18]: (ssSkP1(U_18) | c7_2(U_18, a285)))). % 15.30/5.05 tff(c_304, plain, (![U_15]: (ssSkP3(U_15) | c5_2(U_15, a389)))). % 15.30/5.05 tff(c_504, plain, (![U_25]: (ssSkP4(U_25) | ~c1_2(U_25, a391)))). % 15.30/5.05 tff(c_500, plain, (![U_23]: (ssSkP5(U_23) | ~c2_2(U_23, a392)))). % 15.30/5.05 tff(c_308, plain, (![U_16]: (ssSkP2(U_16) | c6_2(U_16, a379)))). % 15.30/5.05 tff(c_268, plain, (![U_9]: (ssSkP7(U_9) | c10_2(U_9, a446)))). % 15.30/5.05 tff(c_310, plain, (![U_17]: (ssSkP2(U_17) | c7_2(U_17, a379)))). % 15.30/5.05 tff(c_496, plain, (![U_22]: (ssSkP6(U_22) | ~c4_2(U_22, a412)))). % 15.30/5.05 tff(c_570, plain, (![U_30]: (ssSkP0(U_30) | ~c8_2(U_30, a274)))). % 15.30/5.05 tff(c_1475, plain, (c6_2(a414, a415))). % 15.30/5.05 tff(c_1474, plain, (~c9_2(a313, a314))). % 15.30/5.05 tff(c_1472, plain, (~c2_1(a448))). % 15.30/5.05 tff(c_1470, plain, (~c8_2(a422, a423))). % 15.30/5.05 tff(c_1467, plain, (~c5_2(a300, a301))). % 15.30/5.05 tff(c_1466, plain, (c1_2(a272, a273))). % 15.30/5.05 tff(c_1465, plain, (~c8_2(a283, a284))). % 15.30/5.05 tff(c_1464, plain, (~c2_2(a310, a311))). % 15.30/5.05 tff(c_1463, plain, (~c5_2(a356, a357))). % 15.30/5.06 tff(c_1462, plain, (~ssSkC31)). % 15.30/5.06 tff(c_1461, plain, (~c8_2(a414, a415))). % 15.30/5.06 tff(c_1460, plain, (c8_2(a345, a346))). % 15.30/5.06 tff(c_1457, plain, (~c4_2(a272, a273))). % 15.30/5.06 tff(c_1456, plain, (~c2_2(a313, a314))). % 15.30/5.06 tff(c_1455, plain, (~c10_2(a330, a331))). % 15.30/5.06 tff(c_1453, plain, (c1_2(a356, a357))). % 15.30/5.06 tff(c_1452, plain, (c7_2(a323, a324))). % 15.30/5.06 tff(c_1450, plain, (~c2_2(a371, a372))). % 15.30/5.06 tff(c_1449, plain, (~c9_2(a323, a324))). % 15.30/5.06 tff(c_1448, plain, (c4_2(a310, a311))). % 15.30/5.06 tff(c_1447, plain, (~c6_2(a422, a423))). % 15.30/5.06 tff(c_1442, plain, (~c7_2(a333, a335))). % 15.30/5.06 tff(c_1441, plain, (c5_2(a403, a404))). % 15.30/5.06 tff(c_1440, plain, (~c9_2(a371, a373))). % 15.30/5.06 tff(c_1439, plain, (~c1_2(a371, a372))). % 15.30/5.06 tff(c_1438, plain, (~c1_2(a434, a435))). % 15.30/5.06 tff(c_1436, plain, (~c3_2(a283, a284))). % 15.30/5.06 tff(c_1435, plain, (c2_2(a345, a346))). % 15.30/5.06 tff(c_1434, plain, (~c2_2(a272, a273))). % 15.30/5.06 tff(c_1433, plain, (c6_2(a300, a301))). % 15.30/5.06 tff(c_1432, plain, (c4_2(a323, a324))). % 15.30/5.06 tff(c_1431, plain, (c8_2(a297, a298))). % 15.30/5.06 tff(c_1430, plain, (~c3_2(a339, a340))). % 15.30/5.06 tff(c_1429, plain, (~c9_2(a339, a341))). % 15.30/5.06 tff(c_1428, plain, (c2_2(a367, a368))). % 15.30/5.06 tff(c_1426, plain, (~c7_2(a403, a404))). % 15.30/5.06 tff(c_1427, plain, (c6_2(a330, a331))). % 15.30/5.06 tff(c_1425, plain, (~ssSkC36)). % 15.30/5.06 tff(c_1423, plain, (~c6_2(a371, a373))). % 15.30/5.06 tff(c_1421, plain, (~c3_2(a348, a349))). % 15.30/5.06 tff(c_1420, plain, (c1_2(a308, a309))). % 15.30/5.06 tff(c_1418, plain, (c8_2(a333, a334))). % 15.30/5.06 tff(c_1417, plain, (~c10_2(a422, a423))). % 15.30/5.06 tff(c_1416, plain, (c8_2(a308, a309))). % 15.30/5.06 tff(c_1415, plain, (~ssSkC28)). % 15.30/5.06 tff(c_1414, plain, (~c1_2(a371, a373))). % 15.30/5.06 tff(c_1413, plain, (c4_2(a300, a301))). % 15.30/5.06 tff(c_1412, plain, (~c10_2(a345, a346))). % 15.30/5.06 tff(c_1408, plain, (c9_2(a333, a334))). % 15.30/5.06 tff(c_1407, plain, (c3_2(a403, a404))). % 15.30/5.06 tff(c_1406, plain, (c7_2(a367, a368))). % 15.30/5.06 tff(c_1405, plain, (~c5_2(a339, a341))). % 15.30/5.06 tff(c_1404, plain, (~c4_2(a313, a314))). % 15.30/5.06 tff(c_1403, plain, (~c7_0)). % 15.30/5.06 tff(c_1402, plain, (c9_2(a339, a340))). % 15.30/5.06 tff(c_1401, plain, (~c7_2(a333, a334))). % 15.30/5.06 tff(c_1400, plain, (c5_1(a343))). % 15.30/5.06 tff(c_1399, plain, (c1_2(a330, a331))). % 15.30/5.06 tff(c_1398, plain, (~c9_2(a333, a335))). % 15.30/5.06 tff(c_1397, plain, (c4_2(a339, a341))). % 15.30/5.06 tff(c_1396, plain, (c10_2(a367, a368))). % 15.30/5.06 tff(c_1395, plain, (~c8_2(a350, a351))). % 15.30/5.06 tff(c_1394, plain, (~c5_2(a297, a298))). % 15.30/5.06 tff(c_1393, plain, (~c7_2(a308, a309))). % 15.30/5.06 tff(c_1392, plain, (~c7_2(a339, a340))). % 15.30/5.06 tff(c_1391, plain, (~c5_2(a352, a353))). % 15.30/5.06 tff(c_1390, plain, (~c2_2(a352, a353))). % 15.30/5.06 tff(c_1389, plain, (c9_2(a434, a435))). % 15.30/5.06 tff(c_1388, plain, (~c4_2(a297, a298))). % 15.30/5.06 tff(c_1387, plain, (~c6_2(a356, a357))). % 15.30/5.06 tff(c_1386, plain, (c2_2(a414, a415))). % 15.30/5.06 tff(c_1385, plain, (c5_2(a333, a335))). % 15.30/5.06 tff(c_1384, plain, (~c6_2(a310, a311))). % 15.30/5.06 tff(c_1383, plain, (c4_2(a434, a435))). % 15.30/5.06 tff(c_1382, plain, (~ssSkC32)). % 15.30/5.06 tff(c_1381, plain, (c6_2(a348, a349))). % 15.30/5.06 tff(c_1379, plain, (c7_2(a348, a349))). % 15.30/5.06 tff(c_1377, plain, (~ssSkC0)). % 15.30/5.06 tff(c_1376, plain, (~c8_1(a343))). % 15.30/5.06 tff(c_1372, plain, (c2_2(a350, a351))). % 15.30/5.06 tff(c_1371, plain, (c6_2(a352, a353))). % 15.30/5.06 tff(c_1370, plain, (~ssSkC7)). % 15.30/5.06 tff(c_1368, plain, (~c4_1(a278))). % 15.30/5.06 tff(c_1365, plain, (c7_2(a350, a351))). % 15.30/5.06 tff(c_1363, plain, (~ssSkC15)). % 15.30/5.06 tff(c_1361, plain, (~c1_0)). % 15.30/5.06 tff(c_1357, plain, (~ssSkC23)). % 15.30/5.06 tff(c_1355, plain, (~ssSkC20)). % 15.30/5.06 tff(c_1352, plain, (c10_1(a448))). % 15.30/5.06 tff(c_1348, plain, (~ssSkC26)). % 15.30/5.06 tff(c_1347, plain, (~c10_1(a308))). % 15.30/5.06 tff(c_1346, plain, (~c4_1(a394))). % 15.30/5.06 tff(c_1343, plain, (~c7_1(a386))). % 15.30/5.06 tff(c_1342, plain, (~c6_1(a339))). % 15.30/5.06 tff(c_1341, plain, (~c9_1(a307))). % 15.30/5.06 tff(c_1338, plain, (~c8_0)). % 15.30/5.06 tff(c_1337, plain, (~c5_0)). % 15.30/5.06 tff(c_1335, plain, (~c7_1(a427))). % 15.30/5.06 tff(c_1333, plain, (~c6_1(a434))). % 15.30/5.06 tff(c_1332, plain, (~c2_1(a310))). % 15.30/5.06 tff(c_1331, plain, (~c6_1(a348))). % 15.30/5.06 tff(c_1330, plain, (~c3_1(a350))). % 15.30/5.06 tff(c_1329, plain, (~c1_1(a414))). % 15.30/5.06 tff(c_1327, plain, (~c6_1(a360))). % 15.30/5.06 tff(c_1326, plain, (~c3_1(a406))). % 15.30/5.06 tff(c_1325, plain, (~c2_1(a356))). % 15.30/5.06 tff(c_1324, plain, (~c7_1(a360))). % 15.30/5.06 tff(c_1323, plain, (~c1_1(a330))). % 15.30/5.06 tff(c_1322, plain, (~c3_1(a403))). % 15.30/5.06 tff(c_1321, plain, (~c5_1(a360))). % 15.30/5.06 tff(c_1320, plain, (~c10_1(a323))). % 15.30/5.06 tff(c_1318, plain, (~ssSkC10)). % 15.30/5.06 tff(c_1316, plain, (~c8_1(a352))). % 15.30/5.06 tff(c_1315, plain, (~c10_1(a362))). % 15.30/5.06 tff(c_1314, plain, (~c3_1(a323))). % 15.30/5.06 tff(c_1313, plain, (~c5_1(a310))). % 15.30/5.06 tff(c_1312, plain, (~c5_1(a308))). % 15.30/5.06 tff(c_1311, plain, (~c8_1(a300))). % 15.30/5.06 tff(c_1308, plain, (~c7_1(a297))). % 15.30/5.06 tff(c_1307, plain, (~c4_1(a297))). % 15.30/5.06 tff(c_1306, plain, (c8_1(a307))). % 15.30/5.06 tff(c_1305, plain, (c1_1(a394))). % 15.30/5.06 tff(c_1302, plain, (c5_1(a272))). % 15.30/5.06 tff(c_1298, plain, (c8_1(a442))). % 15.30/5.06 tff(c_1296, plain, (c1_1(a422))). % 15.30/5.06 tff(c_1297, plain, (c10_1(a352))). % 15.30/5.06 tff(c_1293, plain, (c8_1(a333))). % 15.30/5.06 tff(c_1292, plain, (c3_1(a394))). % 15.30/5.06 tff(c_1285, plain, (c7_1(a434))). % 15.30/5.06 tff(c_1280, plain, (c2_1(a350))). % 15.30/5.06 tff(c_1276, plain, (c8_1(a356))). % 15.30/5.06 tff(c_1275, plain, (c2_1(a386))). % 15.30/5.06 tff(c_1272, plain, (c9_1(a386))). % 15.30/5.06 tff(c_1270, plain, (c6_1(a371))). % 15.30/5.06 tff(c_1266, plain, (c4_1(a283))). % 15.30/5.06 tff(c_1265, plain, (c1_1(a345))). % 15.30/5.06 tff(c_1260, plain, (~c10_0)). % 15.30/5.06 tff(c_1259, plain, (~c5_1(a277))). % 15.30/5.06 tff(c_1254, plain, (c6_1(a296))). % 15.30/5.06 tff(c_1253, plain, (~c10_1(a281))). % 15.30/5.06 tff(c_1252, plain, (~c2_1(a283))). % 15.30/5.06 tff(c_1251, plain, (c10_1(a296))). % 15.30/5.06 tff(c_1250, plain, (~c7_1(a296))). % 15.30/5.06 tff(c_1221, plain, (c9_0)). % 15.30/5.07 tff(c_1212, plain, (ndr1_0)). % 15.30/5.07 tff(c_1211, plain, (~c6_0)). % 15.30/5.07 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.30/5.07 %------------------------------------------------------------------------------