%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN522-1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n003.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 : 600s % DateTime : Thu Jul 21 09:03:36 EDT 2022 % Result : Satisfiable 0.20s 0.41s % Output : Saturation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN522-1 : TPTP v8.1.0. Released v2.1.0. % 0.12/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n003.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 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 12 08:31:00 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.20/0.41 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.41 % 0.20/0.41 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.41 |- c4_0 % 0.20/0.41 |- c1_0 \/ c5_1 a118 % 0.20/0.41 |- c1_0 \/ c1_1 a118 % 0.20/0.41 |- ndr1_1 $U \/ ssSkP4 $U % 0.20/0.41 |- ndr1_1 a128 \/ ssSkC5 % 0.20/0.41 |- c3_1 a128 \/ ssSkC5 % 0.20/0.41 |- ndr1_1 a125 \/ ssSkC4 % 0.20/0.41 |- ndr1_1 $U \/ ssSkP3 $U % 0.20/0.41 |- ndr1_1 $U \/ ssSkP2 $U % 0.20/0.41 |- ndr1_1 $U \/ ssSkP1 $U % 0.20/0.41 |- c3_1 a109 \/ ssSkC2 % 0.20/0.41 |- ndr1_1 a106 \/ ssSkC1 % 0.20/0.41 |- ndr1_1 $U \/ ssSkP0 $U % 0.20/0.41 |- ~c1_0 \/ ndr1_1 a121 % 0.20/0.41 |- ~c2_1 a118 \/ c1_0 % 0.20/0.41 |- ~c1_1 a114 \/ c2_0 % 0.20/0.41 |- ~ssSkC0 \/ ~ssSkC1 \/ c3_1 a108 % 0.20/0.41 |- ~c2_1 a134 \/ ssSkC7 % 0.20/0.41 |- c4_2 a128 a129 \/ ssSkC5 % 0.20/0.41 |- c2_2 a128 a129 \/ ssSkC5 % 0.20/0.41 |- ~c2_1 a128 \/ ssSkC5 % 0.20/0.41 |- c1_2 a125 a126 \/ ssSkC4 % 0.20/0.41 |- ~c4_1 a125 \/ ssSkC4 % 0.20/0.41 |- c4_2 $U a119 \/ ssSkP3 $U % 0.20/0.41 |- c5_2 $U a116 \/ ssSkP2 $U % 0.20/0.41 |- c1_2 $U a116 \/ ssSkP2 $U % 0.20/0.41 |- c2_2 $U a115 \/ ssSkP1 $U % 0.20/0.41 |- c5_2 $U a115 \/ ssSkP1 $U % 0.20/0.41 |- ~c1_1 a109 \/ ssSkC2 % 0.20/0.41 |- c1_2 a106 a107 \/ ssSkC1 % 0.20/0.41 |- c4_2 a106 a107 \/ ssSkC1 % 0.20/0.41 |- c2_2 a106 a107 \/ ssSkC1 % 0.20/0.41 |- ~c5_1 a106 \/ ssSkC1 % 0.20/0.41 |- c4_2 $U a104 \/ ssSkP0 $U % 0.20/0.41 |- c3_2 $U a104 \/ ssSkP0 $U % 0.20/0.41 |- ~c5_1 a133 \/ ~ssSkC6 \/ c2_0 % 0.20/0.41 |- ~c2_1 a133 \/ ~ssSkC6 \/ c2_0 % 0.20/0.41 |- ~c1_1 a130 \/ ~ssSkC4 \/ ~ssSkC5 % 0.20/0.41 |- ~c1_0 \/ c3_2 a121 a122 % 0.20/0.41 |- ~c1_0 \/ ~ssSkC3 \/ ndr1_1 a112 % 0.20/0.41 |- ~c4_1 a108 \/ ~ssSkC0 \/ ~ssSkC1 % 0.20/0.41 |- ~c1_0 \/ ~c5_0 \/ c3_0 % 0.20/0.41 |- ~c4_2 $U a131 \/ ssSkP4 $U % 0.20/0.41 |- ~c1_2 $U a131 \/ ssSkP4 $U % 0.20/0.41 |- ~c1_2 a128 a129 \/ ssSkC5 % 0.20/0.41 |- ~c4_2 a125 a127 \/ ssSkC4 % 0.20/0.41 |- ~c3_2 a125 a127 \/ ssSkC4 % 0.20/0.41 |- ~c2_2 a125 a127 \/ ssSkC4 % 0.20/0.41 |- ~c3_2 a125 a126 \/ ssSkC4 % 0.20/0.41 |- ~c5_2 a125 a126 \/ ssSkC4 % 0.20/0.41 |- ~c3_2 $U a119 \/ ssSkP3 $U % 0.20/0.41 |- ~c2_2 $U a119 \/ ssSkP3 $U % 0.20/0.41 |- ~c2_2 $U a116 \/ ssSkP2 $U % 0.20/0.41 |- ~c4_2 $U a115 \/ ssSkP1 $U % 0.20/0.41 |- ~c1_2 $U a104 \/ ssSkP0 $U % 0.20/0.41 |- ~c3_0 \/ c4_1 a137 % 0.20/0.41 |- ~c3_0 \/ c1_1 a137 % 0.20/0.41 |- ~c1_0 \/ ~c2_2 a121 a122 % 0.20/0.41 |- ~c1_0 \/ ~ssSkC3 \/ c2_2 a112 a113 % 0.20/0.41 |- ~c1_0 \/ ~c5_2 a112 a113 \/ ~ssSkC3 % 0.20/0.41 |- ~c1_0 \/ ~c3_2 a112 a113 \/ ~ssSkC3 % 0.20/0.41 |- ~ssSkP4 $U \/ c2_2 $U a132 \/ c5_1 $U \/ ssSkC6 % 0.20/0.41 |- ~ssSkP4 $U \/ c5_1 $U \/ c5_2 $U a132 \/ ssSkC6 % 0.20/0.41 |- ~ssSkP4 $U \/ c1_2 $U a132 \/ c5_1 $U \/ ssSkC6 % 0.20/0.41 |- ~ndr1_1 a130 \/ ~ssSkC4 \/ ~ssSkC5 \/ c2_2 a130 $U \/ c5_2 a130 $U % 0.20/0.41 |- ~c3_2 a114 $U \/ ~ndr1_1 a114 \/ c2_0 \/ c5_2 a114 $U % 0.20/0.41 |- ~ssSkP3 $U \/ c2_2 $U a120 \/ c3_0 \/ c4_1 $U % 0.20/0.41 |- ~ssSkP3 $U \/ c3_0 \/ c4_1 $U \/ c5_2 $U a120 % 0.20/0.41 |- ~c1_0 \/ ~ndr1_1 a112 \/ ~ssSkC3 \/ c1_2 a112 $U \/ c5_2 a112 $U % 0.20/0.41 |- ~c1_2 $U a120 \/ ~ssSkP3 $U \/ c3_0 \/ c4_1 $U % 0.20/0.41 |- ~ndr1_1 a114 \/ c1_2 a114 $U \/ c2_0 \/ c4_2 a114 $U \/ c5_2 a114 $U % 0.20/0.41 |- ~ndr1_1 a108 \/ ~ssSkC0 \/ ~ssSkC1 \/ c1_2 a108 $U \/ c2_2 a108 $U \/ % 0.20/0.41 c4_2 a108 $U % 0.20/0.41 |- ~c5_2 a134 $U \/ ~ndr1_1 a134 \/ c1_2 a134 $U \/ c4_2 a134 $U \/ ssSkC7 % 0.20/0.41 |- ~c3_0 \/ ~c4_1 $V \/ ~ssSkP1 $U \/ ~ssSkP2 $U \/ c2_1 $V \/ c4_2 $U a117 % 0.20/0.41 |- ~c3_0 \/ ~c4_1 $V \/ ~ssSkP1 $U \/ ~ssSkP2 $U \/ c2_1 $V \/ c3_2 $U a117 % 0.20/0.41 |- ~c1_0 \/ ~c1_2 a121 $U \/ ~c4_2 a121 $U \/ ~ndr1_1 a121 \/ c3_2 a121 $U % 0.20/0.41 |- ~c1_0 \/ ~c1_2 a121 $U \/ ~c5_2 a121 $U \/ ~ndr1_1 a121 \/ c3_2 a121 $U % 0.20/0.41 |- ~c3_0 \/ ~c4_1 $V \/ ~c5_2 $U a117 \/ ~ssSkP1 $U \/ ~ssSkP2 $U \/ % 0.20/0.41 c2_1 $V % 0.20/0.41 |- ~c1_2 a134 $U \/ ~c2_2 a134 $U \/ ~c3_2 a134 $U \/ ~ndr1_1 a134 \/ % 0.20/0.41 ssSkC7 % 0.20/0.41 |- ~c2_2 a130 $U \/ ~c3_2 a130 $U \/ ~c4_2 a130 $U \/ ~ndr1_1 a130 \/ % 0.20/0.41 ~ssSkC4 \/ ~ssSkC5 % 0.20/0.41 |- ~c1_0 \/ ~c3_1 $U \/ ~c4_1 $U \/ ~ndr1_1 $U \/ c4_2 $U $V \/ c5_0 \/ % 0.20/0.41 c5_2 $U $V % 0.20/0.41 |- ~c5_2 $U $V \/ ~ndr1_1 $U \/ ~ssSkP0 $U \/ c2_2 $U $V \/ c2_2 $U a105 \/ % 0.20/0.41 c3_2 $U $V \/ ssSkC0 % 0.20/0.41 |- ~c2_2 $U $V \/ ~c4_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c4_2 $U $V \/ % 0.20/0.41 c5_2 $U a111 \/ ssSkC3 % 0.20/0.41 |- ~c2_2 $U $V \/ ~c4_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_2 $U a111 \/ % 0.20/0.41 c4_2 $U $V \/ ssSkC3 % 0.20/0.42 |- ~c4_2 $U a105 \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ ~ssSkP0 $U \/ % 0.20/0.42 c2_2 $U $V \/ c3_2 $U $V \/ ssSkC0 % 0.20/0.42 |- ~c3_2 $U a105 \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ ~ssSkP0 $U \/ % 0.20/0.42 c2_2 $U $V \/ c3_2 $U $V \/ ssSkC0 % 0.20/0.42 |- ~c4_1 $U \/ ~c5_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_2 $U $V \/ % 0.20/0.42 c3_0 \/ c3_2 $U $V \/ ndr1_1 a139 % 0.20/0.42 |- ~c2_0 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_2 $U $V \/ c5_1 $U \/ % 0.20/0.42 c5_2 $U $V \/ c5_2 $U a138 % 0.20/0.42 |- ~c2_2 $U $V \/ ~c3_2 $U a111 \/ ~c4_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ % 0.20/0.42 c4_2 $U $V \/ ssSkC3 % 0.20/0.42 |- ~c4_1 $U \/ ~c5_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_2 $U $V \/ % 0.20/0.42 c2_2 a139 a140 \/ c3_0 \/ c3_2 $U $V % 0.20/0.42 |- ~c4_1 $U \/ ~c5_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c1_2 a139 a140 \/ % 0.20/0.42 c2_2 $U $V \/ c3_0 \/ c3_2 $U $V % 0.20/0.42 |- ~c4_1 $U \/ ~c5_1 $U \/ ~c5_1 a139 \/ ~ndr1_1 $U \/ c1_2 $U $V \/ % 0.20/0.42 c2_2 $U $V \/ c3_0 \/ c3_2 $U $V % 0.20/0.42 |- ~c2_0 \/ ~c4_2 $U a138 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_2 $U $V \/ % 0.20/0.42 c5_1 $U \/ c5_2 $U $V % 0.20/0.42 |- ~c4_1 $U \/ ~c4_2 a139 a140 \/ ~c5_1 $U \/ ~ndr1_1 $U \/ c1_2 $U $V \/ % 0.20/0.42 c2_2 $U $V \/ c3_0 \/ c3_2 $U $V % 0.20/0.42 |- ~c1_2 $U $V \/ ~c3_1 $U \/ ~c3_2 $U $V \/ ~c4_1 a110 \/ ~c5_1 $U \/ % 0.20/0.42 ~c5_2 $U $V \/ ~ndr1_1 $U \/ ~ssSkC2 % 0.20/0.42 |- ~c1_2 $U $V \/ ~c3_1 $U \/ ~c3_1 a110 \/ ~c3_2 $U $V \/ ~c5_1 $U \/ % 0.20/0.42 ~c5_2 $U $V \/ ~ndr1_1 $U \/ ~ssSkC2 % 0.20/0.42 |- ~c1_2 $U $V \/ ~c3_1 $U \/ ~c3_2 $U $V \/ ~c5_1 $U \/ ~c5_2 $U $V \/ % 0.20/0.42 ~ndr1_1 $U \/ ~ndr1_1 a110 \/ ~ssSkC2 \/ c1_2 a110 $W \/ c5_2 a110 $W % 0.20/0.42 |- ndr1_0 % 0.20/0.42 |- ~ndr1_1 a114 \/ c2_0 \/ c5_2 a114 a104 \/ ssSkP0 a114 % 0.20/0.42 |- c3_0 \/ c4_1 $_20 \/ ndr1_1 $_20 % 0.20/0.42 |- c2_0 \/ c3_0 \/ c4_1 a114 \/ c5_2 a114 a104 \/ ssSkP0 a114 % 0.20/0.42 |- c5_1 $_23 \/ ndr1_1 $_23 \/ ssSkC6 % 0.20/0.42 |- c2_0 \/ c5_1 a114 \/ c5_2 a114 a104 \/ ssSkC6 \/ ssSkP0 a114 % 0.20/0.42 |- ~c1_0 \/ ~ssSkC3 \/ c1_2 a112 $_25 \/ c5_1 a112 \/ c5_2 a112 $_25 \/ % 0.20/0.42 ssSkC6 % 0.20/0.42 |- ~c1_0 \/ ~ssSkC3 \/ c1_2 a112 $_25 \/ c3_0 \/ c4_1 a112 \/ % 0.20/0.42 c5_2 a112 $_25 % 0.20/0.42 |- ~ssSkC4 \/ ~ssSkC5 \/ c2_2 a130 $_31 \/ c5_1 a130 \/ c5_2 a130 $_31 \/ % 0.20/0.42 ssSkC6 % 0.20/0.42 |- ~ssSkC4 \/ ~ssSkC5 \/ c2_2 a130 $_31 \/ c3_0 \/ c4_1 a130 \/ % 0.20/0.42 c5_2 a130 $_31 % 0.20/0.42 |- ~c1_0 \/ ~c1_2 a121 a115 \/ ~ndr1_1 a121 \/ c3_2 a121 a115 \/ % 0.20/0.42 ssSkP1 a121 % 0.20/0.42 |- ~c1_0 \/ ~ndr1_1 a121 \/ c3_2 a121 a116 \/ ssSkP2 a121 % 0.20/0.42 |- ~c1_0 \/ c3_2 a121 a116 \/ c5_1 a121 \/ ssSkC6 \/ ssSkP2 a121 % 0.20/0.42 |- ~c1_0 \/ c3_0 \/ c3_2 a121 a116 \/ c4_1 a121 \/ ssSkP2 a121 % 0.20/0.42 |- c1_2 a114 $_33 \/ c2_0 \/ c4_2 a114 $_33 \/ c5_1 a114 \/ % 0.20/0.42 c5_2 a114 $_33 \/ ssSkC6 % 0.20/0.42 |- c1_2 a114 $_33 \/ c2_0 \/ c3_0 \/ c4_1 a114 \/ c4_2 a114 $_33 \/ % 0.20/0.42 c5_2 a114 $_33 % 0.20/0.42 |- ~ndr1_1 a134 \/ c1_2 a134 a115 \/ c4_2 a134 a115 \/ ssSkC7 \/ % 0.20/0.42 ssSkP1 a134 % 0.20/0.42 |- c1_2 a134 a115 \/ c5_1 a134 \/ ssSkC6 \/ ssSkC7 \/ ssSkP1 a134 % 0.20/0.42 |- c1_2 a134 a115 \/ c3_0 \/ c4_1 a134 \/ ssSkC7 \/ ssSkP1 a134 % 0.20/0.42 |- ~c1_0 \/ ~c1_2 a121 a119 \/ ~ndr1_1 a121 \/ c3_2 a121 a119 \/ % 0.20/0.42 ssSkP3 a121 % 0.20/0.42 |- ~ssSkC0 \/ ~ssSkC1 \/ c1_2 a108 $_41 \/ c2_2 a108 $_41 \/ % 0.20/0.42 c4_2 a108 $_41 \/ c5_1 a108 \/ ssSkC6 % 0.20/0.42 |- ~ssSkC0 \/ ~ssSkC1 \/ c1_2 a108 $_41 \/ c2_2 a108 $_41 \/ c3_0 \/ % 0.20/0.42 c4_1 a108 \/ c4_2 a108 $_41 % 0.20/0.42 |- ~c2_2 a130 a104 \/ ~ndr1_1 a130 \/ ~ssSkC4 \/ ~ssSkC5 \/ ssSkP0 a130 % 0.20/0.42 |- ~c3_0 \/ ~c4_1 $_50 \/ c2_1 $_50 \/ ndr1_1 $_49 % 0.20/0.42 |- ~c1_0 \/ ~c3_1 a106 \/ ~c4_1 a106 \/ c4_2 a106 $_60 \/ c5_0 \/ % 0.20/0.42 c5_2 a106 $_60 \/ ssSkC1 % 0.20/0.42 |- ~c1_0 \/ ~c3_1 a128 \/ ~c4_1 a128 \/ c4_2 a128 $_60 \/ c5_0 \/ % 0.20/0.42 c5_2 a128 $_60 \/ ssSkC5 % 0.20/0.42 |- ~c1_0 \/ ~c3_1 $_59 \/ ~c4_1 $_59 \/ c4_2 $_59 $_60 \/ c5_0 \/ % 0.20/0.42 c5_1 $_59 \/ c5_2 $_59 $_60 \/ ssSkC6 % 0.20/0.42 |- ~ndr1_1 a114 \/ ~ssSkP0 a114 \/ c1_2 a114 $_64 \/ c2_0 \/ % 0.20/0.42 c2_2 a114 $_64 \/ c2_2 a114 a105 \/ c3_0 \/ c3_2 a114 $_64 \/ % 0.20/0.42 c4_1 a114 \/ c4_2 a114 $_64 \/ ssSkC0 % 0.20/0.42 |- ~ndr1_1 a114 \/ ~ssSkP0 a114 \/ c1_2 a114 $_64 \/ c2_0 \/ % 0.20/0.42 c2_2 a114 $_64 \/ c2_2 a114 a105 \/ c3_2 a114 $_64 \/ c4_2 a114 $_64 \/ % 0.20/0.42 c5_1 a114 \/ ssSkC0 \/ ssSkC6 % 0.20/0.42 |- ~ndr1_1 $_63 \/ ~ssSkP0 $_63 \/ c2_2 $_63 a105 \/ c2_2 $_63 a116 \/ % 0.20/0.42 c3_2 $_63 a116 \/ ssSkC0 \/ ssSkP2 $_63 % 0.20/0.42 |- ~c4_1 $_66 \/ ~ndr1_1 $_66 \/ c1_2 $_66 a115 \/ c4_2 $_66 a115 \/ % 0.20/0.42 c5_2 $_66 a111 \/ ssSkC3 \/ ssSkP1 $_66 % 0.20/0.42 |- ~c4_1 a106 \/ c1_2 a106 a115 \/ c4_2 a106 a115 \/ c5_2 a106 a111 \/ % 0.20/0.42 ssSkC1 \/ ssSkC3 \/ ssSkP1 a106 % 0.20/0.42 |- ~c4_1 a128 \/ c1_2 a128 a115 \/ c4_2 a128 a115 \/ c5_2 a128 a111 \/ % 0.20/0.42 ssSkC3 \/ ssSkC5 \/ ssSkP1 a128 % 0.20/0.42 |- ~c4_1 $_68 \/ c1_2 $_68 a115 \/ c4_2 $_68 a115 \/ c5_1 $_68 \/ % 0.20/0.42 c5_2 $_68 a111 \/ ssSkC3 \/ ssSkC6 \/ ssSkP1 $_68 % 0.20/0.42 |- ~c4_1 $_70 \/ ~ndr1_1 $_70 \/ c1_2 $_70 a115 \/ c2_2 $_70 a111 \/ % 0.20/0.42 c4_2 $_70 a115 \/ ssSkC3 \/ ssSkP1 $_70 % 0.20/0.42 |- ~c4_1 a106 \/ c1_2 a106 a115 \/ c2_2 a106 a111 \/ c4_2 a106 a115 \/ % 0.20/0.42 ssSkC1 \/ ssSkC3 \/ ssSkP1 a106 % 0.20/0.42 |- ~c4_1 a128 \/ c1_2 a128 a115 \/ c2_2 a128 a111 \/ c4_2 a128 a115 \/ % 0.20/0.42 ssSkC3 \/ ssSkC5 \/ ssSkP1 a128 % 0.20/0.42 |- ~c4_1 $_72 \/ c1_2 $_72 a115 \/ c2_2 $_72 a111 \/ c4_2 $_72 a115 \/ % 0.20/0.42 c5_1 $_72 \/ ssSkC3 \/ ssSkC6 \/ ssSkP1 $_72 % 0.20/0.42 |- ~c4_2 a114 a105 \/ ~ndr1_1 a114 \/ ~ssSkP0 a114 \/ c1_2 a114 $_75 \/ % 0.20/0.42 c2_0 \/ c2_2 a114 $_75 \/ c3_0 \/ c3_2 a114 $_75 \/ c4_1 a114 \/ % 0.20/0.42 c4_2 a114 $_75 \/ ssSkC0 % 0.20/0.42 |- ~c4_2 a114 a105 \/ ~ndr1_1 a114 \/ ~ssSkP0 a114 \/ c1_2 a114 $_75 \/ % 0.20/0.42 c2_0 \/ c2_2 a114 $_75 \/ c3_2 a114 $_75 \/ c4_2 a114 $_75 \/ % 0.20/0.42 c5_1 a114 \/ ssSkC0 \/ ssSkC6 % 0.20/0.42 |- ~c4_2 $_74 a105 \/ ~ndr1_1 $_74 \/ ~ssSkP0 $_74 \/ c2_2 $_74 a116 \/ % 0.20/0.42 c3_2 $_74 a116 \/ ssSkC0 \/ ssSkP2 $_74 % 0.20/0.42 |- ~c3_2 a114 a105 \/ ~ndr1_1 a114 \/ ~ssSkP0 a114 \/ c1_2 a114 $_78 \/ % 0.20/0.42 c2_0 \/ c2_2 a114 $_78 \/ c3_0 \/ c3_2 a114 $_78 \/ c4_1 a114 \/ % 0.20/0.42 c4_2 a114 $_78 \/ ssSkC0 % 0.20/0.42 |- ~c3_2 a114 a105 \/ ~ndr1_1 a114 \/ ~ssSkP0 a114 \/ c1_2 a114 $_78 \/ % 0.20/0.42 c2_0 \/ c2_2 a114 $_78 \/ c3_2 a114 $_78 \/ c4_2 a114 $_78 \/ % 0.20/0.42 c5_1 a114 \/ ssSkC0 \/ ssSkC6 % 0.20/0.42 |- ~c3_2 $_77 a105 \/ ~ndr1_1 $_77 \/ ~ssSkP0 $_77 \/ c2_2 $_77 a116 \/ % 0.20/0.42 c3_2 $_77 a116 \/ ssSkC0 \/ ssSkP2 $_77 % 0.20/0.42 |- ~c2_0 \/ c2_2 a106 $_81 \/ c3_2 a106 $_81 \/ c5_1 a106 \/ % 0.20/0.42 c5_2 a106 $_81 \/ c5_2 a106 a138 \/ ssSkC1 % 0.20/0.42 |- ~c2_0 \/ c2_2 a125 $_81 \/ c3_2 a125 $_81 \/ c5_1 a125 \/ % 0.20/0.42 c5_2 a125 $_81 \/ c5_2 a125 a138 \/ ssSkC4 % 0.20/0.42 |- ~c2_0 \/ c2_2 a128 $_81 \/ c3_2 a128 $_81 \/ c5_1 a128 \/ % 0.20/0.42 c5_2 a128 $_81 \/ c5_2 a128 a138 \/ ssSkC5 % 0.20/0.42 |- ~c2_0 \/ c2_2 $_80 $_81 \/ c3_2 $_80 $_81 \/ c5_1 $_80 \/ % 0.20/0.42 c5_2 $_80 $_81 \/ c5_2 $_80 a138 \/ ssSkC6 % 0.20/0.42 |- ~c2_0 \/ c2_2 $_80 $_81 \/ c3_0 \/ c3_2 $_80 $_81 \/ c4_1 $_80 \/ % 0.20/0.42 c5_1 $_80 \/ c5_2 $_80 $_81 \/ c5_2 $_80 a138 % 0.20/0.42 |- ~c4_1 a128 \/ ~c5_1 a128 \/ c1_2 a128 $_94 \/ c2_2 a128 $_94 \/ c3_0 \/ % 0.20/0.42 c3_2 a128 $_94 \/ ndr1_1 a139 \/ ssSkC5 % 0.20/0.42 |- ~c4_1 a128 \/ ~c5_1 a128 \/ ~c5_1 a139 \/ c1_2 a128 $_97 \/ % 0.20/0.42 c2_2 a128 $_97 \/ c3_0 \/ c3_2 a128 $_97 \/ ssSkC5 % 0.20/0.42 |- ~c1_2 $_99 a115 \/ ~c3_1 $_99 \/ ~c3_2 $_99 a115 \/ ~c4_1 a110 \/ % 0.20/0.42 ~c5_1 $_99 \/ ~ndr1_1 $_99 \/ ~ssSkC2 \/ ssSkP1 $_99 % 0.20/0.42 |- ~c1_2 $_99 a116 \/ ~c3_1 $_99 \/ ~c3_2 $_99 a116 \/ ~c4_1 a110 \/ % 0.20/0.42 ~c5_1 $_99 \/ ~ndr1_1 $_99 \/ ~ssSkC2 \/ ssSkP2 $_99 % 0.20/0.42 |- ~c1_2 $_103 a115 \/ ~c3_1 $_103 \/ ~c3_1 a110 \/ ~c3_2 $_103 a115 \/ % 0.20/0.42 ~c5_1 $_103 \/ ~ndr1_1 $_103 \/ ~ssSkC2 \/ ssSkP1 $_103 % 0.20/0.42 |- ~c1_2 $_103 a116 \/ ~c3_1 $_103 \/ ~c3_1 a110 \/ ~c3_2 $_103 a116 \/ % 0.20/0.42 ~c5_1 $_103 \/ ~ndr1_1 $_103 \/ ~ssSkC2 \/ ssSkP2 $_103 % 0.20/0.42 |- ~c4_1 a128 \/ ~c5_1 a128 \/ c1_2 a128 $_108 \/ c2_2 a128 $_108 \/ % 0.20/0.42 c2_2 a139 a140 \/ c3_0 \/ c3_2 a128 $_108 \/ ssSkC5 % 0.20/0.42 |- ~c4_1 a128 \/ ~c5_1 a128 \/ c1_2 a128 $_111 \/ c1_2 a139 a140 \/ % 0.20/0.42 c2_2 a128 $_111 \/ c3_0 \/ c3_2 a128 $_111 \/ ssSkC5 % 0.20/0.42 |- ~c1_2 $_123 a115 \/ ~c3_1 $_123 \/ ~c3_2 $_123 a115 \/ ~c5_1 $_123 \/ % 0.20/0.42 ~ndr1_1 $_123 \/ ~ndr1_1 a110 \/ ~ssSkC2 \/ c1_2 a110 $_125 \/ % 0.20/0.42 c5_2 a110 $_125 \/ ssSkP1 $_123 % 0.20/0.42 |- ~c1_2 $_123 a116 \/ ~c3_1 $_123 \/ ~c3_2 $_123 a116 \/ ~c5_1 $_123 \/ % 0.20/0.42 ~ndr1_1 $_123 \/ ~ndr1_1 a110 \/ ~ssSkC2 \/ c1_2 a110 $_125 \/ % 0.20/0.42 c5_2 a110 $_125 \/ ssSkP2 $_123 % 0.20/0.42 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.42 %------------------------------------------------------------------------------