%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN421+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 : n019.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 18.77s 6.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SYN421+1 : TPTP v9.0.0. Released v2.1.0. % 0.08/0.14 % 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.15/0.36 % Computer : n019.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Wed Apr 9 07:23:32 EDT 2025 % 0.15/0.36 % CPUTime : % 18.77/6.52 % 18.77/6.52 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.77/6.52 % 18.77/6.52 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.10/6.54 %$ 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 > a607 > a606 > a605 > a604 > a603 > a602 > a601 > a600 > a599 > a598 > a597 > a596 > a595 > a594 > a593 > a592 > a591 > a590 > a589 > a588 > a587 > a586 > a585 > a584 > a583 > a582 > a581 > a580 > a579 > a578 > a577 > a576 > a575 > a574 > a573 > a572 > a571 > a570 > a569 > a568 > a567 > a566 > a565 > a564 > a563 > a562 > a561 > a560 > a559 > a558 > a557 > a556 > a555 > a554 > a553 > a552 > a551 > a550 > a549 > a548 > a547 > a546 > a545 > a544 > a543 > a542 > a541 > a540 > a539 > a538 > a537 > a536 > a535 > a534 > a533 > a532 > a531 > a530 > a529 > a528 > a527 > a526 > a525 > a524 > a523 > a522 > a521 > a520 > a519 > a518 > a517 > a516 > a515 > a514 > a513 > a512 > a511 > a510 > a509 > a508 > a507 > a506 > a505 > a504 > a503 > a502 > a501 > a500 > a499 > a498 > a497 > a496 > a495 > a494 > a493 > a492 > a491 > a490 > a489 > a488 > a487 > a486 > a485 > a484 > a483 > a482 > a481 > a480 > a479 > a478 > a477 > a476 > a475 > a474 > a473 > a472 > a471 > a470 > a469 > a468 > a467 > a466 > a465 > a464 > a463 > a462 > a461 > a460 > a459 > a458 > a457 > a456 > a455 > a454 > a453 > a452 > a451 > a450 > a449 % 19.10/6.54 % 19.10/6.54 %Foreground sorts: % 19.10/6.54 % 19.10/6.54 % 19.10/6.54 %Background operators: % 19.10/6.54 % 19.10/6.54 % 19.10/6.54 %Foreground operators: % 19.10/6.54 tff(a565, type, a565: $i). % 19.10/6.54 tff(c7_0, type, c7_0: $o). % 19.10/6.54 tff(a492, type, a492: $i). % 19.10/6.54 tff(a544, type, a544: $i). % 19.10/6.54 tff(a577, type, a577: $i). % 19.10/6.54 tff(a586, type, a586: $i). % 19.10/6.54 tff(a473, type, a473: $i). % 19.10/6.54 tff(a601, type, a601: $i). % 19.10/6.54 tff(a506, type, a506: $i). % 19.10/6.54 tff(a457, type, a457: $i). % 19.10/6.54 tff(a600, type, a600: $i). % 19.10/6.54 tff(a580, type, a580: $i). % 19.10/6.54 tff(a535, type, a535: $i). % 19.10/6.54 tff(a542, type, a542: $i). % 19.10/6.54 tff(c4_0, type, c4_0: $o). % 19.10/6.54 tff(a541, type, a541: $i). % 19.10/6.54 tff(a556, type, a556: $i). % 19.10/6.54 tff(a550, type, a550: $i). % 19.10/6.54 tff(c3_0, type, c3_0: $o). % 19.10/6.54 tff(a477, type, a477: $i). % 19.10/6.54 tff(a460, type, a460: $i). % 19.10/6.54 tff(a594, type, a594: $i). % 19.10/6.54 tff(a490, type, a490: $i). % 19.10/6.54 tff(a567, type, a567: $i). % 19.10/6.54 tff(a484, type, a484: $i). % 19.10/6.54 tff(c1_2, type, c1_2: ($i * $i) > $o). % 19.10/6.54 tff(a503, type, a503: $i). % 19.10/6.54 tff(a585, type, a585: $i). % 19.10/6.54 tff(a471, type, a471: $i). % 19.10/6.54 tff(a520, type, a520: $i). % 19.10/6.54 tff(a495, type, a495: $i). % 19.10/6.54 tff(a502, type, a502: $i). % 19.10/6.54 tff(a493, type, a493: $i). % 19.10/6.54 tff(a537, type, a537: $i). % 19.10/6.54 tff(a511, type, a511: $i). % 19.10/6.54 tff(a454, type, a454: $i). % 19.10/6.54 tff(a564, type, a564: $i). % 19.10/6.54 tff(a508, type, a508: $i). % 19.10/6.54 tff(a510, type, a510: $i). % 19.10/6.54 tff(a487, type, a487: $i). % 19.10/6.54 tff(a488, type, a488: $i). % 19.10/6.54 tff(a530, type, a530: $i). % 19.10/6.54 tff(a553, type, a553: $i). % 19.10/6.54 tff(a569, type, a569: $i). % 19.10/6.54 tff(a449, type, a449: $i). % 19.10/6.54 tff(a528, type, a528: $i). % 19.10/6.54 tff(a462, type, a462: $i). % 19.10/6.54 tff(a458, type, a458: $i). % 19.10/6.54 tff(c8_0, type, c8_0: $o). % 19.10/6.54 tff(a536, type, a536: $i). % 19.10/6.54 tff(a459, type, a459: $i). % 19.10/6.54 tff(a467, type, a467: $i). % 19.10/6.54 tff(a461, type, a461: $i). % 19.10/6.54 tff(a596, type, a596: $i). % 19.10/6.54 tff(a498, type, a498: $i). % 19.10/6.54 tff(a505, type, a505: $i). % 19.10/6.54 tff(a456, type, a456: $i). % 19.10/6.54 tff(a532, type, a532: $i). % 19.10/6.54 tff(a504, type, a504: $i). % 19.10/6.54 tff(a468, type, a468: $i). % 19.10/6.54 tff(c5_0, type, c5_0: $o). % 19.10/6.54 tff(a539, type, a539: $i). % 19.10/6.54 tff(a551, type, a551: $i). % 19.10/6.54 tff(a572, type, a572: $i). % 19.10/6.54 tff(a518, type, a518: $i). % 19.10/6.54 tff(a546, type, a546: $i). % 19.10/6.54 tff(a599, type, a599: $i). % 19.10/6.54 tff(c6_0, type, c6_0: $o). % 19.10/6.54 tff(c8_2, type, c8_2: ($i * $i) > $o). % 19.10/6.54 tff(a602, type, a602: $i). % 19.10/6.54 tff(a453, type, a453: $i). % 19.10/6.54 tff(a606, type, a606: $i). % 19.10/6.54 tff(a570, type, a570: $i). % 19.10/6.54 tff(a499, type, a499: $i). % 19.10/6.54 tff(a605, type, a605: $i). % 19.10/6.54 tff(a533, type, a533: $i). % 19.10/6.54 tff(a500, type, a500: $i). % 19.10/6.54 tff(a472, type, a472: $i). % 19.10/6.54 tff(a470, type, a470: $i). % 19.10/6.54 tff(a598, type, a598: $i). % 19.10/6.54 tff(a516, type, a516: $i). % 19.10/6.54 tff(a524, type, a524: $i). % 19.10/6.54 tff(a563, type, a563: $i). % 19.10/6.54 tff(a451, type, a451: $i). % 19.10/6.54 tff(a571, type, a571: $i). % 19.10/6.54 tff(a543, type, a543: $i). % 19.10/6.54 tff(a509, type, a509: $i). % 19.10/6.54 tff(a589, type, a589: $i). % 19.10/6.54 tff(a558, type, a558: $i). % 19.10/6.54 tff(c1_0, type, c1_0: $o). % 19.10/6.54 tff(c8_1, type, c8_1: $i > $o). % 19.10/6.54 tff(a465, type, a465: $i). % 19.10/6.54 tff(a469, type, a469: $i). % 19.10/6.54 tff(c2_1, type, c2_1: $i > $o). % 19.10/6.54 tff(a549, type, a549: $i). % 19.10/6.54 tff(a555, type, a555: $i). % 19.10/6.54 tff(ndr1_1, type, ndr1_1: $i > $o). % 19.10/6.54 tff(c2_0, type, c2_0: $o). % 19.10/6.54 tff(c4_1, type, c4_1: $i > $o). % 19.10/6.54 tff(a529, type, a529: $i). % 19.10/6.54 tff(a475, type, a475: $i). % 19.10/6.54 tff(a557, type, a557: $i). % 19.10/6.54 tff(a575, type, a575: $i). % 19.10/6.54 tff(a597, type, a597: $i). % 19.10/6.54 tff(a591, type, a591: $i). % 19.10/6.54 tff(a494, type, a494: $i). % 19.10/6.54 tff(a545, type, a545: $i). % 19.10/6.54 tff(a491, type, a491: $i). % 19.10/6.54 tff(a562, type, a562: $i). % 19.10/6.54 tff(a463, type, a463: $i). % 19.10/6.54 tff(a474, type, a474: $i). % 19.10/6.54 tff(a581, type, a581: $i). % 19.10/6.54 tff(a568, type, a568: $i). % 19.10/6.54 tff(a593, type, a593: $i). % 19.10/6.54 tff(a479, type, a479: $i). % 19.10/6.54 tff(a489, type, a489: $i). % 19.10/6.54 tff(c9_1, type, c9_1: $i > $o). % 19.10/6.54 tff(a584, type, a584: $i). % 19.10/6.54 tff(c10_1, type, c10_1: $i > $o). % 19.10/6.54 tff(c10_0, type, c10_0: $o). % 19.10/6.54 tff(a482, type, a482: $i). % 19.10/6.54 tff(a603, type, a603: $i). % 19.10/6.54 tff(a452, type, a452: $i). % 19.10/6.54 tff(c6_2, type, c6_2: ($i * $i) > $o). % 19.10/6.54 tff(a507, type, a507: $i). % 19.10/6.54 tff(a587, type, a587: $i). % 19.10/6.54 tff(a578, type, a578: $i). % 19.10/6.54 tff(a559, type, a559: $i). % 19.10/6.54 tff(a478, type, a478: $i). % 19.10/6.54 tff(a464, type, a464: $i). % 19.10/6.54 tff(a552, type, a552: $i). % 19.10/6.54 tff(a548, type, a548: $i). % 19.10/6.54 tff(a534, type, a534: $i). % 19.10/6.54 tff(a588, type, a588: $i). % 19.10/6.54 tff(a525, type, a525: $i). % 19.10/6.54 tff(a523, type, a523: $i). % 19.10/6.54 tff(a595, type, a595: $i). % 19.10/6.54 tff(a531, type, a531: $i). % 19.10/6.54 tff(a522, type, a522: $i). % 19.10/6.54 tff(a573, type, a573: $i). % 19.10/6.54 tff(ndr1_0, type, ndr1_0: $o). % 19.10/6.54 tff(a480, type, a480: $i). % 19.10/6.54 tff(a485, type, a485: $i). % 19.10/6.54 tff(a476, type, a476: $i). % 19.10/6.54 tff(a483, type, a483: $i). % 19.10/6.54 tff(a455, type, a455: $i). % 19.10/6.54 tff(a538, type, a538: $i). % 19.10/6.54 tff(a501, type, a501: $i). % 19.10/6.54 tff(a486, type, a486: $i). % 19.10/6.54 tff(c9_2, type, c9_2: ($i * $i) > $o). % 19.10/6.54 tff(a547, type, a547: $i). % 19.10/6.54 tff(a450, type, a450: $i). % 19.10/6.54 tff(c10_2, type, c10_2: ($i * $i) > $o). % 19.10/6.54 tff(a527, type, a527: $i). % 19.10/6.54 tff(a526, type, a526: $i). % 19.10/6.54 tff(a576, type, a576: $i). % 19.10/6.54 tff(a561, type, a561: $i). % 19.10/6.54 tff(a481, type, a481: $i). % 19.10/6.54 tff(c1_1, type, c1_1: $i > $o). % 19.10/6.54 tff(a497, type, a497: $i). % 19.10/6.54 tff(a607, type, a607: $i). % 19.10/6.54 tff(a521, type, a521: $i). % 19.10/6.54 tff(c5_2, type, c5_2: ($i * $i) > $o). % 19.10/6.54 tff(a496, type, a496: $i). % 19.10/6.54 tff(a540, type, a540: $i). % 19.10/6.54 tff(c9_0, type, c9_0: $o). % 19.10/6.54 tff(a519, type, a519: $i). % 19.10/6.54 tff(c7_1, type, c7_1: $i > $o). % 19.10/6.54 tff(c6_1, type, c6_1: $i > $o). % 19.10/6.54 tff(a590, type, a590: $i). % 19.10/6.54 tff(c4_2, type, c4_2: ($i * $i) > $o). % 19.10/6.54 tff(a517, type, a517: $i). % 19.10/6.54 tff(a560, type, a560: $i). % 19.10/6.54 tff(a582, type, a582: $i). % 19.10/6.54 tff(a566, type, a566: $i). % 19.10/6.54 tff(a554, type, a554: $i). % 19.10/6.54 tff(a515, type, a515: $i). % 19.10/6.54 tff(c5_1, type, c5_1: $i > $o). % 19.10/6.54 tff(c7_2, type, c7_2: ($i * $i) > $o). % 19.10/6.54 tff(a583, type, a583: $i). % 19.10/6.54 tff(c3_2, type, c3_2: ($i * $i) > $o). % 19.10/6.54 tff(a514, type, a514: $i). % 19.10/6.54 tff(a466, type, a466: $i). % 19.10/6.54 tff(c2_2, type, c2_2: ($i * $i) > $o). % 19.10/6.54 tff(a604, type, a604: $i). % 19.10/6.54 tff(a513, type, a513: $i). % 19.10/6.54 tff(a512, type, a512: $i). % 19.10/6.54 tff(a574, type, a574: $i). % 19.10/6.54 tff(a592, type, a592: $i). % 19.10/6.54 tff(c3_1, type, c3_1: $i > $o). % 19.10/6.54 tff(a579, type, a579: $i). % 19.10/6.54 % 19.10/6.54 %Saturated clause set: % 19.10/6.54 tff(c_6677, plain, (~c2_1(a601))). % 19.10/6.54 tff(c_6674, plain, (~c2_1(a566))). % 19.10/6.54 tff(c_6666, plain, (~c6_1(a601))). % 19.10/6.54 tff(c_6665, plain, (~c3_1(a601))). % 19.10/6.54 tff(c_6660, plain, (c8_1(a601))). % 19.10/6.54 tff(c_6641, plain, (~ndr1_1(a601))). % 19.10/6.54 tff(c_6634, plain, (c8_1(a566))). % 19.10/6.54 tff(c_6626, plain, (~c6_1(a566))). % 19.10/6.54 tff(c_6624, plain, (c5_1(a566))). % 19.10/6.54 tff(c_6609, plain, (~ndr1_1(a566))). % 19.10/6.54 tff(c_6452, plain, (~c10_2(a509, a510))). % 19.10/6.54 tff(c_6433, plain, (c3_2(a509, a510))). % 19.10/6.54 tff(c_6424, plain, (~c2_2(a509, a510))). % 19.10/6.54 tff(c_6261, plain, (~c1_1(a509))). % 19.10/6.54 tff(c_6258, plain, (c10_1(a509))). % 19.10/6.54 tff(c_6248, plain, (c6_1(a509))). % 19.10/6.54 tff(c_6245, plain, (~c3_1(a509))). % 19.10/6.54 tff(c_6242, plain, (ndr1_1(a509))). % 19.10/6.54 tff(c_6159, plain, (c5_1(a601))). % 19.10/6.54 tff(c_6150, plain, (~c10_1(a601))). % 19.10/6.54 tff(c_6147, plain, (~c3_1(a566))). % 19.10/6.54 tff(c_6118, plain, (~c2_1(a513))). % 19.10/6.54 tff(c_6111, plain, (c8_1(a513))). % 19.10/6.54 tff(c_6105, plain, (~c3_1(a513))). % 19.10/6.54 tff(c_6109, plain, (c5_1(a513))). % 19.10/6.54 tff(c_6090, plain, (~ndr1_1(a513))). % 19.10/6.55 tff(c_6038, plain, (![X80_111]: (~c9_2(X80_111, a558) | ~c9_1(X80_111) | ~c3_1(X80_111)))). % 19.10/6.55 tff(c_6032, plain, (![X61_214]: (~c9_1(X61_214) | ~c3_1(X61_214) | ~c2_2(X61_214, a558) | c2_2(X61_214, a544) | c10_2(X61_214, a544) | ~ndr1_1(X61_214) | c7_1(X61_214) | c5_1(X61_214)))). % 19.10/6.55 tff(c_6015, plain, (![X80_111]: (~c4_2(X80_111, a558) | ~c9_1(X80_111) | ~c3_1(X80_111)))). % 19.10/6.55 tff(c_6007, plain, (![X80_111]: (~c3_2(X80_111, a558) | ~c9_1(X80_111) | ~c3_1(X80_111)))). % 19.10/6.55 tff(c_6002, plain, (c9_1(a592))). % 19.10/6.55 tff(c_5994, plain, (~c8_1(a592))). % 19.10/6.55 tff(c_5991, plain, (~c2_2(a586, a587))). % 19.10/6.55 tff(c_5988, plain, (~c2_2(a538, a540))). % 19.10/6.55 tff(c_5963, plain, (![X61_87, X46_208]: (~c2_2(X61_87, X46_208) | c4_2(X61_87, X46_208) | c3_2(X61_87, X46_208) | c2_2(X61_87, a544) | c10_2(X61_87, a544) | ~ndr1_1(X61_87) | c7_1(X61_87) | c5_1(X61_87)))). % 19.10/6.55 tff(c_5971, plain, (c2_2(a460, a461))). % 19.10/6.55 tff(c_5955, plain, (![X44_64, X46_68, X45_67]: (~c2_2(X44_64, X46_68) | c4_2(X44_64, X46_68) | c3_2(X44_64, X46_68) | c2_2(X44_64, X45_67) | c10_2(X44_64, X45_67) | ~c4_2(X44_64, X45_67) | ~ndr1_1(X44_64) | c7_1(X44_64)))). % 19.10/6.55 tff(c_5948, plain, (~c9_1(a449))). % 19.10/6.55 tff(c_5941, plain, (![X80_111]: (ndr1_1(X80_111) | ~c9_1(X80_111) | ~c3_1(X80_111)))). % 19.10/6.55 tff(c_5885, plain, (~c6_2(a602, a603))). % 19.10/6.55 tff(c_5870, plain, (~c7_2(a602, a603))). % 19.10/6.55 tff(c_5865, plain, (~c8_2(a602, a603))). % 19.10/6.55 tff(c_5789, plain, (![X71_99]: (c2_1(X71_99) | ~c1_1(X71_99) | c5_1(X71_99) | ~c4_1(X71_99)))). % 19.10/6.55 tff(c_5791, plain, (~c1_1(a547))). % 19.10/6.55 tff(c_5767, plain, (![X19_31]: (~c6_1(X19_31) | c2_1(X19_31) | ~c1_1(X19_31)))). % 19.10/6.55 tff(c_5775, plain, (~c4_1(a602))). % 19.10/6.55 tff(c_5770, plain, (~c6_1(a602))). % 19.10/6.55 tff(c_5758, plain, (![X117_157]: (~c7_1(X117_157) | ~c6_1(X117_157) | c2_1(X117_157)))). % 19.10/6.55 tff(c_5753, plain, (c7_1(a602))). % 19.10/6.55 tff(c_5750, plain, (ndr1_1(a602))). % 19.10/6.55 tff(c_5722, plain, (~c1_2(a605, a606))). % 19.10/6.55 tff(c_5719, plain, (c2_2(a605, a606))). % 19.10/6.55 tff(c_5675, plain, (~c3_2(a605, a606))). % 19.10/6.55 tff(c_5656, plain, (![X104_140, X105_142]: (~c7_2(X104_140, a589) | ~c3_2(X104_140, X105_142) | ~c1_2(X104_140, X105_142) | ~ndr1_1(X104_140) | c10_1(X104_140)))). % 19.10/6.55 tff(c_5652, plain, (~c4_1(a585))). % 19.10/6.55 tff(c_5636, plain, (![X71_99]: (c10_1(X71_99) | c3_1(X71_99) | c5_1(X71_99) | ~c4_1(X71_99)))). % 19.10/6.55 tff(c_5639, plain, (c3_1(a460))). % 19.10/6.55 tff(c_5642, plain, (~c5_1(a605))). % 19.10/6.55 tff(c_5638, plain, (c3_1(a547))). % 19.10/6.55 tff(c_5624, plain, (![X33_50]: (c10_1(X33_50) | ~c6_1(X33_50) | c3_1(X33_50)))). % 19.10/6.55 tff(c_5621, plain, (ndr1_1(a605))). % 19.10/6.55 tff(c_5616, plain, (~c4_1(a605))). % 19.10/6.55 tff(c_5586, plain, (![X104_140, X105_142]: (~c10_2(X104_140, a589) | ~c3_2(X104_140, X105_142) | ~c1_2(X104_140, X105_142) | ~ndr1_1(X104_140) | c10_1(X104_140)))). % 19.10/6.55 tff(c_5579, plain, (~c7_2(a538, a540))). % 19.10/6.55 tff(c_5550, plain, (![X30_46, X31_48]: (c1_1(X30_46) | c9_1(X30_46) | ~c9_2(X30_46, X31_48) | ~c7_2(X30_46, X31_48) | c10_2(X30_46, X31_48) | ~ndr1_1(X30_46)))). % 19.10/6.55 tff(c_5539, plain, (c5_1(a502))). % 19.10/6.55 tff(c_5535, plain, (~c9_1(a502))). % 19.10/6.55 tff(c_5527, plain, (~c1_2(a460, a461))). % 19.10/6.55 tff(c_5524, plain, (~c1_2(a599, a600))). % 19.10/6.55 tff(c_5523, plain, (~c1_2(a538, a539))). % 19.10/6.55 tff(c_5497, plain, (![X104_140, X105_142]: (~c2_2(X104_140, a589) | ~c3_2(X104_140, X105_142) | ~c1_2(X104_140, X105_142) | ~ndr1_1(X104_140) | c10_1(X104_140)))). % 19.10/6.55 tff(c_5485, plain, (~c8_1(a481))). % 19.10/6.55 tff(c_5476, plain, (![X61_191]: (c7_2(X61_191, a553) | ~c5_2(X61_191, a544) | ~ndr1_1(X61_191) | ~c8_1(X61_191) | c5_1(X61_191)))). % 19.10/6.55 tff(c_5444, plain, (![X69_96, X70_98]: (c7_2(X69_96, a553) | c8_2(X69_96, X70_98) | ~c5_2(X69_96, X70_98) | ~c9_2(X69_96, X70_98) | ~ndr1_1(X69_96) | ~c8_1(X69_96)))). % 19.10/6.55 tff(c_5431, plain, (~c4_1(a513))). % 19.10/6.55 tff(c_5426, plain, (~c6_1(a513))). % 19.10/6.55 tff(c_5415, plain, (![X61_187]: (c10_2(X61_187, a553) | ~c5_2(X61_187, a544) | ~ndr1_1(X61_187) | ~c8_1(X61_187) | c5_1(X61_187)))). % 19.10/6.55 tff(c_5366, plain, (![X61_87]: (c8_2(X61_87, a553) | c8_2(X61_87, a544) | ~c5_2(X61_87, a544) | ~ndr1_1(X61_87) | ~c8_1(X61_87) | c5_1(X61_87)))). % 19.10/6.55 tff(c_5382, plain, (![X69_96, X70_98]: (c10_2(X69_96, a553) | c8_2(X69_96, X70_98) | ~c5_2(X69_96, X70_98) | ~c9_2(X69_96, X70_98) | ~ndr1_1(X69_96) | ~c8_1(X69_96)))). % 19.10/6.55 tff(c_5379, plain, (~c8_1(a475))). % 19.10/6.55 tff(c_5376, plain, (~c8_1(a538))). % 19.10/6.56 tff(c_5348, plain, (![X69_96, X70_98]: (c8_2(X69_96, a553) | c8_2(X69_96, X70_98) | ~c5_2(X69_96, X70_98) | ~c9_2(X69_96, X70_98) | ~ndr1_1(X69_96) | ~c8_1(X69_96)))). % 19.10/6.56 tff(c_5345, plain, (c9_1(a513))). % 19.10/6.56 tff(c_5332, plain, (c5_1(a537))). % 19.10/6.56 tff(c_5327, plain, (![X43_63]: (c9_1(X43_63) | c5_1(X43_63)))). % 19.10/6.56 tff(c_5307, plain, (~c6_1(a449))). % 19.10/6.56 tff(c_5304, plain, (c5_1(a449))). % 19.10/6.56 tff(c_5293, plain, (~ndr1_1(a449))). % 19.10/6.56 tff(c_5255, plain, (![X52_76]: (c9_2(X52_76, a527) | ~c9_1(X52_76) | ~c6_1(X52_76)))). % 19.10/6.56 tff(c_5228, plain, (![X52_76]: (c8_2(X52_76, a527) | ~c9_1(X52_76) | ~c6_1(X52_76)))). % 19.10/6.56 tff(c_5225, plain, (~c4_1(a481))). % 19.10/6.56 tff(c_5220, plain, (~c6_1(a481))). % 19.10/6.56 tff(c_5213, plain, (![X52_76]: (c7_2(X52_76, a527) | ~c9_1(X52_76) | ~c6_1(X52_76)))). % 19.10/6.56 tff(c_5199, plain, (![X52_76]: (ndr1_1(X52_76) | ~c9_1(X52_76) | ~c6_1(X52_76)))). % 19.10/6.56 tff(c_5192, plain, (![X14_25]: (~c5_2(a481, X14_25) | ~c3_2(a481, X14_25) | ~c7_2(a481, X14_25)))). % 19.10/6.56 tff(c_5168, plain, (![X61_87]: (c4_2(X61_87, a544) | c5_1(X61_87)))). % 19.10/6.56 tff(c_5163, plain, (![X61_87]: (c9_2(X61_87, a544) | c5_1(X61_87)))). % 19.10/6.56 tff(c_5130, plain, (![X61_87]: (~c8_2(X61_87, a544) | c5_1(X61_87)))). % 19.10/6.56 tff(c_4925, plain, (~c5_2(a538, a539))). % 19.10/6.56 tff(c_4913, plain, (c9_2(a538, a540))). % 19.10/6.56 tff(c_4892, plain, (c6_2(a538, a540))). % 19.10/6.56 tff(c_4889, plain, (c3_2(a538, a539))). % 19.10/6.56 tff(c_4882, plain, (~c6_2(a538, a539))). % 19.10/6.56 tff(c_4873, plain, (~c8_1(a537))). % 19.10/6.56 tff(c_4867, plain, (![X61_87]: (ndr1_1(X61_87) | c5_1(X61_87)))). % 19.10/6.56 tff(c_4838, plain, (~c4_2(a538, a540))). % 19.10/6.56 tff(c_4829, plain, (~c1_1(a537))). % 19.10/6.56 tff(c_4822, plain, (~c9_1(a537))). % 19.10/6.56 tff(c_4756, plain, (~c9_2(a504, a505))). % 19.10/6.56 tff(c_4718, plain, (ndr1_1(a538))). % 19.10/6.56 tff(c_4706, plain, (c2_2(a560, a561))). % 19.10/6.56 tff(c_4684, plain, (~c2_2(a504, a505))). % 19.10/6.56 tff(c_4681, plain, (~c10_2(a475, a476))). % 19.10/6.56 tff(c_4675, plain, (~c7_2(a475, a476))). % 19.10/6.56 tff(c_4657, plain, (c9_2(a475, a476))). % 19.10/6.56 tff(c_4653, plain, (~c3_2(a504, a505))). % 19.10/6.56 tff(c_4647, plain, (c1_2(a560, a561))). % 19.10/6.56 tff(c_4632, plain, (c3_1(a449))). % 19.10/6.56 tff(c_4628, plain, (c1_1(a455))). % 19.10/6.56 tff(c_4620, plain, (~c2_1(a449))). % 19.10/6.56 tff(c_4624, plain, (ndr1_1(a475))). % 19.10/6.56 tff(c_4615, plain, (c8_1(a449))). % 19.10/6.56 tff(c_4606, plain, (ndr1_1(a560))). % 19.10/6.56 tff(c_4600, plain, (c5_1(a547))). % 19.10/6.56 tff(c_4596, plain, (c6_1(a547))). % 19.10/6.56 tff(c_4585, plain, (~c8_1(a455))). % 19.10/6.56 tff(c_4572, plain, (ndr1_1(a504))). % 19.10/6.56 tff(c_4569, plain, (c10_1(a504))). % 19.10/6.56 tff(c_4562, plain, (~c2_1(a586))). % 19.10/6.56 tff(c_4561, plain, (~c2_1(a515))). % 19.10/6.56 tff(c_4547, plain, (![X7_17]: (~c7_1(X7_17) | ~c2_1(X7_17) | ~c8_1(X7_17)))). % 19.10/6.56 tff(c_4551, plain, (c9_1(a455))). % 19.10/6.56 tff(c_4539, plain, (~c6_2(a515, a516))). % 19.10/6.56 tff(c_4534, plain, (~c4_1(a489))). % 19.10/6.56 tff(c_4528, plain, (![X71_99]: (c6_1(X71_99) | c5_1(X71_99) | ~c4_1(X71_99)))). % 19.10/6.56 tff(c_4514, plain, (![X79_110]: (c1_2(X79_110, a557) | c10_1(X79_110) | c8_1(X79_110)))). % 19.10/6.56 tff(c_4510, plain, (![X79_110]: (~c8_2(X79_110, a557) | c10_1(X79_110) | c8_1(X79_110)))). % 19.10/6.56 tff(c_4506, plain, (![X79_110]: (~c6_2(X79_110, a557) | c10_1(X79_110) | c8_1(X79_110)))). % 19.10/6.56 tff(c_4500, plain, (~c10_2(a515, a516))). % 19.10/6.56 tff(c_4488, plain, (![X79_110]: (ndr1_1(X79_110) | c10_1(X79_110) | c8_1(X79_110)))). % 19.10/6.56 tff(c_4485, plain, (ndr1_1(a515))). % 19.10/6.56 tff(c_4482, plain, (c8_1(a515))). % 19.10/6.56 tff(c_4392, plain, (~c1_1(a460))). % 19.10/6.56 tff(c_4391, plain, (~c1_1(a597))). % 19.10/6.56 tff(c_4383, plain, (![X19_31]: (c7_1(X19_31) | ~c1_1(X19_31)))). % 19.10/6.56 tff(c_4377, plain, (c3_2(a599, a600))). % 19.10/6.56 tff(c_4373, plain, (~c9_2(a494, a495))). % 19.10/6.56 tff(c_4364, plain, (~c6_2(a494, a495))). % 19.10/6.56 tff(c_4360, plain, (~c5_2(a599, a600))). % 19.10/6.56 tff(c_4351, plain, (~c4_2(a586, a587))). % 19.10/6.56 tff(c_4338, plain, (c10_2(a494, a495))). % 19.10/6.56 tff(c_4335, plain, (~c5_2(a489, a490))). % 19.10/6.56 tff(c_4332, plain, (~c1_2(a489, a490))). % 19.10/6.56 tff(c_4329, plain, (~c1_2(a586, a588))). % 19.10/6.56 tff(c_4321, plain, (~c2_2(a489, a490))). % 19.10/6.56 tff(c_4315, plain, (~c5_2(a519, a520))). % 19.10/6.56 tff(c_4308, plain, (c3_2(a586, a588))). % 19.10/6.56 tff(c_4306, plain, (c10_2(a481, a483))). % 19.10/6.56 tff(c_4302, plain, (~c7_2(a519, a520))). % 19.10/6.56 tff(c_4299, plain, (c5_2(a481, a483))). % 19.10/6.56 tff(c_4292, plain, (c9_2(a519, a520))). % 19.10/6.56 tff(c_4286, plain, (c6_2(a481, a482))). % 19.10/6.57 tff(c_4277, plain, (c10_2(a481, a482))). % 19.10/6.57 tff(c_4274, plain, (~c7_2(a481, a483))). % 19.10/6.57 tff(c_4267, plain, (~c2_2(a599, a600))). % 19.10/6.57 tff(c_4263, plain, (c4_2(a481, a482))). % 19.10/6.57 tff(c_4258, plain, (~c8_2(a586, a588))). % 19.10/6.57 tff(c_4256, plain, (~c1_2(a586, a587))). % 19.10/6.57 tff(c_4252, plain, (~c5_2(a586, a587))). % 19.10/6.57 tff(c_4242, plain, (ndr1_1(a494))). % 19.10/6.57 tff(c_4221, plain, (~c4_1(a494))). % 19.10/6.57 tff(c_4217, plain, (ndr1_1(a519))). % 19.10/6.57 tff(c_4214, plain, (~c1_1(a494))). % 19.10/6.57 tff(c_4211, plain, (c4_2(a460, a461))). % 19.10/6.57 tff(c_4205, plain, (c8_1(a586))). % 19.10/6.57 tff(c_4203, plain, (~c8_1(a519))). % 19.10/6.57 tff(c_4201, plain, (~c6_1(a489))). % 19.10/6.57 tff(c_4198, plain, (ndr1_1(a586))). % 19.10/6.57 tff(c_4195, plain, (ndr1_1(a489))). % 19.10/6.57 tff(c_4193, plain, (~c7_2(a464, a466))). % 19.10/6.57 tff(c_4187, plain, (~c10_1(a489))). % 19.10/6.57 tff(c_4185, plain, (c3_2(a460, a461))). % 19.10/6.57 tff(c_4180, plain, (~c10_2(a460, a461))). % 19.10/6.57 tff(c_4178, plain, (~c5_1(a585))). % 19.10/6.57 tff(c_4174, plain, (ndr1_1(a599))). % 19.10/6.57 tff(c_4170, plain, (~c7_1(a597))). % 19.10/6.57 tff(c_4168, plain, (c9_1(a519))). % 19.10/6.57 tff(c_4166, plain, (~c2_2(a464, a465))). % 19.10/6.57 tff(c_4164, plain, (~c6_2(a464, a465))). % 19.10/6.57 tff(c_4159, plain, (c5_2(a464, a466))). % 19.10/6.57 tff(c_4157, plain, (c10_2(a464, a465))). % 19.10/6.57 tff(c_4132, plain, (~c4_1(a599))). % 19.10/6.57 tff(c_4122, plain, (ndr1_1(a481))). % 19.10/6.57 tff(c_4102, plain, (ndr1_1(a464))). % 19.10/6.57 tff(c_4098, plain, (ndr1_1(a460))). % 19.10/6.57 tff(c_4087, plain, (~c6_0)). % 19.10/6.57 tff(c_4080, plain, (c3_1(a464))). % 19.10/6.57 tff(c_4066, plain, (c6_1(a460))). % 19.10/6.57 tff(c_4063, plain, (~c7_1(a460))). % 19.10/6.57 tff(c_4058, plain, (c7_0)). % 19.10/6.57 tff(c_4048, plain, (~c4_1(a454))). % 19.10/6.57 tff(c_4033, plain, (~c8_0)). % 19.10/6.57 tff(c_4016, plain, (c1_0)). % 19.10/6.57 tff(c_4008, plain, (c9_0)). % 19.10/6.57 tff(c_4007, plain, (c5_0)). % 19.10/6.57 tff(c_4000, plain, (~c4_0)). % 19.10/6.57 tff(c_3999, plain, (~c3_0)). % 19.10/6.57 tff(c_3998, plain, (ndr1_0)). % 19.10/6.57 tff(c_3928, plain, (~c2_0)). % 19.10/6.57 tff(c_3927, plain, (c10_0)). % 19.10/6.57 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.10/6.57 %------------------------------------------------------------------------------