%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN867-1 : TPTP v9.0.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %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 : 300s % DateTime : Wed Apr 9 10:05:57 PM UTC 2025 % Result : Satisfiable 8.76s 2.84s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN867-1 : TPTP v9.0.0. Released v2.5.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n005.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 : 300 % 0.13/0.34 % DateTime : Wed Apr 9 08:32:57 EDT 2025 % 0.13/0.34 % CPUTime : % 8.76/2.83 % 8.76/2.84 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.76/2.84 % 8.76/2.84 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.76/2.85 %$ ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 > ssPv19_10r1r1r1r1r1r1r1r1r1r1 > ssNder1_10r1r1r1r1r1r1r1r1r1r1 > ssNder1_9r1r1r1r1r1r1r1r1r1 > ssPv21_8r1r1r1r1r1r1r1r1 > ssNder1_8r1r1r1r1r1r1r1r1 > ssPv22_7r1r1r1r1r1r1r1 > ssNder1_7r1r1r1r1r1r1r1 > ssPv23_6r1r1r1r1r1r1 > ssNder1_6r1r1r1r1r1r1 > ssPv24_5r1r1r1r1r1 > ssNder1_5r1r1r1r1r1 > ssNder1_4r1r1r1r1 > ssPv26_3r1r1r1 > ssNder1_3r1r1r1 > ssNder1_2r1r1 > ssNder1_1r1 > #nlpp > ssNder1_0 > skc39 > skc38 > skc37 > skc36 > skc35 > skc34 > skc33 > skc32 > skc31 > skc30 > skc29 > skc28 > skc27 > skc26 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 % 8.76/2.85 % 8.76/2.85 %Foreground sorts: % 8.76/2.85 % 8.76/2.85 % 8.76/2.85 %Background operators: % 8.76/2.85 % 8.76/2.85 % 8.76/2.85 %Foreground operators: % 8.76/2.85 tff(ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc34, type, skc34: $i). % 8.76/2.85 tff(ssPv26_3r1r1r1, type, ssPv26_3r1r1r1: ($i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_7r1r1r1r1r1r1r1, type, ssNder1_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv19_10r1r1r1r1r1r1r1r1r1r1, type, ssPv19_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc29, type, skc29: $i). % 8.76/2.85 tff(skc39, type, skc39: $i). % 8.76/2.85 tff(skc25, type, skc25: $i). % 8.76/2.85 tff(ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_10r1r1r1r1r1r1r1r1r1r1, type, ssNder1_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv21_8r1r1r1r1r1r1r1r1, type, ssPv21_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc36, type, skc36: $i). % 8.76/2.85 tff(ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc26, type, skc26: $i). % 8.76/2.85 tff(skc24, type, skc24: $i). % 8.76/2.85 tff(ssNder1_2r1r1, type, ssNder1_2r1r1: ($i * $i) > $o). % 8.76/2.85 tff(skc32, type, skc32: $i). % 8.76/2.85 tff(ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc20, type, skc20: $i). % 8.76/2.85 tff(ssPv22_7r1r1r1r1r1r1r1, type, ssPv22_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc23, type, skc23: $i). % 8.76/2.85 tff(skc38, type, skc38: $i). % 8.76/2.85 tff(ssNder1_0, type, ssNder1_0: $o). % 8.76/2.85 tff(skc21, type, skc21: $i). % 8.76/2.85 tff(ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc22, type, skc22: $i). % 8.76/2.85 tff(ssNder1_11r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_11r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc27, type, skc27: $i). % 8.76/2.85 tff(ssNder1_8r1r1r1r1r1r1r1r1, type, ssNder1_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_5r1r1r1r1r1, type, ssNder1_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_9r1r1r1r1r1r1r1r1r1, type, ssNder1_9r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_3r1r1r1, type, ssNder1_3r1r1r1: ($i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc37, type, skc37: $i). % 8.76/2.85 tff(skc31, type, skc31: $i). % 8.76/2.85 tff(ssNder1_6r1r1r1r1r1r1, type, ssNder1_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc35, type, skc35: $i). % 8.76/2.85 tff(ssNder1_4r1r1r1r1, type, ssNder1_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv24_5r1r1r1r1r1, type, ssPv24_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc30, type, skc30: $i). % 8.76/2.85 tff(ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv23_6r1r1r1r1r1r1, type, ssPv23_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc33, type, skc33: $i). % 8.76/2.85 tff(ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(ssNder1_1r1, type, ssNder1_1r1: $i > $o). % 8.76/2.85 tff(ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 8.76/2.85 tff(skc28, type, skc28: $i). % 8.76/2.85 % 8.76/2.85 %Saturated clause set: % 8.76/2.85 tff(c_1457, plain, (![X_1820, X9_1833, X2_1823, X5_1826, X1_1822, W_1818, Y_1819, X7_1815, X3_1827, X11_1824, Z_1821, U_1830, X10_1825, X4_1831, X8_1816, V_1829, X6_1832]: (ssPv22_7r1r1r1r1r1r1r1(U_1830, V_1829, W_1818, X_1820, Y_1819, Z_1821, X1_1822) | ssPv19_10r1r1r1r1r1r1r1r1r1r1(U_1830, V_1829, W_1818, X_1820, Y_1819, Z_1821, X1_1822, X2_1823, X3_1827, X4_1831) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1830, V_1829, W_1818, X_1820, Y_1819, Z_1821, X1_1822, X2_1823, X3_1827, X4_1831, X5_1826, X6_1832, X7_1815, X8_1816) | ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1830, V_1829, W_1818, X_1820, Y_1819, Z_1821, X1_1822, X2_1823, X3_1827, X4_1831, X5_1826, X6_1832, X7_1815, X8_1816, X9_1833, X10_1825, X11_1824) | ~ssPv23_6r1r1r1r1r1r1(U_1830, V_1829, W_1818, X_1820, Y_1819, Z_1821)))). % 8.76/2.85 tff(c_1452, plain, (![X1_390, X13_393, X5_381, X11_391, X9_386, X12_387, Y_395, Z_388, X10_400, X_394, W_383, X6_382, X4_398, X7_389, X2_392, X8_397, U_385, X3_384, V_396]: (ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_385, V_396, W_383, X_394, Y_395, Z_388, X1_390, X2_392, X3_384, X4_398, X5_381, X6_382, X7_389, X8_397, X9_386, X10_400, X11_391) | ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_385, V_396, W_383, X_394, Y_395, Z_388, X1_390, X2_392, X3_384, X4_398, X5_381, X6_382, X7_389, X8_397, X9_386, X10_400, X11_391, X12_387, X13_393) | ~ssPv23_6r1r1r1r1r1r1(U_385, V_396, W_383, X_394, Y_395, Z_388)))). % 8.76/2.85 tff(c_1441, plain, (![U_532, X8_544, W_528, X7_536, X5_526, Z_535, X4_545, X12_534, Y_542, X9_533, X3_530, X6_527, X1_537, X_541, X10_547, X2_539, X11_538, V_543]: (~ssPv24_5r1r1r1r1r1(U_532, V_543, W_528, X_541, Y_542) | ~ssPv21_8r1r1r1r1r1r1r1r1(U_532, V_543, W_528, X_541, Y_542, Z_535, X1_537, X2_539) | ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_532, V_543, W_528, X_541, Y_542, Z_535, X1_537, X2_539, X3_530, X4_545, X5_526, X6_527, X7_536, X8_544, X9_533, X10_547, X11_538, X12_534) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_532, V_543, W_528, X_541, Y_542, Z_535, X1_537, X2_539, X3_530, X4_545, X5_526, X6_527, X7_536, X8_544)))). % 8.76/2.85 tff(c_1322, plain, (![X9_731, X6_725, X1_735, W_726, X3_728, X11_736, X4_744, X19_743, V_741, X5_724, X7_734, X8_742, U_730, X18_745, X13_738, X10_747, Z_733, X2_737, X15_727, Y_740, X14_746, X16_723, X17_729, X_739, X12_732]: (ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_730, V_741, W_726, X_739, Y_740, Z_733, X1_735, X2_737, X3_728, X4_744, X5_724, X6_725, X7_734, X8_742, X9_731, X10_747, X11_736, X12_732) | ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_730, V_741, W_726, X_739, Y_740, Z_733, X1_735, X2_737, X3_728, X4_744, X5_724, X6_725, X7_734, X8_742, X9_731, X10_747, X11_736, X12_732, X13_738, X14_746, X15_727, X16_723, X17_729, X18_745, X19_743) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_730, V_741, W_726, X_739, Y_740, Z_733, X1_735, X2_737, X3_728, X4_744, X5_724, X6_725, X7_734, X8_742) | ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_730, V_741, W_726, X_739, Y_740, Z_733, X1_735, X2_737, X3_728, X4_744, X5_724, X6_725, X7_734, X8_742, X9_731, X10_747, X11_736, X12_732, X13_738, X14_746, X15_727, X16_723, X17_729, X18_745)))). % 8.76/2.85 tff(c_1360, plain, (![X13_844, X17_835, X8_850, X5_829, X7_840, X4_852, X16_828, X21_845, X12_838, X6_831, X22_830, Y_847, V_849, Z_839, X11_842, U_836, X3_834, X10_855, X15_833, X_846, X14_854, W_832, X9_837, X19_851, X2_843, X20_848, X1_841, X18_853]: (ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_836, V_849, W_832, X_846, Y_847, Z_839, X1_841, X2_843, X3_834, X4_852, X5_829, X6_831, X7_840, X8_850, X9_837, X10_855, X11_842, X12_838, X13_844) | ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_836, V_849, W_832, X_846, Y_847, Z_839, X1_841, X2_843, X3_834, X4_852, X5_829, X6_831, X7_840, X8_850, X9_837, X10_855, X11_842, X12_838, X13_844, X14_854, X15_833, X16_828, X17_835, X18_853, X19_851, X20_848, X21_845, X22_830) | ~ssPv23_6r1r1r1r1r1r1(U_836, V_849, W_832, X_846, Y_847, Z_839) | ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_836, V_849, W_832, X_846, Y_847, Z_839, X1_841, X2_843, X3_834, X4_852, X5_829, X6_831, X7_840, X8_850, X9_837, X10_855, X11_842, X12_838, X13_844, X14_854, X15_833, X16_828, X17_835, X18_853)))). % 8.76/2.85 tff(c_1417, plain, (![X6_1547, X8_1539, U_1542, Z_1549, X2_1546, X9_1538, X11_1535, X3_1550, X10_1540, X_1541, V_1551, X5_1552, Y_1544, X4_1536, W_1537, X7_1534, X1_1543]: (ssPv22_7r1r1r1r1r1r1r1(U_1542, V_1551, W_1537, X_1541, Y_1544, Z_1549, X1_1543) | ssPv19_10r1r1r1r1r1r1r1r1r1r1(U_1542, V_1551, W_1537, X_1541, Y_1544, Z_1549, X1_1543, X2_1546, X3_1550, X4_1536) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1542, V_1551, W_1537, X_1541, Y_1544, Z_1549, X1_1543, X2_1546, X3_1550, X4_1536, X5_1552, X6_1547, X7_1534, X8_1539) | ssPv23_6r1r1r1r1r1r1(U_1542, V_1551, W_1537, X_1541, Y_1544, Z_1549) | ~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1542, V_1551, W_1537, X_1541, Y_1544, Z_1549, X1_1543, X2_1546, X3_1550, X4_1536, X5_1552, X6_1547, X7_1534, X8_1539, X9_1538, X10_1540) | ~ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1542, V_1551, W_1537, X_1541, Y_1544, Z_1549, X1_1543, X2_1546, X3_1550, X4_1536, X5_1552, X6_1547, X7_1534, X8_1539, X9_1538, X10_1540, X11_1535)))). % 8.76/2.85 tff(c_1362, plain, (![X22_802, X21_817, Y_819, X7_812, X16_800, W_804, X20_820, U_808, X11_814, V_821, X5_801, X14_826, X13_816, X17_807, X_818, X9_809, X8_822, X2_815, X18_825, Z_811, X19_823, X3_806, X10_827, X4_824, X6_803, X12_810, X15_805, X1_813]: (ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_808, V_821, W_804, X_818, Y_819, Z_811, X1_813, X2_815, X3_806, X4_824, X5_801, X6_803, X7_812, X8_822, X9_809, X10_827, X11_814) | ~ssPv23_6r1r1r1r1r1r1(U_808, V_821, W_804, X_818, Y_819, Z_811) | ~ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_808, V_821, W_804, X_818, Y_819, Z_811, X1_813, X2_815, X3_806, X4_824, X5_801, X6_803, X7_812, X8_822, X9_809, X10_827, X11_814, X12_810, X13_816, X14_826, X15_805) | ~ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_808, V_821, W_804, X_818, Y_819, Z_811, X1_813, X2_815, X3_806, X4_824, X5_801, X6_803, X7_812, X8_822, X9_809, X10_827, X11_814, X12_810, X13_816, X14_826, X15_805, X16_800, X17_807, X18_825, X19_823, X20_820, X21_817, X22_802)))). % 8.76/2.85 tff(c_1346, plain, (![X1_786, X3_779, X13_789, X4_796, X16_774, X19_795, X7_785, X14_798, W_777, X2_788, X8_794, X5_775, X12_783, Y_791, X15_778, V_793, X20_792, X11_787, X6_776, Z_784, X17_780, X9_782, X18_797, X10_799, X_790, U_781]: (ssPv23_6r1r1r1r1r1r1(U_781, V_793, W_777, X_790, Y_791, Z_784) | ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_781, V_793, W_777, X_790, Y_791, Z_784, X1_786, X2_788, X3_779, X4_796, X5_775, X6_776, X7_785, X8_794, X9_782, X10_799, X11_787, X12_783, X13_789, X14_798, X15_778, X16_774, X17_780, X18_797, X19_795, X20_792) | ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_781, V_793, W_777, X_790, Y_791, Z_784, X1_786, X2_788, X3_779, X4_796, X5_775, X6_776, X7_785, X8_794, X9_782, X10_799, X11_787, X12_783, X13_789, X14_798, X15_778, X16_774, X17_780, X18_797, X19_795) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_781, V_793, W_777, X_790, Y_791, Z_784, X1_786, X2_788, X3_779, X4_796, X5_775, X6_776, X7_785, X8_794)))). % 8.76/2.86 tff(c_1342, plain, (![X8_768, X16_748, X14_772, X_764, X9_756, X13_763, X2_762, X20_766, V_767, U_755, X12_757, X19_769, X17_754, W_751, X5_749, X3_753, X6_750, Z_758, X1_760, Y_765, X11_761, X18_771, X15_752, X10_773, X7_759, X4_770]: (ssPv24_5r1r1r1r1r1(U_755, V_767, W_751, X_764, Y_765) | ssPv19_10r1r1r1r1r1r1r1r1r1r1(U_755, V_767, W_751, X_764, Y_765, Z_758, X1_760, X2_762, X3_753, X4_770) | ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_755, V_767, W_751, X_764, Y_765, Z_758, X1_760, X2_762, X3_753, X4_770, X5_749, X6_750, X7_759, X8_768, X9_756, X10_773, X11_761, X12_757, X13_763, X14_772, X15_752, X16_748, X17_754, X18_771, X19_769, X20_766) | ~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_755, V_767, W_751, X_764, Y_765, Z_758, X1_760, X2_762, X3_753, X4_770, X5_749, X6_750, X7_759, X8_768, X9_756, X10_773, X11_761, X12_757, X13_763, X14_772, X15_752, X16_748, X17_754, X18_771)))). % 8.76/2.86 tff(c_1336, plain, (![X17_677, V_689, U_678, X1_683, Y_688, X11_684, W_674, X9_679, X_687, X5_672, X10_695, X19_691, X7_682, X15_675, X16_671, X12_680, X18_693, X6_673, X2_685, Z_681, X13_686, X14_694, X8_690, X4_692, X3_676]: (ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_678, V_689, W_674, X_687, Y_688, Z_681, X1_683, X2_685, X3_676, X4_692, X5_672, X6_673, X7_682, X8_690) | ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_678, V_689, W_674, X_687, Y_688, Z_681, X1_683, X2_685, X3_676, X4_692, X5_672, X6_673, X7_682, X8_690, X9_679, X10_695, X11_684) | ~ssPv23_6r1r1r1r1r1r1(U_678, V_689, W_674, X_687, Y_688, Z_681) | ~ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_678, V_689, W_674, X_687, Y_688, Z_681, X1_683, X2_685, X3_676, X4_692, X5_672, X6_673, X7_682, X8_690, X9_679, X10_695, X11_684, X12_680, X13_686, X14_694, X15_675, X16_671, X17_677, X18_693, X19_691)))). % 8.76/2.86 tff(c_1150, plain, (![X7_448, Y_454, X1_449, X_453, X12_446, X4_457, X8_456, V_455, X5_440, X10_458, Z_447, X3_443, X11_450, X2_451, U_444, X13_452, W_442, X9_445, X6_441]: (ssPv23_6r1r1r1r1r1r1(U_444, V_455, W_442, X_453, Y_454, Z_447) | ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_444, V_455, W_442, X_453, Y_454, Z_447, X1_449, X2_451, X3_443, X4_457, X5_440, X6_441, X7_448, X8_456, X9_445, X10_458, X11_450, X12_446, X13_452) | ~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_444, V_455, W_442, X_453, Y_454, Z_447, X1_449, X2_451, X3_443, X4_457, X5_440, X6_441, X7_448, X8_456, X9_445, X10_458) | ~ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_444, V_455, W_442, X_453, Y_454, Z_447, X1_449, X2_451, X3_443, X4_457, X5_440, X6_441, X7_448, X8_456, X9_445, X10_458, X11_450)))). % 8.76/2.86 tff(c_1328, plain, (![X6_648, X12_655, X9_654, X10_670, V_664, X13_661, X11_659, X_662, X1_658, X17_652, Y_663, X3_651, W_649, U_653, X19_666, X18_668, X8_665, X7_657, X14_669, X4_667, X5_647, Z_656, X15_650, X16_646, X2_660]: (ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_653, V_664, W_649, X_662, Y_663, Z_656, X1_658, X2_660, X3_651, X4_667, X5_647, X6_648, X7_657, X8_665, X9_654, X10_670, X11_659, X12_655) | ~ssPv24_5r1r1r1r1r1(U_653, V_664, W_649, X_662, Y_663) | ~ssPv21_8r1r1r1r1r1r1r1r1(U_653, V_664, W_649, X_662, Y_663, Z_656, X1_658, X2_660) | ~ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_653, V_664, W_649, X_662, Y_663, Z_656, X1_658, X2_660, X3_651, X4_667, X5_647, X6_648, X7_657, X8_665, X9_654, X10_670, X11_659, X12_655, X13_661, X14_669, X15_650, X16_646, X17_652, X18_668, X19_666)))). % 8.76/2.86 tff(c_1180, plain, (![X2_432, X4_438, X_434, X13_433, X10_439, X8_437, X3_424, X11_431, X6_422, X9_426, X5_421, X7_429, Z_428, X1_430, W_423, X12_427, V_436, Y_435, U_425]: (ssPv22_7r1r1r1r1r1r1r1(U_425, V_436, W_423, X_434, Y_435, Z_428, X1_430) | ssPv19_10r1r1r1r1r1r1r1r1r1r1(U_425, V_436, W_423, X_434, Y_435, Z_428, X1_430, X2_432, X3_424, X4_438) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_425, V_436, W_423, X_434, Y_435, Z_428, X1_430, X2_432, X3_424, X4_438, X5_421, X6_422, X7_429, X8_437) | ~ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_425, V_436, W_423, X_434, Y_435, Z_428, X1_430, X2_432, X3_424, X4_438, X5_421, X6_422, X7_429, X8_437, X9_426, X10_439, X11_431, X12_427, X13_433)))). % 8.76/2.86 tff(c_1356, plain, (![X_713, X16_696, X11_709, X8_717, X15_700, X17_702, X20_715, X10_722, X2_710, W_699, X9_704, X19_718, X14_721, X12_705, X7_707, X4_719, X3_701, X21_712, V_716, U_703, Z_706, X6_698, X13_711, X1_708, X18_720, Y_714, X5_697]: (ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_703, V_716, W_699, X_713, Y_714, Z_706, X1_708, X2_710, X3_701, X4_719, X5_697, X6_698, X7_707, X8_717, X9_704, X10_722, X11_709, X12_705, X13_711, X14_721, X15_700, X16_696, X17_702, X18_720, X19_718, X20_715, X21_712)))). % 8.76/2.86 tff(c_1344, plain, (![X10_645, X6_622, X5_621, X8_640, X15_624, X20_638, X13_635, X16_620, X17_626, X11_633, X4_642, V_639, X_636, X2_634, W_623, X1_632, X18_643, X3_625, X19_641, Y_637, Z_630, X9_628, U_627, X14_644, X12_629, X7_631]: (ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_627, V_639, W_623, X_636, Y_637, Z_630, X1_632, X2_634, X3_625, X4_642, X5_621, X6_622, X7_631, X8_640, X9_628, X10_645, X11_633, X12_629, X13_635, X14_644, X15_624, X16_620, X17_626, X18_643, X19_641, X20_638)))). % 8.76/2.86 tff(c_1332, plain, (![X5_596, X13_610, X_611, X17_601, X4_616, X18_617, X14_618, X11_608, X9_603, X2_609, X1_607, X12_604, X7_606, Z_605, Y_612, U_602, W_598, X15_599, X8_614, X6_597, V_613, X3_600, X16_595, X19_615, X10_619]: (ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_602, V_613, W_598, X_611, Y_612, Z_605, X1_607, X2_609, X3_600, X4_616, X5_596, X6_597, X7_606, X8_614, X9_603, X10_619, X11_608, X12_604, X13_610, X14_618, X15_599, X16_595, X17_601, X18_617, X19_615)))). % 8.76/2.86 tff(c_1280, plain, (![U_532, X8_544, W_528, X7_536, X5_526, Z_535, X16_525, X4_545, X12_534, Y_542, X9_533, X3_530, X14_546, X6_527, X1_537, X_541, X13_540, X10_547, X2_539, X11_538, X15_529, V_543, X17_531]: (ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_532, V_543, W_528, X_541, Y_542, Z_535, X1_537, X2_539, X3_530, X4_545, X5_526, X6_527, X7_536, X8_544, X9_533, X10_547, X11_538, X12_534, X13_540, X14_546, X15_529, X16_525, X17_531, skc20)))). % 8.76/2.86 tff(c_1316, plain, (![V_589, X10_594, W_574, X8_590, X3_576, X15_575, U_578, X16_571, X18_592, X4_591, Y_588, X_587, X11_584, X9_579, X13_586, X1_583, X14_593, X2_585, X6_573, Z_581, X17_577, X12_580, X7_582, X5_572]: (ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_578, V_589, W_574, X_587, Y_588, Z_581, X1_583, X2_585, X3_576, X4_591, X5_572, X6_573, X7_582, X8_590, X9_579, X10_594, X11_584, X12_580, X13_586, X14_593, X15_575, X16_571, X17_577, X18_592)))). % 8.76/2.86 tff(c_1274, plain, (![X11_561, X_564, X3_553, V_566, X17_554, X1_560, X9_556, Z_558, X6_550, X15_552, X8_567, X13_563, X16_548, X7_559, X5_549, X14_569, U_555, X10_570, X2_562, Y_565, X12_557, W_551, X4_568]: (~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_555, V_566, W_551, X_564, Y_565, Z_558, X1_560, X2_562, X3_553, X4_568, X5_549, X6_550, X7_559, X8_567, X9_556, X10_570, X11_561, X12_557, X13_563, X14_569, X15_552, X16_548, X17_554, skc21)))). % 8.76/2.86 tff(c_1298, plain, (![U_509, X1_514, Y_519, X17_508, X9_510, X6_504, X8_521, X16_502, X3_507, X2_516, W_505, X14_523, X5_503, X15_506, V_520, X7_513, X4_522, Z_512, X_518, X12_511, X11_515, X10_524, X13_517]: (ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_509, V_520, W_505, X_518, Y_519, Z_512, X1_514, X2_516, X3_507, X4_522, X5_503, X6_504, X7_513, X8_521, X9_510, X10_524, X11_515, X12_511, X13_517, X14_523, X15_506, X16_502, X17_508)))). % 8.76/2.86 tff(c_1270, plain, (![X6_482, X2_493, Y_496, X12_488, W_483, X10_501, X5_481, X16_480, X15_484, X7_490, X8_498, X9_487, V_497, Z_489, X11_492, X14_500, X_495, X4_499, X1_491, U_486, X13_494, X3_485]: (ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_486, V_497, W_483, X_495, Y_496, Z_489, X1_491, X2_493, X3_485, X4_499, X5_481, X6_482, X7_490, X8_498, X9_487, X10_501, X11_492, X12_488, X13_494, X14_500, X15_484, X16_480)))). % 8.76/2.86 tff(c_1200, plain, (![X1_390, X13_393, X5_381, X11_391, X9_386, X12_387, Y_395, Z_388, X10_400, X_394, W_383, X6_382, X4_398, X14_399, X7_389, X2_392, X8_397, U_385, X3_384, V_396]: (ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_385, V_396, W_383, X_394, Y_395, Z_388, X1_390, X2_392, X3_384, X4_398, X5_381, X6_382, X7_389, X8_397, X9_386, X10_400, X11_391, X12_387, X13_393, X14_399, skc22)))). % 8.76/2.86 tff(c_1132, plain, (![U_347, X3_346, X_355, W_345, X6_344, X12_349, X4_359, X8_358, Z_350, X5_343, X1_352, X10_360, X9_348, X2_354, X11_353, X7_351, Y_356, V_357]: (ssPv26_3r1r1r1(U_347, V_357, W_345) | ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_347, V_357, W_345, X_355, Y_356, Z_350, X1_352, X2_354, X3_346, X4_359, X5_343, X6_344, X7_351, X8_358, X9_348, X10_360, X11_353, X12_349) | ~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_347, V_357, W_345, X_355, Y_356, Z_350, X1_352, X2_354, X3_346, X4_359, X5_343, X6_344, X7_351) | ~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_347, V_357, W_345, X_355, Y_356, Z_350, X1_352, X2_354, X3_346, X4_359, X5_343, X6_344, X7_351, X8_358, X9_348)))). % 8.76/2.86 tff(c_1206, plain, (![X1_410, X_414, W_403, Y_415, X4_418, U_405, X12_407, V_416, X13_413, Z_408, X11_411, X7_409, X14_419, X9_406, X3_404, X6_402, X5_401, X10_420, X2_412, X8_417]: (~ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_405, V_416, W_403, X_414, Y_415, Z_408, X1_410, X2_412, X3_404, X4_418, X5_401, X6_402, X7_409, X8_417, X9_406, X10_420, X11_411, X12_407, X13_413, X14_419, skc23)))). % 8.76/2.86 tff(c_1222, plain, (![X3_463, X2_471, W_461, X6_460, Y_474, X13_472, X10_479, X14_478, X7_468, X8_476, X5_459, X9_465, V_475, X15_462, X12_466, Z_467, X_473, X11_470, U_464, X1_469, X4_477]: (ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_464, V_475, W_461, X_473, Y_474, Z_467, X1_469, X2_471, X3_463, X4_477, X5_459, X6_460, X7_468, X8_476, X9_465, X10_479, X11_470, X12_466, X13_472, X14_478, X15_462)))). % 8.76/2.86 tff(c_1202, plain, (![X8_377, X5_361, V_376, Z_368, X_374, X4_378, X9_366, X3_364, U_365, X13_373, X2_372, Y_375, X11_371, X12_367, X6_362, X7_369, X10_380, W_363, X1_370, X14_379]: (ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_365, V_376, W_363, X_374, Y_375, Z_368, X1_370, X2_372, X3_364, X4_378, X5_361, X6_362, X7_369, X8_377, X9_366, X10_380, X11_371, X12_367, X13_373, X14_379)))). % 8.76/2.86 tff(c_1162, plain, (![U_328, X8_340, X7_332, V_339, X10_342, X11_334, X2_335, X6_325, X3_327, X9_329, X12_330, X5_324, Y_338, X4_341, X_337, W_326, X13_336, X1_333, Z_331]: (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_328, V_339, W_326, X_337, Y_338, Z_331, X1_333, X2_335, X3_327, X4_341, X5_324, X6_325, X7_332, X8_340, X9_329, X10_342, X11_334, X12_330, X13_336)))). % 8.76/2.86 tff(c_1138, plain, (![X7_314, W_308, X6_307, X4_322, X9_311, X1_315, X12_312, V_320, Z_313, X_318, X2_317, X3_309, X8_321, Y_319, U_310, X11_316, X5_306, X10_323]: (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_310, V_320, W_308, X_318, Y_319, Z_313, X1_315, X2_317, X3_309, X4_322, X5_306, X6_307, X7_314, X8_321, X9_311, X10_323, X11_316, X12_312)))). % 8.76/2.86 tff(c_1094, plain, (![X6_290, V_302, X_300, X3_292, X8_303, Z_295, X9_294, U_293, X11_298, X7_296, Y_301, X2_299, X5_289, W_291, X10_305, X1_297, X4_304]: (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_293, V_302, W_291, X_300, Y_301, Z_295, X1_297, X2_299, X3_292, X4_304, X5_289, X6_290, X7_296, X8_303, X9_294, X10_305, X11_298)))). % 8.76/2.86 tff(c_960, plain, (![X2_267, X5_258, X_268, X9_263, V_270, Z_264, W_260, X1_266, U_262, X4_272, Y_269, X8_271, X7_265, X3_261, X6_259]: (~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_262, V_270, W_260, X_268, Y_269, Z_264, X1_266, X2_267, X3_261, X4_272, X5_258, X6_259, X7_265, X8_271, X9_263, skc25)))). % 8.76/2.86 tff(c_1028, plain, (![Z_279, X8_286, X9_278, V_285, X2_282, X6_274, X10_288, X7_280, X3_276, X1_281, X_283, Y_284, X4_287, X5_273, U_277, W_275]: (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_277, V_285, W_275, X_283, Y_284, Z_279, X1_281, X2_282, X3_276, X4_287, X5_273, X6_274, X7_280, X8_286, X9_278, X10_288)))). % 8.76/2.86 tff(c_964, plain, (![Z_219, X5_214, X2_222, X_223, U_218, W_216, X1_221, V_225, Y_224, X4_227, X3_217, X8_226, X6_215, X7_220]: (~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_218, V_225, W_216, X_223, Y_224, Z_219, X1_221, X2_222, X3_217, X4_227, X5_214, X6_215, X7_220, X8_226, skc27)))). % 8.76/2.86 tff(c_980, plain, (![W_245, X2_252, Y_254, X4_257, X7_250, X8_256, X5_243, U_247, Z_249, V_255, X3_246, X9_248, X_253, X6_244, X1_251]: (ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_247, V_255, W_245, X_253, Y_254, Z_249, X1_251, X2_252, X3_246, X4_257, X5_243, X6_244, X7_250, X8_256, X9_248, skc24)))). % 8.76/2.86 tff(c_966, plain, (![X7_206, X2_208, X1_207, X6_201, U_204, W_202, X_209, V_211, X3_203, Z_205, X8_212, X5_200, Y_210, X4_213]: (ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_204, V_211, W_202, X_209, Y_210, Z_205, X1_207, X2_208, X3_203, X4_213, X5_200, X6_201, X7_206, X8_212, skc26)))). % 8.76/2.86 tff(c_1020, plain, (![X7_235, W_230, X4_242, X2_237, X5_228, U_232, Y_239, X8_241, Z_234, X1_236, X3_231, X_238, V_240, X9_233, X6_229]: (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_232, V_240, W_230, X_238, Y_239, Z_234, X1_236, X2_237, X3_231, X4_242, X5_228, X6_229, X7_235, X8_241, X9_233)))). % 8.76/2.86 tff(c_900, plain, (![X3_176, V_184, X5_173, X6_174, Z_178, X4_185, X_182, Y_183, X1_180, W_175, U_177, X2_181, X7_179]: (~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_177, V_184, W_175, X_182, Y_183, Z_178, X1_180, X2_181, X3_176, X4_185, X5_173, X6_174, X7_179, skc29)))). % 8.76/2.86 tff(c_958, plain, (![X1_193, W_188, Y_196, V_197, X_195, U_190, X4_199, X6_187, X8_198, X2_194, X5_186, X7_192, Z_191, X3_189]: (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_190, V_197, W_188, X_195, Y_196, Z_191, X1_193, X2_194, X3_189, X4_199, X5_186, X6_187, X7_192, X8_198)))). % 8.76/2.86 tff(c_956, plain, (![U_164, X7_166, X6_161, Y_170, W_162, X1_167, X3_163, X_169, Z_165, V_171, X2_168, X4_172, X5_160]: (ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_164, V_171, W_162, X_169, Y_170, Z_165, X1_167, X2_168, X3_163, X4_172, X5_160, X6_161, X7_166, skc28)))). % 8.76/2.86 tff(c_888, plain, (![X_156, Z_152, X2_155, X7_153, X1_154, X5_147, Y_157, V_158, X6_148, U_151, W_149, X4_159, X3_150]: (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_151, V_158, W_149, X_156, Y_157, Z_152, X1_154, X2_155, X3_150, X4_159, X5_147, X6_148, X7_153)))). % 8.76/2.86 tff(c_818, plain, (![X5_135, X3_138, V_145, U_139, Y_144, X1_141, Z_140, X2_142, X_143, W_137, X6_136, X4_146]: (~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_139, V_145, W_137, X_143, Y_144, Z_140, X1_141, X2_142, X3_138, X4_146, X5_135, X6_136, skc31)))). % 8.76/2.86 tff(c_814, plain, (![X3_126, X5_123, U_127, W_125, X6_124, V_133, X1_129, X2_130, X4_134, Z_128, Y_132, X_131]: (ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_127, V_133, W_125, X_131, Y_132, Z_128, X1_129, X2_130, X3_126, X4_134, X5_123, X6_124, skc30)))). % 8.76/2.86 tff(c_816, plain, (![X4_122, X_119, X2_118, X3_114, Y_120, X1_117, X6_112, W_113, Z_116, V_121, X5_111, U_115]: (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U_115, V_121, W_113, X_119, Y_120, Z_116, X1_117, X2_118, X3_114, X4_122, X5_111, X6_112)))). % 8.76/2.86 tff(c_810, plain, (![Y_108, Z_104, X3_102, X5_100, X4_110, V_109, U_103, W_101, X1_105, X_107, X2_106]: (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U_103, V_109, W_101, X_107, Y_108, Z_104, X1_105, X2_106, X3_102, X4_110, X5_100)))). % 8.76/2.86 tff(c_664, plain, (![X2_95, X1_94, Z_93, X4_99, X3_91, U_92, V_98, W_90, X_96, Y_97]: (ssNder1_10r1r1r1r1r1r1r1r1r1r1(U_92, V_98, W_90, X_96, Y_97, Z_93, X1_94, X2_95, X3_91, X4_99)))). % 8.76/2.86 tff(c_584, plain, (![Z_84, U_83, X3_82, Y_88, V_89, X_87, X1_85, X2_86, W_81]: (ssNder1_9r1r1r1r1r1r1r1r1r1(U_83, V_89, W_81, X_87, Y_88, Z_84, X1_85, X2_86, X3_82)))). % 8.76/2.86 tff(c_398, plain, (![X_70, U_67, X1_69, Y_71, Z_68, V_72, W_66]: (~ssPv21_8r1r1r1r1r1r1r1r1(U_67, V_72, W_66, X_70, Y_71, Z_68, X1_69, skc33)))). % 8.76/2.86 tff(c_468, plain, (![Y_64, V_65, Z_61, U_60, X1_62, W_59, X_63]: (ssPv21_8r1r1r1r1r1r1r1r1(U_60, V_65, W_59, X_63, Y_64, Z_61, X1_62, skc32)))). % 8.76/2.86 tff(c_512, plain, (![V_80, X2_77, Z_75, W_73, Y_79, X1_76, U_74, X_78]: (ssNder1_8r1r1r1r1r1r1r1r1(U_74, V_80, W_73, X_78, Y_79, Z_75, X1_76, X2_77)))). % 8.76/2.86 tff(c_304, plain, (![W_46, U_47, Y_50, Z_48, V_51, X_49]: (~ssPv22_7r1r1r1r1r1r1r1(U_47, V_51, W_46, X_49, Y_50, Z_48, skc35)))). % 8.76/2.86 tff(c_384, plain, (![V_45, X_43, Y_44, Z_42, W_40, U_41]: (ssPv22_7r1r1r1r1r1r1r1(U_41, V_45, W_40, X_43, Y_44, Z_42, skc34)))). % 8.76/2.86 tff(c_416, plain, (![Y_57, Z_54, U_53, X_56, V_58, X1_55, W_52]: (ssNder1_7r1r1r1r1r1r1r1(U_53, V_58, W_52, X_56, Y_57, Z_54, X1_55)))). % 8.76/2.86 tff(c_396, plain, (![V_39, Z_36, U_35, X_37, Y_38, W_34]: (ssNder1_6r1r1r1r1r1r1(U_35, V_39, W_34, X_37, Y_38, Z_36)))). % 8.76/2.86 tff(c_378, plain, (![W_29, Y_32, X_31, V_33, U_30]: (~ssPv23_6r1r1r1r1r1r1(U_30, V_33, W_29, X_31, Y_32, skc37)))). % 8.76/2.86 tff(c_298, plain, (![V_28, W_24, X_26, Y_27, U_25]: (ssPv23_6r1r1r1r1r1r1(U_25, V_28, W_24, X_26, Y_27, skc36)))). % 8.76/2.86 tff(c_262, plain, (![U_11, V_12, W_13, X_14]: (ssPv24_5r1r1r1r1r1(U_11, V_12, W_13, X_14, skc38)))). % 8.76/2.86 tff(c_250, plain, (![U_15, V_16, W_17, X_18]: (~ssPv24_5r1r1r1r1r1(U_15, V_16, W_17, X_18, skc39)))). % 8.76/2.86 tff(c_300, plain, (![U_20, X_21, Y_22, W_19, V_23]: (ssNder1_5r1r1r1r1r1(U_20, V_23, W_19, X_21, Y_22)))). % 8.76/2.86 tff(c_264, plain, (![U_7, V_8, W_9, X_10]: (ssNder1_4r1r1r1r1(U_7, V_8, W_9, X_10)))). % 8.76/2.86 tff(c_244, plain, (![U_4, V_5, W_6]: (ssNder1_3r1r1r1(U_4, V_5, W_6)))). % 8.76/2.86 tff(c_234, plain, (![U_2, V_3]: (ssNder1_2r1r1(U_2, V_3)))). % 8.76/2.86 tff(c_118, plain, (![U_1]: (ssNder1_1r1(U_1)))). % 8.76/2.86 tff(c_2, plain, (ssNder1_0)). % 8.76/2.86 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.76/2.86 %------------------------------------------------------------------------------