%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN430+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n005.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:02:25 EDT 2022 % Result : CounterSatisfiable 0.50s 0.69s % Output : Saturation 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SYN430+1 : TPTP v8.1.0. Released v2.1.0. % 0.04/0.14 % Command : metis --show proof --show saturation %s % 0.13/0.35 % Computer : n005.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jul 12 03:57:06 EDT 2022 % 0.13/0.35 % CPUTime : % 0.13/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.50/0.69 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.50/0.69 % 0.50/0.69 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.50/0.69 |- hskp23 % 0.50/0.69 |- ~c1_1 a105 \/ ~hskp0 % 0.50/0.69 |- ~c2_1 a105 \/ ~hskp0 % 0.50/0.69 |- ~hskp0 \/ c3_1 a105 % 0.50/0.69 |- ~c0_1 a107 \/ ~hskp1 % 0.50/0.69 |- ~c1_1 a107 \/ ~hskp1 % 0.50/0.69 |- ~c3_1 a107 \/ ~hskp1 % 0.50/0.69 |- ~c1_1 a122 \/ ~hskp10 % 0.50/0.69 |- ~c3_1 a122 \/ ~hskp10 % 0.50/0.69 |- ~hskp10 \/ c2_1 a122 % 0.50/0.69 |- ~c0_1 a123 \/ ~hskp11 % 0.50/0.69 |- ~c1_1 a123 \/ ~hskp11 % 0.50/0.69 |- ~hskp11 \/ c3_1 a123 % 0.50/0.69 |- ~c3_1 a126 \/ ~hskp12 % 0.50/0.69 |- ~hskp12 \/ c0_1 a126 % 0.50/0.69 |- ~hskp12 \/ c1_1 a126 % 0.50/0.69 |- ~c1_1 a127 \/ ~hskp13 % 0.50/0.69 |- ~c2_1 a127 \/ ~hskp13 % 0.50/0.69 |- ~c3_1 a127 \/ ~hskp13 % 0.50/0.69 |- ~c0_1 a128 \/ ~hskp14 % 0.50/0.69 |- ~c2_1 a128 \/ ~hskp14 % 0.50/0.69 |- ~hskp14 \/ c3_1 a128 % 0.50/0.69 |- ~c0_1 a106 \/ ~hskp15 % 0.50/0.69 |- ~c2_1 a106 \/ ~hskp15 % 0.50/0.69 |- ~hskp15 \/ c3_1 a106 % 0.50/0.69 |- ~c1_1 a113 \/ ~hskp16 % 0.50/0.69 |- ~c3_1 a113 \/ ~hskp16 % 0.50/0.69 |- ~hskp16 \/ c0_1 a113 % 0.50/0.69 |- ~c0_1 a115 \/ ~hskp17 % 0.50/0.69 |- ~hskp17 \/ c1_1 a115 % 0.50/0.69 |- ~hskp17 \/ c2_1 a115 % 0.50/0.69 |- ~c3_1 a116 \/ ~hskp18 % 0.50/0.69 |- ~hskp18 \/ c0_1 a116 % 0.50/0.69 |- ~hskp18 \/ c1_1 a116 % 0.50/0.69 |- ~c1_1 a117 \/ ~hskp19 % 0.50/0.69 |- ~c2_1 a117 \/ ~hskp19 % 0.50/0.69 |- ~hskp19 \/ c0_1 a117 % 0.50/0.69 |- ~c1_1 a108 \/ ~hskp2 % 0.50/0.69 |- ~c2_1 a108 \/ ~hskp2 % 0.50/0.69 |- ~hskp2 \/ c3_1 a108 % 0.50/0.69 |- ~c0_1 a119 \/ ~hskp20 % 0.50/0.69 |- ~hskp20 \/ c1_1 a119 % 0.50/0.69 |- ~hskp20 \/ c2_1 a119 % 0.50/0.69 |- ~hskp21 \/ c1_1 a121 % 0.50/0.69 |- ~hskp21 \/ c2_1 a121 % 0.50/0.69 |- ~hskp21 \/ c3_1 a121 % 0.50/0.69 |- ~c0_1 a129 \/ ~hskp22 % 0.50/0.69 |- ~c3_1 a129 \/ ~hskp22 % 0.50/0.69 |- ~hskp22 \/ c1_1 a129 % 0.50/0.69 |- ~c1_1 a130 % 0.50/0.69 |- ~c2_1 a130 % 0.50/0.69 |- c3_1 a130 % 0.50/0.69 |- ndr1_0 % 0.50/0.69 |- ~c1_1 a131 \/ ~hskp24 % 0.50/0.69 |- ~hskp24 \/ c0_1 a131 % 0.50/0.69 |- ~hskp24 \/ c3_1 a131 % 0.50/0.69 |- ~c1_1 a109 \/ ~hskp3 % 0.50/0.69 |- ~c2_1 a109 \/ ~hskp3 % 0.50/0.69 |- ~hskp3 \/ c3_1 a109 % 0.50/0.69 |- ~c1_1 a110 \/ ~hskp4 % 0.50/0.69 |- ~c2_1 a110 \/ ~hskp4 % 0.50/0.69 |- ~c3_1 a110 \/ ~hskp4 % 0.50/0.69 |- ~c1_1 a111 \/ ~hskp5 % 0.50/0.69 |- ~hskp5 \/ c0_1 a111 % 0.50/0.69 |- ~hskp5 \/ c2_1 a111 % 0.50/0.69 |- ~c0_1 a112 \/ ~hskp6 % 0.50/0.69 |- ~c1_1 a112 \/ ~hskp6 % 0.50/0.69 |- ~c2_1 a112 \/ ~hskp6 % 0.50/0.69 |- ~c0_1 a114 \/ ~hskp7 % 0.50/0.69 |- ~hskp7 \/ c1_1 a114 % 0.50/0.69 |- ~hskp7 \/ c2_1 a114 % 0.50/0.69 |- ~c0_1 a118 \/ ~hskp8 % 0.50/0.69 |- ~c1_1 a118 \/ ~hskp8 % 0.50/0.69 |- ~c2_1 a118 \/ ~hskp8 % 0.50/0.69 |- ~c0_1 a120 \/ ~hskp9 % 0.50/0.69 |- ~c1_1 a120 \/ ~hskp9 % 0.50/0.69 |- ~c2_1 a120 \/ ~hskp9 % 0.50/0.69 |- ~c1_1 $U \/ ~c2_1 $U \/ c3_1 $U \/ hskp0 \/ hskp15 % 0.50/0.69 |- ~c1_1 $V \/ c0_1 $V \/ c3_1 $V \/ hskp1 \/ hskp2 % 0.50/0.69 |- ~c3_1 $X9 \/ c0_1 $X9 \/ c1_1 $X9 \/ hskp10 \/ hskp21 % 0.50/0.69 |- hskp11 \/ hskp6 \/ hskp7 % 0.50/0.69 |- ~c1_1 $X13 \/ ~c2_1 $X13 \/ c0_1 $X13 \/ hskp12 \/ hskp13 % 0.50/0.69 |- ~c1_1 $X14 \/ ~c2_1 $X14 \/ c3_1 $X14 \/ hskp14 \/ hskp22 % 0.50/0.69 |- c0_1 $Z \/ c1_1 $Z \/ c3_1 $Z \/ hskp16 \/ hskp6 % 0.50/0.69 |- hskp17 \/ hskp18 \/ hskp7 % 0.50/0.69 |- ~c1_1 $X5 \/ ~c3_1 $X4 \/ c0_1 $X4 \/ c2_1 $X4 \/ c2_1 $X5 \/ % 0.50/0.69 c3_1 $X5 \/ hskp19 % 0.50/0.69 |- hskp20 \/ hskp8 \/ hskp9 % 0.50/0.69 |- ~c0_1 $W \/ ~c2_1 $W \/ c3_1 $W \/ hskp3 \/ hskp4 % 0.50/0.69 |- ~c0_1 $X \/ ~c1_1 $Y \/ ~c2_1 $Y \/ c2_1 $X \/ c3_1 $X \/ c3_1 $Y \/ % 0.50/0.69 hskp5 % 0.50/0.69 |- ~c0_1 $X3 \/ ~c1_1 $X1 \/ ~c1_1 $X3 \/ ~c2_1 $X2 \/ ~c2_1 $X3 \/ % 0.50/0.69 c0_1 $X1 \/ c0_1 $X2 \/ c1_1 $X2 \/ c2_1 $X1 % 0.50/0.69 |- ~c0_1 $X10 \/ ~c1_1 $X10 \/ ~c1_1 $X12 \/ ~c3_1 $X12 \/ c0_1 $X11 \/ % 0.50/0.69 c0_1 $X12 \/ c1_1 $X11 \/ c2_1 $X10 \/ c2_1 $X11 % 0.50/0.69 |- ~c0_1 $X7 \/ ~c1_1 $X7 \/ ~c3_1 $X7 \/ ~c3_1 $X8 \/ c0_1 $X8 \/ c2_1 $X8 % 0.50/0.69 |- c2_1 a114 \/ hskp11 \/ hskp6 % 0.50/0.69 |- c1_1 a114 \/ hskp11 \/ hskp6 % 0.50/0.69 |- c2_1 a114 \/ hskp17 \/ hskp18 % 0.50/0.69 |- c1_1 a114 \/ hskp17 \/ hskp18 % 0.50/0.69 |- hskp12 \/ hskp13 \/ hskp17 \/ hskp18 % 0.50/0.69 |- c1_1 a116 \/ hskp12 \/ hskp13 \/ hskp17 % 0.50/0.69 |- c0_1 a116 \/ hskp12 \/ hskp13 \/ hskp17 % 0.50/0.69 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp6 % 0.50/0.69 |- c3_1 a114 \/ hskp0 \/ hskp15 \/ hskp17 \/ hskp18 % 0.50/0.69 |- c3_1 a114 \/ hskp0 \/ hskp11 \/ hskp15 \/ hskp6 % 0.50/0.69 |- c0_1 a114 \/ c3_1 a114 \/ hskp1 \/ hskp17 \/ hskp18 \/ hskp2 % 0.50/0.69 |- c0_1 a114 \/ c3_1 a114 \/ hskp1 \/ hskp11 \/ hskp2 \/ hskp6 % 0.50/0.69 |- c0_1 a130 \/ hskp10 \/ hskp21 % 0.50/0.69 |- c3_1 a114 \/ hskp14 \/ hskp17 \/ hskp18 \/ hskp22 % 0.50/0.69 |- c3_1 a114 \/ hskp11 \/ hskp14 \/ hskp22 \/ hskp6 % 0.50/0.69 |- ~hskp1 \/ c0_1 a107 \/ c1_1 a107 \/ hskp16 \/ hskp6 % 0.50/0.69 |- ~hskp4 \/ c0_1 a110 \/ c1_1 a110 \/ hskp16 \/ hskp6 % 0.50/0.69 |- ~hskp10 \/ c0_1 a122 \/ c1_1 a122 \/ hskp16 \/ hskp6 % 0.50/0.69 |- ~hskp13 \/ c0_1 a127 \/ c1_1 a127 \/ hskp16 \/ hskp6 % 0.50/0.69 |- c0_1 $_5 \/ c1_1 $_5 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~c0_1 a114 \/ c3_1 a114 \/ hskp17 \/ hskp18 \/ hskp3 \/ hskp4 % 0.50/0.69 |- ~c0_1 a114 \/ c3_1 a114 \/ hskp11 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.69 |- ~hskp0 \/ c0_1 a105 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp1 \/ c0_1 a107 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp2 \/ c0_1 a108 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp3 \/ c0_1 a109 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp4 \/ c0_1 a110 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp8 \/ c0_1 a118 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp9 \/ c0_1 a120 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.69 |- ~hskp11 \/ c0_1 a123 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp13 \/ c0_1 a127 \/ hskp10 \/ hskp16 \/ hskp21 \/ hskp6 % 0.50/0.70 |- c0_1 $_7 \/ c3_1 $_7 \/ hskp1 \/ hskp10 \/ hskp16 \/ hskp2 \/ hskp21 \/ % 0.50/0.70 hskp6 % 0.50/0.70 |- hskp10 \/ hskp16 \/ hskp20 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ ~c1_1 a114 \/ ~c3_1 $_9 \/ c0_1 $_9 \/ c2_1 $_9 \/ % 0.50/0.70 hskp11 \/ hskp14 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ ~c1_1 a114 \/ ~c3_1 $_9 \/ c0_1 $_9 \/ c2_1 $_9 \/ % 0.50/0.70 hskp14 \/ hskp17 \/ hskp18 \/ hskp22 % 0.50/0.70 |- ~c0_1 a114 \/ ~c1_1 a114 \/ ~c3_1 $_9 \/ c0_1 $_9 \/ c2_1 $_9 \/ % 0.50/0.70 hskp0 \/ hskp11 \/ hskp15 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ ~c1_1 a114 \/ ~c3_1 $_9 \/ c0_1 $_9 \/ c2_1 $_9 \/ % 0.50/0.70 hskp0 \/ hskp15 \/ hskp17 \/ hskp18 % 0.50/0.70 |- ~c0_1 $_8 \/ ~c1_1 $_8 \/ ~c3_1 $_8 \/ c0_1 a130 % 0.50/0.70 |- ~c0_1 $_8 \/ ~c1_1 $_8 \/ ~c3_1 $_8 \/ c0_1 $_9 \/ c1_1 $_9 \/ % 0.50/0.70 c2_1 $_9 \/ hskp16 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 a130 \/ hskp11 \/ hskp14 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 a130 \/ hskp14 \/ hskp17 \/ hskp18 \/ hskp22 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 a130 \/ hskp0 \/ hskp11 \/ hskp15 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 a130 \/ hskp0 \/ hskp15 \/ hskp17 \/ hskp18 % 0.50/0.70 |- ~c3_1 $_11 \/ c0_1 $_11 \/ c0_1 $_12 \/ c2_1 $_11 \/ c2_1 $_12 \/ % 0.50/0.70 c3_1 $_12 \/ hskp10 \/ hskp16 \/ hskp19 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~c1_1 $_12 \/ c0_1 a130 \/ c2_1 $_12 \/ c3_1 $_12 \/ hskp19 % 0.50/0.70 |- ~c1_1 $_12 \/ c0_1 $_11 \/ c1_1 $_11 \/ c2_1 $_11 \/ c2_1 $_12 \/ % 0.50/0.70 c3_1 $_12 \/ hskp16 \/ hskp19 \/ hskp6 % 0.50/0.70 |- c0_1 a130 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 % 0.50/0.70 |- c0_1 a130 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp3 \/ hskp4 % 0.50/0.70 |- c0_1 a130 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp22 % 0.50/0.70 |- c0_1 a130 \/ hskp0 \/ hskp12 \/ hskp13 \/ hskp15 \/ hskp17 \/ hskp19 % 0.50/0.70 |- ~c0_1 $_16 \/ c2_1 $_16 \/ c3_1 $_16 \/ c3_1 a114 \/ hskp17 \/ hskp18 \/ % 0.50/0.70 hskp5 % 0.50/0.70 |- ~c0_1 $_18 \/ c2_1 $_18 \/ c3_1 $_18 \/ c3_1 a114 \/ hskp11 \/ hskp5 \/ % 0.50/0.70 hskp6 % 0.50/0.70 |- ~hskp22 \/ c0_1 a129 \/ hskp1 \/ hskp10 \/ hskp16 \/ hskp2 \/ hskp21 \/ % 0.50/0.70 hskp6 % 0.50/0.70 |- ~c1_1 $X5 \/ c0_1 $_20 \/ c2_1 $X5 \/ c2_1 $_20 \/ c3_1 $X5 \/ hskp1 \/ % 0.50/0.70 hskp10 \/ hskp16 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~c0_1 $X7 \/ ~c1_1 $X7 \/ ~c3_1 $X7 \/ c0_1 $_20 \/ c2_1 $_20 \/ % 0.50/0.70 hskp1 \/ hskp10 \/ hskp16 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_25 \/ c1_1 $_25 \/ c2_1 $_25 \/ hskp11 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_27 \/ c1_1 $_27 \/ c2_1 $_27 \/ hskp0 \/ hskp11 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_29 \/ c0_1 a130 \/ c2_1 $_29 \/ c3_1 $_29 \/ c3_1 a116 \/ % 0.50/0.70 hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp5 % 0.50/0.70 |- c0_1 $_36 \/ c1_1 $_36 \/ c2_1 $_36 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ c0_1 a118 \/ c1_1 a118 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ c0_1 a120 \/ c1_1 a120 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp14 \/ c0_1 a128 \/ c1_1 a128 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- c0_1 a120 \/ c1_1 a120 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp20 \/ hskp6 \/ hskp8 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_38 \/ c1_1 $_38 \/ c2_1 $_38 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp18 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_40 \/ c1_1 $_40 \/ c2_1 $_40 \/ hskp0 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp18 \/ hskp6 % 0.50/0.70 |- hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp20 \/ % 0.50/0.70 hskp22 \/ hskp6 % 0.50/0.70 |- hskp0 \/ hskp12 \/ hskp13 \/ hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ % 0.50/0.70 hskp20 \/ hskp6 % 0.50/0.70 |- hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp20 \/ hskp3 \/ % 0.50/0.70 hskp4 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_44 \/ ~c1_1 $_42 \/ ~c1_1 $_44 \/ ~c2_1 $_44 \/ c0_1 $_42 \/ % 0.50/0.70 c0_1 $_43 \/ c1_1 $_43 \/ c2_1 $_42 \/ c2_1 a116 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ ~c1_1 $_42 \/ ~c1_1 a114 \/ ~c2_1 $_43 \/ c0_1 $_42 \/ % 0.50/0.70 c0_1 $_43 \/ c1_1 $_43 \/ c2_1 $_42 \/ hskp17 \/ hskp18 % 0.50/0.70 |- ~c0_1 a114 \/ ~c1_1 $_42 \/ ~c1_1 a114 \/ ~c2_1 $_43 \/ c0_1 $_42 \/ % 0.50/0.70 c0_1 $_43 \/ c1_1 $_43 \/ c2_1 $_42 \/ hskp11 \/ hskp6 % 0.50/0.70 |- ~c0_1 a116 \/ ~c1_1 $_42 \/ ~c1_1 a116 \/ ~c2_1 $_43 \/ c0_1 $_42 \/ % 0.50/0.70 c0_1 $_43 \/ c0_1 a120 \/ c1_1 $_43 \/ c1_1 a120 \/ c2_1 $_42 \/ % 0.50/0.70 hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp20 \/ hskp6 \/ % 0.50/0.70 hskp8 % 0.50/0.70 |- ~c0_1 a116 \/ ~c1_1 $_42 \/ ~c1_1 a116 \/ ~c2_1 $_43 \/ c0_1 $_36 \/ % 0.50/0.70 c0_1 $_42 \/ c0_1 $_43 \/ c1_1 $_36 \/ c1_1 $_43 \/ c2_1 $_36 \/ % 0.50/0.70 c2_1 $_42 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~c0_1 a116 \/ ~c1_1 $_42 \/ ~c1_1 a116 \/ ~c2_1 $_43 \/ c0_1 $_42 \/ % 0.50/0.70 c0_1 $_43 \/ c0_1 a130 \/ c1_1 $_43 \/ c2_1 $_42 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp17 \/ hskp19 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_48 \/ c2_1 $_48 \/ hskp1 \/ hskp10 \/ hskp11 \/ % 0.50/0.70 hskp14 \/ hskp16 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_50 \/ c2_1 $_50 \/ hskp0 \/ hskp1 \/ hskp10 \/ % 0.50/0.70 hskp11 \/ hskp15 \/ hskp16 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_58 \/ c2_1 $_58 \/ hskp1 \/ hskp10 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp18 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 a114 \/ c0_1 $_60 \/ c2_1 $_60 \/ hskp0 \/ hskp1 \/ hskp10 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp18 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- c0_1 $_64 \/ c1_1 $_64 \/ c2_1 $_64 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp0 \/ c0_1 a105 \/ c1_1 a105 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp15 \/ c0_1 a106 \/ c1_1 a106 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp2 \/ c0_1 a108 \/ c1_1 a108 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ c0_1 a118 \/ c1_1 a118 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ c0_1 a120 \/ c1_1 a120 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp14 \/ c0_1 a128 \/ c1_1 a128 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~c0_1 $X3 \/ ~c1_1 $X1 \/ ~c1_1 $X3 \/ ~c2_1 $X3 \/ c0_1 $X1 \/ % 0.50/0.70 c0_1 $_65 \/ c1_1 $_65 \/ c2_1 $X1 \/ hskp12 \/ hskp13 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- c0_1 $_68 \/ c1_1 $_68 \/ c2_1 $_68 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp0 \/ c0_1 a105 \/ c1_1 a105 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp15 \/ c0_1 a106 \/ c1_1 a106 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp2 \/ c0_1 a108 \/ c1_1 a108 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp3 \/ c0_1 a109 \/ c1_1 a109 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ c0_1 a118 \/ c1_1 a118 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ c0_1 a120 \/ c1_1 a120 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 $X3 \/ ~c1_1 $X1 \/ ~c1_1 $X3 \/ ~c2_1 $X3 \/ c0_1 $X1 \/ % 0.50/0.70 c0_1 $_69 \/ c1_1 $_69 \/ c2_1 $X1 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp22 \/ hskp6 % 0.50/0.70 |- c0_1 $_72 \/ c1_1 $_72 \/ c2_1 $_72 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp2 \/ c0_1 a108 \/ c1_1 a108 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp3 \/ c0_1 a109 \/ c1_1 a109 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ c0_1 a118 \/ c1_1 a118 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ c0_1 a120 \/ c1_1 a120 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~hskp14 \/ c0_1 a128 \/ c1_1 a128 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~c0_1 $X3 \/ ~c1_1 $X1 \/ ~c1_1 $X3 \/ ~c2_1 $X3 \/ c0_1 $X1 \/ % 0.50/0.70 c0_1 $_73 \/ c1_1 $_73 \/ c2_1 $X1 \/ hskp0 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp15 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_74 \/ ~c1_1 $_74 \/ c0_1 $_75 \/ c0_1 a114 \/ c1_1 $_75 \/ % 0.50/0.70 c2_1 $_74 \/ c2_1 $_75 \/ hskp14 \/ hskp17 \/ hskp18 \/ hskp22 % 0.50/0.70 |- ~c0_1 $_78 \/ ~c1_1 $_78 \/ c0_1 $_79 \/ c0_1 a114 \/ c1_1 $_79 \/ % 0.50/0.70 c2_1 $_78 \/ c2_1 $_79 \/ hskp11 \/ hskp14 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_82 \/ ~c1_1 $_82 \/ c0_1 $_83 \/ c0_1 a114 \/ c1_1 $_83 \/ % 0.50/0.70 c2_1 $_82 \/ c2_1 $_83 \/ hskp1 \/ hskp17 \/ hskp18 \/ hskp2 % 0.50/0.70 |- ~c0_1 $_86 \/ ~c1_1 $_86 \/ c0_1 $_87 \/ c0_1 a114 \/ c1_1 $_87 \/ % 0.50/0.70 c2_1 $_86 \/ c2_1 $_87 \/ hskp1 \/ hskp11 \/ hskp2 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_90 \/ ~c1_1 $_90 \/ c0_1 $_91 \/ c0_1 a114 \/ c1_1 $_91 \/ % 0.50/0.70 c2_1 $_90 \/ c2_1 $_91 \/ hskp0 \/ hskp15 \/ hskp17 \/ hskp18 % 0.50/0.70 |- ~c0_1 $_94 \/ ~c1_1 $_94 \/ c0_1 $_95 \/ c0_1 a114 \/ c1_1 $_95 \/ % 0.50/0.70 c2_1 $_94 \/ c2_1 $_95 \/ hskp0 \/ hskp11 \/ hskp15 \/ hskp6 % 0.50/0.70 |- c0_1 $_107 \/ c2_1 a116 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~c1_1 $Y \/ ~c2_1 $Y \/ c2_1 $_108 \/ c2_1 a116 \/ c3_1 $Y \/ % 0.50/0.70 c3_1 $_108 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp5 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_109 \/ c0_1 a120 \/ c1_1 a120 \/ c2_1 $_109 \/ c3_1 $_109 \/ % 0.50/0.70 c3_1 a116 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp20 \/ % 0.50/0.70 hskp5 \/ hskp6 \/ hskp8 % 0.50/0.70 |- c0_1 $_113 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp15 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp7 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp20 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp11 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp14 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~hskp22 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp6 % 0.50/0.70 |- ~c1_1 $Y \/ ~c2_1 $Y \/ c2_1 $_114 \/ c3_1 $Y \/ c3_1 $_114 \/ hskp1 \/ % 0.50/0.70 hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 0.50/0.70 hskp21 \/ hskp3 \/ hskp4 \/ hskp5 \/ hskp6 % 0.50/0.70 |- c0_1 $_117 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp7 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp20 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp11 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp14 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- ~hskp22 \/ hskp0 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp15 \/ % 0.50/0.70 hskp16 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp6 % 0.50/0.70 |- c0_1 $_121 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp15 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp7 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp8 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp20 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp9 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~hskp11 \/ hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp16 \/ % 0.50/0.70 hskp17 \/ hskp19 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_123 \/ c0_1 $_124 \/ c1_1 $_124 \/ c2_1 $_123 \/ c2_1 $_124 \/ % 0.50/0.70 c3_1 $_123 \/ c3_1 a116 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ % 0.50/0.70 hskp19 \/ hskp5 \/ hskp6 % 0.50/0.70 |- ~c0_1 $_137 \/ c0_1 $_138 \/ c2_1 $_137 \/ c3_1 $_137 \/ c3_1 a116 \/ % 0.50/0.70 hskp1 \/ hskp10 \/ hskp12 \/ hskp13 \/ hskp16 \/ hskp17 \/ hskp19 \/ % 0.50/0.70 hskp2 \/ hskp21 \/ hskp5 \/ hskp6 % 0.50/0.70 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.50/0.70 %------------------------------------------------------------------------------