%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN546+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %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 : 0s % DateTime : Thu Jul 21 03:51:22 EDT 2022 % Result : CounterSatisfiable 0.77s 0.96s % Output : Model 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN546+1 : TPTP v8.1.0. Released v2.1.0. % 0.10/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.14/0.34 % Computer : n010.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 % DateTime : Mon Jul 11 21:37:00 EDT 2022 % 0.14/0.34 % CPUTime : % 0.14/0.35 Defaulting to tptp format. % 0.77/0.96 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.77/0.96 % 0.77/0.96 MODEL (CONTEXT): % 0.77/0.96 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.77/0.96 -__-v__(=0) % 0.77/0.96 +__con201 % 0.77/0.96 -__con202 % 0.77/0.96 +__con203 % 0.77/0.96 -__con204 % 0.77/0.96 -__con205 % 0.77/0.96 -__con206 % 0.77/0.96 +__con209 % 0.77/0.96 +__con210 % 0.77/0.96 +__con211 % 0.77/0.96 +__con212 % 0.77/0.96 +__con213 % 0.77/0.96 +__con214 % 0.77/0.96 +__con215 % 0.77/0.96 -__con216 % 0.77/0.96 +__con217 % 0.77/0.96 -__con221 % 0.77/0.96 +__con222 % 0.77/0.96 +__con223 % 0.77/0.96 +__con224 % 0.77/0.96 +__con225 % 0.77/0.96 +__con226 % 0.77/0.96 -__con230 % 0.77/0.96 +__con231 % 0.77/0.96 -__con232 % 0.77/0.96 +__con233 % 0.77/0.96 -__con234 % 0.77/0.96 +__con235 % 0.77/0.96 +__con236 % 0.77/0.96 +__con237 % 0.77/0.96 +__con238 % 0.77/0.96 -__con239 % 0.77/0.96 -__con240 % 0.77/0.96 +__con241 % 0.77/0.96 -__con242 % 0.77/0.96 -__con243 % 0.77/0.96 -__con244 % 0.77/0.96 -__con245 % 0.77/0.96 -__con246 % 0.77/0.96 +__con248 % 0.77/0.96 +__con249 % 0.77/0.96 +__con250 % 0.77/0.96 -__con251 % 0.77/0.96 +__con252 % 0.77/0.96 -__con253 % 0.77/0.96 -__con254 % 0.77/0.96 -__con255 % 0.77/0.96 -__con257 % 0.77/0.96 -__con258 % 0.77/0.96 -__con259 % 0.77/0.96 -__con260 % 0.77/0.96 +__con269 % 0.77/0.96 -__con271 % 0.77/0.96 +__con272 % 0.77/0.96 -__con273 % 0.77/0.96 -__con274 % 0.77/0.96 -__con275 % 0.77/0.96 +__con276 % 0.77/0.96 -__con277 % 0.77/0.96 -__con278 % 0.77/0.96 -__con279 % 0.77/0.96 -__con280 % 0.77/0.96 -__con281 % 0.77/0.96 -__con282 % 0.77/0.96 -__con283 % 0.77/0.96 -__con284 % 0.77/0.96 -__con285 % 0.77/0.96 -__con286 % 0.77/0.96 -__con287 % 0.77/0.96 -__con288 % 0.77/0.96 -__con289 % 0.77/0.96 +__con290 % 0.77/0.96 -__con291 % 0.77/0.96 +__con292 % 0.77/0.96 +__con293 % 0.77/0.96 -__con294 % 0.77/0.96 -__con295 % 0.77/0.96 -__con296 % 0.77/0.96 -__con297 % 0.77/0.96 -__con298 % 0.77/0.96 -__con299 % 0.77/0.96 +__con300 % 0.77/0.96 -__con301 % 0.77/0.96 -__con306 % 0.77/0.96 +__con308 % 0.77/0.96 +__con309 % 0.77/0.96 +__con310 % 0.77/0.96 -__con311 % 0.77/0.96 +__con312 % 0.77/0.96 +__con313 % 0.77/0.96 -__con314 % 0.77/0.96 +__con315 % 0.77/0.96 -__con316 % 0.77/0.96 +__con319 % 0.77/0.96 -__con320 % 0.77/0.96 -__con335 % 0.77/0.96 -__con341 % 0.77/0.96 +__con342 % 0.77/0.96 +__con343 % 0.77/0.96 -c1_0 % 0.77/0.96 +c1_1(a387) % 0.77/0.96 -c1_1(a298) % 0.77/0.96 +c1_2(a300, a389) % 0.77/0.96 +c1_2(a302, a389) % 0.77/0.96 +c1_2(a305, a306) % 0.77/0.96 +c1_2(a311, a312) % 0.77/0.96 +c1_2(a345, a346) % 0.77/0.96 +c1_2(a345, a389) % 0.77/0.96 +c1_2(a347, a348) % 0.77/0.96 +c1_2(a347, a444) % 0.77/0.96 +c1_2(a369, =0) % 0.77/0.96 +c1_2(a369, a389) % 0.77/0.96 +c1_2(a380, a383) % 0.77/0.96 +c1_2(a385, a389) % 0.77/0.96 +c1_2(a423, a389) % 0.77/0.96 +c1_2(a423, a424) % 0.77/0.96 -c1_2(a330, a331) % 0.77/0.96 -c1_2(a380, a381) % 0.77/0.96 -c1_2(a380, a382) % 0.77/0.96 +c2_0 % 0.77/0.96 +c2_1(=0) % 0.77/0.96 +c2_1(a300) % 0.77/0.96 +c2_1(a302) % 0.77/0.96 +c2_1(a345) % 0.77/0.96 +c2_1(a369) % 0.77/0.96 +c2_1(a385) % 0.77/0.96 +c2_1(a423) % 0.77/0.96 -c2_1(a315) % 0.77/0.96 -c2_1(a330) % 0.77/0.96 -c2_1(a354) % 0.77/0.96 -c2_1(a380) % 0.77/0.96 -c2_1(a445) % 0.77/0.96 +c2_2(a300, a389) % 0.77/0.96 +c2_2(a302, a389) % 0.77/0.96 +c2_2(a305, a306) % 0.77/0.96 +c2_2(a328, a329) % 0.77/0.96 +c2_2(a345, a346) % 0.77/0.96 +c2_2(a345, a389) % 0.77/0.96 +c2_2(a347, a348) % 0.77/0.96 +c2_2(a347, a444) % 0.77/0.96 +c2_2(a369, a389) % 0.77/0.96 +c2_2(a380, a381) % 0.77/0.96 +c2_2(a385, a389) % 0.77/0.96 +c2_2(a423, a389) % 0.77/0.96 -c2_2(a330, a332) % 0.77/0.96 +c3_0 % 0.77/0.96 +c3_1(a300) % 0.77/0.96 +c3_1(a302) % 0.77/0.96 +c3_1(a309) % 0.77/0.96 +c3_1(a345) % 0.77/0.96 +c3_1(a354) % 0.77/0.96 +c3_1(a369) % 0.77/0.96 +c3_1(a371) % 0.77/0.96 +c3_1(a379) % 0.77/0.96 +c3_1(a385) % 0.77/0.96 +c3_1(a400) % 0.77/0.96 +c3_1(a417) % 0.77/0.96 +c3_1(a423) % 0.77/0.96 +c3_1(a425) % 0.77/0.96 +c3_1(a441) % 0.77/0.96 -c3_1(a298) % 0.77/0.96 +c3_2(a300, a390) % 0.77/0.96 +c3_2(a302, a390) % 0.77/0.96 +c3_2(a345, a390) % 0.77/0.96 +c3_2(a347, a348) % 0.77/0.96 +c3_2(a369, a390) % 0.77/0.96 +c3_2(a376, a377) % 0.77/0.96 +c3_2(a380, a382) % 0.77/0.96 +c3_2(a385, a390) % 0.77/0.96 +c3_2(a387, a388) % 0.77/0.96 +c3_2(a423, a390) % 0.77/0.96 +c3_2(a425, a426) % 0.77/0.96 +c3_2(a445, a446) % 0.77/0.96 -c3_2(a305, a306) % 0.77/0.96 -c3_2(a385, a386) % 0.77/0.96 -c3_2(a417, a418) % 0.77/0.96 +c4_0 % 0.77/0.96 +c4_1(a300) % 0.77/0.96 +c4_1(a302) % 0.77/0.96 +c4_1(a305) % 0.77/0.96 +c4_1(a311) % 0.77/0.96 +c4_1(a328) % 0.77/0.96 +c4_1(a330) % 0.77/0.96 +c4_1(a342) % 0.77/0.96 +c4_1(a345) % 0.77/0.96 +c4_1(a347) % 0.77/0.96 +c4_1(a369) % 0.77/0.96 +c4_1(a376) % 0.77/0.96 +c4_1(a380) % 0.77/0.96 +c4_1(a385) % 0.77/0.96 +c4_1(a387) % 0.77/0.96 +c4_1(a413) % 0.77/0.96 +c4_1(a417) % 0.77/0.96 +c4_1(a423) % 0.77/0.96 +c4_1(a425) % 0.77/0.96 +c4_1(a445) % 0.77/0.96 +c4_2(a330, a331) % 0.77/0.96 +c4_2(a347, a444) % 0.77/0.96 +c4_2(a380, a319) % 0.77/0.96 +c4_2(a425, a426) % 0.77/0.96 +c4_2(a445, a447) % 0.77/0.96 -c4_2(a311, a312) % 0.77/0.96 -c4_2(a311, a313) % 0.77/0.96 -c4_2(a347, a348) % 0.77/0.96 -c5_0 % 0.77/0.96 +c5_1(a354) % 0.77/0.96 +c5_1(a385) % 0.77/0.96 +c5_1(a400) % 0.77/0.96 +c5_1(a417) % 0.77/0.96 +c5_1(a441) % 0.77/0.96 -c5_1(a305) % 0.77/0.96 +c5_2(a300, a301) % 0.77/0.96 +c5_2(a328, a329) % 0.77/0.96 +c5_2(a380, a381) % 0.77/0.96 +c5_2(a423, a424) % 0.77/0.96 -c5_2(a311, a312) % 0.77/0.96 -c5_2(a311, a313) % 0.77/0.96 -c5_2(a330, a331) % 0.77/0.96 -c5_2(a330, a332) % 0.77/0.96 -c5_2(a376, a377) % 0.77/0.96 +c6_0 % 0.77/0.96 +c6_1(a328) % 0.77/0.96 +c6_1(a345) % 0.77/0.96 +c6_1(a380) % 0.77/0.96 +c6_1(a387) % 0.77/0.96 -c6_1(a330) % 0.77/0.96 +c6_2(a330, a331) % 0.77/0.96 +c6_2(a380, a383) % 0.77/0.96 -c6_2(a376, a377) % 0.77/0.96 -c6_2(a380, a382) % 0.77/0.96 -c6_2(a385, a386) % 0.77/0.96 -c6_2(a417, a418) % 0.77/0.96 +c7_0 % 0.77/0.96 +c7_1(a354) % 0.77/0.96 +c7_1(a400) % 0.77/0.96 +c7_1(a441) % 0.77/0.96 -c7_1(a309) % 0.77/0.96 +c7_2(a387, a388) % 0.77/0.96 -c7_2(a311, a313) % 0.77/0.96 +c8_0 % 0.77/0.96 +c8_1(a298) % 0.77/0.96 +c8_1(a315) % 0.77/0.96 +c8_1(a317) % 0.77/0.96 +c8_1(a330) % 0.77/0.96 +c8_1(a347) % 0.77/0.96 +c8_1(a354) % 0.77/0.96 +c8_1(a380) % 0.77/0.96 +c8_1(a445) % 0.77/0.96 -c8_1(a423) % 0.77/0.96 +c8_2(a305, a306) % 0.77/0.96 +c8_2(a423, a424) % 0.77/0.96 -c8_2(a330, a332) % 0.77/0.96 -c8_2(a380, a381) % 0.77/0.96 -c8_2(a380, a383) % 0.77/0.96 -c8_2(a385, a386) % 0.77/0.96 +epred1_0 % 0.77/0.96 +epred2_0 % 0.77/0.96 +epred3_0 % 0.77/0.96 +epred4_0 % 0.77/0.96 +epred5_0 % 0.77/0.96 +ndr1_0 % 0.77/0.96 +ndr1_1(a300) % 0.77/0.96 +ndr1_1(a302) % 0.77/0.96 +ndr1_1(a305) % 0.77/0.96 +ndr1_1(a311) % 0.77/0.96 +ndr1_1(a328) % 0.77/0.96 +ndr1_1(a330) % 0.77/0.96 +ndr1_1(a342) % 0.77/0.96 +ndr1_1(a345) % 0.77/0.96 +ndr1_1(a347) % 0.77/0.96 +ndr1_1(a369) % 0.77/0.96 +ndr1_1(a376) % 0.77/0.96 +ndr1_1(a380) % 0.77/0.96 +ndr1_1(a385) % 0.77/0.96 +ndr1_1(a387) % 0.77/0.96 +ndr1_1(a417) % 0.77/0.96 +ndr1_1(a423) % 0.77/0.96 +ndr1_1(a425) % 0.77/0.96 +ndr1_1(a445) % 0.77/0.96 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------