%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN419+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n013.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:47 EDT 2022 % Result : CounterSatisfiable 0.51s 0.75s % Output : Model 0.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN419+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.34 % Computer : n013.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % DateTime : Mon Jul 11 12:18:45 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 Defaulting to tptp format. % 0.51/0.75 SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.51/0.75 % 0.51/0.75 MODEL (CONTEXT): % 0.51/0.75 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.51/0.75 -__-v__(=0) % 0.51/0.75 +__con175 % 0.51/0.75 +__con176 % 0.51/0.75 +__con177 % 0.51/0.75 -__con180 % 0.51/0.75 -__con181 % 0.51/0.75 -__con182 % 0.51/0.75 +__con183 % 0.51/0.75 +__con184 % 0.51/0.75 -__con185 % 0.51/0.75 +__con186 % 0.51/0.75 +__con187 % 0.51/0.75 +__con188 % 0.51/0.75 -__con189 % 0.51/0.75 +__con190 % 0.51/0.75 +__con192 % 0.51/0.75 +__con193 % 0.51/0.75 +__con194 % 0.51/0.75 +__con195 % 0.51/0.75 +__con196 % 0.51/0.75 -__con197 % 0.51/0.75 +__con198 % 0.51/0.75 -__con199 % 0.51/0.75 +__con207 % 0.51/0.75 +__con208 % 0.51/0.75 +__con209 % 0.51/0.75 +__con210 % 0.51/0.75 -__con212 % 0.51/0.75 +__con213 % 0.51/0.75 -__con214 % 0.51/0.75 -__con215 % 0.51/0.75 -__con216 % 0.51/0.75 +__con217 % 0.51/0.75 +__con218 % 0.51/0.75 +__con219 % 0.51/0.75 +__con220 % 0.51/0.75 +__con234 % 0.51/0.75 +__con235 % 0.51/0.75 +__con236 % 0.51/0.75 -__con238 % 0.51/0.75 +__con239 % 0.51/0.75 +__con248 % 0.51/0.75 +__con249 % 0.51/0.75 +__con257 % 0.51/0.75 +__con258 % 0.51/0.75 +__con259 % 0.51/0.75 +__con260 % 0.51/0.75 +__con261 % 0.51/0.75 +__con262 % 0.51/0.75 -__con263 % 0.51/0.75 +__con264 % 0.51/0.75 -__con271 % 0.51/0.75 +__con272 % 0.51/0.75 +__con280 % 0.51/0.75 +__con281 % 0.51/0.75 +__con282 % 0.51/0.75 +__con283 % 0.51/0.75 +__con284 % 0.51/0.75 +__con285 % 0.51/0.75 +__con286 % 0.51/0.75 +__con287 % 0.51/0.75 +__con288 % 0.51/0.75 +__con289 % 0.51/0.75 +__con290 % 0.51/0.75 +__con301 % 0.51/0.75 +__con302 % 0.51/0.75 +__con311 % 0.51/0.75 -__con325 % 0.51/0.75 +__con326 % 0.51/0.75 -__con333 % 0.51/0.75 -__con334 % 0.51/0.75 +__con335 % 0.51/0.75 +c10_0 % 0.51/0.75 +c10_1(a149) % 0.51/0.75 +c10_1(a160) % 0.51/0.75 +c10_1(a174) % 0.51/0.75 -c10_1(a173) % 0.51/0.75 +c10_2(a163, a164) % 0.51/0.75 +c1_0 % 0.51/0.75 +c1_1(a163) % 0.51/0.75 +c1_1(a175) % 0.51/0.75 +c2_0 % 0.51/0.75 +c2_1(a157) % 0.51/0.75 +c2_2(a200, a202) % 0.51/0.75 +c3_0 % 0.51/0.75 +c3_2(a200, a202) % 0.51/0.75 +c4_0 % 0.51/0.75 +c5_0 % 0.51/0.75 +c5_2(a200, a201) % 0.51/0.75 -c5_2(a163, a164) % 0.51/0.75 +c6_0 % 0.51/0.75 +c6_1(a173) % 0.51/0.75 +c6_1(a232) % 0.51/0.75 +c6_2(a163, a164) % 0.51/0.75 +c7_0 % 0.51/0.75 +c7_1(a173) % 0.51/0.75 +c7_2(a149, a150) % 0.51/0.75 +c8_0 % 0.51/0.75 +c8_1(a215) % 0.51/0.75 +c8_2(a232, a233) % 0.51/0.75 +c9_0 % 0.51/0.75 +c9_1(a174) % 0.51/0.75 +c9_2(a163, a164) % 0.51/0.75 +c9_2(a200, a202) % 0.51/0.75 +epred1_0 % 0.51/0.75 +epred2_0 % 0.51/0.75 +epred3_0 % 0.51/0.75 +epred5_0 % 0.51/0.75 +epred6_0 % 0.51/0.75 +epred7_0 % 0.51/0.75 +ndr1_0 % 0.51/0.75 +ndr1_1(a149) % 0.51/0.75 +ndr1_1(a152) % 0.51/0.75 +ndr1_1(a163) % 0.51/0.75 +ndr1_1(a173) % 0.51/0.75 +ndr1_1(a200) % 0.51/0.75 +ndr1_1(a232) % 0.51/0.75 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------