%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN544+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 : n005.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:52 PM UTC 2025 % Result : CounterSatisfiable 18.68s 6.10s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN544+1 : TPTP v9.0.0. Released v2.1.0. % 0.11/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 : n005.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:58:57 EDT 2025 % 0.13/0.35 % CPUTime : % 18.68/6.10 % 18.68/6.10 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.68/6.10 % 18.68/6.10 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.68/6.11 %$ c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ndr1_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a99 > a98 > a97 > a96 > a95 > a94 > a93 > a92 > a91 > a90 > a9 > a89 > a88 > a87 > a86 > a85 > a84 > a83 > a82 > a81 > a80 > a8 > a79 > a78 > a77 > a76 > a75 > a74 > a73 > a72 > a71 > a70 > a7 > a69 > a68 > a67 > a66 > a65 > a64 > a63 > a62 > a61 > a60 > a6 > a59 > a58 > a57 > a56 > a55 > a54 > a53 > a52 > a51 > a50 > a5 > a49 > a48 > a47 > a46 > a45 > a44 > a43 > a42 > a41 > a40 > a4 > a39 > a38 > a37 > a36 > a35 > a34 > a33 > a32 > a31 > a30 > a3 > a29 > a28 > a27 > a26 > a25 > a24 > a23 > a22 > a21 > a20 > a2 > a19 > a18 > a17 > a16 > a15 > a146 > a145 > a144 > a143 > a142 > a141 > a140 > a14 > a139 > a138 > a137 > a136 > a135 > a134 > a133 > a132 > a131 > a130 > a13 > a129 > a128 > a127 > a126 > a125 > a124 > a123 > a122 > a121 > a120 > a12 > a119 > a118 > a117 > a116 > a115 > a114 > a113 > a112 > a111 > a110 > a11 > a109 > a108 > a107 > a106 > a105 > a104 > a103 > a102 > a101 > a100 > a10 > a1 % 18.68/6.11 % 18.68/6.11 %Foreground sorts: % 18.68/6.11 % 18.68/6.11 % 18.68/6.11 %Background operators: % 18.68/6.11 % 18.68/6.11 % 18.68/6.11 %Foreground operators: % 18.68/6.11 tff(a99, type, a99: $i). % 18.68/6.11 tff(a143, type, a143: $i). % 18.68/6.11 tff(c7_0, type, c7_0: $o). % 18.68/6.11 tff(a1, type, a1: $i). % 18.68/6.11 tff(a94, type, a94: $i). % 18.68/6.11 tff(a68, type, a68: $i). % 18.68/6.11 tff(a101, type, a101: $i). % 18.68/6.11 tff(a100, type, a100: $i). % 18.68/6.11 tff(a108, type, a108: $i). % 18.68/6.11 tff(a89, type, a89: $i). % 18.68/6.11 tff(a64, type, a64: $i). % 18.68/6.11 tff(a112, type, a112: $i). % 18.68/6.11 tff(a3, type, a3: $i). % 18.68/6.11 tff(a97, type, a97: $i). % 18.68/6.11 tff(a32, type, a32: $i). % 18.68/6.11 tff(a35, type, a35: $i). % 18.68/6.11 tff(c4_0, type, c4_0: $o). % 18.68/6.11 tff(a47, type, a47: $i). % 18.68/6.11 tff(a73, type, a73: $i). % 18.68/6.11 tff(a34, type, a34: $i). % 18.68/6.11 tff(a146, type, a146: $i). % 18.68/6.11 tff(a69, type, a69: $i). % 18.68/6.11 tff(a124, type, a124: $i). % 18.68/6.11 tff(a122, type, a122: $i). % 18.68/6.11 tff(a141, type, a141: $i). % 18.68/6.11 tff(a120, type, a120: $i). % 18.68/6.11 tff(a61, type, a61: $i). % 18.68/6.11 tff(c3_0, type, c3_0: $o). % 18.68/6.11 tff(a140, type, a140: $i). % 18.68/6.11 tff(a26, type, a26: $i). % 18.68/6.11 tff(a138, type, a138: $i). % 18.68/6.11 tff(a103, type, a103: $i). % 18.68/6.11 tff(c1_2, type, c1_2: ($i * $i) > $o). % 18.68/6.11 tff(a60, type, a60: $i). % 18.68/6.12 tff(a40, type, a40: $i). % 18.68/6.12 tff(a113, type, a113: $i). % 18.68/6.12 tff(a130, type, a130: $i). % 18.68/6.12 tff(a36, type, a36: $i). % 18.68/6.12 tff(a75, type, a75: $i). % 18.68/6.12 tff(a62, type, a62: $i). % 18.68/6.12 tff(a15, type, a15: $i). % 18.68/6.12 tff(a145, type, a145: $i). % 18.68/6.12 tff(a119, type, a119: $i). % 18.68/6.12 tff(a93, type, a93: $i). % 18.68/6.12 tff(a107, type, a107: $i). % 18.68/6.12 tff(a72, type, a72: $i). % 18.68/6.12 tff(a67, type, a67: $i). % 18.68/6.12 tff(a131, type, a131: $i). % 18.68/6.12 tff(a31, type, a31: $i). % 18.68/6.12 tff(a86, type, a86: $i). % 18.68/6.12 tff(a88, type, a88: $i). % 18.68/6.12 tff(c8_0, type, c8_0: $o). % 18.68/6.12 tff(a83, type, a83: $i). % 18.68/6.12 tff(a63, type, a63: $i). % 18.68/6.12 tff(a23, type, a23: $i). % 18.68/6.12 tff(a12, type, a12: $i). % 18.68/6.12 tff(a10, type, a10: $i). % 18.68/6.12 tff(a126, type, a126: $i). % 18.68/6.12 tff(a110, type, a110: $i). % 18.68/6.12 tff(a78, type, a78: $i). % 18.68/6.12 tff(a33, type, a33: $i). % 18.68/6.12 tff(a121, type, a121: $i). % 18.68/6.12 tff(a41, type, a41: $i). % 18.68/6.12 tff(a43, type, a43: $i). % 18.68/6.12 tff(a29, type, a29: $i). % 18.68/6.12 tff(a17, type, a17: $i). % 18.68/6.12 tff(a74, type, a74: $i). % 18.68/6.12 tff(a51, type, a51: $i). % 18.68/6.12 tff(a136, type, a136: $i). % 18.68/6.12 tff(a125, type, a125: $i). % 18.68/6.12 tff(c5_0, type, c5_0: $o). % 18.68/6.12 tff(a127, type, a127: $i). % 18.68/6.12 tff(a98, type, a98: $i). % 18.68/6.12 tff(a111, type, a111: $i). % 18.68/6.12 tff(a142, type, a142: $i). % 18.68/6.12 tff(a28, type, a28: $i). % 18.68/6.12 tff(a58, type, a58: $i). % 18.68/6.12 tff(c6_0, type, c6_0: $o). % 18.68/6.12 tff(a84, type, a84: $i). % 18.68/6.12 tff(a104, type, a104: $i). % 18.68/6.12 tff(c8_2, type, c8_2: ($i * $i) > $o). % 18.68/6.12 tff(a14, type, a14: $i). % 18.68/6.12 tff(a22, type, a22: $i). % 18.68/6.12 tff(a87, type, a87: $i). % 18.68/6.12 tff(a134, type, a134: $i). % 18.68/6.12 tff(a139, type, a139: $i). % 18.68/6.12 tff(a77, type, a77: $i). % 18.68/6.12 tff(a18, type, a18: $i). % 18.68/6.12 tff(a46, type, a46: $i). % 18.68/6.12 tff(a7, type, a7: $i). % 18.68/6.12 tff(a11, type, a11: $i). % 18.68/6.12 tff(a118, type, a118: $i). % 18.68/6.12 tff(a76, type, a76: $i). % 18.68/6.12 tff(a39, type, a39: $i). % 18.68/6.12 tff(a25, type, a25: $i). % 18.68/6.12 tff(c1_0, type, c1_0: $o). % 18.68/6.12 tff(a71, type, a71: $i). % 18.68/6.12 tff(c8_1, type, c8_1: $i > $o). % 18.68/6.12 tff(a53, type, a53: $i). % 18.68/6.12 tff(a38, type, a38: $i). % 18.68/6.12 tff(a50, type, a50: $i). % 18.68/6.12 tff(a105, type, a105: $i). % 18.68/6.12 tff(c2_1, type, c2_1: $i > $o). % 18.68/6.12 tff(a9, type, a9: $i). % 18.68/6.12 tff(a129, type, a129: $i). % 18.68/6.12 tff(a2, type, a2: $i). % 18.68/6.12 tff(ndr1_1, type, ndr1_1: $i > $o). % 18.68/6.12 tff(c2_0, type, c2_0: $o). % 18.68/6.12 tff(c4_1, type, c4_1: $i > $o). % 18.68/6.12 tff(a45, type, a45: $i). % 18.68/6.12 tff(a6, type, a6: $i). % 18.68/6.12 tff(c6_2, type, c6_2: ($i * $i) > $o). % 18.68/6.12 tff(a90, type, a90: $i). % 18.68/6.12 tff(a52, type, a52: $i). % 18.68/6.12 tff(a80, type, a80: $i). % 18.68/6.12 tff(a21, type, a21: $i). % 18.68/6.12 tff(a123, type, a123: $i). % 18.68/6.12 tff(a116, type, a116: $i). % 18.68/6.12 tff(a20, type, a20: $i). % 18.68/6.12 tff(a66, type, a66: $i). % 18.68/6.12 tff(a92, type, a92: $i). % 18.68/6.12 tff(a79, type, a79: $i). % 18.68/6.12 tff(a57, type, a57: $i). % 18.68/6.12 tff(a4, type, a4: $i). % 18.68/6.12 tff(ndr1_0, type, ndr1_0: $o). % 18.68/6.12 tff(a48, type, a48: $i). % 18.68/6.12 tff(a44, type, a44: $i). % 18.68/6.12 tff(a117, type, a117: $i). % 18.68/6.12 tff(a42, type, a42: $i). % 18.68/6.12 tff(a85, type, a85: $i). % 18.68/6.12 tff(a30, type, a30: $i). % 18.68/6.12 tff(a56, type, a56: $i). % 18.68/6.12 tff(a54, type, a54: $i). % 18.68/6.12 tff(a137, type, a137: $i). % 18.68/6.12 tff(a133, type, a133: $i). % 18.68/6.12 tff(a49, type, a49: $i). % 18.68/6.12 tff(a5, type, a5: $i). % 18.68/6.12 tff(c1_1, type, c1_1: $i > $o). % 18.68/6.12 tff(a16, type, a16: $i). % 18.68/6.12 tff(a115, type, a115: $i). % 18.68/6.12 tff(a19, type, a19: $i). % 18.68/6.12 tff(a96, type, a96: $i). % 18.68/6.12 tff(a27, type, a27: $i). % 18.68/6.12 tff(c5_2, type, c5_2: ($i * $i) > $o). % 18.68/6.12 tff(a70, type, a70: $i). % 18.68/6.12 tff(a37, type, a37: $i). % 18.68/6.12 tff(c7_1, type, c7_1: $i > $o). % 18.68/6.12 tff(c6_1, type, c6_1: $i > $o). % 18.68/6.12 tff(a95, type, a95: $i). % 18.68/6.12 tff(a135, type, a135: $i). % 18.68/6.12 tff(c4_2, type, c4_2: ($i * $i) > $o). % 18.68/6.12 tff(a114, type, a114: $i). % 18.68/6.12 tff(a82, type, a82: $i). % 18.68/6.12 tff(a55, type, a55: $i). % 18.68/6.12 tff(a8, type, a8: $i). % 18.68/6.12 tff(a144, type, a144: $i). % 18.68/6.12 tff(a106, type, a106: $i). % 18.68/6.12 tff(a91, type, a91: $i). % 18.68/6.12 tff(c5_1, type, c5_1: $i > $o). % 18.68/6.12 tff(a13, type, a13: $i). % 18.68/6.12 tff(a81, type, a81: $i). % 18.68/6.12 tff(c7_2, type, c7_2: ($i * $i) > $o). % 18.68/6.12 tff(c3_2, type, c3_2: ($i * $i) > $o). % 18.68/6.12 tff(a24, type, a24: $i). % 18.68/6.12 tff(a109, type, a109: $i). % 18.68/6.12 tff(c2_2, type, c2_2: ($i * $i) > $o). % 18.68/6.12 tff(a102, type, a102: $i). % 18.68/6.12 tff(a65, type, a65: $i). % 18.68/6.12 tff(a128, type, a128: $i). % 18.68/6.12 tff(a59, type, a59: $i). % 18.68/6.12 tff(a132, type, a132: $i). % 18.68/6.12 tff(c3_1, type, c3_1: $i > $o). % 18.68/6.12 % 18.68/6.12 %Saturated clause set: % 18.68/6.12 tff(c_8329, plain, (~c4_2(a44, a45))). % 18.68/6.12 tff(c_8324, plain, (![X36_54]: (~c5_2(a44, X36_54) | ~c4_2(a44, X36_54)))). % 18.68/6.12 tff(c_8320, plain, (c5_2(a44, a45))). % 18.68/6.12 tff(c_8315, plain, (~c7_1(a44))). % 18.68/6.12 tff(c_8302, plain, (~c8_2(a44, a45))). % 18.68/6.12 tff(c_8300, plain, (ndr1_1(a44))). % 18.68/6.12 tff(c_8299, plain, (~c2_1(a44))). % 18.68/6.12 tff(c_8260, plain, (![X81_267, X82_268]: (c6_2(X81_267, X82_268) | ~c4_1(X81_267) | c3_2(X81_267, a6) | c4_2(X81_267, a6) | ~c3_1(X81_267) | ~c2_1(X81_267) | ~c6_2(X81_267, a22) | ~c2_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_8203, plain, (![X81_267, X82_268]: (c6_2(X81_267, X82_268) | ~c4_1(X81_267) | c3_2(X81_267, a6) | c4_2(X81_267, a6) | ~c3_1(X81_267) | ~c2_1(X81_267) | ~c6_2(X81_267, a22) | ~c3_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_8090, plain, (![X81_267, X82_268]: (c6_2(X81_267, X82_268) | ~c4_1(X81_267) | c3_2(X81_267, a6) | c4_2(X81_267, a6) | ~c3_1(X81_267) | ~c2_1(X81_267) | ~c6_2(X81_267, a22) | ~c6_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_7669, plain, (![Z_264, X137_265]: (~c6_2(Z_264, a22) | ~c2_2(Z_264, a23) | ~c5_2(Z_264, X137_265) | c1_2(Z_264, X137_265) | c6_2(Z_264, X137_265) | ~c7_2(Z_264, X137_265) | ~c4_1(Z_264) | c3_2(Z_264, a6) | c4_2(Z_264, a6) | ~ndr1_1(Z_264) | ~c3_1(Z_264) | ~c2_1(Z_264)))). % 18.68/6.12 tff(c_7668, plain, (![Z_264, X137_265]: (~c6_2(Z_264, a22) | ~c3_2(Z_264, a23) | ~c5_2(Z_264, X137_265) | c1_2(Z_264, X137_265) | c6_2(Z_264, X137_265) | ~c7_2(Z_264, X137_265) | ~c4_1(Z_264) | c3_2(Z_264, a6) | c4_2(Z_264, a6) | ~ndr1_1(Z_264) | ~c3_1(Z_264) | ~c2_1(Z_264)))). % 18.68/6.12 tff(c_7670, plain, (![Z_264, X137_265]: (~c7_2(Z_264, a22) | ~c2_2(Z_264, a23) | ~c5_2(Z_264, X137_265) | c1_2(Z_264, X137_265) | c6_2(Z_264, X137_265) | ~c7_2(Z_264, X137_265) | ~c4_1(Z_264) | c3_2(Z_264, a6) | c4_2(Z_264, a6) | ~ndr1_1(Z_264) | ~c3_1(Z_264) | ~c2_1(Z_264)))). % 18.68/6.12 tff(c_7671, plain, (![Z_264, X137_265]: (~c7_2(Z_264, a22) | ~c6_2(Z_264, a23) | ~c5_2(Z_264, X137_265) | c1_2(Z_264, X137_265) | c6_2(Z_264, X137_265) | ~c7_2(Z_264, X137_265) | ~c4_1(Z_264) | c3_2(Z_264, a6) | c4_2(Z_264, a6) | ~ndr1_1(Z_264) | ~c3_1(Z_264) | ~c2_1(Z_264)))). % 18.68/6.12 tff(c_8113, plain, (~c4_1(a96))). % 18.68/6.12 tff(c_7672, plain, (![Z_264, X137_265]: (~c6_2(Z_264, a22) | ~c6_2(Z_264, a23) | ~c5_2(Z_264, X137_265) | c1_2(Z_264, X137_265) | c6_2(Z_264, X137_265) | ~c7_2(Z_264, X137_265) | ~c4_1(Z_264) | c3_2(Z_264, a6) | c4_2(Z_264, a6) | ~ndr1_1(Z_264) | ~c3_1(Z_264) | ~c2_1(Z_264)))). % 18.68/6.12 tff(c_7673, plain, (![Z_264, X137_265]: (~c7_2(Z_264, a22) | ~c3_2(Z_264, a23) | ~c5_2(Z_264, X137_265) | c1_2(Z_264, X137_265) | c6_2(Z_264, X137_265) | ~c7_2(Z_264, X137_265) | ~c4_1(Z_264) | c3_2(Z_264, a6) | c4_2(Z_264, a6) | ~ndr1_1(Z_264) | ~c3_1(Z_264) | ~c2_1(Z_264)))). % 18.68/6.12 tff(c_7799, plain, (![X81_267, X82_268]: (~c6_2(X81_267, a22) | ~c3_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | c7_2(X81_267, X82_268) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_7971, plain, (~c6_2(a68, a23))). % 18.68/6.12 tff(c_7802, plain, (![X81_267, X82_268]: (~c7_2(X81_267, a22) | ~c6_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | c7_2(X81_267, X82_268) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_7945, plain, (~c2_2(a68, a23))). % 18.68/6.12 tff(c_7801, plain, (![X81_267, X82_268]: (~c7_2(X81_267, a22) | ~c2_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | c7_2(X81_267, X82_268) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_7800, plain, (![X81_267, X82_268]: (~c6_2(X81_267, a22) | ~c2_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | c7_2(X81_267, X82_268) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_7803, plain, (![X81_267, X82_268]: (~c6_2(X81_267, a22) | ~c6_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | c7_2(X81_267, X82_268) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.12 tff(c_7835, plain, (~c3_2(a68, a23))). % 18.68/6.12 tff(c_7804, plain, (![X81_267, X82_268]: (~c7_2(X81_267, a22) | ~c3_2(X81_267, a23) | ~c5_2(X81_267, X82_268) | c1_2(X81_267, X82_268) | ~c5_1(X81_267) | c7_2(X81_267, X82_268) | ~c4_2(X81_267, X82_268) | ~ndr1_1(X81_267) | ~c7_1(X81_267)))). % 18.68/6.13 tff(c_7816, plain, (![X81_269]: (~c8_1(X81_269) | ~c5_1(X81_269) | ~c4_2(X81_269, a115) | ~ndr1_1(X81_269) | ~c7_1(X81_269)))). % 18.68/6.13 tff(c_7757, plain, (![X81_108, X82_110]: (~c5_1(X81_108) | c7_2(X81_108, X82_110) | c8_2(X81_108, X82_110) | ~c4_2(X81_108, X82_110) | ~ndr1_1(X81_108) | ~c7_1(X81_108)))). % 18.68/6.13 tff(c_7754, plain, (~c4_1(a122))). % 18.68/6.13 tff(c_7753, plain, (~c4_1(a117))). % 18.68/6.13 tff(c_7752, plain, (~c4_1(a27))). % 18.68/6.13 tff(c_7751, plain, (~c4_1(a127))). % 18.68/6.13 tff(c_7750, plain, (~c4_1(a18))). % 18.68/6.13 tff(c_7724, plain, (![X142_187]: (~c5_1(X142_187) | ~c6_1(X142_187) | ~c4_1(X142_187)))). % 18.68/6.13 tff(c_7696, plain, (~c2_1(a104))). % 18.68/6.13 tff(c_7692, plain, (~c8_1(a104))). % 18.68/6.13 tff(c_7684, plain, (~ndr1_1(a104))). % 18.68/6.13 tff(c_7573, plain, (![Z_7, X137_261]: (c6_2(Z_7, X137_261) | c8_2(Z_7, X137_261) | ~c7_2(Z_7, X137_261) | ~c4_1(Z_7) | c3_2(Z_7, a6) | c4_2(Z_7, a6) | ~ndr1_1(Z_7) | ~c3_1(Z_7) | ~c2_1(Z_7)))). % 18.68/6.13 tff(c_7626, plain, (c3_2(a136, a108))). % 18.68/6.13 tff(c_7589, plain, (![X148_194]: (c4_2(a136, X148_194) | c7_2(a136, X148_194) | c3_2(a136, X148_194)))). % 18.68/6.13 tff(c_7588, plain, (~c4_1(a60))). % 18.68/6.13 tff(c_7587, plain, (~c4_1(a47))). % 18.68/6.13 tff(c_7561, plain, (![X135_177, X137_181, X136_180]: (c6_2(X135_177, X137_181) | c8_2(X135_177, X137_181) | ~c7_2(X135_177, X137_181) | ~c4_1(X135_177) | c3_2(X135_177, X136_180) | ~c8_2(X135_177, X136_180) | c4_2(X135_177, X136_180) | ~ndr1_1(X135_177)))). % 18.68/6.13 tff(c_7498, plain, (![Z_253]: (~c7_2(Z_253, a22) | ~c3_2(Z_253, a23) | ~c5_2(Z_253, a6) | c1_2(Z_253, a6) | ~ndr1_1(Z_253) | ~c3_1(Z_253) | ~c2_1(Z_253)))). % 18.68/6.13 tff(c_7497, plain, (![Z_253]: (~c6_2(Z_253, a22) | ~c6_2(Z_253, a23) | ~c5_2(Z_253, a6) | c1_2(Z_253, a6) | ~ndr1_1(Z_253) | ~c3_1(Z_253) | ~c2_1(Z_253)))). % 18.68/6.13 tff(c_7496, plain, (![Z_253]: (~c7_2(Z_253, a22) | ~c6_2(Z_253, a23) | ~c5_2(Z_253, a6) | c1_2(Z_253, a6) | ~ndr1_1(Z_253) | ~c3_1(Z_253) | ~c2_1(Z_253)))). % 18.68/6.13 tff(c_7495, plain, (![Z_253]: (~c7_2(Z_253, a22) | ~c2_2(Z_253, a23) | ~c5_2(Z_253, a6) | c1_2(Z_253, a6) | ~ndr1_1(Z_253) | ~c3_1(Z_253) | ~c2_1(Z_253)))). % 18.68/6.13 tff(c_7494, plain, (![Z_253]: (~c6_2(Z_253, a22) | ~c2_2(Z_253, a23) | ~c5_2(Z_253, a6) | c1_2(Z_253, a6) | ~ndr1_1(Z_253) | ~c3_1(Z_253) | ~c2_1(Z_253)))). % 18.68/6.13 tff(c_7493, plain, (![Z_253]: (~c6_2(Z_253, a22) | ~c3_2(Z_253, a23) | ~c5_2(Z_253, a6) | c1_2(Z_253, a6) | ~ndr1_1(Z_253) | ~c3_1(Z_253) | ~c2_1(Z_253)))). % 18.68/6.13 tff(c_7461, plain, (![Z_7]: (c8_2(Z_7, a6) | ~c3_1(Z_7) | ~c2_1(Z_7)))). % 18.68/6.13 tff(c_7458, plain, (c1_2(a24, a25))). % 18.68/6.13 tff(c_7454, plain, (![Z_7]: (c2_2(Z_7, a6) | ~c3_1(Z_7) | ~c2_1(Z_7)))). % 18.68/6.13 tff(c_7451, plain, (~c4_2(a24, a25))). % 18.68/6.13 tff(c_7444, plain, (~c6_2(a24, a25))). % 18.68/6.13 tff(c_7441, plain, (~c3_1(a68))). % 18.68/6.13 tff(c_7427, plain, (![Z_7]: (~c7_2(Z_7, a6) | ~c3_1(Z_7) | ~c2_1(Z_7)))). % 18.68/6.13 tff(c_7425, plain, (~c3_1(a127))). % 18.68/6.13 tff(c_7424, plain, (c3_2(a24, a25))). % 18.68/6.13 tff(c_7421, plain, (c6_1(a127))). % 18.68/6.13 tff(c_7416, plain, (c7_1(a127))). % 18.68/6.13 tff(c_7408, plain, (c8_1(a127))). % 18.68/6.13 tff(c_7405, plain, (c2_2(a24, a26))). % 18.68/6.13 tff(c_7375, plain, (![Z_7]: (ndr1_1(Z_7) | ~c3_1(Z_7) | ~c2_1(Z_7)))). % 18.68/6.13 tff(c_7373, plain, (~c4_2(a24, a26))). % 18.68/6.13 tff(c_7366, plain, (~c6_2(a24, a26))). % 18.68/6.13 tff(c_7361, plain, (c1_1(a68))). % 18.68/6.13 tff(c_7363, plain, (c1_1(a51))). % 18.68/6.13 tff(c_7362, plain, (c1_1(a136))). % 18.68/6.13 tff(c_7350, plain, (![X52_75]: (~c4_1(X52_75) | c1_1(X52_75)))). % 18.68/6.13 tff(c_7348, plain, (c3_2(a60, a62))). % 18.68/6.13 tff(c_7347, plain, (~c3_1(a24))). % 18.68/6.13 tff(c_7340, plain, (~c7_2(a24, a26))). % 18.68/6.13 tff(c_7337, plain, (~c4_2(a60, a62))). % 18.68/6.13 tff(c_7336, plain, (~c2_2(a60, a61))). % 18.68/6.13 tff(c_7333, plain, (~c5_2(a60, a61))). % 18.68/6.13 tff(c_7270, plain, (c8_2(a60, a61))). % 18.68/6.13 tff(c_7273, plain, (ndr1_1(a24))). % 18.68/6.13 tff(c_7269, plain, (c2_2(a60, a62))). % 18.68/6.13 tff(c_7242, plain, (![X48_70, X49_72]: (c3_2(X48_70, a56) | ~c6_2(X48_70, X49_72) | ~c1_2(X48_70, X49_72) | ~c4_2(X48_70, X49_72) | ~ndr1_1(X48_70) | c5_1(X48_70)))). % 18.68/6.13 tff(c_7245, plain, (~c3_1(a27))). % 18.68/6.13 tff(c_7244, plain, (~c3_1(a122))). % 18.68/6.13 tff(c_7243, plain, (~c3_1(a85))). % 18.68/6.13 tff(c_7232, plain, (~c3_1(a136))). % 18.68/6.13 tff(c_7240, plain, (~c3_1(a117))). % 18.68/6.13 tff(c_7206, plain, (![X44_65]: (~c7_1(X44_65) | c2_1(X44_65) | ~c3_1(X44_65)))). % 18.68/6.13 tff(c_7205, plain, (ndr1_1(a60))). % 18.68/6.13 tff(c_7204, plain, (~c4_2(a96, a97))). % 18.68/6.13 tff(c_7176, plain, (![X125_165, X126_167]: (c1_2(X125_165, X126_167) | c6_2(X125_165, X126_167) | ~c4_2(X125_165, X126_167) | ~ndr1_1(X125_165) | c4_1(X125_165) | c7_1(X125_165)))). % 18.68/6.13 tff(c_7123, plain, (![X48_70, X49_72]: (c7_2(X48_70, a56) | ~c6_2(X48_70, X49_72) | ~c1_2(X48_70, X49_72) | ~c4_2(X48_70, X49_72) | ~ndr1_1(X48_70) | c5_1(X48_70)))). % 18.68/6.13 tff(c_7121, plain, (~c4_2(a29, a31))). % 18.68/6.13 tff(c_7120, plain, (~c4_2(a39, a41))). % 18.68/6.13 tff(c_7100, plain, (![X48_70, X49_72]: (~c2_2(X48_70, a56) | ~c6_2(X48_70, X49_72) | ~c1_2(X48_70, X49_72) | ~c4_2(X48_70, X49_72) | ~ndr1_1(X48_70) | c5_1(X48_70)))). % 18.68/6.13 tff(c_7082, plain, (![X5_13, X7_17, X6_16]: (~c4_2(X5_13, X7_17) | ~c2_2(X5_13, X7_17) | ~c8_2(X5_13, X7_17) | c7_1(X5_13) | c7_2(X5_13, X6_16) | ~c8_2(X5_13, X6_16) | ~ndr1_1(X5_13)))). % 18.68/6.13 tff(c_7059, plain, (![X21_37, X22_39]: (~c6_2(X21_37, a22) | ~c3_2(X21_37, a23) | ~c5_2(X21_37, X22_39) | c1_2(X21_37, X22_39) | ~c8_2(X21_37, X22_39) | ~ndr1_1(X21_37)))). % 18.68/6.13 tff(c_7038, plain, (![X21_37, X22_39]: (~c6_2(X21_37, a22) | ~c2_2(X21_37, a23) | ~c5_2(X21_37, X22_39) | c1_2(X21_37, X22_39) | ~c8_2(X21_37, X22_39) | ~ndr1_1(X21_37)))). % 18.68/6.13 tff(c_7037, plain, (~c2_2(a136, a23))). % 18.68/6.13 tff(c_7016, plain, (![X21_37, X22_39]: (~c7_2(X21_37, a22) | ~c2_2(X21_37, a23) | ~c5_2(X21_37, X22_39) | c1_2(X21_37, X22_39) | ~c8_2(X21_37, X22_39) | ~ndr1_1(X21_37)))). % 18.68/6.13 tff(c_6993, plain, (![X21_37, X22_39]: (~c7_2(X21_37, a22) | ~c6_2(X21_37, a23) | ~c5_2(X21_37, X22_39) | c1_2(X21_37, X22_39) | ~c8_2(X21_37, X22_39) | ~ndr1_1(X21_37)))). % 18.68/6.14 tff(c_6992, plain, (~c6_2(a136, a23))). % 18.68/6.14 tff(c_6971, plain, (![X21_37, X22_39]: (~c6_2(X21_37, a22) | ~c6_2(X21_37, a23) | ~c5_2(X21_37, X22_39) | c1_2(X21_37, X22_39) | ~c8_2(X21_37, X22_39) | ~ndr1_1(X21_37)))). % 18.68/6.14 tff(c_6968, plain, (~c3_2(a136, a23))). % 18.68/6.14 tff(c_6947, plain, (![X21_37, X22_39]: (~c7_2(X21_37, a22) | ~c3_2(X21_37, a23) | ~c5_2(X21_37, X22_39) | c1_2(X21_37, X22_39) | ~c8_2(X21_37, X22_39) | ~ndr1_1(X21_37)))). % 18.68/6.14 tff(c_6946, plain, (~c1_2(a96, a97))). % 18.68/6.14 tff(c_6943, plain, (~c6_2(a96, a97))). % 18.68/6.14 tff(c_6942, plain, (~c5_1(a104))). % 18.68/6.14 tff(c_6938, plain, (c7_2(a96, a97))). % 18.68/6.14 tff(c_6917, plain, (c3_1(a96))). % 18.68/6.14 tff(c_6863, plain, (c2_1(a96))). % 18.68/6.14 tff(c_6862, plain, (~c2_1(a64))). % 18.68/6.14 tff(c_6858, plain, (~c8_1(a64))). % 18.68/6.14 tff(c_6852, plain, (~ndr1_1(a64))). % 18.68/6.14 tff(c_6848, plain, (c6_1(a18))). % 18.68/6.14 tff(c_6838, plain, (c1_1(a18))). % 18.68/6.14 tff(c_6810, plain, (ndr1_1(a96))). % 18.68/6.14 tff(c_6798, plain, (~c4_2(a27, a28))). % 18.68/6.14 tff(c_6781, plain, (c2_2(a27, a28))). % 18.68/6.14 tff(c_6760, plain, (~c6_2(a27, a28))). % 18.68/6.14 tff(c_6733, plain, (![X76_102, X77_104]: (c1_2(X76_102, X77_104) | c7_2(X76_102, X77_104) | ~c3_2(X76_102, X77_104) | ~ndr1_1(X76_102) | c7_1(X76_102) | ~c3_1(X76_102)))). % 18.68/6.14 tff(c_6696, plain, (c6_1(a27))). % 18.68/6.14 tff(c_6695, plain, (c7_1(a27))). % 18.68/6.14 tff(c_6687, plain, (c8_1(a27))). % 18.68/6.14 tff(c_6678, plain, (ndr1_1(a27))). % 18.68/6.14 tff(c_6672, plain, (c7_1(a136))). % 18.68/6.14 tff(c_6671, plain, (~c7_2(a136, a108))). % 18.68/6.14 tff(c_6668, plain, (~c5_2(a136, a108))). % 18.68/6.14 tff(c_6665, plain, (~c2_1(a93))). % 18.68/6.14 tff(c_6661, plain, (~c8_1(a93))). % 18.68/6.14 tff(c_6657, plain, (~ndr1_1(a93))). % 18.68/6.14 tff(c_6642, plain, (c6_2(a68, a115))). % 18.68/6.14 tff(c_6654, plain, (c7_1(a68))). % 18.68/6.14 tff(c_6643, plain, (c8_1(a68))). % 18.68/6.14 tff(c_6627, plain, (![X66_91]: (c6_2(a68, X66_91) | c7_2(a68, X66_91)))). % 18.68/6.14 tff(c_6626, plain, (ndr1_1(a68))). % 18.68/6.14 tff(c_6598, plain, (c4_2(a37, a38))). % 18.68/6.14 tff(c_5815, plain, (![X114_151, X115_153]: (~c5_2(X114_151, a108) | ~c8_2(X114_151, X115_153) | ~c5_2(X114_151, X115_153) | ~ndr1_1(X114_151) | c7_1(X114_151)))). % 18.68/6.14 tff(c_5813, plain, (![X114_151, X115_153]: (c6_2(X114_151, a108) | ~c8_2(X114_151, X115_153) | ~c5_2(X114_151, X115_153) | ~ndr1_1(X114_151) | c7_1(X114_151)))). % 18.68/6.14 tff(c_6554, plain, (c5_2(a37, a38))). % 18.68/6.14 tff(c_6545, plain, (~c5_2(a134, a135))). % 18.68/6.14 tff(c_6544, plain, (~c5_2(a47, a48))). % 18.68/6.14 tff(c_5814, plain, (![X114_151, X115_153]: (~c7_2(X114_151, a108) | ~c8_2(X114_151, X115_153) | ~c5_2(X114_151, X115_153) | ~ndr1_1(X114_151) | c7_1(X114_151)))). % 18.68/6.14 tff(c_6515, plain, (~c2_1(a120))). % 18.68/6.14 tff(c_6511, plain, (~c8_1(a120))). % 18.68/6.14 tff(c_6507, plain, (~ndr1_1(a120))). % 18.68/6.14 tff(c_6502, plain, (c3_2(a37, a38))). % 18.68/6.14 tff(c_6495, plain, (~c2_1(a37))). % 18.68/6.14 tff(c_6492, plain, (~c2_1(a47))). % 18.68/6.14 tff(c_6469, plain, (![X147_212]: (c4_1(X147_212) | c6_1(X147_212) | ~c2_1(X147_212)))). % 18.68/6.14 tff(c_6471, plain, (![X147_212]: (c7_1(X147_212) | ~c2_1(X147_212)))). % 18.68/6.14 tff(c_6470, plain, (~c2_1(a34))). % 18.68/6.14 tff(c_6468, plain, (~c2_1(a59))). % 18.68/6.14 tff(c_6467, plain, (~c2_1(a136))). % 18.68/6.14 tff(c_6446, plain, (![X147_193]: (~c2_1(X147_193) | c8_1(X147_193)))). % 18.68/6.14 tff(c_6443, plain, (c4_1(a68))). % 18.68/6.14 tff(c_6440, plain, (c4_1(a136))). % 18.68/6.14 tff(c_6439, plain, (~c8_1(a51))). % 18.68/6.14 tff(c_6435, plain, (~ndr1_1(a51))). % 18.68/6.14 tff(c_6434, plain, (c4_1(a51))). % 18.68/6.14 tff(c_6420, plain, (![X91_120]: (c1_1(X91_120) | c4_1(X91_120) | ~c5_1(X91_120)))). % 18.68/6.14 tff(c_6413, plain, (ndr1_1(a37))). % 18.68/6.14 tff(c_6295, plain, (~c8_1(a136))). % 18.68/6.14 tff(c_5776, plain, (![X148_194]: (c7_2(a136, X148_194) | c3_2(a136, X148_194) | c8_2(a136, X148_194)))). % 18.68/6.14 tff(c_6145, plain, (~c8_1(a59))). % 18.68/6.14 tff(c_6141, plain, (~ndr1_1(a59))). % 18.68/6.14 tff(c_6122, plain, (c5_1(a68))). % 18.68/6.14 tff(c_6120, plain, (c2_1(a68))). % 18.68/6.14 tff(c_6112, plain, (~c1_1(a64))). % 18.68/6.14 tff(c_6104, plain, (c5_2(a39, a40))). % 18.68/6.14 tff(c_6083, plain, (c6_2(a39, a41))). % 18.68/6.14 tff(c_6077, plain, (~c4_2(a134, a135))). % 18.68/6.14 tff(c_6074, plain, (~c4_2(a39, a40))). % 18.68/6.14 tff(c_6063, plain, (~c5_2(a39, a41))). % 18.68/6.14 tff(c_6059, plain, (c6_2(a29, a31))). % 18.68/6.14 tff(c_6056, plain, (c5_2(a29, a31))). % 18.68/6.14 tff(c_6053, plain, (c8_2(a134, a135))). % 18.68/6.14 tff(c_6051, plain, (c1_2(a29, a30))). % 18.68/6.14 tff(c_6050, plain, (c7_2(a29, a30))). % 18.68/6.14 tff(c_6048, plain, (c3_2(a134, a135))). % 18.68/6.14 tff(c_6047, plain, (~c4_1(a35))). % 18.68/6.14 tff(c_6045, plain, (~c2_2(a39, a41))). % 18.68/6.14 tff(c_6042, plain, (c3_2(a39, a40))). % 18.68/6.14 tff(c_6039, plain, (c6_1(a122))). % 18.68/6.14 tff(c_6038, plain, (c6_1(a117))). % 18.68/6.14 tff(c_6028, plain, (![X110_146]: (c4_1(X110_146) | c6_1(X110_146) | ~c8_1(X110_146)))). % 18.68/6.14 tff(c_6025, plain, (c2_2(a29, a30))). % 18.68/6.14 tff(c_6024, plain, (~c1_1(a37))). % 18.68/6.14 tff(c_6022, plain, (~c2_1(a83))). % 18.68/6.14 tff(c_6021, plain, (~c2_1(a51))). % 18.68/6.14 tff(c_5989, plain, (~c1_1(a134))). % 18.68/6.14 tff(c_5983, plain, (ndr1_1(a39))). % 18.68/6.14 tff(c_5982, plain, (c7_2(a85, a86))). % 18.68/6.14 tff(c_5980, plain, (~c8_2(a85, a86))). % 18.68/6.14 tff(c_5974, plain, (~c1_2(a85, a86))). % 18.68/6.14 tff(c_5971, plain, (ndr1_1(a134))). % 18.68/6.14 tff(c_5970, plain, (ndr1_1(a29))). % 18.68/6.14 tff(c_5969, plain, (~c6_1(a37))). % 18.68/6.14 tff(c_5968, plain, (~c2_1(a24))). % 18.68/6.14 tff(c_5895, plain, (![X123_163]: (~c3_2(X123_163, a115) | ~c8_1(X123_163)))). % 18.68/6.14 tff(c_5958, plain, (~c8_1(a34))). % 18.68/6.14 tff(c_5959, plain, (~c5_0)). % 18.68/6.14 tff(c_5954, plain, (~ndr1_1(a34))). % 18.68/6.14 tff(c_5951, plain, (~c7_1(a83))). % 18.68/6.14 tff(c_5949, plain, (c7_1(a85))). % 18.68/6.14 tff(c_5897, plain, (![X123_163]: (~c7_2(X123_163, a115) | ~c8_1(X123_163)))). % 18.68/6.14 tff(c_5945, plain, (ndr1_1(a85))). % 18.68/6.15 tff(c_5943, plain, (~c4_1(a85))). % 18.68/6.15 tff(c_5899, plain, (![X123_163]: (~c8_2(X123_163, a115) | ~c8_1(X123_163)))). % 18.68/6.15 tff(c_5940, plain, (c8_2(a47, a48))). % 18.68/6.15 tff(c_5939, plain, (~c1_2(a47, a48))). % 18.68/6.15 tff(c_5938, plain, (~c1_2(a47, a49))). % 18.68/6.15 tff(c_5937, plain, (~c2_2(a47, a48))). % 18.68/6.15 tff(c_5936, plain, (c7_1(a122))). % 18.68/6.15 tff(c_5935, plain, (c7_1(a117))). % 18.68/6.15 tff(c_5902, plain, (![X79_106]: (~c8_1(X79_106) | c7_1(X79_106)))). % 18.68/6.15 tff(c_5893, plain, (![X123_163]: (ndr1_1(X123_163) | ~c8_1(X123_163)))). % 18.68/6.15 tff(c_5926, plain, (~c5_1(a120))). % 18.68/6.15 tff(c_5925, plain, (c7_2(a47, a49))). % 18.68/6.15 tff(c_5924, plain, (~c2_2(a47, a49))). % 18.68/6.15 tff(c_5922, plain, (~c1_0)). % 18.68/6.15 tff(c_5923, plain, (~c6_1(a47))). % 18.68/6.15 tff(c_10, plain, (c3_2(a136, a137))). % 18.68/6.15 tff(c_12, plain, (c1_2(a136, a137))). % 18.68/6.15 tff(c_5789, plain, (~c3_2(a122, a123))). % 18.68/6.15 tff(c_5787, plain, (c5_2(a122, a123))). % 18.68/6.15 tff(c_5921, plain, (ndr1_1(a47))). % 18.68/6.15 tff(c_5920, plain, (~c8_0)). % 18.68/6.15 tff(c_8, plain, (c5_2(a136, a137))). % 18.68/6.15 tff(c_5788, plain, (~c1_2(a122, a123))). % 18.68/6.15 tff(c_5784, plain, (ndr1_1(a122))). % 18.68/6.15 tff(c_14, plain, (ndr1_1(a136))). % 18.68/6.15 tff(c_5907, plain, (c5_1(a51))). % 18.68/6.15 tff(c_5906, plain, (c3_1(a59))). % 18.68/6.15 tff(c_5904, plain, (~c4_1(a59))). % 18.68/6.15 tff(c_5903, plain, (~c7_1(a51))). % 18.68/6.15 tff(c_5901, plain, (~c2_1(a117))). % 18.68/6.15 tff(c_18, plain, (c5_1(a136))). % 18.68/6.15 tff(c_5783, plain, (~c1_1(a122))). % 18.68/6.15 tff(c_5900, plain, (c8_1(a117))). % 18.68/6.15 tff(c_5785, plain, (c8_1(a122))). % 18.68/6.15 tff(c_5779, plain, (c7_0)). % 18.68/6.15 tff(c_6, plain, (~c2_0)). % 18.68/6.15 tff(c_5819, plain, (~c3_0)). % 18.68/6.15 tff(c_34, plain, (c4_0)). % 18.68/6.15 tff(c_36, plain, (c6_0)). % 18.68/6.15 tff(c_3938, plain, (ndr1_0)). % 18.68/6.15 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.68/6.15 %------------------------------------------------------------------------------