%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN421+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n008.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:49:49 EDT 2022 % Result : CounterSatisfiable 0.60s 0.83s % Output : Model 0.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN421+1 : TPTP v8.1.0. Released v2.1.0. % 0.00/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.33 % Computer : n008.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Tue Jul 12 00:43:23 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.34 Defaulting to tptp format. % 0.60/0.83 SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.60/0.83 % 0.60/0.83 MODEL (CONTEXT): % 0.60/0.83 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.60/0.83 -__-v__(=0) % 0.60/0.83 -__con208 % 0.60/0.83 +__con209 % 0.60/0.83 +__con210 % 0.60/0.83 -__con211 % 0.60/0.83 +__con212 % 0.60/0.83 +__con213 % 0.60/0.83 -__con215 % 0.60/0.83 -__con216 % 0.60/0.83 +__con218 % 0.60/0.83 +__con219 % 0.60/0.83 +__con222 % 0.60/0.83 +__con223 % 0.60/0.83 -__con234 % 0.60/0.83 +__con235 % 0.60/0.83 +__con236 % 0.60/0.83 +__con237 % 0.60/0.83 +__con238 % 0.60/0.83 -__con239 % 0.60/0.83 +__con243 % 0.60/0.83 +__con244 % 0.60/0.83 -__con245 % 0.60/0.83 -__con246 % 0.60/0.83 +__con247 % 0.60/0.83 -__con248 % 0.60/0.83 -__con249 % 0.60/0.83 +__con250 % 0.60/0.83 -__con254 % 0.60/0.83 -__con255 % 0.60/0.83 -__con256 % 0.60/0.83 +__con257 % 0.60/0.83 -__con258 % 0.60/0.83 -__con259 % 0.60/0.83 +__con260 % 0.60/0.83 +__con263 % 0.60/0.83 +__con264 % 0.60/0.83 +__con275 % 0.60/0.83 -__con278 % 0.60/0.83 +__con279 % 0.60/0.83 +__con280 % 0.60/0.83 +__con281 % 0.60/0.83 +__con284 % 0.60/0.83 -__con285 % 0.60/0.83 -__con286 % 0.60/0.83 -__con287 % 0.60/0.83 +__con303 % 0.60/0.83 +__con304 % 0.60/0.83 +__con307 % 0.60/0.83 +__con308 % 0.60/0.83 -__con309 % 0.60/0.83 +__con310 % 0.60/0.83 -__con311 % 0.60/0.83 +__con312 % 0.60/0.83 -__con313 % 0.60/0.83 -__con314 % 0.60/0.83 +__con315 % 0.60/0.83 -__con316 % 0.60/0.83 -__con317 % 0.60/0.83 -__con318 % 0.60/0.83 -__con319 % 0.60/0.83 -__con320 % 0.60/0.83 -__con321 % 0.60/0.83 +__con322 % 0.60/0.83 -__con324 % 0.60/0.83 -__con325 % 0.60/0.83 -__con330 % 0.60/0.83 -__con331 % 0.60/0.83 -__con332 % 0.60/0.83 +__con334 % 0.60/0.83 +__con335 % 0.60/0.83 +__con336 % 0.60/0.83 +__con337 % 0.60/0.83 +__con339 % 0.60/0.83 +__con340 % 0.60/0.83 +c10_0 % 0.60/0.83 +c10_1(a460) % 0.60/0.83 +c10_1(a464) % 0.60/0.83 +c10_1(a478) % 0.60/0.83 +c10_1(a481) % 0.60/0.83 +c10_1(a514) % 0.60/0.83 +c10_1(a515) % 0.60/0.83 +c10_1(a517) % 0.60/0.83 +c10_1(a519) % 0.60/0.83 +c10_1(a537) % 0.60/0.83 +c10_1(a547) % 0.60/0.83 +c10_1(a560) % 0.60/0.83 +c10_2(a464, a465) % 0.60/0.83 +c10_2(a481, a482) % 0.60/0.83 +c10_2(a481, a483) % 0.60/0.83 -c10_2(a460, a461) % 0.60/0.83 +c1_0 % 0.60/0.83 +c1_1(a460) % 0.60/0.83 +c1_1(a478) % 0.60/0.83 +c1_1(a481) % 0.60/0.83 +c1_1(a514) % 0.60/0.83 +c1_1(a515) % 0.60/0.83 +c1_1(a517) % 0.60/0.83 +c1_1(a519) % 0.60/0.83 +c1_1(a537) % 0.60/0.83 +c1_1(a547) % 0.60/0.83 +c1_1(a560) % 0.60/0.83 +c1_2(a560, a561) % 0.60/0.83 -c2_0 % 0.60/0.83 +c2_1(=0) % 0.60/0.83 -c2_1(a514) % 0.60/0.83 -c2_1(a537) % 0.60/0.83 -c2_1(a547) % 0.60/0.83 +c2_2(a560, a561) % 0.60/0.83 -c2_2(a464, a465) % 0.60/0.83 -c3_0 % 0.60/0.83 +c3_1(a464) % 0.60/0.83 +c3_2(a460, a461) % 0.60/0.83 +c4_0 % 0.60/0.83 -c4_1(a454) % 0.60/0.83 -c4_1(a494) % 0.60/0.83 -c4_1(a499) % 0.60/0.83 -c4_1(a599) % 0.60/0.83 -c4_1(a605) % 0.60/0.83 +c4_2(a460, a461) % 0.60/0.83 +c4_2(a460, a607) % 0.60/0.83 +c4_2(a481, a482) % 0.60/0.83 +c4_2(a537, a607) % 0.60/0.83 +c4_2(a547, a607) % 0.60/0.83 +c5_1(a460) % 0.60/0.83 +c5_1(a537) % 0.60/0.83 +c5_1(a547) % 0.60/0.83 +c5_2(a464, a466) % 0.60/0.83 +c5_2(a481, a483) % 0.60/0.83 +c6_0 % 0.60/0.83 +c6_1(a460) % 0.60/0.83 +c6_1(a547) % 0.60/0.83 +c6_2(a481, a482) % 0.60/0.83 -c6_2(a464, a465) % 0.60/0.83 +c7_0 % 0.60/0.83 +c7_1(a478) % 0.60/0.83 +c7_1(a514) % 0.60/0.83 +c7_1(a537) % 0.60/0.83 +c7_1(a547) % 0.60/0.83 -c7_1(a460) % 0.60/0.83 -c7_2(a464, a466) % 0.60/0.83 -c8_0 % 0.60/0.83 +c8_1(a515) % 0.60/0.83 +c8_1(a586) % 0.60/0.83 +c8_2(a517, a518) % 0.60/0.83 +c9_0 % 0.60/0.83 +c9_1(a493) % 0.60/0.83 +c9_1(a517) % 0.60/0.83 +c9_1(a519) % 0.60/0.83 +c9_1(a585) % 0.60/0.83 +c9_2(a517, a518) % 0.60/0.83 +epred2_0 % 0.60/0.83 +epred4_0 % 0.60/0.83 +ndr1_0 % 0.60/0.83 +ndr1_1(a460) % 0.60/0.83 +ndr1_1(a464) % 0.60/0.83 +ndr1_1(a478) % 0.60/0.83 +ndr1_1(a481) % 0.60/0.83 +ndr1_1(a514) % 0.60/0.83 +ndr1_1(a515) % 0.60/0.83 +ndr1_1(a517) % 0.60/0.83 +ndr1_1(a519) % 0.60/0.83 +ndr1_1(a537) % 0.60/0.83 +ndr1_1(a547) % 0.60/0.83 +ndr1_1(a560) % 0.60/0.83 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------