%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN544+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:20 EDT 2022 % Result : CounterSatisfiable 0.59s 0.84s % Output : Model 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN544+1 : TPTP v8.1.0. Released v2.1.0. % 0.11/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.33 % Computer : n010.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % DateTime : Mon Jul 11 14:52:00 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 Defaulting to tptp format. % 0.59/0.84 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.84 % 0.59/0.84 MODEL (CONTEXT): % 0.59/0.84 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.84 -__-v__(=0) % 0.59/0.84 -__con198 % 0.59/0.84 -__con199 % 0.59/0.84 +__con200 % 0.59/0.84 -__con201 % 0.59/0.84 +__con202 % 0.59/0.84 -__con203 % 0.59/0.84 -__con205 % 0.59/0.84 +__con206 % 0.59/0.84 -__con207 % 0.59/0.84 -__con208 % 0.59/0.84 -__con209 % 0.59/0.84 -__con210 % 0.59/0.84 -__con211 % 0.59/0.84 -__con212 % 0.59/0.84 -__con213 % 0.59/0.84 -__con214 % 0.59/0.84 -__con215 % 0.59/0.84 -__con216 % 0.59/0.84 -__con217 % 0.59/0.84 -__con218 % 0.59/0.84 -__con220 % 0.59/0.84 -__con221 % 0.59/0.84 -__con222 % 0.59/0.84 -__con224 % 0.59/0.84 +__con226 % 0.59/0.84 -__con227 % 0.59/0.84 +__con231 % 0.59/0.84 +__con232 % 0.59/0.84 +__con233 % 0.59/0.84 -__con234 % 0.59/0.84 +__con236 % 0.59/0.84 +__con237 % 0.59/0.84 +__con240 % 0.59/0.84 +__con241 % 0.59/0.84 -__con243 % 0.59/0.84 +__con244 % 0.59/0.84 -__con245 % 0.59/0.84 +__con250 % 0.59/0.84 +__con257 % 0.59/0.84 -__con261 % 0.59/0.84 -__con263 % 0.59/0.84 -__con264 % 0.59/0.84 +__con265 % 0.59/0.84 -__con266 % 0.59/0.84 +__con267 % 0.59/0.84 +__con268 % 0.59/0.84 -__con271 % 0.59/0.84 +__con272 % 0.59/0.84 +__con273 % 0.59/0.84 -__con276 % 0.59/0.84 +__con278 % 0.59/0.84 +__con292 % 0.59/0.84 +__con293 % 0.59/0.84 +__con310 % 0.59/0.84 -__con311 % 0.59/0.84 +__con312 % 0.59/0.84 -__con313 % 0.59/0.84 -__con314 % 0.59/0.84 -__con315 % 0.59/0.84 +__con316 % 0.59/0.84 +__con322 % 0.59/0.84 +__con324 % 0.59/0.84 +__con340 % 0.59/0.84 +__con341 % 0.59/0.84 +__con342 % 0.59/0.84 -__con347 % 0.59/0.84 -__con348 % 0.59/0.84 +__con350 % 0.59/0.84 +__con353 % 0.59/0.84 +c1_0 % 0.59/0.84 +c1_1(a16) % 0.59/0.84 +c1_1(a24) % 0.59/0.84 +c1_1(a27) % 0.59/0.84 +c1_1(a64) % 0.59/0.84 +c1_1(a96) % 0.59/0.84 +c1_1(a136) % 0.59/0.84 -c1_1(a122) % 0.59/0.84 -c1_1(a134) % 0.59/0.84 +c1_2(a24, a25) % 0.59/0.84 +c1_2(a64, =0) % 0.59/0.84 +c1_2(a134, =0) % 0.59/0.84 +c1_2(a136, a137) % 0.59/0.84 -c1_2(a64, a1) % 0.59/0.84 -c1_2(a122, a123) % 0.59/0.84 -c1_2(a134, a1) % 0.59/0.84 -c2_0 % 0.59/0.84 +c2_1(a51) % 0.59/0.84 +c2_1(a52) % 0.59/0.84 +c2_1(a96) % 0.59/0.84 +c2_1(a136) % 0.59/0.84 -c2_1(a16) % 0.59/0.84 -c2_1(a117) % 0.59/0.84 +c2_2(a27, a28) % 0.59/0.84 -c2_2(a81, a63) % 0.59/0.84 -c3_0 % 0.59/0.85 +c3_1(a59) % 0.59/0.85 +c3_1(a96) % 0.59/0.85 +c3_2(a81, a82) % 0.59/0.85 +c3_2(a134, a135) % 0.59/0.85 +c3_2(a136, =0) % 0.59/0.85 +c3_2(a136, a137) % 0.59/0.85 -c3_2(a27, a115) % 0.59/0.85 -c3_2(a52, a115) % 0.59/0.85 -c3_2(a117, a115) % 0.59/0.85 -c3_2(a122, a115) % 0.59/0.85 -c3_2(a122, a123) % 0.59/0.85 +c4_0 % 0.59/0.85 +c4_1(a64) % 0.59/0.85 +c4_1(a96) % 0.59/0.85 -c4_1(a52) % 0.59/0.85 -c4_1(a59) % 0.59/0.85 +c4_2(a59, a70) % 0.59/0.85 +c4_2(a64, a1) % 0.59/0.85 +c4_2(a64, a2) % 0.59/0.85 +c4_2(a81, a63) % 0.59/0.85 +c4_2(a81, a82) % 0.59/0.85 +c4_2(a96, a70) % 0.59/0.85 -c4_2(a134, a135) % 0.59/0.85 +c5_0 % 0.59/0.85 +c5_1(a51) % 0.59/0.85 +c5_1(a52) % 0.59/0.85 +c5_1(a136) % 0.59/0.85 +c5_2(a59, =0) % 0.59/0.85 +c5_2(a59, a69) % 0.59/0.85 +c5_2(a96, a69) % 0.59/0.85 +c5_2(a122, a123) % 0.59/0.85 +c5_2(a136, a137) % 0.59/0.85 -c5_2(a81, a63) % 0.59/0.85 +c6_0 % 0.59/0.85 +c6_1(a27) % 0.59/0.85 +c6_1(a52) % 0.59/0.85 +c6_1(a59) % 0.59/0.85 +c6_1(a117) % 0.59/0.85 +c6_1(a122) % 0.59/0.85 +c6_1(a134) % 0.59/0.85 -c6_1(a81) % 0.59/0.85 +c6_2(a64, a3) % 0.59/0.85 +c7_0 % 0.59/0.85 +c7_1(a27) % 0.59/0.85 +c7_1(a52) % 0.59/0.85 +c7_1(a59) % 0.59/0.85 +c7_1(a81) % 0.59/0.85 +c7_1(a117) % 0.59/0.85 +c7_1(a122) % 0.59/0.85 -c7_1(a51) % 0.59/0.85 -c7_2(a27, a115) % 0.59/0.85 -c7_2(a34, _0) % 0.59/0.85 -c7_2(a52, a115) % 0.59/0.85 -c7_2(a117, a115) % 0.59/0.85 -c7_2(a122, a115) % 0.59/0.85 +c8_0 % 0.59/0.85 +c8_1(a27) % 0.59/0.85 +c8_1(a52) % 0.59/0.85 +c8_1(a117) % 0.59/0.85 +c8_1(a122) % 0.59/0.85 -c8_1(a16) % 0.59/0.85 -c8_1(a51) % 0.59/0.85 +c8_2(a81, a82) % 0.59/0.85 +c8_2(a134, a1) % 0.59/0.85 +c8_2(a134, a135) % 0.59/0.85 -c8_2(a27, a115) % 0.59/0.85 -c8_2(a52, a115) % 0.59/0.85 -c8_2(a117, a115) % 0.59/0.85 -c8_2(a122, a115) % 0.59/0.85 +epred1_0 % 0.59/0.85 -epred2_0 % 0.59/0.85 +epred3_0 % 0.59/0.85 +epred4_0 % 0.59/0.85 +epred5_0 % 0.59/0.85 -epred7_0 % 0.59/0.85 +ndr1_0 % 0.59/0.85 +ndr1_1(_0) % 0.59/0.85 +ndr1_1(a24) % 0.59/0.85 +ndr1_1(a27) % 0.59/0.85 +ndr1_1(a35) % 0.59/0.85 +ndr1_1(a52) % 0.59/0.85 +ndr1_1(a59) % 0.59/0.85 +ndr1_1(a117) % 0.59/0.85 +ndr1_1(a122) % 0.59/0.85 +ndr1_1(a134) % 0.59/0.85 +ndr1_1(a136) % 0.59/0.85 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------