%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN543+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 : n018.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 49.83s 35.08s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN543+1 : TPTP v9.0.0. Released v2.1.0. % 0.08/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.14/0.34 % Computer : n018.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 07:58:32 EDT 2025 % 0.14/0.35 % CPUTime : % 49.83/35.08 % 49.83/35.08 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 49.83/35.09 % 49.83/35.09 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 49.96/35.10 %$ c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c0_1 > #nlpp > ndr1_0 > hskp9 > hskp8 > hskp7 > hskp64 > hskp63 > hskp62 > hskp61 > hskp60 > hskp6 > hskp59 > hskp58 > hskp57 > hskp56 > hskp55 > hskp54 > hskp53 > hskp52 > hskp51 > hskp50 > hskp5 > hskp49 > hskp48 > hskp47 > hskp46 > hskp45 > hskp44 > hskp43 > hskp42 > hskp41 > hskp40 > hskp4 > hskp39 > hskp38 > hskp37 > hskp36 > hskp35 > hskp34 > hskp33 > hskp32 > hskp31 > hskp30 > hskp3 > hskp29 > hskp28 > hskp27 > hskp26 > hskp25 > hskp24 > hskp23 > hskp22 > hskp21 > hskp20 > hskp2 > hskp19 > hskp18 > hskp17 > hskp16 > hskp15 > hskp14 > hskp13 > hskp12 > hskp11 > hskp10 > hskp1 > hskp0 > a99 > a98 > a97 > a96 > a95 > a94 > a93 > a92 > a91 > a90 > a89 > a87 > a86 > a85 > a84 > a82 > a81 > a80 > a79 > a78 > a156 > a154 > a153 > a152 > a150 > a149 > a148 > a147 > a146 > a145 > a143 > a142 > a141 > a140 > a138 > a137 > a136 > a135 > a133 > a131 > a129 > a128 > a127 > a126 > a125 > a124 > a123 > a121 > a120 > a119 > a118 > a117 > a116 > a115 > a114 > a113 > a111 > a109 > a108 > a106 > a105 > a103 > a102 > a101 > a100 % 49.96/35.10 % 49.96/35.10 %Foreground sorts: % 49.96/35.10 % 49.96/35.10 % 49.96/35.10 %Background operators: % 49.96/35.10 % 49.96/35.10 % 49.96/35.10 %Foreground operators: % 49.96/35.10 tff(a99, type, a99: $i). % 49.96/35.10 tff(hskp53, type, hskp53: $o). % 49.96/35.10 tff(a143, type, a143: $i). % 49.96/35.10 tff(hskp50, type, hskp50: $o). % 49.96/35.10 tff(hskp31, type, hskp31: $o). % 49.96/35.10 tff(a94, type, a94: $i). % 49.96/35.10 tff(a101, type, a101: $i). % 49.96/35.10 tff(a100, type, a100: $i). % 49.96/35.10 tff(a108, type, a108: $i). % 49.96/35.10 tff(a149, type, a149: $i). % 49.96/35.10 tff(a89, type, a89: $i). % 49.96/35.10 tff(hskp17, type, hskp17: $o). % 49.96/35.10 tff(a97, type, a97: $i). % 49.96/35.10 tff(hskp19, type, hskp19: $o). % 49.96/35.10 tff(hskp42, type, hskp42: $o). % 49.96/35.10 tff(hskp61, type, hskp61: $o). % 49.96/35.10 tff(a146, type, a146: $i). % 49.96/35.10 tff(a124, type, a124: $i). % 49.96/35.10 tff(hskp64, type, hskp64: $o). % 49.96/35.10 tff(a141, type, a141: $i). % 49.96/35.10 tff(a120, type, a120: $i). % 49.96/35.10 tff(a140, type, a140: $i). % 49.96/35.10 tff(hskp37, type, hskp37: $o). % 49.96/35.10 tff(hskp44, type, hskp44: $o). % 49.96/35.10 tff(hskp47, type, hskp47: $o). % 49.96/35.10 tff(a138, type, a138: $i). % 49.96/35.10 tff(a103, type, a103: $i). % 49.96/35.10 tff(hskp46, type, hskp46: $o). % 49.96/35.10 tff(a113, type, a113: $i). % 49.96/35.10 tff(hskp6, type, hskp6: $o). % 49.96/35.10 tff(hskp43, type, hskp43: $o). % 49.96/35.10 tff(hskp10, type, hskp10: $o). % 49.96/35.10 tff(a145, type, a145: $i). % 49.96/35.10 tff(a147, type, a147: $i). % 49.96/35.10 tff(a119, type, a119: $i). % 49.96/35.10 tff(a93, type, a93: $i). % 49.96/35.10 tff(hskp57, type, hskp57: $o). % 49.96/35.10 tff(hskp23, type, hskp23: $o). % 49.96/35.10 tff(hskp13, type, hskp13: $o). % 49.96/35.10 tff(hskp52, type, hskp52: $o). % 49.96/35.10 tff(a153, type, a153: $i). % 49.96/35.10 tff(a131, type, a131: $i). % 49.96/35.10 tff(a86, type, a86: $i). % 49.96/35.10 tff(hskp32, type, hskp32: $o). % 49.96/35.10 tff(hskp14, type, hskp14: $o). % 49.96/35.10 tff(a126, type, a126: $i). % 49.96/35.10 tff(hskp45, type, hskp45: $o). % 49.96/35.10 tff(a78, type, a78: $i). % 49.96/35.10 tff(hskp18, type, hskp18: $o). % 49.96/35.10 tff(a121, type, a121: $i). % 49.96/35.10 tff(hskp5, type, hskp5: $o). % 49.96/35.10 tff(hskp58, type, hskp58: $o). % 49.96/35.10 tff(a136, type, a136: $i). % 49.96/35.10 tff(a125, type, a125: $i). % 49.96/35.10 tff(hskp12, type, hskp12: $o). % 49.96/35.10 tff(a127, type, a127: $i). % 49.96/35.10 tff(hskp59, type, hskp59: $o). % 49.96/35.10 tff(a98, type, a98: $i). % 49.96/35.10 tff(hskp55, type, hskp55: $o). % 49.96/35.10 tff(hskp29, type, hskp29: $o). % 49.96/35.10 tff(a111, type, a111: $i). % 49.96/35.10 tff(a142, type, a142: $i). % 49.96/35.10 tff(a84, type, a84: $i). % 49.96/35.10 tff(a154, type, a154: $i). % 49.96/35.10 tff(a87, type, a87: $i). % 49.96/35.10 tff(hskp2, type, hskp2: $o). % 49.96/35.10 tff(hskp56, type, hskp56: $o). % 49.96/35.10 tff(hskp28, type, hskp28: $o). % 49.96/35.10 tff(hskp1, type, hskp1: $o). % 49.96/35.10 tff(hskp27, type, hskp27: $o). % 49.96/35.10 tff(hskp62, type, hskp62: $o). % 49.96/35.10 tff(hskp41, type, hskp41: $o). % 49.96/35.10 tff(a118, type, a118: $i). % 49.96/35.10 tff(hskp33, type, hskp33: $o). % 49.96/35.10 tff(hskp3, type, hskp3: $o). % 49.96/35.10 tff(a105, type, a105: $i). % 49.96/35.10 tff(c2_1, type, c2_1: $i > $o). % 49.96/35.10 tff(a129, type, a129: $i). % 49.96/35.10 tff(hskp63, type, hskp63: $o). % 49.96/35.10 tff(hskp4, type, hskp4: $o). % 49.96/35.10 tff(c0_1, type, c0_1: $i > $o). % 49.96/35.10 tff(hskp20, type, hskp20: $o). % 49.96/35.10 tff(c4_1, type, c4_1: $i > $o). % 49.96/35.10 tff(hskp36, type, hskp36: $o). % 49.96/35.10 tff(hskp16, type, hskp16: $o). % 49.96/35.10 tff(hskp11, type, hskp11: $o). % 49.96/35.10 tff(hskp30, type, hskp30: $o). % 49.96/35.10 tff(a90, type, a90: $i). % 49.96/35.10 tff(hskp60, type, hskp60: $o). % 49.96/35.10 tff(hskp48, type, hskp48: $o). % 49.96/35.10 tff(hskp24, type, hskp24: $o). % 49.96/35.10 tff(hskp51, type, hskp51: $o). % 49.96/35.10 tff(a80, type, a80: $i). % 49.96/35.10 tff(a123, type, a123: $i). % 49.96/35.10 tff(a116, type, a116: $i). % 49.96/35.10 tff(hskp49, type, hskp49: $o). % 49.96/35.10 tff(a92, type, a92: $i). % 49.96/35.10 tff(hskp26, type, hskp26: $o). % 49.96/35.10 tff(a79, type, a79: $i). % 49.96/35.10 tff(ndr1_0, type, ndr1_0: $o). % 49.96/35.10 tff(hskp25, type, hskp25: $o). % 49.96/35.10 tff(a117, type, a117: $i). % 49.96/35.10 tff(hskp22, type, hskp22: $o). % 49.96/35.10 tff(hskp54, type, hskp54: $o). % 49.96/35.10 tff(a85, type, a85: $i). % 49.96/35.10 tff(a150, type, a150: $i). % 49.96/35.10 tff(a137, type, a137: $i). % 49.96/35.10 tff(a133, type, a133: $i). % 49.96/35.10 tff(hskp9, type, hskp9: $o). % 49.96/35.10 tff(c1_1, type, c1_1: $i > $o). % 49.96/35.10 tff(a115, type, a115: $i). % 49.96/35.10 tff(a96, type, a96: $i). % 49.96/35.10 tff(a156, type, a156: $i). % 49.96/35.10 tff(hskp39, type, hskp39: $o). % 49.96/35.10 tff(a148, type, a148: $i). % 49.96/35.10 tff(a95, type, a95: $i). % 49.96/35.10 tff(hskp38, type, hskp38: $o). % 49.96/35.10 tff(a135, type, a135: $i). % 49.96/35.10 tff(a114, type, a114: $i). % 49.96/35.10 tff(a82, type, a82: $i). % 49.96/35.10 tff(a106, type, a106: $i). % 49.96/35.10 tff(a91, type, a91: $i). % 49.96/35.10 tff(c5_1, type, c5_1: $i > $o). % 49.96/35.10 tff(a81, type, a81: $i). % 49.96/35.10 tff(a109, type, a109: $i). % 49.96/35.10 tff(hskp34, type, hskp34: $o). % 49.96/35.10 tff(a102, type, a102: $i). % 49.96/35.10 tff(hskp8, type, hskp8: $o). % 49.96/35.10 tff(a128, type, a128: $i). % 49.96/35.10 tff(hskp15, type, hskp15: $o). % 49.96/35.10 tff(hskp35, type, hskp35: $o). % 49.96/35.10 tff(hskp0, type, hskp0: $o). % 49.96/35.10 tff(hskp7, type, hskp7: $o). % 49.96/35.10 tff(hskp21, type, hskp21: $o). % 49.96/35.10 tff(a152, type, a152: $i). % 49.96/35.10 tff(c3_1, type, c3_1: $i > $o). % 49.96/35.10 tff(hskp40, type, hskp40: $o). % 49.96/35.10 % 49.96/35.10 %Saturated clause set: % 49.99/35.11 tff(c_446842, plain, (![X65_71]: (~c4_1(X65_71) | c3_1(X65_71) | c2_1(X65_71)))). % 49.99/35.11 tff(c_446812, plain, (![X59_65]: (~c2_1(X59_65) | c5_1(X59_65) | c3_1(X59_65)))). % 49.99/35.11 tff(c_446700, plain, (![X87_14132]: (~c1_1(X87_14132) | ~c0_1(X87_14132)))). % 49.99/35.11 tff(c_446664, plain, (![X73_79]: (~c4_1(X73_79) | ~c1_1(X73_79) | c3_1(X73_79)))). % 49.99/35.11 tff(c_446618, plain, (![X22_14128]: (~c0_1(X22_14128) | c2_1(X22_14128)))). % 49.99/35.11 tff(c_446506, plain, (![X64_70]: (~c4_1(X64_70) | ~c1_1(X64_70) | c5_1(X64_70)))). % 49.99/35.11 tff(c_446398, plain, (![X27_33]: (~c4_1(X27_33) | ~c3_1(X27_33) | c0_1(X27_33)))). % 49.99/35.11 tff(c_446370, plain, (![X13_19]: (~c0_1(X13_19) | c5_1(X13_19) | c3_1(X13_19)))). % 49.99/35.11 tff(c_446246, plain, (![X52_14118]: (c2_1(X52_14118) | c1_1(X52_14118)))). % 49.99/35.11 tff(c_446174, plain, (![X52_58]: (c5_1(X52_58) | c4_1(X52_58) | c1_1(X52_58)))). % 49.99/35.11 tff(c_446064, plain, (![X25_14113]: (~c3_1(X25_14113) | ~c4_1(X25_14113) | c2_1(X25_14113)))). % 49.99/35.11 tff(c_446070, plain, (~c4_1(a137))). % 49.99/35.11 tff(c_446044, plain, (![X25_31]: (~c4_1(X25_31) | c5_1(X25_31) | c2_1(X25_31)))). % 49.99/35.11 tff(c_445979, plain, (![X19_25]: (~c4_1(X19_25) | c3_1(X19_25) | c0_1(X19_25)))). % 49.99/35.11 tff(c_445930, plain, (![X16_22]: (~c5_1(X16_22) | ~c3_1(X16_22) | c2_1(X16_22)))). % 49.99/35.11 tff(c_445840, plain, (![X90_96]: (c0_1(X90_96) | ~c3_1(X90_96) | ~c2_1(X90_96)))). % 49.99/35.11 tff(c_445813, plain, (![X40_46]: (~c5_1(X40_46) | ~c3_1(X40_46) | c0_1(X40_46)))). % 49.99/35.11 tff(c_445779, plain, (![X30_36]: (~c0_1(X30_36) | c3_1(X30_36) | c1_1(X30_36)))). % 49.99/35.11 tff(c_445669, plain, (![Y_14101]: (c1_1(Y_14101) | c0_1(Y_14101)))). % 49.99/35.11 tff(c_445675, plain, (c1_1(a137))). % 49.99/35.11 tff(c_445646, plain, (c2_1(a128))). % 49.99/35.12 tff(c_445580, plain, (![X92_98]: (~c4_1(X92_98) | ~c3_1(X92_98) | ~c1_1(X92_98)))). % 49.99/35.12 tff(c_445571, plain, (c0_1(a146))). % 49.99/35.12 tff(c_445536, plain, (c1_1(a135))). % 49.99/35.12 tff(c_445499, plain, (c1_1(a84))). % 49.99/35.12 tff(c_445502, plain, (c1_1(a149))). % 49.99/35.12 tff(c_445410, plain, (![X82_88]: (~c4_1(X82_88) | ~c1_1(X82_88) | c2_1(X82_88)))). % 49.99/35.12 tff(c_445373, plain, (~c0_1(a137))). % 49.99/35.12 tff(c_445354, plain, (![X85_91]: (~c0_1(X85_91) | c5_1(X85_91) | c4_1(X85_91)))). % 49.99/35.12 tff(c_445312, plain, (~c0_1(a84))). % 49.99/35.12 tff(c_445289, plain, (~c0_1(a149))). % 49.99/35.12 tff(c_445292, plain, (![X90_96]: (~c3_1(X90_96) | ~c2_1(X90_96) | c5_1(X90_96)))). % 49.99/35.12 tff(c_445288, plain, (~c0_1(a133))). % 49.99/35.12 tff(c_445282, plain, (~c4_1(a133))). % 49.99/35.12 tff(c_445262, plain, (![X84_90]: (~c4_1(X84_90) | c5_1(X84_90) | c3_1(X84_90)))). % 49.99/35.12 tff(c_445258, plain, (~c1_1(a106))). % 49.99/35.12 tff(c_445259, plain, (c0_1(a106))). % 49.99/35.12 tff(c_444420, plain, (![X88_94]: (~c2_1(X88_94) | ~c1_1(X88_94) | c5_1(X88_94)))). % 49.99/35.12 tff(c_444408, plain, (![X37_43]: (~c4_1(X37_43) | ~c2_1(X37_43) | c0_1(X37_43)))). % 49.99/35.12 tff(c_444405, plain, (c3_1(a128))). % 49.99/35.12 tff(c_444398, plain, (![X49_55]: (~c4_1(X49_55) | c3_1(X49_55) | c1_1(X49_55)))). % 49.99/35.12 tff(c_444388, plain, (c2_1(a84))). % 49.99/35.12 tff(c_444366, plain, (c2_1(a156))). % 49.99/35.12 tff(c_444370, plain, (![X77_83]: (~c5_1(X77_83) | c4_1(X77_83) | c2_1(X77_83)))). % 49.99/35.12 tff(c_444367, plain, (c1_1(a156))). % 49.99/35.12 tff(c_444005, plain, (![X83_89]: (~c5_1(X83_89) | ~c1_1(X83_89) | c2_1(X83_89)))). % 49.99/35.12 tff(c_444002, plain, (~c2_1(a133))). % 49.99/35.12 tff(c_443992, plain, (![X86_92]: (~c2_1(X86_92) | c5_1(X86_92) | c4_1(X86_92)))). % 49.99/35.12 tff(c_443989, plain, (~c1_1(a128))). % 49.99/35.12 tff(c_443987, plain, (c3_1(a106))). % 49.99/35.12 tff(c_443985, plain, (c5_1(a156))). % 49.99/35.12 tff(c_443983, plain, (~c3_1(a133))). % 49.99/35.12 tff(c_443981, plain, (c3_1(a137))). % 49.99/35.12 tff(c_443977, plain, (~c4_1(a84))). % 49.99/35.12 tff(c_443971, plain, (~c3_1(a84))). % 49.99/35.12 tff(c_443969, plain, (~c3_1(a156))). % 49.99/35.12 tff(c_443967, plain, (c2_1(a146))). % 49.99/35.12 tff(c_443965, plain, (~c2_1(a137))). % 49.99/35.12 tff(c_443963, plain, (~c5_1(a137))). % 49.99/35.12 tff(c_443958, plain, (c5_1(a84))). % 49.99/35.12 tff(c_443959, plain, (hskp3)). % 49.99/35.12 tff(c_441668, plain, (c0_1(a128))). % 49.99/35.12 tff(c_441666, plain, (~hskp9)). % 49.99/35.12 tff(c_441665, plain, (~hskp24)). % 49.99/35.12 tff(c_441664, plain, (~c3_1(a135))). % 49.99/35.12 tff(c_441662, plain, (c5_1(a146))). % 49.99/35.12 tff(c_441660, plain, (~c0_1(a135))). % 49.99/35.12 tff(c_441658, plain, (~c4_1(a149))). % 49.99/35.12 tff(c_441656, plain, (c4_1(a128))). % 49.99/35.12 tff(c_441654, plain, (~hskp10)). % 49.99/35.12 tff(c_441653, plain, (~hskp51)). % 49.99/35.12 tff(c_441652, plain, (~hskp61)). % 49.99/35.12 tff(c_441651, plain, (~c5_1(a133))). % 49.99/35.12 tff(c_441649, plain, (c2_1(a106))). % 49.99/35.12 tff(c_441647, plain, (~c0_1(a156))). % 49.99/35.12 tff(c_441645, plain, (~hskp39)). % 49.99/35.12 tff(c_441644, plain, (~hskp54)). % 49.99/35.12 tff(c_441643, plain, (hskp57)). % 49.99/35.12 tff(c_441642, plain, (~hskp14)). % 49.99/35.12 tff(c_441638, plain, (~c2_1(a135))). % 49.99/35.12 tff(c_441639, plain, (hskp42)). % 49.99/35.12 tff(c_441641, plain, (c2_1(a149))). % 49.99/35.12 tff(c_438893, plain, (~hskp18)). % 49.99/35.12 tff(c_438890, plain, (c1_1(a133))). % 49.99/35.12 tff(c_438891, plain, (hskp41)). % 49.99/35.12 tff(c_438892, plain, (~hskp15)). % 49.99/35.12 tff(c_438839, plain, (~c3_1(a149))). % 49.99/35.12 tff(c_438840, plain, (hskp53)). % 49.99/35.12 tff(c_377373, plain, (~hskp27)). % 49.99/35.12 tff(c_377372, plain, (~hskp19)). % 49.99/35.12 tff(c_377371, plain, (~hskp11)). % 49.99/35.12 tff(c_377370, plain, (~hskp55)). % 49.99/35.12 tff(c_377369, plain, (~hskp52)). % 49.99/35.12 tff(c_377366, plain, (~hskp20)). % 49.99/35.13 tff(c_377365, plain, (~hskp12)). % 49.99/35.13 tff(c_377363, plain, (~c4_1(a106))). % 49.99/35.13 tff(c_377364, plain, (hskp21)). % 49.99/35.13 tff(c_377307, plain, (~c1_1(a146))). % 49.99/35.13 tff(c_377308, plain, (hskp50)). % 49.99/35.13 tff(c_829, plain, (~hskp49)). % 49.99/35.13 tff(c_828, plain, (~hskp29)). % 49.99/35.13 tff(c_827, plain, (~hskp23)). % 49.99/35.13 tff(c_826, plain, (~hskp40)). % 49.99/35.13 tff(c_825, plain, (~hskp2)). % 49.99/35.13 tff(c_824, plain, (~hskp25)). % 49.99/35.13 tff(c_823, plain, (~hskp48)). % 49.99/35.13 tff(c_822, plain, (~hskp5)). % 49.99/35.13 tff(c_821, plain, (~hskp26)). % 49.99/35.13 tff(c_820, plain, (hskp43)). % 49.99/35.13 tff(c_819, plain, (~hskp47)). % 49.99/35.13 tff(c_818, plain, (~hskp44)). % 49.99/35.13 tff(c_817, plain, (~hskp16)). % 49.99/35.13 tff(c_816, plain, (~hskp6)). % 49.99/35.13 tff(c_815, plain, (~hskp22)). % 49.99/35.13 tff(c_775, plain, (hskp38)). % 49.99/35.13 tff(c_774, plain, (ndr1_0)). % 49.99/35.13 tff(c_665, plain, (~hskp7)). % 49.99/35.13 tff(c_664, plain, (~hskp46)). % 49.99/35.13 tff(c_663, plain, (~hskp28)). % 49.99/35.13 tff(c_662, plain, (~hskp64)). % 49.99/35.13 tff(c_661, plain, (~hskp13)). % 49.99/35.13 tff(c_660, plain, (~hskp60)). % 49.99/35.13 tff(c_659, plain, (~hskp58)). % 49.99/35.13 tff(c_658, plain, (~hskp45)). % 49.99/35.13 tff(c_657, plain, (~hskp36)). % 49.99/35.13 tff(c_656, plain, (~hskp37)). % 49.99/35.13 tff(c_655, plain, (~hskp59)). % 49.99/35.13 tff(c_654, plain, (~hskp56)). % 49.99/35.13 tff(c_653, plain, (~hskp34)). % 49.99/35.13 tff(c_652, plain, (~hskp17)). % 49.99/35.13 tff(c_651, plain, (~hskp30)). % 49.99/35.13 tff(c_650, plain, (~hskp62)). % 49.99/35.13 tff(c_649, plain, (~hskp31)). % 49.99/35.13 tff(c_648, plain, (~hskp33)). % 49.99/35.13 tff(c_647, plain, (~hskp35)). % 49.99/35.13 tff(c_646, plain, (~hskp32)). % 49.99/35.13 tff(c_645, plain, (~hskp8)). % 49.99/35.13 tff(c_644, plain, (~hskp63)). % 49.99/35.13 tff(c_643, plain, (~hskp4)). % 49.99/35.13 tff(c_642, plain, (~hskp1)). % 49.99/35.13 tff(c_641, plain, (~hskp0)). % 49.99/35.13 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 49.99/35.13 %------------------------------------------------------------------------------