%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN867-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n011.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:09:02 EDT 2022 % Result : Satisfiable 0.19s 0.59s % Output : Saturation 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN867-1 : TPTP v8.1.0. Released v2.5.0. % 0.12/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jul 11 13:58:12 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.59 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.59 % 0.19/0.59 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.59 |- ssNder1_0 % 0.19/0.59 |- ssNder1_1r1 $U % 0.19/0.59 |- ssNder1_2r1r1 $U $V % 0.19/0.59 |- ssNder1_3r1r1r1 $U $V $W % 0.19/0.59 |- ssNder1_4r1r1r1r1 $U $V $W $X % 0.19/0.60 |- ssPv24_5r1r1r1r1r1 $U $V $W $X skc38 % 0.19/0.60 |- ~ssPv24_5r1r1r1r1r1 $U $V $W $X skc39 % 0.19/0.60 |- ssNder1_5r1r1r1r1r1 $U $V $W $X $Y % 0.19/0.60 |- ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y skc36 % 0.19/0.60 |- ~ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y skc37 % 0.19/0.60 |- ssNder1_6r1r1r1r1r1r1 $U $V $W $X $Y $Z % 0.19/0.60 |- ssPv22_7r1r1r1r1r1r1r1 $U $V $W $X $Y $Z skc34 % 0.19/0.60 |- ~ssPv22_7r1r1r1r1r1r1r1 $U $V $W $X $Y $Z skc35 % 0.19/0.60 |- ssNder1_7r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 |- ssPv21_8r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 skc32 % 0.19/0.60 |- ~ssPv21_8r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 skc33 % 0.19/0.60 |- ssNder1_8r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 |- ssNder1_9r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 |- ssNder1_10r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 |- ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 $X5 % 0.19/0.60 |- ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 $X5 % 0.19/0.60 $X6 % 0.19/0.60 |- ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 skc30 % 0.19/0.60 |- ~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 skc31 % 0.19/0.60 |- ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 % 0.19/0.60 |- ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 skc28 % 0.19/0.60 |- ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 skc29 % 0.19/0.60 |- ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 $X8 % 0.19/0.60 |- ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 skc26 % 0.19/0.60 |- ~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 skc27 % 0.19/0.60 |- ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 $X9 % 0.19/0.60 |- ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 $X9 skc24 % 0.19/0.60 |- ~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 $X9 skc25 % 0.19/0.60 |- ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 $X9 $X10 % 0.19/0.60 |- ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 % 0.19/0.60 |- ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 % 0.19/0.60 |- ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 % 0.19/0.60 |- ~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 $X9 \/ % 0.19/0.60 ~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 \/ % 0.19/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 \/ ssPv26_3r1r1r1 $U $V $W % 0.19/0.60 |- ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 |- ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 skc22 % 0.19/0.60 |- ~ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z % 0.19/0.60 $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 skc23 % 0.19/0.60 |- ~ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 \/ % 0.19/0.60 ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 $X8 \/ % 0.19/0.60 ssPv19_10r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 \/ % 0.19/0.60 ssPv22_7r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 |- ~ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 \/ % 0.19/0.60 ~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 % 0.19/0.60 $X4 $X5 $X6 $X7 $X8 $X9 $X10 \/ % 0.19/0.60 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.19/0.60 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 \/ % 0.19/0.60 ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y $Z % 0.19/0.60 |- ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z % 0.19/0.60 $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.19/0.60 |- ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z % 0.19/0.60 $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 $X16 % 0.19/0.60 |- ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y % 0.19/0.60 $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.19/0.60 $X16 $X17 % 0.19/0.60 |- ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y % 0.19/0.60 $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.19/0.60 $X16 $X17 skc20 % 0.19/0.60 |- ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y % 0.19/0.60 $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.19/0.60 $X16 $X17 skc21 % 0.19/0.60 |- ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 % 0.19/0.60 |- ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 % 0.19/0.60 |- ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W % 0.19/0.60 $X $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 $X20 % 0.19/0.60 |- ~ssPv21_8r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 \/ % 0.19/0.60 ~ssPv24_5r1r1r1r1r1 $U $V $W $X $Y \/ % 0.19/0.60 ~ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 \/ % 0.19/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 % 0.19/0.60 |- ~ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y $Z \/ % 0.19/0.60 ~ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 \/ % 0.19/0.60 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 \/ % 0.19/0.60 ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 $X8 % 0.19/0.60 |- ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V % 0.19/0.60 $W $X $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 % 0.19/0.60 $X14 $X15 $X16 $X17 $X18 $X19 $X20 $X21 % 0.19/0.60 |- ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 $X8 \/ % 0.19/0.60 ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y % 0.19/0.60 $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.19/0.60 $X16 $X17 $X18 \/ % 0.19/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 \/ % 0.19/0.60 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 % 0.19/0.60 |- ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y % 0.19/0.60 $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.19/0.60 $X16 $X17 $X18 \/ % 0.19/0.60 ssPv19_10r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 \/ % 0.19/0.60 ssPv24_5r1r1r1r1r1 $U $V $W $X $Y \/ % 0.19/0.60 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 $X20 % 0.19/0.60 |- ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 $X3 $X4 % 0.19/0.60 $X5 $X6 $X7 $X8 \/ ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y $Z \/ % 0.19/0.60 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 $X20 \/ % 0.19/0.60 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X % 0.19/0.60 $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 % 0.19/0.60 $X15 $X16 $X17 $X18 $X19 % 0.19/0.60 |- ~ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V % 0.19/0.60 $W $X $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 % 0.19/0.60 $X14 $X15 $X16 $X17 $X18 $X19 $X20 $X21 $X22 \/ % 0.19/0.60 ~ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y $Z \/ % 0.19/0.60 ~ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z % 0.19/0.60 $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 \/ % 0.19/0.60 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 $X2 % 0.19/0.60 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 % 0.44/0.60 |- ~ssPv23_6r1r1r1r1r1r1 $U $V $W $X $Y $Z \/ % 0.44/0.60 ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y % 0.44/0.60 $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 $X14 $X15 % 0.44/0.60 $X16 $X17 $X18 \/ % 0.44/0.60 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V $W $X $Y $Z $X1 % 0.44/0.60 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 \/ % 0.44/0.60 ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $U $V % 0.44/0.60 $W $X $Y $Z $X1 $X2 $X3 $X4 $X5 $X6 $X7 $X8 $X9 $X10 $X11 $X12 $X13 % 0.44/0.60 $X14 $X15 $X16 $X17 $X18 $X19 $X20 $X21 $X22 % 0.44/0.60 |- ~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 $_616 $_617 $_618 $_619 $_632 $_633 % 0.44/0.60 $_620 $_624 $_625 $_626 $_627 $_628 $_629 \/ % 0.44/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_616 $_617 $_618 $_619 % 0.44/0.60 $_632 $_633 $_620 $_624 $_625 $_626 $_627 $_628 $_629 $_630 skc26 % 0.44/0.60 $_621 $_622 $_623 \/ ssPv26_3r1r1r1 $_616 $_617 $_618 % 0.44/0.60 |- ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_634 $_635 $_636 $_637 % 0.44/0.60 $_649 $_650 $_638 $_642 $_643 $_644 $_645 $_646 skc30 $_648 skc26 % 0.44/0.60 $_639 $_640 $_641 \/ ssPv26_3r1r1r1 $_634 $_635 $_636 % 0.44/0.60 |- ssPv19_10r1r1r1r1r1r1r1r1r1r1 $_755 $_756 $_757 $_758 $_779 $_780 $_759 % 0.44/0.60 $_770 $_772 $_773 \/ % 0.44/0.60 ssPv24_5r1r1r1r1r1 $_755 $_756 $_757 $_758 $_779 \/ % 0.44/0.60 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_755 $_756 % 0.44/0.60 $_757 $_758 $_779 $_780 $_759 $_770 $_772 $_773 $_774 $_775 $_776 % 0.44/0.60 $_777 $_778 $_760 $_761 $_762 $_763 $_764 $_765 $_766 $_767 skc20 % 0.44/0.60 $_769 $_771 % 0.44/0.60 |- ssPv23_6r1r1r1r1r1r1 $_806 $_807 $_808 $_809 $_830 $_831 \/ % 0.44/0.60 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_806 $_807 % 0.44/0.60 $_808 $_809 $_830 $_831 $_810 $_821 $_823 $_824 $_825 $_826 $_827 % 0.44/0.60 skc28 $_829 $_811 $_812 $_813 $_814 $_815 $_816 $_817 $_818 $_819 % 0.44/0.60 $_820 $_822 \/ % 0.44/0.60 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_806 $_807 % 0.44/0.60 $_808 $_809 $_830 $_831 $_810 $_821 $_823 $_824 $_825 $_826 $_827 % 0.44/0.60 skc28 $_829 $_811 $_812 $_813 $_814 $_815 $_816 $_817 $_818 $_819 % 0.44/0.60 $_820 % 0.44/0.60 |- ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_885 $_886 $_887 $_888 $_908 % 0.44/0.60 $_909 $_889 $_900 $_901 $_902 $_903 $_904 $_905 $_906 \/ % 0.44/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_885 $_886 $_887 $_888 % 0.44/0.60 $_908 $_909 $_889 $_900 $_901 $_902 $_903 $_904 $_905 $_906 $_907 % 0.44/0.60 $_890 $_891 $_892 \/ % 0.44/0.60 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_885 $_886 % 0.44/0.60 $_887 $_888 $_908 $_909 $_889 $_900 $_901 $_902 $_903 $_904 $_905 % 0.44/0.60 $_906 $_907 $_890 $_891 $_892 $_893 $_894 $_895 $_896 $_897 skc20 % 0.44/0.60 $_899 % 0.44/0.60 |- ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_910 $_911 $_912 $_913 % 0.44/0.60 $_932 $_933 $_914 $_924 $_925 $_926 $_927 $_928 $_929 skc28 $_931 % 0.44/0.60 $_915 $_916 $_917 \/ % 0.44/0.60 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_910 $_911 % 0.44/0.60 $_912 $_913 $_932 $_933 $_914 $_924 $_925 $_926 $_927 $_928 $_929 % 0.44/0.60 skc28 $_931 $_915 $_916 $_917 $_918 $_919 $_920 $_921 $_922 skc20 % 0.44/0.60 $_923 % 0.44/0.60 |- ~ssPv21_8r1r1r1r1r1r1r1r1 $_934 $_935 $_936 $_937 $_955 $_956 $_938 % 0.44/0.60 $_948 \/ ~ssPv24_5r1r1r1r1r1 $_934 $_935 $_936 $_937 $_955 \/ % 0.44/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_934 $_935 $_936 $_937 % 0.44/0.60 $_955 $_956 $_938 $_948 $_949 $_950 $_951 $_952 $_953 skc28 $_954 % 0.44/0.60 $_939 $_940 $_941 % 0.44/0.60 |- ~ssPv24_5r1r1r1r1r1 $_957 $_958 $_959 $_960 $_972 \/ % 0.44/0.60 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_957 $_958 $_959 $_960 % 0.44/0.60 $_972 $_973 $_961 skc32 $_966 $_967 $_968 $_969 $_970 skc28 $_971 % 0.44/0.60 $_962 $_963 $_964 % 0.44/0.60 |- ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_974 $_975 $_976 $_977 % 0.44/0.60 skc38 $_989 $_978 skc32 $_982 $_983 $_984 $_985 $_986 skc28 $_987 % 0.44/0.60 $_979 $_980 $_981 % 0.44/0.60 |- ~ssPv23_6r1r1r1r1r1r1 $_1005 $_1006 $_1007 $_1008 $_1031 $_1032 \/ % 0.44/0.60 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1005 $_1006 $_1007 % 0.44/0.60 $_1008 $_1031 $_1032 $_1009 $_1020 $_1024 $_1025 $_1026 $_1027 $_1028 % 0.44/0.60 $_1029 $_1030 $_1010 $_1011 $_1012 $_1013 \/ % 0.44/0.60 ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1005 % 0.44/0.60 $_1006 $_1007 $_1008 $_1031 $_1032 $_1009 $_1020 $_1024 $_1025 $_1026 % 0.44/0.60 $_1027 $_1028 $_1029 $_1030 $_1010 $_1011 $_1012 $_1013 $_1014 $_1015 % 0.44/0.60 $_1016 $_1017 skc20 $_1019 $_1021 $_1022 $_1023 % 0.44/0.60 |- ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1033 $_1034 $_1035 % 0.44/0.60 $_1036 $_1058 skc36 $_1037 $_1047 $_1051 $_1052 $_1053 $_1054 $_1055 % 0.44/0.60 $_1056 $_1057 $_1038 $_1039 $_1040 $_1041 \/ % 0.44/0.60 ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1033 % 0.44/0.60 $_1034 $_1035 $_1036 $_1058 skc36 $_1037 $_1047 $_1051 $_1052 $_1053 % 0.44/0.60 $_1054 $_1055 $_1056 $_1057 $_1038 $_1039 $_1040 $_1041 $_1042 $_1043 % 0.44/0.60 $_1044 $_1045 skc20 $_1046 $_1048 $_1049 $_1050 % 0.44/0.60 |- ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1086 $_1087 $_1088 % 0.44/0.60 $_1089 $_1105 skc36 $_1090 $_1097 $_1098 $_1099 $_1100 $_1101 $_1102 % 0.44/0.60 $_1103 $_1104 $_1091 $_1092 $_1093 $_1094 \/ % 0.44/0.60 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1086 $_1087 $_1088 $_1089 % 0.44/0.60 $_1105 skc36 $_1090 $_1097 $_1098 $_1099 $_1100 $_1101 $_1102 $_1103 % 0.44/0.60 $_1104 $_1091 $_1092 % 0.44/0.60 |- ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1106 $_1107 $_1108 $_1109 % 0.44/0.60 $_1123 skc36 $_1110 $_1115 $_1116 $_1117 $_1118 $_1119 $_1120 % 0.44/0.60 $_1121 \/ % 0.44/0.60 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1106 $_1107 $_1108 $_1109 % 0.44/0.60 $_1123 skc36 $_1110 $_1115 $_1116 $_1117 $_1118 $_1119 $_1120 $_1121 % 0.44/0.60 $_1122 $_1111 $_1112 \/ % 0.44/0.60 ssPv19_10r1r1r1r1r1r1r1r1r1r1 $_1106 $_1107 $_1108 $_1109 $_1123 skc36 % 0.44/0.60 $_1110 $_1115 $_1116 $_1117 \/ % 0.44/0.60 ssPv22_7r1r1r1r1r1r1r1 $_1106 $_1107 $_1108 $_1109 $_1123 skc36 $_1110 % 0.44/0.60 |- ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 $_1124 $_1125 $_1126 $_1127 % 0.44/0.60 $_1139 skc36 $_1128 $_1131 $_1132 $_1133 $_1134 $_1135 $_1136 skc28 % 0.44/0.60 $_1138 $_1129 $_1130 \/ % 0.44/0.60 ssPv19_10r1r1r1r1r1r1r1r1r1r1 $_1124 $_1125 $_1126 $_1127 $_1139 skc36 % 0.44/0.60 $_1128 $_1131 $_1132 $_1133 \/ % 0.44/0.60 ssPv22_7r1r1r1r1r1r1r1 $_1124 $_1125 $_1126 $_1127 $_1139 skc36 $_1128 % 0.44/0.60 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.44/0.60 %------------------------------------------------------------------------------