%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN519-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:51:01 EDT 2022 % Result : Satisfiable 0.54s 0.72s % Output : Model 0.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN519-1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.34 % Computer : n008.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % DateTime : Mon Jul 11 16:08:08 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 Defaulting to tptp format. % 0.54/0.72 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.54/0.72 % 0.54/0.72 MODEL (CONTEXT): % 0.54/0.72 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.54/0.72 -__-v__(=0) % 0.54/0.72 -__con257 % 0.54/0.72 -__con258 % 0.54/0.72 -__con259 % 0.54/0.72 +__con260 % 0.54/0.72 +__con261 % 0.54/0.72 -__con262 % 0.54/0.72 +__con264 % 0.54/0.72 -__con269 % 0.54/0.72 -__con270 % 0.54/0.72 -__con272 % 0.54/0.72 -__con273 % 0.54/0.72 -__con275 % 0.54/0.72 +__con276 % 0.54/0.72 +__con277 % 0.54/0.72 -__con278 % 0.54/0.72 -__con279 % 0.54/0.72 -__con280 % 0.54/0.72 +__con281 % 0.54/0.72 +__con282 % 0.54/0.72 +__con283 % 0.54/0.72 -__con284 % 0.54/0.72 -__con289 % 0.54/0.72 +__con290 % 0.54/0.72 -__con291 % 0.54/0.72 -__con292 % 0.54/0.72 -__con293 % 0.54/0.72 -__con294 % 0.54/0.72 +__con295 % 0.54/0.72 +__con296 % 0.54/0.72 +__con297 % 0.54/0.72 +__con298 % 0.54/0.72 +__con299 % 0.54/0.72 +c0_1(_0) % 0.54/0.72 +c1_0 % 0.54/0.72 +c1_1(=0) % 0.54/0.72 +c1_1(a173) % 0.54/0.72 +c1_1(a159) % 0.54/0.72 +c1_1(a125) % 0.54/0.72 +c1_1(a103) % 0.54/0.72 +c1_1(a72) % 0.54/0.72 +c1_1(a66) % 0.54/0.72 +c1_1(a46) % 0.54/0.72 +c1_1(a27) % 0.54/0.72 +c1_1(a149) % 0.54/0.72 +c1_1(a135) % 0.54/0.72 +c1_1(a114) % 0.54/0.72 +c1_1(a110) % 0.54/0.72 +c1_1(a107) % 0.54/0.72 +c1_1(a91) % 0.54/0.72 +c1_1(a85) % 0.54/0.72 +c1_1(a43) % 0.54/0.72 +c1_1(a34) % 0.54/0.72 +c1_1(a128) % 0.54/0.72 +c1_1(a96) % 0.54/0.72 +c1_1(a58) % 0.54/0.72 +c1_1(a123) % 0.54/0.72 +c1_1(a61) % 0.54/0.72 -c1_1(a139) % 0.54/0.72 -c1_1(a99) % 0.54/0.72 -c1_1(a47) % 0.54/0.72 -c1_1(a38) % 0.54/0.72 -c1_1(a145) % 0.54/0.72 -c1_1(a29) % 0.54/0.72 -c1_1(a132) % 0.54/0.72 -c1_1(a49) % 0.54/0.72 -c1_1(a122) % 0.54/0.72 -c1_1(a140) % 0.54/0.72 +c1_2(a173, a100) % 0.54/0.72 +c1_2(a173, a44) % 0.54/0.72 +c1_2(a173, a101) % 0.54/0.72 +c1_2(a173, a56) % 0.54/0.72 +c1_2(a159, a100) % 0.54/0.72 +c1_2(a125, a100) % 0.54/0.72 +c1_2(a103, a100) % 0.54/0.72 +c1_2(a103, a44) % 0.54/0.72 +c1_2(a103, a101) % 0.54/0.72 +c1_2(a72, a73) % 0.54/0.72 +c1_2(a72, a45) % 0.54/0.72 +c1_2(a72, a101) % 0.54/0.72 +c1_2(a72, a28) % 0.54/0.72 +c1_2(a70, a101) % 0.54/0.72 +c1_2(a70, a28) % 0.54/0.72 +c1_2(a66, a100) % 0.54/0.72 +c1_2(a46, a100) % 0.54/0.72 +c1_2(a27, a100) % 0.54/0.72 +c1_2(a27, a44) % 0.54/0.72 +c1_2(a27, a101) % 0.54/0.72 +c1_2(a168, a100) % 0.54/0.72 +c1_2(a168, a169) % 0.54/0.72 +c1_2(a156, a100) % 0.54/0.72 +c1_2(a149, a100) % 0.54/0.72 +c1_2(a135, a101) % 0.54/0.72 +c1_2(a135, a28) % 0.54/0.72 +c1_2(a114, a100) % 0.54/0.72 +c1_2(a110, a100) % 0.54/0.72 +c1_2(a110, a56) % 0.54/0.72 +c1_2(a107, =0) % 0.54/0.72 +c1_2(a107, a100) % 0.54/0.72 +c1_2(a107, a44) % 0.54/0.72 +c1_2(a99, a28) % 0.54/0.72 +c1_2(a91, a100) % 0.54/0.72 +c1_2(a47, =0) % 0.54/0.72 +c1_2(a47, a100) % 0.54/0.72 +c1_2(a47, a45) % 0.54/0.72 +c1_2(a47, a32) % 0.54/0.72 +c1_2(a47, a78) % 0.54/0.72 +c1_2(a43, a100) % 0.54/0.72 +c1_2(a38, a100) % 0.54/0.72 +c1_2(a121, a45) % 0.54/0.72 +c1_2(a121, a28) % 0.54/0.72 +c1_2(a90, a101) % 0.54/0.72 +c1_2(a90, a28) % 0.54/0.72 +c1_2(a87, a100) % 0.54/0.72 +c1_2(a83, a100) % 0.54/0.72 +c1_2(a83, a84) % 0.54/0.72 +c1_2(a83, a45) % 0.54/0.72 +c1_2(a34, a100) % 0.54/0.72 +c1_2(a34, a44) % 0.54/0.72 +c1_2(a34, a101) % 0.54/0.72 +c1_2(a29, a100) % 0.54/0.72 +c1_2(a80, a101) % 0.54/0.72 +c1_2(a80, a28) % 0.54/0.72 +c1_2(a128, a100) % 0.54/0.72 +c1_2(a96, a45) % 0.54/0.72 +c1_2(a96, a101) % 0.54/0.72 +c1_2(a96, a97) % 0.54/0.72 +c1_2(a96, a28) % 0.54/0.72 +c1_2(a132, a101) % 0.54/0.72 +c1_2(a132, a28) % 0.54/0.72 +c1_2(a74, a100) % 0.54/0.72 +c1_2(a74, a75) % 0.54/0.72 +c1_2(a49, =0) % 0.54/0.72 +c1_2(a49, a56) % 0.54/0.72 +c1_2(a49, a28) % 0.54/0.72 +c1_2(a58, =0) % 0.54/0.72 +c1_2(a58, a100) % 0.54/0.72 +c1_2(a123, a100) % 0.54/0.72 +c1_2(a61, a100) % 0.54/0.72 +c1_2(a61, a63) % 0.54/0.72 +c1_2(a61, a62) % 0.54/0.72 +c1_2(a93, a101) % 0.54/0.72 +c1_2(a93, a28) % 0.54/0.72 +c1_2(a122, a59) % 0.54/0.72 +c1_2(a122, a28) % 0.54/0.72 +c1_2(a140, a31) % 0.54/0.72 +c1_2(a140, a101) % 0.54/0.72 +c1_2(a140, a32) % 0.54/0.72 +c1_2(a140, a78) % 0.54/0.72 +c1_2(a140, a28) % 0.54/0.72 -c1_2(a173, a106) % 0.54/0.72 -c1_2(a159, a106) % 0.54/0.72 -c1_2(a125, a106) % 0.54/0.72 -c1_2(a103, a106) % 0.54/0.72 -c1_2(a72, a106) % 0.54/0.72 -c1_2(a66, a106) % 0.54/0.72 -c1_2(a46, a106) % 0.54/0.72 -c1_2(a27, a106) % 0.54/0.72 -c1_2(a168, a170) % 0.54/0.72 -c1_2(a149, a152) % 0.54/0.72 -c1_2(a149, a106) % 0.54/0.72 -c1_2(a135, a106) % 0.54/0.72 -c1_2(a114, a106) % 0.54/0.72 -c1_2(a110, a106) % 0.54/0.72 -c1_2(a107, a108) % 0.54/0.72 -c1_2(a107, a106) % 0.54/0.72 -c1_2(a91, a59) % 0.54/0.72 -c1_2(a91, a92) % 0.54/0.72 -c1_2(a91, a106) % 0.54/0.72 -c1_2(a85, a106) % 0.54/0.72 -c1_2(a85, a78) % 0.54/0.72 -c1_2(a43, a106) % 0.54/0.72 -c1_2(a34, a35) % 0.54/0.72 -c1_2(a34, a106) % 0.54/0.72 -c1_2(a128, a106) % 0.54/0.72 -c1_2(a96, a106) % 0.54/0.72 -c1_2(a58, a106) % 0.54/0.72 -c1_2(a123, a106) % 0.54/0.72 -c1_2(a61, a106) % 0.54/0.72 +c2_0 % 0.54/0.72 +c2_1(=0) % 0.54/0.72 +c2_1(a125) % 0.54/0.72 +c2_1(a72) % 0.54/0.72 +c2_1(a70) % 0.54/0.72 +c2_1(a66) % 0.54/0.72 +c2_1(a46) % 0.54/0.72 +c2_1(a168) % 0.54/0.72 +c2_1(a156) % 0.54/0.72 +c2_1(a149) % 0.54/0.72 +c2_1(a139) % 0.54/0.72 +c2_1(a135) % 0.54/0.72 +c2_1(a114) % 0.54/0.72 +c2_1(a110) % 0.54/0.72 +c2_1(a107) % 0.54/0.72 +c2_1(a99) % 0.54/0.72 +c2_1(a91) % 0.54/0.72 +c2_1(a85) % 0.54/0.72 +c2_1(a47) % 0.54/0.72 +c2_1(a43) % 0.54/0.72 +c2_1(a41) % 0.54/0.72 +c2_1(a38) % 0.54/0.72 +c2_1(a145) % 0.54/0.72 +c2_1(a90) % 0.54/0.72 +c2_1(a87) % 0.54/0.72 +c2_1(a83) % 0.54/0.72 +c2_1(a33) % 0.54/0.72 +c2_1(a29) % 0.54/0.72 +c2_1(a80) % 0.54/0.72 +c2_1(a128) % 0.54/0.72 +c2_1(a96) % 0.54/0.72 +c2_1(a132) % 0.54/0.72 +c2_1(a74) % 0.54/0.72 +c2_1(a123) % 0.54/0.72 +c2_1(a61) % 0.54/0.72 +c2_1(a93) % 0.54/0.72 +c2_1(a140) % 0.54/0.72 -c2_1(a173) % 0.54/0.72 -c2_1(a103) % 0.54/0.72 -c2_1(a27) % 0.54/0.72 -c2_1(a121) % 0.54/0.72 -c2_1(a34) % 0.54/0.72 -c2_1(a49) % 0.54/0.72 -c2_1(a58) % 0.54/0.72 -c2_1(a122) % 0.54/0.72 +c2_2(=0, a101) % 0.54/0.72 +c2_2(a72, a73) % 0.54/0.72 +c2_2(a156, =0) % 0.54/0.72 +c2_2(a156, a59) % 0.54/0.72 +c2_2(a156, a157) % 0.54/0.72 +c2_2(a149, a150) % 0.54/0.72 +c2_2(a114, =0) % 0.54/0.72 +c2_2(a114, a59) % 0.54/0.72 +c2_2(a107, a108) % 0.54/0.72 +c2_2(a107, a106) % 0.54/0.72 +c2_2(a91, =0) % 0.54/0.72 +c2_2(a91, a59) % 0.54/0.72 +c2_2(a85, a101) % 0.54/0.72 +c2_2(a47, =0) % 0.54/0.72 +c2_2(a47, a45) % 0.54/0.72 +c2_2(a121, a45) % 0.54/0.72 +c2_2(a121, a32) % 0.54/0.72 +c2_2(a121, a78) % 0.54/0.72 +c2_2(a87, =0) % 0.54/0.72 +c2_2(a87, a59) % 0.54/0.72 +c2_2(a87, a89) % 0.54/0.72 +c2_2(a87, a88) % 0.54/0.72 +c2_2(a83, =0) % 0.54/0.72 +c2_2(a83, a59) % 0.54/0.72 +c2_2(a83, a84) % 0.54/0.72 +c2_2(a34, a100) % 0.54/0.72 +c2_2(a34, a35) % 0.54/0.72 +c2_2(a74, a76) % 0.54/0.72 +c2_2(a49, =0) % 0.54/0.72 +c2_2(a49, a45) % 0.54/0.72 +c2_2(a49, a56) % 0.54/0.72 +c2_2(a49, a32) % 0.54/0.72 +c2_2(a49, a78) % 0.54/0.72 +c2_2(a58, a106) % 0.54/0.72 +c2_2(a122, =0) % 0.54/0.72 +c2_2(a122, a59) % 0.54/0.72 +c2_2(a122, a45) % 0.54/0.72 +c2_2(a122, a32) % 0.54/0.72 +c2_2(a122, a78) % 0.54/0.72 +c2_2(a140, a31) % 0.54/0.72 +c2_2(a140, a32) % 0.54/0.72 +c2_2(a140, a106) % 0.54/0.72 +c2_2(a140, a78) % 0.54/0.72 +c2_2(a142, =0) % 0.54/0.72 -c2_2(a173, a44) % 0.54/0.72 -c2_2(a159, a44) % 0.54/0.72 -c2_2(a103, a44) % 0.54/0.72 -c2_2(a66, a67) % 0.54/0.72 -c2_2(a46, a101) % 0.54/0.72 -c2_2(a27, a44) % 0.54/0.72 -c2_2(a168, a171) % 0.54/0.72 -c2_2(a156, a32) % 0.54/0.72 -c2_2(a156, a78) % 0.54/0.72 -c2_2(a149, a44) % 0.54/0.72 -c2_2(a149, a151) % 0.54/0.72 -c2_2(a149, a152) % 0.54/0.72 -c2_2(a114, a32) % 0.54/0.72 -c2_2(a114, a78) % 0.54/0.72 -c2_2(a110, a111) % 0.54/0.72 -c2_2(a107, a44) % 0.54/0.72 -c2_2(a99, a101) % 0.54/0.72 -c2_2(a91, a44) % 0.54/0.72 -c2_2(a91, a92) % 0.54/0.72 -c2_2(a91, a45) % 0.54/0.72 -c2_2(a91, a32) % 0.54/0.72 -c2_2(a91, a78) % 0.54/0.72 -c2_2(a87, a32) % 0.54/0.72 -c2_2(a87, a78) % 0.54/0.72 -c2_2(a83, a32) % 0.54/0.72 -c2_2(a83, a78) % 0.54/0.72 -c2_2(a34, a44) % 0.54/0.72 -c2_2(a61, a62) % 0.54/0.72 -c3_0 % 0.54/0.72 +c3_1(=0) % 0.54/0.72 +c3_1(a173) % 0.54/0.72 +c3_1(a159) % 0.54/0.72 +c3_1(a125) % 0.54/0.72 +c3_1(a103) % 0.54/0.72 +c3_1(a66) % 0.54/0.72 +c3_1(a46) % 0.54/0.72 +c3_1(a27) % 0.54/0.72 +c3_1(a168) % 0.54/0.72 +c3_1(a156) % 0.54/0.72 +c3_1(a149) % 0.54/0.72 +c3_1(a114) % 0.54/0.72 +c3_1(a110) % 0.54/0.72 +c3_1(a107) % 0.54/0.72 +c3_1(a91) % 0.54/0.72 +c3_1(a85) % 0.54/0.72 +c3_1(a47) % 0.54/0.72 +c3_1(a43) % 0.54/0.72 +c3_1(a38) % 0.54/0.72 +c3_1(a87) % 0.54/0.72 +c3_1(a83) % 0.54/0.72 +c3_1(a34) % 0.54/0.72 +c3_1(a29) % 0.54/0.72 +c3_1(a128) % 0.54/0.72 +c3_1(a74) % 0.54/0.72 +c3_1(a58) % 0.54/0.72 +c3_1(a123) % 0.54/0.72 +c3_1(a61) % 0.54/0.72 -c3_1(a72) % 0.54/0.72 -c3_1(a70) % 0.54/0.72 -c3_1(a135) % 0.54/0.72 -c3_1(a99) % 0.54/0.72 -c3_1(a121) % 0.54/0.72 -c3_1(a90) % 0.54/0.72 -c3_1(a80) % 0.54/0.72 -c3_1(a96) % 0.54/0.72 -c3_1(a132) % 0.54/0.72 -c3_1(a49) % 0.54/0.72 -c3_1(a93) % 0.54/0.72 -c3_1(a122) % 0.54/0.72 -c3_1(a140) % 0.54/0.72 +c3_2(a173, a44) % 0.54/0.72 +c3_2(a159, a44) % 0.54/0.72 +c3_2(a125, a126) % 0.54/0.72 +c3_2(a103, a44) % 0.54/0.72 +c3_2(a72, a73) % 0.54/0.72 +c3_2(a72, a45) % 0.54/0.72 +c3_2(a72, a28) % 0.54/0.72 +c3_2(a66, a67) % 0.54/0.72 +c3_2(a27, a44) % 0.54/0.72 +c3_2(a168, a170) % 0.54/0.72 +c3_2(a156, a59) % 0.54/0.72 +c3_2(a149, a44) % 0.54/0.72 +c3_2(a149, a151) % 0.54/0.72 +c3_2(a149, a150) % 0.54/0.72 +c3_2(a135, a45) % 0.54/0.72 +c3_2(a135, a28) % 0.54/0.72 +c3_2(a114, a59) % 0.54/0.72 +c3_2(a110, a111) % 0.54/0.72 +c3_2(a107, a44) % 0.54/0.72 +c3_2(a91, a59) % 0.54/0.72 +c3_2(a91, a44) % 0.54/0.72 +c3_2(a38, a39) % 0.54/0.72 +c3_2(a121, a45) % 0.54/0.72 +c3_2(a121, a28) % 0.54/0.72 +c3_2(a87, a59) % 0.54/0.72 +c3_2(a87, a89) % 0.54/0.72 +c3_2(a87, a88) % 0.54/0.72 +c3_2(a83, a59) % 0.54/0.72 +c3_2(a83, a84) % 0.54/0.72 +c3_2(a34, a44) % 0.54/0.72 +c3_2(a29, a30) % 0.54/0.72 +c3_2(a128, =0) % 0.54/0.72 +c3_2(a96, a45) % 0.54/0.72 +c3_2(a96, a101) % 0.54/0.72 +c3_2(a96, a97) % 0.54/0.72 +c3_2(a96, a28) % 0.54/0.72 +c3_2(a74, a76) % 0.54/0.72 +c3_2(a122, a59) % 0.54/0.72 -c3_2(a173, a100) % 0.54/0.72 -c3_2(a173, a174) % 0.54/0.72 -c3_2(a173, a56) % 0.54/0.72 -c3_2(a173, a78) % 0.54/0.72 -c3_2(a159, a100) % 0.54/0.72 -c3_2(a159, a78) % 0.54/0.72 -c3_2(a125, a100) % 0.54/0.72 -c3_2(a125, a78) % 0.54/0.72 -c3_2(a103, a104) % 0.54/0.72 -c3_2(a103, a100) % 0.54/0.72 -c3_2(a103, a78) % 0.54/0.72 -c3_2(a66, a100) % 0.54/0.72 -c3_2(a66, a78) % 0.54/0.72 -c3_2(a46, a100) % 0.54/0.72 -c3_2(a46, a78) % 0.54/0.72 -c3_2(a27, a100) % 0.54/0.72 -c3_2(a27, a78) % 0.54/0.72 -c3_2(a168, a100) % 0.54/0.72 -c3_2(a168, a169) % 0.54/0.72 -c3_2(a168, a171) % 0.54/0.72 -c3_2(a168, a78) % 0.54/0.72 -c3_2(a156, a100) % 0.54/0.72 -c3_2(a149, a100) % 0.54/0.72 -c3_2(a149, a78) % 0.54/0.72 -c3_2(a114, a100) % 0.54/0.72 -c3_2(a110, a100) % 0.54/0.72 -c3_2(a110, a56) % 0.54/0.72 -c3_2(a110, a78) % 0.54/0.72 -c3_2(a107, a100) % 0.54/0.72 -c3_2(a107, a78) % 0.54/0.72 -c3_2(a91, a100) % 0.54/0.72 -c3_2(a85, a101) % 0.54/0.72 -c3_2(a85, a78) % 0.54/0.72 -c3_2(a47, a100) % 0.54/0.72 -c3_2(a47, a78) % 0.54/0.72 -c3_2(a43, a100) % 0.54/0.72 -c3_2(a43, a106) % 0.54/0.72 -c3_2(a43, a78) % 0.54/0.72 -c3_2(a38, a100) % 0.54/0.72 -c3_2(a38, a78) % 0.54/0.72 -c3_2(a87, a100) % 0.54/0.72 -c3_2(a83, a100) % 0.54/0.72 -c3_2(a34, a100) % 0.54/0.72 -c3_2(a34, a78) % 0.54/0.72 -c3_2(a29, a100) % 0.54/0.72 -c3_2(a29, a78) % 0.54/0.72 -c3_2(a128, a100) % 0.54/0.72 -c3_2(a128, a106) % 0.54/0.72 -c3_2(a128, a78) % 0.54/0.72 -c3_2(a74, a100) % 0.54/0.72 -c3_2(a74, a78) % 0.54/0.72 -c3_2(a49, a56) % 0.54/0.72 -c3_2(a49, a78) % 0.54/0.72 -c3_2(a58, a100) % 0.54/0.72 -c3_2(a58, a78) % 0.54/0.72 -c3_2(a123, a100) % 0.54/0.72 -c3_2(a123, a78) % 0.54/0.72 -c3_2(a61, a100) % 0.54/0.72 -c3_2(a61, a78) % 0.54/0.72 -c3_2(a61, a64) % 0.54/0.72 +c4_0 % 0.54/0.72 +c4_1(=0) % 0.54/0.72 +c4_1(a173) % 0.54/0.72 +c4_1(a159) % 0.54/0.72 +c4_1(a125) % 0.54/0.72 +c4_1(a103) % 0.54/0.72 +c4_1(a66) % 0.54/0.72 +c4_1(a46) % 0.54/0.72 +c4_1(a27) % 0.54/0.72 +c4_1(a168) % 0.54/0.72 +c4_1(a149) % 0.54/0.72 +c4_1(a110) % 0.54/0.72 +c4_1(a107) % 0.54/0.72 +c4_1(a85) % 0.54/0.72 +c4_1(a47) % 0.54/0.72 +c4_1(a43) % 0.54/0.72 +c4_1(a38) % 0.54/0.72 +c4_1(a34) % 0.54/0.72 +c4_1(a29) % 0.54/0.72 +c4_1(a128) % 0.54/0.72 +c4_1(a74) % 0.54/0.72 +c4_1(a49) % 0.54/0.72 +c4_1(a58) % 0.54/0.72 +c4_1(a123) % 0.54/0.72 +c4_1(a61) % 0.54/0.72 -c4_1(a70) % 0.54/0.72 -c4_1(a156) % 0.54/0.72 -c4_1(a114) % 0.54/0.72 -c4_1(a99) % 0.54/0.72 -c4_1(a91) % 0.54/0.72 -c4_1(a121) % 0.54/0.72 -c4_1(a90) % 0.54/0.72 -c4_1(a87) % 0.54/0.72 -c4_1(a83) % 0.54/0.72 -c4_1(a80) % 0.54/0.72 -c4_1(a132) % 0.54/0.72 -c4_1(a122) % 0.54/0.72 -c4_1(a140) % 0.54/0.72 +c4_2(=0, a32) % 0.54/0.72 +c4_2(=0, a106) % 0.54/0.72 +c4_2(=0, a78) % 0.54/0.72 +c4_2(a173, a100) % 0.54/0.72 +c4_2(a173, a45) % 0.54/0.72 +c4_2(a173, a56) % 0.54/0.72 +c4_2(a173, a106) % 0.54/0.72 +c4_2(a173, a78) % 0.54/0.72 +c4_2(a159, a100) % 0.54/0.72 +c4_2(a159, a45) % 0.54/0.72 +c4_2(a159, a106) % 0.54/0.72 +c4_2(a159, a78) % 0.54/0.72 +c4_2(a125, a100) % 0.54/0.72 +c4_2(a125, a106) % 0.54/0.72 +c4_2(a125, a78) % 0.54/0.72 +c4_2(a103, a104) % 0.54/0.72 +c4_2(a103, a100) % 0.54/0.72 +c4_2(a103, a45) % 0.54/0.72 +c4_2(a103, a106) % 0.54/0.72 +c4_2(a103, a78) % 0.54/0.72 +c4_2(a72, a106) % 0.54/0.72 +c4_2(a66, a100) % 0.54/0.72 +c4_2(a66, a106) % 0.54/0.72 +c4_2(a66, a78) % 0.54/0.72 +c4_2(a46, a100) % 0.54/0.72 +c4_2(a46, a106) % 0.54/0.72 +c4_2(a46, a78) % 0.54/0.72 +c4_2(a27, a100) % 0.54/0.72 +c4_2(a27, a45) % 0.54/0.72 +c4_2(a27, a106) % 0.54/0.72 +c4_2(a27, a78) % 0.54/0.72 +c4_2(a168, a100) % 0.54/0.72 +c4_2(a168, a78) % 0.54/0.72 +c4_2(a156, a100) % 0.54/0.72 +c4_2(a149, a100) % 0.54/0.72 +c4_2(a149, a45) % 0.54/0.72 +c4_2(a149, a106) % 0.54/0.72 +c4_2(a149, a78) % 0.54/0.72 +c4_2(a135, a106) % 0.54/0.72 +c4_2(a114, a100) % 0.54/0.72 +c4_2(a114, a106) % 0.54/0.72 +c4_2(a110, a100) % 0.54/0.72 +c4_2(a110, a106) % 0.54/0.72 +c4_2(a110, a78) % 0.54/0.72 +c4_2(a107, a100) % 0.54/0.72 +c4_2(a107, a108) % 0.54/0.72 +c4_2(a107, a45) % 0.54/0.72 +c4_2(a107, a106) % 0.54/0.72 +c4_2(a107, a78) % 0.54/0.72 +c4_2(a91, a100) % 0.54/0.72 +c4_2(a91, a45) % 0.54/0.72 +c4_2(a91, a106) % 0.54/0.72 +c4_2(a85, a106) % 0.54/0.72 +c4_2(a85, a78) % 0.54/0.72 +c4_2(a47, a100) % 0.54/0.72 +c4_2(a47, a78) % 0.54/0.72 +c4_2(a43, a100) % 0.54/0.72 +c4_2(a43, a106) % 0.54/0.72 +c4_2(a43, a78) % 0.54/0.72 +c4_2(a38, a100) % 0.54/0.72 +c4_2(a38, a39) % 0.54/0.72 +c4_2(a38, a78) % 0.54/0.72 +c4_2(a121, a28) % 0.54/0.72 +c4_2(a87, a100) % 0.54/0.72 +c4_2(a83, a100) % 0.54/0.72 +c4_2(a34, a100) % 0.54/0.72 +c4_2(a34, a35) % 0.54/0.72 +c4_2(a34, a45) % 0.54/0.72 +c4_2(a34, a106) % 0.54/0.72 +c4_2(a34, a78) % 0.54/0.72 +c4_2(a29, a100) % 0.54/0.72 +c4_2(a29, a78) % 0.54/0.72 +c4_2(a128, a100) % 0.54/0.72 +c4_2(a128, a106) % 0.54/0.72 +c4_2(a128, a78) % 0.54/0.72 +c4_2(a96, a106) % 0.54/0.72 +c4_2(a74, a100) % 0.54/0.72 +c4_2(a74, a78) % 0.54/0.72 +c4_2(a49, a78) % 0.54/0.72 +c4_2(a58, a100) % 0.54/0.72 +c4_2(a58, a106) % 0.54/0.72 +c4_2(a58, a78) % 0.54/0.72 +c4_2(a123, a100) % 0.54/0.72 +c4_2(a123, a106) % 0.54/0.72 +c4_2(a123, a78) % 0.54/0.72 +c4_2(a61, a100) % 0.54/0.72 +c4_2(a61, a106) % 0.54/0.72 +c4_2(a61, a78) % 0.54/0.72 +c4_2(a61, a62) % 0.54/0.72 +c4_2(a122, a59) % 0.54/0.72 -c4_2(a173, a44) % 0.54/0.72 -c4_2(a159, a44) % 0.54/0.72 -c4_2(a125, a126) % 0.54/0.72 -c4_2(a103, a44) % 0.54/0.72 -c4_2(a72, a73) % 0.54/0.72 -c4_2(a27, a44) % 0.54/0.72 -c4_2(a168, a169) % 0.54/0.72 -c4_2(a149, a44) % 0.54/0.72 -c4_2(a149, a150) % 0.54/0.72 -c4_2(a149, a152) % 0.54/0.72 -c4_2(a107, a44) % 0.54/0.72 -c4_2(a91, a44) % 0.54/0.72 -c4_2(a91, a92) % 0.54/0.72 -c4_2(a87, a89) % 0.54/0.72 -c4_2(a87, a88) % 0.54/0.72 -c4_2(a34, a44) % 0.54/0.72 -c4_2(a61, a63) % 0.54/0.72 -c4_2(a61, a64) % 0.54/0.72 -c4_2(a140, a31) % 0.54/0.72 -c4_2(a140, a32) % 0.54/0.72 -c4_2(a140, a78) % 0.54/0.72 +c5_0 % 0.54/0.72 +c5_1(=0) % 0.54/0.72 +c5_1(a159) % 0.54/0.72 +c5_1(a125) % 0.54/0.72 +c5_1(a103) % 0.54/0.72 +c5_1(a66) % 0.54/0.72 +c5_1(a46) % 0.54/0.72 +c5_1(a27) % 0.54/0.72 +c5_1(a168) % 0.54/0.72 +c5_1(a149) % 0.54/0.72 +c5_1(a135) % 0.54/0.72 +c5_1(a107) % 0.54/0.72 +c5_1(a91) % 0.54/0.72 +c5_1(a85) % 0.54/0.72 +c5_1(a47) % 0.54/0.72 +c5_1(a43) % 0.54/0.72 +c5_1(a41) % 0.54/0.72 +c5_1(a38) % 0.54/0.72 +c5_1(a34) % 0.54/0.72 +c5_1(a33) % 0.54/0.72 +c5_1(a29) % 0.54/0.72 +c5_1(a128) % 0.54/0.72 +c5_1(a74) % 0.54/0.72 +c5_1(a58) % 0.54/0.72 +c5_1(a94) % 0.54/0.72 +c5_1(a123) % 0.54/0.72 +c5_1(a61) % 0.54/0.72 -c5_1(a173) % 0.54/0.72 -c5_1(a70) % 0.54/0.72 -c5_1(a114) % 0.54/0.72 -c5_1(a110) % 0.54/0.72 -c5_1(a99) % 0.54/0.72 -c5_1(a121) % 0.54/0.72 -c5_1(a80) % 0.54/0.72 -c5_1(a132) % 0.54/0.72 -c5_1(a49) % 0.54/0.72 -c5_1(a122) % 0.54/0.72 -c5_1(a140) % 0.54/0.72 +c5_2(=0, a45) % 0.54/0.72 +c5_2(=0, a32) % 0.54/0.72 +c5_2(=0, a78) % 0.54/0.72 +c5_2(a173, a44) % 0.54/0.72 +c5_2(a173, a56) % 0.54/0.72 +c5_2(a173, a78) % 0.54/0.72 +c5_2(a159, a78) % 0.54/0.72 +c5_2(a125, a78) % 0.54/0.72 +c5_2(a103, a44) % 0.54/0.72 +c5_2(a103, a78) % 0.54/0.72 +c5_2(a66, a67) % 0.54/0.72 +c5_2(a66, a78) % 0.54/0.72 +c5_2(a46, a78) % 0.54/0.72 +c5_2(a27, a44) % 0.54/0.72 +c5_2(a27, a78) % 0.54/0.72 +c5_2(a168, a170) % 0.54/0.72 +c5_2(a168, a78) % 0.54/0.72 +c5_2(a149, a78) % 0.54/0.72 +c5_2(a110, a56) % 0.54/0.72 +c5_2(a110, a78) % 0.54/0.72 +c5_2(a107, a78) % 0.54/0.72 +c5_2(a91, a44) % 0.54/0.72 +c5_2(a91, a92) % 0.54/0.72 +c5_2(a85, a78) % 0.54/0.72 +c5_2(a47, a78) % 0.54/0.72 +c5_2(a43, a78) % 0.54/0.72 +c5_2(a38, a78) % 0.54/0.72 +c5_2(a87, a88) % 0.54/0.72 +c5_2(a34, a44) % 0.54/0.72 +c5_2(a34, a35) % 0.54/0.72 +c5_2(a34, a78) % 0.54/0.72 +c5_2(a29, a78) % 0.54/0.72 +c5_2(a128, a78) % 0.54/0.72 +c5_2(a74, a78) % 0.54/0.72 +c5_2(a49, a56) % 0.54/0.72 +c5_2(a49, a78) % 0.54/0.72 +c5_2(a58, a78) % 0.54/0.72 +c5_2(a123, a78) % 0.54/0.72 +c5_2(a61, a78) % 0.54/0.72 -c5_2(a173, a174) % 0.54/0.72 -c5_2(a156, a157) % 0.54/0.72 -c5_2(a149, a151) % 0.54/0.72 -c5_2(a110, a111) % 0.54/0.72 -c5_2(a85, a101) % 0.54/0.72 -c5_2(a38, a39) % 0.54/0.72 -c5_2(a29, a30) % 0.54/0.72 -c5_2(a96, a97) % 0.54/0.72 -c5_2(a61, a63) % 0.54/0.72 -c5_2(a140, a31) % 0.54/0.72 +ndr1_0 % 0.54/0.72 +ndr1_1(=0) % 0.54/0.72 +ndr1_1(a173) % 0.54/0.72 +ndr1_1(a159) % 0.54/0.72 +ndr1_1(a125) % 0.54/0.72 +ndr1_1(a103) % 0.54/0.72 +ndr1_1(a72) % 0.54/0.72 +ndr1_1(a70) % 0.54/0.72 +ndr1_1(a66) % 0.54/0.72 +ndr1_1(a46) % 0.54/0.72 +ndr1_1(a27) % 0.54/0.72 +ndr1_1(a168) % 0.54/0.72 +ndr1_1(a156) % 0.54/0.72 +ndr1_1(a149) % 0.54/0.72 +ndr1_1(a135) % 0.54/0.72 +ndr1_1(a114) % 0.54/0.72 +ndr1_1(a110) % 0.54/0.72 +ndr1_1(a107) % 0.54/0.72 +ndr1_1(a99) % 0.54/0.72 +ndr1_1(a91) % 0.54/0.72 +ndr1_1(a85) % 0.54/0.72 +ndr1_1(a47) % 0.54/0.72 +ndr1_1(a43) % 0.54/0.72 +ndr1_1(a38) % 0.54/0.72 +ndr1_1(a121) % 0.54/0.72 +ndr1_1(a90) % 0.54/0.72 +ndr1_1(a87) % 0.54/0.72 +ndr1_1(a83) % 0.54/0.72 +ndr1_1(a34) % 0.54/0.72 +ndr1_1(a29) % 0.54/0.72 +ndr1_1(a80) % 0.54/0.72 +ndr1_1(a128) % 0.54/0.72 +ndr1_1(a96) % 0.54/0.72 +ndr1_1(a132) % 0.54/0.72 +ndr1_1(a74) % 0.54/0.72 +ndr1_1(a49) % 0.54/0.72 +ndr1_1(a58) % 0.54/0.72 +ndr1_1(a123) % 0.54/0.72 +ndr1_1(a61) % 0.54/0.72 +ndr1_1(a93) % 0.54/0.72 +ndr1_1(a122) % 0.54/0.72 +ndr1_1(a140) % 0.54/0.72 +ndr1_1(a142) % 0.54/0.72 +ssSkC0 % 0.54/0.72 +ssSkC1 % 0.54/0.72 +ssSkC10 % 0.54/0.72 +ssSkC11 % 0.54/0.72 +ssSkC12 % 0.54/0.72 +ssSkC13 % 0.54/0.72 +ssSkC14 % 0.54/0.72 +ssSkC15 % 0.54/0.72 +ssSkC16 % 0.54/0.72 +ssSkC17 % 0.54/0.72 +ssSkC18 % 0.54/0.72 +ssSkC19 % 0.54/0.72 +ssSkC2 % 0.54/0.72 +ssSkC20 % 0.54/0.72 +ssSkC21 % 0.54/0.72 +ssSkC22 % 0.54/0.72 +ssSkC23 % 0.54/0.72 +ssSkC24 % 0.54/0.72 +ssSkC25 % 0.54/0.72 +ssSkC26 % 0.54/0.72 +ssSkC28 % 0.54/0.72 +ssSkC29 % 0.54/0.72 +ssSkC3 % 0.54/0.72 +ssSkC30 % 0.54/0.72 +ssSkC31 % 0.54/0.72 +ssSkC32 % 0.54/0.72 +ssSkC33 % 0.54/0.72 +ssSkC34 % 0.54/0.72 +ssSkC35 % 0.54/0.72 +ssSkC36 % 0.54/0.72 +ssSkC37 % 0.54/0.72 +ssSkC38 % 0.54/0.72 +ssSkC39 % 0.54/0.72 +ssSkC4 % 0.54/0.72 +ssSkC40 % 0.54/0.72 +ssSkC41 % 0.54/0.72 +ssSkC42 % 0.54/0.72 +ssSkC43 % 0.54/0.72 +ssSkC44 % 0.54/0.72 +ssSkC45 % 0.54/0.72 +ssSkC5 % 0.54/0.72 +ssSkC6 % 0.54/0.72 +ssSkC7 % 0.54/0.72 +ssSkC8 % 0.54/0.72 +ssSkC9 % 0.54/0.72 +ssSkP0(_0) % 0.54/0.72 +ssSkP1(a156) % 0.54/0.72 +ssSkP1(a114) % 0.54/0.72 +ssSkP1(a91) % 0.54/0.72 +ssSkP1(a47) % 0.54/0.72 +ssSkP1(a87) % 0.54/0.72 +ssSkP1(a83) % 0.54/0.72 +ssSkP1(a49) % 0.54/0.72 +ssSkP1(a122) % 0.54/0.72 +ssSkP1(a142) % 0.54/0.72 +ssSkP2(=0) % 0.54/0.72 -ssSkP2(a140) % 0.54/0.72 +ssSkP3(=0) % 0.54/0.72 -ssSkP3(a173) % 0.54/0.72 -ssSkP3(a159) % 0.54/0.72 -ssSkP3(a103) % 0.54/0.72 -ssSkP3(a27) % 0.54/0.72 -ssSkP3(a149) % 0.54/0.72 -ssSkP3(a107) % 0.54/0.72 -ssSkP3(a91) % 0.54/0.72 -ssSkP3(a34) % 0.54/0.72 +ssSkP4(=0) % 0.54/0.72 -ssSkP4(a156) % 0.54/0.72 -ssSkP4(a114) % 0.54/0.72 -ssSkP4(a91) % 0.54/0.72 -ssSkP4(a87) % 0.54/0.72 -ssSkP4(a83) % 0.54/0.72 -ssSkP4(a122) % 0.54/0.72 +ssSkP5(=0) % 0.54/0.72 +ssSkP6(=0) % 0.54/0.72 +ssSkP7(=0) % 0.54/0.72 +ssSkP7(a85) % 0.54/0.72 -ssSkP7(a173) % 0.54/0.72 -ssSkP7(a159) % 0.54/0.72 -ssSkP7(a125) % 0.54/0.72 -ssSkP7(a103) % 0.54/0.72 -ssSkP7(a66) % 0.54/0.72 -ssSkP7(a46) % 0.54/0.72 -ssSkP7(a27) % 0.54/0.72 -ssSkP7(a168) % 0.54/0.72 -ssSkP7(a156) % 0.54/0.72 -ssSkP7(a149) % 0.54/0.72 -ssSkP7(a114) % 0.54/0.72 -ssSkP7(a110) % 0.54/0.72 -ssSkP7(a107) % 0.54/0.72 -ssSkP7(a91) % 0.54/0.72 -ssSkP7(a47) % 0.54/0.72 -ssSkP7(a43) % 0.54/0.72 -ssSkP7(a38) % 0.54/0.72 -ssSkP7(a87) % 0.54/0.72 -ssSkP7(a83) % 0.54/0.72 -ssSkP7(a34) % 0.54/0.72 -ssSkP7(a29) % 0.54/0.72 -ssSkP7(a128) % 0.54/0.72 -ssSkP7(a74) % 0.54/0.72 -ssSkP7(a58) % 0.54/0.72 -ssSkP7(a123) % 0.54/0.72 -ssSkP7(a61) % 0.54/0.72 +ssSkP8(=0) % 0.54/0.72 +ssSkP9(=0) % 0.54/0.72 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------