%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN418+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n024.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.69s 0.88s % Output : Model 0.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYN418+1 : TPTP v8.1.0. Released v2.1.0. % 0.11/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.33 % Computer : n024.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 : Mon Jul 11 17:34:43 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.33 Defaulting to tptp format. % 0.69/0.88 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.88 % 0.69/0.88 MODEL (CONTEXT): % 0.69/0.88 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.88 -__-v__(=0) % 0.69/0.88 -__con194 % 0.69/0.88 +__con195 % 0.69/0.88 -__con196 % 0.69/0.88 +__con197 % 0.69/0.88 -__con200 % 0.69/0.88 -__con201 % 0.69/0.88 -__con202 % 0.69/0.88 +__con203 % 0.69/0.88 +__con204 % 0.69/0.88 +__con205 % 0.69/0.88 +__con206 % 0.69/0.88 +__con207 % 0.69/0.88 +__con208 % 0.69/0.88 +__con209 % 0.69/0.88 +__con210 % 0.69/0.88 +__con211 % 0.69/0.88 +__con212 % 0.69/0.88 +__con213 % 0.69/0.88 +__con214 % 0.69/0.88 +__con221 % 0.69/0.88 +__con222 % 0.69/0.88 +__con223 % 0.69/0.88 +__con224 % 0.69/0.88 +__con225 % 0.69/0.88 +__con226 % 0.69/0.88 +__con227 % 0.69/0.88 +__con234 % 0.69/0.88 +__con235 % 0.69/0.88 +__con236 % 0.69/0.88 +__con237 % 0.69/0.88 +__con238 % 0.69/0.88 +__con239 % 0.69/0.88 +__con240 % 0.69/0.88 +__con241 % 0.69/0.88 +__con242 % 0.69/0.88 +__con243 % 0.69/0.88 +__con244 % 0.69/0.88 +__con245 % 0.69/0.88 +__con246 % 0.69/0.88 +__con247 % 0.69/0.88 +__con248 % 0.69/0.88 +__con249 % 0.69/0.88 +__con250 % 0.69/0.88 +__con251 % 0.69/0.88 +__con252 % 0.69/0.88 +__con253 % 0.69/0.88 -__con303 % 0.69/0.88 +__con304 % 0.69/0.88 +__con305 % 0.69/0.88 +__con306 % 0.69/0.88 +__con307 % 0.69/0.88 +__con326 % 0.69/0.88 +__con327 % 0.69/0.88 +__con328 % 0.69/0.88 +__con336 % 0.69/0.88 +__con337 % 0.69/0.88 +__con341 % 0.69/0.88 -__con356 % 0.69/0.88 +__con357 % 0.69/0.88 -__con365 % 0.69/0.88 +__con366 % 0.69/0.88 -__con427 % 0.69/0.88 +__con428 % 0.69/0.88 +__con429 % 0.69/0.88 +__con430 % 0.69/0.88 -__con435 % 0.69/0.88 +__con436 % 0.69/0.88 +c10_0 % 0.69/0.88 +c10_1(a6) % 0.69/0.88 +c10_1(a102) % 0.69/0.88 +c10_1(a134) % 0.69/0.88 +c10_2(a22, a23) % 0.69/0.88 +c10_2(a33, a34) % 0.69/0.88 -c10_2(a136, a137) % 0.69/0.88 +c1_0 % 0.69/0.88 +c1_1(a22) % 0.69/0.88 +c1_2(a3, a4) % 0.69/0.88 +c2_0 % 0.69/0.88 -c2_1(a127) % 0.69/0.88 +c2_2(a22, a23) % 0.69/0.88 +c2_2(a136, a137) % 0.69/0.88 -c3_0 % 0.69/0.88 +c3_1(a18) % 0.69/0.88 +c3_1(a33) % 0.69/0.88 +c3_1(a44) % 0.69/0.88 +c3_2(a134, a135) % 0.69/0.88 -c4_0 % 0.69/0.88 +c4_1(a1) % 0.69/0.88 +c4_1(a18) % 0.69/0.88 +c4_1(a33) % 0.69/0.88 +c4_1(a44) % 0.69/0.88 +c4_1(a102) % 0.69/0.88 +c4_1(a127) % 0.69/0.88 +c5_2(a3, a4) % 0.69/0.88 -c5_2(a136, a137) % 0.69/0.88 +c6_1(a1) % 0.69/0.88 +c6_1(a18) % 0.69/0.88 +c6_1(a33) % 0.69/0.88 +c6_2(a1, a2) % 0.69/0.88 -c6_2(a134, a135) % 0.69/0.88 +c7_0 % 0.69/0.88 +c7_1(=0) % 0.69/0.88 +c7_1(a19) % 0.69/0.88 +c7_1(a136) % 0.69/0.88 +c7_2(a22, a23) % 0.69/0.88 +c8_0 % 0.69/0.88 +c8_1(a22) % 0.69/0.88 -c8_1(a136) % 0.69/0.88 -c8_2(a134, a135) % 0.69/0.88 -c9_0 % 0.69/0.88 +c9_1(a1) % 0.69/0.88 +c9_1(a100) % 0.69/0.88 +epred1_0 % 0.69/0.88 +epred2_0 % 0.69/0.88 +ndr1_0 % 0.69/0.88 +ndr1_1(a1) % 0.69/0.88 +ndr1_1(a3) % 0.69/0.88 +ndr1_1(a19) % 0.69/0.88 +ndr1_1(a22) % 0.69/0.88 +ndr1_1(a31) % 0.69/0.88 +ndr1_1(a33) % 0.69/0.88 +ndr1_1(a100) % 0.69/0.88 +ndr1_1(a102) % 0.69/0.88 +ndr1_1(a134) % 0.69/0.88 +ndr1_1(a136) % 0.69/0.88 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------