%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN036-2 : TPTP v8.1.0. Bugfixed v1.2.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n015.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 08:58:44 EDT 2022 % Result : Satisfiable 0.91s 1.14s % Output : Saturation 0.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN036-2 : TPTP v8.1.0. Bugfixed v1.2.0. % 0.04/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n015.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 : Mon Jul 11 22:40:09 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.91/1.14 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.91/1.14 % 0.91/1.14 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.91/1.14 |- ~big_p $U1 \/ ~big_q $U \/ big_p $X \/ big_p (f1 $X) \/ big_q $W \/ % 0.91/1.14 big_q $W1 \/ big_q $X1 \/ big_q (f2 $X1) % 0.91/1.14 |- ~big_p $X \/ ~big_p (f1 $X) \/ ~big_q $U \/ ~big_q c8 \/ big_p c9 \/ % 0.91/1.14 big_q $W \/ big_q $X4 \/ big_q $Y1 % 0.91/1.14 |- ~big_p $U1 \/ ~big_p c3 \/ ~big_q $X1 \/ ~big_q (f2 $X1) \/ big_p $Y \/ % 0.91/1.14 big_q $W1 \/ big_q $X2 \/ big_q c4 % 0.91/1.14 |- ~big_p c3 \/ ~big_q c8 \/ big_p $Y \/ big_p c9 \/ big_q $X2 \/ % 0.91/1.14 big_q $X4 \/ big_q $Y1 \/ big_q c4 % 0.91/1.14 |- ~big_p $X5 \/ ~big_p c3 \/ ~big_q c10 \/ ~big_q c8 \/ big_p $Y \/ % 0.91/1.14 big_q $X2 \/ big_q $Y1 \/ big_q c4 % 0.91/1.14 |- ~big_p c3 \/ ~big_q $Y1 \/ big_p $Y \/ big_p c9 \/ big_q $X2 \/ % 0.91/1.14 big_q $X4 \/ big_q c4 \/ big_q c8 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c8 \/ big_p c3 \/ big_p c9 \/ big_q $X2 \/ % 0.91/1.14 big_q $X4 \/ big_q $Y1 \/ big_q c4 % 0.91/1.14 |- ~big_p $Y \/ ~big_q $Y1 \/ big_p c3 \/ big_p c9 \/ big_q $X2 \/ % 0.91/1.14 big_q $X4 \/ big_q c4 \/ big_q c8 % 0.91/1.14 |- ~big_p c11 \/ ~big_q $X7 \/ big_p $X6 \/ big_p c19 \/ big_q $X15 \/ % 0.91/1.14 big_q $X16 \/ big_q $X8 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X6 \/ ~big_q $X7 \/ big_p c11 \/ big_p c19 \/ big_q $X15 \/ % 0.91/1.14 big_q $X16 \/ big_q $X8 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X13 \/ ~big_q c16 \/ big_p $X9 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X10 \/ big_q $X12 \/ big_q $X14 \/ big_q c14 % 0.91/1.14 |- ~big_q c16 \/ ~big_q c18 \/ big_p $X9 \/ big_p c17 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X10 \/ big_q $X12 \/ big_q c14 % 0.91/1.14 |- ~big_p $X13 \/ ~big_q $X12 \/ big_p $X9 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X10 \/ big_q $X14 \/ big_q c14 \/ big_q c16 % 0.91/1.14 |- ~big_p $X17 \/ ~big_q c20 \/ big_p $X9 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X10 \/ big_q $X15 \/ big_q c14 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q $X15 \/ ~big_q (f4 $X15) \/ big_p $X9 \/ big_p c19 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X10 \/ big_q $X16 \/ big_q c14 % 0.91/1.14 |- ~big_p $X17 \/ ~big_q $X15 \/ ~big_q c20 \/ ~big_q (f4 $X15) \/ % 0.91/1.14 big_p $X9 \/ big_p (f3 $X9) \/ big_q $X10 \/ big_q c14 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ big_p c19 \/ big_q $X10 \/ % 0.91/1.14 big_q $X15 \/ big_q $X16 \/ big_q c14 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X15 \/ ~big_q (f4 $X15) \/ % 0.91/1.14 big_p c19 \/ big_q $X10 \/ big_q $X16 \/ big_q c14 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X11 \/ ~big_q c15 \/ % 0.91/1.14 big_p c19 \/ big_q $X15 \/ big_q $X16 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q c7 \/ big_p $X \/ big_p c6 \/ big_p (f1 $X) \/ big_q $W \/ % 0.91/1.14 big_q $X1 \/ big_q (f2 $X1) % 0.91/1.14 |- ~big_p $U1 \/ ~big_q $X1 \/ ~big_q (f2 $X1) \/ big_p $X \/ % 0.91/1.14 big_p (f1 $X) \/ big_q $W \/ big_q $W1 % 0.91/1.14 |- ~big_q $X1 \/ ~big_q c7 \/ ~big_q (f2 $X1) \/ big_p $X \/ big_p c6 \/ % 0.91/1.14 big_p (f1 $X) \/ big_q $W % 0.91/1.14 |- ~big_q c8 \/ big_p $X \/ big_p c9 \/ big_p (f1 $X) \/ big_q $W \/ % 0.91/1.14 big_q $X4 \/ big_q $Y1 % 0.91/1.14 |- ~big_p $X5 \/ ~big_q c10 \/ ~big_q c8 \/ big_p $X \/ big_p (f1 $X) \/ % 0.91/1.14 big_q $W \/ big_q $Y1 % 0.91/1.14 |- ~big_q $Y1 \/ big_p $X \/ big_p c9 \/ big_p (f1 $X) \/ big_q $W \/ % 0.91/1.14 big_q $X4 \/ big_q c8 % 0.91/1.14 |- ~big_p $X5 \/ ~big_q c10 \/ big_p $X \/ big_p (f1 $X) \/ big_q $W \/ % 0.91/1.14 big_q c8 % 0.91/1.14 |- ~big_p $X \/ ~big_p (f1 $X) \/ ~big_q $U \/ big_q $W \/ big_q $W1 \/ % 0.91/1.14 big_q $X1 \/ big_q (f2 $X1) % 0.91/1.14 |- ~big_p $X \/ ~big_p (f1 $X) \/ ~big_q $X1 \/ ~big_q (f2 $X1) \/ % 0.91/1.14 big_q $W \/ big_q $W1 % 0.91/1.14 |- ~big_p $X \/ ~big_p (f1 $X) \/ ~big_q $U \/ ~big_q c10 \/ ~big_q c8 \/ % 0.91/1.14 big_q $W \/ big_q $Y1 % 0.91/1.14 |- ~big_p $X \/ ~big_p (f1 $X) \/ ~big_q $Y1 \/ big_p c9 \/ big_q $W \/ % 0.91/1.14 big_q $X4 \/ big_q c8 % 0.91/1.14 |- ~big_p $X \/ ~big_p (f1 $X) \/ ~big_q $Y1 \/ ~big_q c10 \/ big_q $W \/ % 0.91/1.14 big_q c8 % 0.91/1.14 |- ~big_p c3 \/ big_p $Y \/ big_q $W1 \/ big_q $X1 \/ big_q $X2 \/ % 0.91/1.14 big_q c4 \/ big_q (f2 $X1) % 0.91/1.14 |- ~big_p $X5 \/ ~big_p c3 \/ ~big_q c10 \/ big_p $Y \/ big_q $X2 \/ % 0.91/1.14 big_q c4 \/ big_q c8 % 0.91/1.14 |- ~big_p $U1 \/ ~big_p c3 \/ ~big_q c5 \/ big_p $Y \/ big_q $W1 \/ % 0.91/1.14 big_q $X1 \/ big_q (f2 $X1) % 0.91/1.14 |- ~big_p $U1 \/ ~big_p c3 \/ ~big_q $X1 \/ ~big_q c5 \/ ~big_q (f2 $X1) \/ % 0.91/1.14 big_p $Y \/ big_q $W1 % 0.91/1.14 |- ~big_p c3 \/ ~big_q $X1 \/ ~big_q c5 \/ ~big_q c7 \/ ~big_q (f2 $X1) \/ % 0.91/1.14 big_p $Y \/ big_p c6 % 0.91/1.14 |- ~big_p c3 \/ ~big_q c5 \/ ~big_q c8 \/ big_p $Y \/ big_p c9 \/ % 0.91/1.14 big_q $X4 \/ big_q $Y1 % 0.91/1.14 |- ~big_p $X5 \/ ~big_p c3 \/ ~big_q c10 \/ ~big_q c5 \/ ~big_q c8 \/ % 0.91/1.14 big_p $Y \/ big_q $Y1 % 0.91/1.14 |- ~big_p c3 \/ ~big_q c5 \/ big_p $Y \/ big_p c9 \/ big_q $X4 \/ big_q c8 % 0.91/1.14 |- ~big_p $X5 \/ ~big_p c3 \/ ~big_q c10 \/ ~big_q c5 \/ big_p $Y \/ % 0.91/1.14 big_q c8 % 0.91/1.14 |- ~big_p $Y \/ big_p c3 \/ big_q $W1 \/ big_q $X1 \/ big_q $X2 \/ % 0.91/1.14 big_q c4 \/ big_q (f2 $X1) % 0.91/1.14 |- ~big_p $Y \/ ~big_q $X1 \/ ~big_q (f2 $X1) \/ big_p c3 \/ big_q $W1 \/ % 0.91/1.14 big_q $X2 \/ big_q c4 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c10 \/ ~big_q c8 \/ big_p c3 \/ big_q $X2 \/ % 0.91/1.14 big_q $Y1 \/ big_q c4 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c10 \/ big_p c3 \/ big_q $X2 \/ big_q c4 \/ big_q c8 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c5 \/ big_p c3 \/ big_q $W1 \/ big_q $X1 \/ % 0.91/1.14 big_q (f2 $X1) % 0.91/1.14 |- ~big_p $Y \/ ~big_q $X1 \/ ~big_q c5 \/ ~big_q (f2 $X1) \/ big_p c3 \/ % 0.91/1.14 big_q $W1 % 0.91/1.14 |- ~big_p $Y \/ ~big_q $X1 \/ ~big_q c5 \/ ~big_q c7 \/ ~big_q (f2 $X1) \/ % 0.91/1.14 big_p c3 \/ big_p c6 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c5 \/ ~big_q c8 \/ big_p c3 \/ big_p c9 \/ % 0.91/1.14 big_q $X4 \/ big_q $Y1 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c10 \/ ~big_q c5 \/ ~big_q c8 \/ big_p c3 \/ % 0.91/1.14 big_q $Y1 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c5 \/ big_p c3 \/ big_p c9 \/ big_q $X4 \/ big_q c8 % 0.91/1.14 |- ~big_p $Y \/ ~big_q c10 \/ ~big_q c5 \/ big_p c3 \/ big_q c8 % 0.91/1.14 |- ~big_p $X13 \/ ~big_p c11 \/ ~big_q c16 \/ big_p $X6 \/ big_q $X12 \/ % 0.91/1.14 big_q $X14 \/ big_q $X8 % 0.91/1.14 |- ~big_p $X13 \/ ~big_p c11 \/ ~big_q $X7 \/ big_p $X6 \/ big_q $X14 \/ % 0.91/1.14 big_q $X8 \/ big_q c16 % 0.91/1.14 |- ~big_p $X17 \/ ~big_p c11 \/ ~big_q c20 \/ big_p $X6 \/ big_q $X15 \/ % 0.91/1.14 big_q $X8 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p c11 \/ ~big_q $X15 \/ ~big_q (f4 $X15) \/ big_p $X6 \/ % 0.91/1.14 big_p c19 \/ big_q $X16 \/ big_q $X8 % 0.91/1.14 |- ~big_p $X17 \/ ~big_p c11 \/ ~big_q $X15 \/ ~big_q c20 \/ % 0.91/1.14 ~big_q (f4 $X15) \/ big_p $X6 \/ big_q $X8 % 0.91/1.14 |- ~big_p $X6 \/ ~big_q c16 \/ big_p c11 \/ big_q $X12 \/ big_q $X14 \/ % 0.91/1.14 big_q $X8 % 0.91/1.14 |- ~big_p $X6 \/ ~big_q $X7 \/ big_p c11 \/ big_q $X14 \/ big_q $X8 \/ % 0.91/1.14 big_q c16 % 0.91/1.14 |- ~big_p $X6 \/ ~big_q c20 \/ big_p c11 \/ big_q $X15 \/ big_q $X8 \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X6 \/ ~big_q $X15 \/ ~big_q (f4 $X15) \/ big_p c11 \/ % 0.91/1.14 big_p c19 \/ big_q $X16 \/ big_q $X8 % 0.91/1.14 |- ~big_p $X6 \/ ~big_q $X15 \/ ~big_q c20 \/ ~big_q (f4 $X15) \/ % 0.91/1.14 big_p c11 \/ big_q $X8 % 0.91/1.14 |- ~big_q c18 \/ big_p $X9 \/ big_p c17 \/ big_p (f3 $X9) \/ big_q $X10 \/ % 0.91/1.14 big_q c14 \/ big_q c16 % 0.91/1.14 |- big_p $X9 \/ big_p c19 \/ big_p (f3 $X9) \/ big_q $X15 \/ big_q c14 \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X13 \/ ~big_q c15 \/ ~big_q c16 \/ big_p $X9 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X12 \/ big_q $X14 % 0.91/1.14 |- ~big_q c15 \/ ~big_q c16 \/ ~big_q c18 \/ big_p $X9 \/ big_p c17 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X12 % 0.91/1.14 |- ~big_p $X13 \/ ~big_q c15 \/ big_p $X9 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X14 \/ big_q c16 % 0.91/1.14 |- ~big_q c15 \/ ~big_q c18 \/ big_p $X9 \/ big_p c17 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q c16 % 0.91/1.14 |- ~big_q c15 \/ big_p $X9 \/ big_p c19 \/ big_p (f3 $X9) \/ big_q $X15 \/ % 0.91/1.14 big_q $X16 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X17 \/ ~big_q c15 \/ ~big_q c20 \/ big_p $X9 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X15 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q $X15 \/ ~big_q c15 \/ ~big_q (f4 $X15) \/ big_p $X9 \/ % 0.91/1.14 big_p c19 \/ big_p (f3 $X9) \/ big_q $X16 % 0.91/1.14 |- ~big_p $X17 \/ ~big_q $X15 \/ ~big_q c15 \/ ~big_q c20 \/ % 0.91/1.14 ~big_q (f4 $X15) \/ big_p $X9 \/ big_p (f3 $X9) % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q c16 \/ big_q $X10 \/ % 0.91/1.14 big_q $X12 \/ big_q $X14 \/ big_q c14 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X12 \/ big_q $X10 \/ % 0.91/1.14 big_q $X14 \/ big_q c14 \/ big_q c16 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q c20 \/ big_q $X10 \/ % 0.91/1.14 big_q $X15 \/ big_q c14 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X15 \/ ~big_q c20 \/ % 0.91/1.14 ~big_q (f4 $X15) \/ big_q $X10 \/ big_q c14 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X11 \/ ~big_q c15 \/ % 0.91/1.14 ~big_q c16 \/ big_q $X12 \/ big_q $X14 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X12 \/ ~big_q c15 \/ % 0.91/1.14 big_q $X14 \/ big_q c16 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X11 \/ ~big_q c15 \/ % 0.91/1.14 ~big_q c20 \/ big_q $X15 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X15 \/ ~big_q c15 \/ % 0.91/1.14 ~big_q (f4 $X15) \/ big_p c19 \/ big_q $X16 % 0.91/1.14 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X15 \/ ~big_q c15 \/ % 0.91/1.14 ~big_q c20 \/ ~big_q (f4 $X15) % 0.91/1.14 |- ~big_q c10 \/ ~big_q c5 \/ ~big_q c8 \/ big_p $_13 \/ big_p c19 \/ % 0.91/1.14 big_p c3 \/ big_q $Y1 \/ big_q $_12 \/ big_q c14 \/ big_q (f4 $_12) % 0.91/1.14 |- ~big_q c10 \/ big_p $_13 \/ big_p c19 \/ big_p c3 \/ big_q $X2 \/ % 0.91/1.14 big_q $_12 \/ big_q c14 \/ big_q c4 \/ big_q c8 \/ big_q (f4 $_12) % 0.91/1.14 |- ~big_q c10 \/ ~big_q c5 \/ big_p $_13 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_q $_12 \/ big_q c14 \/ big_q c8 \/ big_q (f4 $_12) % 0.91/1.14 |- ~big_q c10 \/ big_p $X9 \/ big_p $_17 \/ big_p c19 \/ big_p (f1 $_17) \/ % 0.91/1.14 big_q $X15 \/ big_q $_16 \/ big_q c14 \/ big_q c8 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q c5 \/ big_p $X9 \/ big_p c19 \/ big_p c3 \/ big_q $X15 \/ % 0.91/1.14 big_q $_22 \/ big_q $_23 \/ big_q c14 \/ big_q (f2 $_23) \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_q $_26 \/ ~big_q c5 \/ ~big_q (f2 $_26) \/ big_p $X9 \/ % 0.91/1.14 big_p c19 \/ big_p c3 \/ big_q $X15 \/ big_q $_25 \/ big_q c14 \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_q c20 \/ big_p $X9 \/ big_p c11 \/ big_p c19 \/ big_q $X15 \/ % 0.91/1.14 big_q $_28 \/ big_q $_30 \/ big_q c14 \/ big_q (f4 $X15) \/ % 0.91/1.14 big_q (f4 $_28) % 0.91/1.14 |- ~big_q c16 \/ big_p $X9 \/ big_p c11 \/ big_p c19 \/ big_q $X15 \/ % 0.91/1.14 big_q $_48 \/ big_q $_49 \/ big_q $_51 \/ big_q c14 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q $_54 \/ big_p $X9 \/ big_p c11 \/ big_p c19 \/ big_q $X15 \/ % 0.91/1.14 big_q $_52 \/ big_q $_55 \/ big_q c14 \/ big_q c16 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $_53 \/ big_p $X9 \/ big_p c11 \/ big_p c19 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X15 \/ big_q $_52 \/ big_q $_55 \/ big_q c14 \/ big_q c16 % 0.91/1.14 |- ~big_q c10 \/ ~big_q c8 \/ big_p $X9 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_q $X15 \/ big_q $_65 \/ big_q $_67 \/ big_q c14 \/ big_q c4 \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_q c5 \/ ~big_q c8 \/ big_p $X9 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_p c9 \/ big_q $X15 \/ big_q $_68 \/ big_q $_70 \/ big_q c14 \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_q c10 \/ ~big_q c8 \/ big_p $X9 \/ big_p $_110 \/ big_p c19 \/ % 0.91/1.14 big_p (f1 $_110) \/ big_q $X15 \/ big_q $_109 \/ big_q $_112 \/ % 0.91/1.14 big_q c14 \/ big_q (f4 $X15) % 0.91/1.14 |- big_p $X9 \/ big_p $_114 \/ big_p c19 \/ big_p c9 \/ big_p (f1 $_114) \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $_115 \/ big_q c14 \/ big_q c8 % 0.91/1.14 |- ~big_p $_122 \/ ~big_p (f1 $_122) \/ big_p $X9 \/ big_p c19 \/ % 0.91/1.14 big_p c9 \/ big_p (f3 $X9) \/ big_q $X15 \/ big_q $_121 \/ % 0.91/1.14 big_q $_123 \/ big_q c14 \/ big_q c8 % 0.91/1.14 |- big_p $X9 \/ big_p c19 \/ big_p c3 \/ big_q $X15 \/ big_q $_138 \/ % 0.91/1.14 big_q c14 \/ big_q c4 \/ big_q (f2 $_138) \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q $_142 \/ ~big_q (f2 $_142) \/ big_p $X9 \/ big_p c19 \/ % 0.91/1.14 big_p c3 \/ big_q $X15 \/ big_q $_141 \/ big_q $_143 \/ big_q c14 \/ % 0.91/1.14 big_q c4 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_q $_157 \/ ~big_q (f4 $_157) \/ big_p $X9 \/ big_p c11 \/ % 0.91/1.14 big_p c19 \/ big_q $X15 \/ big_q $_158 \/ big_q $_160 \/ big_q c14 \/ % 0.91/1.14 big_q (f4 $X15) % 0.91/1.14 |- ~big_p $_172 \/ ~big_p (f3 $_172) \/ big_p $X9 \/ big_p c19 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X15 \/ big_q $_169 \/ big_q $_171 \/ % 0.91/1.14 big_q c14 \/ big_q c16 % 0.91/1.14 |- ~big_p c11 \/ big_p $X9 \/ big_p $_187 \/ big_p c19 \/ big_p (f3 $X9) \/ % 0.91/1.14 big_q $X15 \/ big_q $_186 \/ big_q $_189 \/ big_q c14 \/ big_q c16 % 0.91/1.14 |- ~big_p c3 \/ big_p $X9 \/ big_p $_200 \/ big_p c19 \/ big_p c9 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X15 \/ big_q $_198 \/ big_q $_199 \/ % 0.91/1.14 big_q c14 \/ big_q c4 \/ big_q c8 % 0.91/1.14 |- ~big_q $_214 \/ ~big_q (f2 $_214) \/ big_p $X9 \/ big_p $_213 \/ % 0.91/1.14 big_p c19 \/ big_p (f1 $_213) \/ big_q $X15 \/ big_q $_211 \/ % 0.91/1.14 big_q $_212 \/ big_q c14 \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $_218 \/ ~big_p (f1 $_218) \/ big_p $X9 \/ big_p c19 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_q $X15 \/ big_q $_216 \/ big_q $_217 \/ % 0.91/1.14 big_q $_219 \/ big_q c14 \/ big_q (f2 $_219) % 0.91/1.14 |- ~big_q c16 \/ big_p $_246 \/ big_p $_247 \/ big_p c11 \/ big_p c19 \/ % 0.91/1.14 big_p c9 \/ big_p (f3 $_246) \/ big_q $X12 \/ big_q $X14 \/ big_q $X8 \/ % 0.91/1.14 big_q $_248 \/ big_q c14 \/ big_q c8 % 0.91/1.14 |- ~big_p c11 \/ big_p $X6 \/ big_p $_250 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_q $X14 \/ big_q $X8 \/ big_q $_249 \/ big_q $_251 \/ big_q c14 \/ % 0.91/1.14 big_q c16 \/ big_q c4 \/ big_q (f4 $_249) % 0.91/1.14 |- ~big_p c11 \/ big_p $X9 \/ big_p $_264 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_q $X15 \/ big_q $_138 \/ big_q $_262 \/ big_q $_263 \/ % 0.91/1.14 big_q $_266 \/ big_q c14 \/ big_q c4 \/ big_q (f4 $X15) \/ % 0.91/1.14 big_q (f4 $_262) % 0.91/1.14 |- ~big_q $_270 \/ big_p $X9 \/ big_p c11 \/ big_p c19 \/ big_q $X15 \/ % 0.91/1.14 big_q $_267 \/ big_q $_268 \/ big_q $_271 \/ big_q c14 \/ % 0.91/1.14 big_q (f4 $X15) \/ big_q (f4 $_267) % 0.91/1.14 |- ~big_q c16 \/ big_p $X9 \/ big_p $_114 \/ big_p $_276 \/ big_p c19 \/ % 0.91/1.14 big_p c9 \/ big_p (f3 $X9) \/ big_p (f3 $_276) \/ big_q $_115 \/ % 0.91/1.14 big_q $_272 \/ big_q $_273 \/ big_q $_275 \/ big_q c14 \/ big_q c8 % 0.91/1.14 |- ~big_p $_279 \/ big_p $X9 \/ big_p $_281 \/ big_p c19 \/ % 0.91/1.14 big_p (f3 $X9) \/ big_p (f3 $_281) \/ big_q $X15 \/ big_q $_277 \/ % 0.91/1.14 big_q $_280 \/ big_q c14 \/ big_q c16 % 0.91/1.14 |- ~big_q $_290 \/ big_p $X9 \/ big_p $_294 \/ big_p c19 \/ % 0.91/1.14 big_p (f1 $_294) \/ big_q $X15 \/ big_q $_292 \/ big_q $_293 \/ % 0.91/1.14 big_q $_295 \/ big_q c14 \/ big_q (f2 $_295) \/ big_q (f4 $X15) % 0.91/1.14 |- ~big_p $_291 \/ big_p $X9 \/ big_p $_294 \/ big_p c19 \/ % 0.91/1.14 big_p (f1 $_294) \/ big_p (f3 $X9) \/ big_q $X15 \/ big_q $_292 \/ % 0.91/1.14 big_q $_293 \/ big_q $_295 \/ big_q c14 \/ big_q (f2 $_295) % 0.91/1.14 |- ~big_p $X6 \/ big_p $_358 \/ big_p c11 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_q $X14 \/ big_q $X8 \/ big_q $_357 \/ big_q c14 \/ big_q c16 \/ % 0.91/1.14 big_q c4 % 0.91/1.14 |- ~big_q $X7 \/ big_p $_364 \/ big_p c11 \/ big_p c19 \/ big_p c9 \/ % 0.91/1.14 big_q $X14 \/ big_q $X8 \/ big_q $_365 \/ big_q c14 \/ big_q c16 \/ % 0.91/1.14 big_q c8 % 0.91/1.14 |- big_p $_469 \/ big_p c19 \/ big_p c3 \/ big_p c9 \/ big_q c14 \/ % 0.91/1.14 big_q c4 % 0.91/1.14 |- ~big_p $U1 \/ big_p $X \/ big_p $_470 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.14 big_p c9 \/ big_p (f1 $X) \/ big_q $W \/ big_q $W1 \/ big_q $X1 \/ % 0.91/1.14 big_q c14 \/ big_q (f2 $X1) % 0.91/1.15 |- ~big_p c11 \/ big_p $X6 \/ big_p $_470 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.15 big_p c9 \/ big_q $X15 \/ big_q $X16 \/ big_q $X8 \/ big_q c14 \/ % 0.91/1.15 big_q (f4 $X15) % 0.91/1.15 |- big_p $X \/ big_p c19 \/ big_p c3 \/ big_p c9 \/ big_p (f1 $X) \/ % 0.91/1.15 big_q $X4 \/ big_q c14 \/ big_q c8 % 0.91/1.15 |- ~big_p c11 \/ big_p $X6 \/ big_p $_470 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.15 big_p c9 \/ big_q $X14 \/ big_q $X8 \/ big_q c14 \/ big_q c16 % 0.91/1.15 |- ~big_q c16 \/ big_p $X9 \/ big_p $_471 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.15 big_p c9 \/ big_p (f3 $X9) \/ big_q $X10 \/ big_q $X12 \/ big_q $X14 \/ % 0.91/1.15 big_q $_472 \/ big_q c14 \/ big_q c8 % 0.91/1.15 |- ~big_q c5 \/ big_p $_471 \/ big_p c19 \/ big_p c3 \/ big_p c9 \/ % 0.91/1.15 big_q $X4 \/ big_q $_472 \/ big_q c14 \/ big_q c8 % 0.91/1.15 |- big_p $_481 \/ big_p c11 \/ big_p c19 \/ big_p c3 \/ big_q $_482 \/ % 0.91/1.15 big_q c14 \/ big_q c4 \/ big_q (f4 $_482) % 0.91/1.15 |- big_p $_493 \/ big_p c19 \/ big_p c9 \/ big_p (f3 $_493) \/ % 0.91/1.15 big_q $_492 \/ big_q c14 \/ big_q c16 \/ big_q c8 % 0.91/1.15 |- big_p $_529 \/ big_p c11 \/ big_p c19 \/ big_p c3 \/ big_p c9 \/ % 0.91/1.15 big_q $_530 % 0.91/1.15 |- ~big_p $X9 \/ ~big_p (f3 $X9) \/ ~big_q $X15 \/ ~big_q c15 \/ % 0.91/1.15 ~big_q c20 \/ big_p $_531 \/ big_p c11 \/ big_p c19 \/ big_p c3 \/ % 0.91/1.15 big_p c9 % 0.98/1.15 |- ~big_p $_536 \/ big_p $_529 \/ big_p $_535 \/ big_p $_537 \/ % 0.98/1.15 big_p c11 \/ big_p c19 \/ big_p c3 \/ big_p c6 \/ big_p c9 % 0.98/1.15 |- big_p $_558 \/ big_p c19 \/ big_p c3 \/ big_p c9 \/ big_p (f1 $_558) \/ % 0.98/1.15 big_q $_553 \/ big_q $_559 \/ big_q c14 \/ big_q (f2 $_559) \/ % 0.98/1.15 big_q (f4 $_553) % 0.98/1.15 |- ~big_p $_571 \/ big_p $_529 \/ big_p $_570 \/ big_p $_572 \/ % 0.98/1.15 big_p $_573 \/ big_p c11 \/ big_p c19 \/ big_p c3 \/ big_p c9 \/ % 0.98/1.15 big_p (f3 $_572) % 0.98/1.15 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.98/1.15 %------------------------------------------------------------------------------