%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN872-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 : n020.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:58 PM UTC 2025 % Result : Satisfiable 17.74s 5.70s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN872-1 : TPTP v9.0.0. Released v2.5.0. % 0.13/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.33 % Computer : n020.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Apr 9 08:33:49 EDT 2025 % 0.13/0.33 % CPUTime : % 17.74/5.70 % 17.74/5.70 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.74/5.70 % 17.74/5.70 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.13/5.71 %$ ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv5_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv17_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv21_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv31_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv35_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv40_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_10r1r1r1r1r1r1r1r1r1r1 > ssPv48_9r1r1r1r1r1r1r1r1r1 > ssNder1_9r1r1r1r1r1r1r1r1r1 > ssPv49_8r1r1r1r1r1r1r1r1 > ssNder1_8r1r1r1r1r1r1r1r1 > ssPv50_7r1r1r1r1r1r1r1 > ssNder1_7r1r1r1r1r1r1r1 > ssPv51_6r1r1r1r1r1r1 > ssNder1_6r1r1r1r1r1r1 > ssPv52_5r1r1r1r1r1 > ssNder1_5r1r1r1r1r1 > ssPv53_4r1r1r1r1 > ssNder1_4r1r1r1r1 > ssPv54_3r1r1r1 > ssNder1_3r1r1r1 > ssPv55_2r1r1 > ssNder1_2r1r1 > ssPv56_1r1 > ssNder1_1r1 > #nlpp > ssNder1_0 > skc75 > skc74 > skc73 > skc72 > skc71 > skc70 > skc69 > skc68 > skc67 > skc66 > skc65 > skc64 > skc63 > skc62 > skc61 > skc60 > skc59 > skc58 > skc57 > skc56 > skc55 > skc54 > skc53 > skc52 > skc51 > skc50 > skc49 > skc48 > skc47 > skc46 > skc45 > skc44 > skc43 > skc42 > skc41 > skc40 > skc39 > skc38 % 18.13/5.71 % 18.13/5.71 %Foreground sorts: % 18.13/5.71 % 18.13/5.71 % 18.13/5.71 %Background operators: % 18.13/5.71 % 18.13/5.71 % 18.13/5.71 %Foreground operators: % 18.13/5.71 tff(ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_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). % 18.13/5.71 tff(ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv40_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv40_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i) > $o). % 18.13/5.71 tff(ssPv53_4r1r1r1r1, type, ssPv53_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc51, type, skc51: $i). % 18.13/5.71 tff(ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(ssNder1_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc61, type, skc61: $i). % 18.13/5.71 tff(ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv52_5r1r1r1r1r1, type, ssPv52_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc59, type, skc59: $i). % 18.13/5.71 tff(ssNder1_7r1r1r1r1r1r1r1, type, ssNder1_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc54, type, skc54: $i). % 18.13/5.71 tff(ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc39, type, skc39: $i). % 18.13/5.71 tff(skc71, type, skc71: $i). % 18.13/5.71 tff(skc57, type, skc57: $i). % 18.13/5.71 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). % 18.13/5.71 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). % 18.13/5.71 tff(skc44, type, skc44: $i). % 18.13/5.71 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). % 18.13/5.71 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). % 18.13/5.71 tff(skc73, type, skc73: $i). % 18.13/5.71 tff(ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_10r1r1r1r1r1r1r1r1r1r1, type, ssNder1_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc52, type, skc52: $i). % 18.13/5.71 tff(ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc63, type, skc63: $i). % 18.13/5.71 tff(ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc75, type, skc75: $i). % 18.13/5.71 tff(skc53, type, skc53: $i). % 18.13/5.71 tff(skc65, type, skc65: $i). % 18.13/5.71 tff(ssPv31_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv31_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). % 18.13/5.71 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). % 18.13/5.71 tff(ssNder1_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc40, type, skc40: $i). % 18.13/5.71 tff(ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc64, type, skc64: $i). % 18.13/5.71 tff(ssNder1_2r1r1, type, ssNder1_2r1r1: ($i * $i) > $o). % 18.13/5.71 tff(ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv56_1r1, type, ssPv56_1r1: $i > $o). % 18.13/5.71 tff(skc46, type, skc46: $i). % 18.13/5.71 tff(skc41, type, skc41: $i). % 18.13/5.71 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). % 18.13/5.71 tff(ssNder1_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(ssNder1_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv51_6r1r1r1r1r1r1, type, ssPv51_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc62, type, skc62: $i). % 18.13/5.71 tff(ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc60, type, skc60: $i). % 18.13/5.71 tff(skc43, type, skc43: $i). % 18.13/5.71 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). % 18.13/5.71 tff(ssPv35_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv35_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv54_3r1r1r1, type, ssPv54_3r1r1r1: ($i * $i * $i) > $o). % 18.13/5.71 tff(skc42, type, skc42: $i). % 18.13/5.71 tff(ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(skc70, type, skc70: $i). % 18.13/5.71 tff(ssPv55_2r1r1, type, ssPv55_2r1r1: ($i * $i) > $o). % 18.13/5.71 tff(ssNder1_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc67, type, skc67: $i). % 18.13/5.71 tff(ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i) > $o). % 18.13/5.71 tff(skc38, type, skc38: $i). % 18.13/5.71 tff(ssNder1_0, type, ssNder1_0: $o). % 18.13/5.71 tff(ssNder1_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(ssPv50_7r1r1r1r1r1r1r1, type, ssPv50_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc49, type, skc49: $i). % 18.13/5.71 tff(ssNder1_11r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_11r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv21_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv21_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_8r1r1r1r1r1r1r1r1, type, ssNder1_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc56, type, skc56: $i). % 18.13/5.71 tff(ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_5r1r1r1r1r1, type, ssNder1_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i) > $o). % 18.13/5.71 tff(ssNder1_9r1r1r1r1r1r1r1r1r1, type, ssNder1_9r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_3r1r1r1, type, ssNder1_3r1r1r1: ($i * $i * $i) > $o). % 18.13/5.71 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). % 18.13/5.71 tff(ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv32_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). % 18.13/5.71 tff(skc66, type, skc66: $i). % 18.13/5.71 tff(ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc74, type, skc74: $i). % 18.13/5.71 tff(skc45, type, skc45: $i). % 18.13/5.71 tff(ssNder1_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc58, type, skc58: $i). % 18.13/5.71 tff(skc48, type, skc48: $i). % 18.13/5.71 tff(ssNder1_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(skc47, type, skc47: $i). % 18.13/5.71 tff(ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_6r1r1r1r1r1r1, type, ssNder1_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_4r1r1r1r1, type, ssNder1_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv49_8r1r1r1r1r1r1r1r1, type, ssPv49_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 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). % 18.13/5.71 tff(ssPv48_9r1r1r1r1r1r1r1r1r1, type, ssPv48_9r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc50, type, skc50: $i). % 18.13/5.71 tff(ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.71 tff(skc55, type, skc55: $i). % 18.13/5.71 tff(ssNder1_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssPv17_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv17_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(skc69, type, skc69: $i). % 18.13/5.71 tff(ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.71 tff(ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.72 tff(ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv30_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). % 18.13/5.72 tff(ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.72 tff(ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.72 tff(skc68, type, skc68: $i). % 18.13/5.72 tff(ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 18.13/5.72 tff(ssNder1_1r1, type, ssNder1_1r1: $i > $o). % 18.13/5.72 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). % 18.13/5.72 tff(skc72, type, skc72: $i). % 18.13/5.72 tff(ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $i) > $o). % 18.13/5.72 tff(ssPv5_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv5_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($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 * $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). % 18.13/5.72 % 18.13/5.72 %Saturated clause set: % 18.13/5.72 tff(c_5154, plain, (![X24_3312, X16_3286, X13_3322, Y_3325, X9_3301, X22_3290, X37_3327, Z_3311, X7_3313, V_3329, X34_3287, X6_3291, X36_3305, X40_3310, X41_3335, U_3297, X11_3320, X43_3307, X1_3314, X38_3300, W_3292, X30_3302, X42_3318, X27_3293, X3_3295, X2_3321, X31_3330, X33_3326, X28_3316, X46_3309, X14_3337, X15_3294, X20_3328, X8_3331, X10_3338, X47_3298, X23_3299, X5_3288, X19_3332, X25_3333, X39_3315, X45_3319, X_3324, X32_3303, X29_3304, X44_3306, X12_3308, X26_3317, X21_3323, X18_3336, X35_3289, X4_3334, X17_3296]: (ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3297, V_3329, W_3292, X_3324, Y_3325, Z_3311, X1_3314, X2_3321, X3_3295, X4_3334, X5_3288, X6_3291, X7_3313, X8_3331, X9_3301, X10_3338, X11_3320, X12_3308, X13_3322, X14_3337, X15_3294, X16_3286, X17_3296, X18_3336, X19_3332, X20_3328, X21_3323, X22_3290, X23_3299, X24_3312) | ~ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3297, V_3329, W_3292, X_3324, Y_3325, Z_3311, X1_3314, X2_3321, X3_3295, X4_3334, X5_3288, X6_3291, X7_3313, X8_3331, X9_3301, X10_3338, X11_3320, X12_3308, X13_3322, X14_3337, X15_3294, X16_3286, X17_3296, X18_3336, X19_3332, X20_3328, X21_3323, X22_3290, X23_3299, X24_3312, X25_3333, X26_3317, X27_3293, X28_3316, X29_3304, X30_3302, X31_3330, X32_3303, X33_3326) | ~ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3297, V_3329, W_3292, X_3324, Y_3325, Z_3311, X1_3314, X2_3321, X3_3295, X4_3334, X5_3288, X6_3291, X7_3313, X8_3331, X9_3301, X10_3338, X11_3320, X12_3308, X13_3322, X14_3337, X15_3294, X16_3286, X17_3296, X18_3336, X19_3332, X20_3328, X21_3323, X22_3290, X23_3299, X24_3312, X25_3333, X26_3317, X27_3293, X28_3316, X29_3304, X30_3302, X31_3330, X32_3303, X33_3326, X34_3287, X35_3289, X36_3305, X37_3327, X38_3300, X39_3315, X40_3310, X41_3335) | ~ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3297, V_3329, W_3292, X_3324, Y_3325, Z_3311, X1_3314, X2_3321, X3_3295, X4_3334, X5_3288, X6_3291, X7_3313, X8_3331, X9_3301, X10_3338, X11_3320, X12_3308, X13_3322, X14_3337, X15_3294, X16_3286, X17_3296, X18_3336, X19_3332, X20_3328, X21_3323, X22_3290, X23_3299, X24_3312, X25_3333, X26_3317, X27_3293, X28_3316, X29_3304, X30_3302, X31_3330, X32_3303, X33_3326, X34_3287, X35_3289, X36_3305, X37_3327, X38_3300, X39_3315, X40_3310, X41_3335, X42_3318, X43_3307, X44_3306, X45_3319, X46_3309, X47_3298)))). % 18.13/5.72 tff(c_5182, plain, (![X_3544, X3_3512, X2_3540, X19_3552, X43_3524, X33_3546, X23_3516, X25_3553, X5_3505, Y_3545, X14_3557, X11_3538, X13_3541, X12_3525, X50_3543, X41_3555, X38_3517, X49_3535, X47_3515, X17_3513, X30_3519, X44_3523, X26_3534, X9_3518, X29_3521, X6_3508, X39_3532, X1_3531, X40_3527, X10_3558, X8_3551, X24_3529, Z_3528, X34_3504, X27_3510, V_3549, X46_3526, X28_3533, X15_3511, X21_3542, X45_3537, X35_3506, X37_3547, X36_3522, U_3514, X4_3554, W_3509, X20_3548, X16_3503, X31_3550, X42_3536, X48_3539, X22_3507, X18_3556, X7_3530, X32_3520]: (ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3514, V_3549, W_3509, X_3544, Y_3545, Z_3528, X1_3531, X2_3540, X3_3512, X4_3554, X5_3505, X6_3508, X7_3530, X8_3551, X9_3518, X10_3558, X11_3538, X12_3525, X13_3541, X14_3557, X15_3511, X16_3503, X17_3513, X18_3556, X19_3552, X20_3548, X21_3542) | ~ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3514, V_3549, W_3509, X_3544, Y_3545, Z_3528, X1_3531, X2_3540, X3_3512, X4_3554, X5_3505, X6_3508, X7_3530, X8_3551, X9_3518, X10_3558, X11_3538, X12_3525, X13_3541, X14_3557, X15_3511, X16_3503, X17_3513, X18_3556, X19_3552, X20_3548, X21_3542, X22_3507, X23_3516, X24_3529, X25_3553, X26_3534, X27_3510, X28_3533, X29_3521) | ~ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3514, V_3549, W_3509, X_3544, Y_3545, Z_3528, X1_3531, X2_3540, X3_3512, X4_3554, X5_3505, X6_3508, X7_3530, X8_3551, X9_3518, X10_3558, X11_3538, X12_3525, X13_3541, X14_3557, X15_3511, X16_3503, X17_3513, X18_3556, X19_3552, X20_3548, X21_3542, X22_3507, X23_3516, X24_3529, X25_3553, X26_3534, X27_3510, X28_3533, X29_3521, X30_3519, X31_3550, X32_3520, X33_3546, X34_3504, X35_3506, X36_3522, X37_3547, X38_3517, X39_3532, X40_3527, X41_3555, X42_3536) | ~ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3514, V_3549, W_3509, X_3544, Y_3545, Z_3528, X1_3531, X2_3540, X3_3512, X4_3554, X5_3505, X6_3508, X7_3530, X8_3551, X9_3518, X10_3558, X11_3538, X12_3525, X13_3541, X14_3557, X15_3511, X16_3503, X17_3513, X18_3556, X19_3552, X20_3548, X21_3542, X22_3507, X23_3516, X24_3529, X25_3553, X26_3534, X27_3510, X28_3533, X29_3521, X30_3519, X31_3550, X32_3520, X33_3546, X34_3504, X35_3506, X36_3522, X37_3547, X38_3517, X39_3532, X40_3527, X41_3555, X42_3536, X43_3524, X44_3523, X45_3537, X46_3526, X47_3515, X48_3539, X49_3535, X50_3543)))). % 18.13/5.72 tff(c_5144, plain, (![X39_3154, Y_3164, X16_3126, X31_3169, X9_3140, X11_3159, X19_3171, X29_3143, X41_3174, X12_3147, X45_3158, X23_3138, X6_3131, X38_3139, X42_3157, X1_3153, X32_3142, X24_3151, X25_3172, X30_3141, X26_3156, X18_3175, X44_3145, X7_3152, X3_3135, X15_3134, V_3168, X_3163, X13_3161, X17_3136, X5_3128, X28_3155, X36_3144, X40_3149, U_3137, Z_3150, X27_3133, X46_3148, X43_3146, X34_3127, X21_3162, W_3132, X8_3170, X4_3173, X14_3176, X37_3166, X35_3129, X33_3165, X2_3160, X10_3177, X20_3167, X22_3130]: (ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3137, V_3168, W_3132, X_3163, Y_3164, Z_3150, X1_3153, X2_3160, X3_3135, X4_3173, X5_3128, X6_3131, X7_3152, X8_3170, X9_3140, X10_3177, X11_3159, X12_3147, X13_3161, X14_3176, X15_3134, X16_3126, X17_3136, X18_3175, X19_3171, X20_3167, X21_3162, X22_3130, X23_3138, X24_3151, X25_3172, X26_3156, X27_3133, X28_3155, X29_3143, X30_3141, X31_3169) | ~ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3137, V_3168, W_3132, X_3163, Y_3164, Z_3150, X1_3153, X2_3160, X3_3135, X4_3173, X5_3128, X6_3131, X7_3152, X8_3170, X9_3140, X10_3177, X11_3159, X12_3147, X13_3161, X14_3176, X15_3134, X16_3126, X17_3136, X18_3175, X19_3171, X20_3167, X21_3162, X22_3130, X23_3138, X24_3151, X25_3172) | ~ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3137, V_3168, W_3132, X_3163, Y_3164, Z_3150, X1_3153, X2_3160, X3_3135, X4_3173, X5_3128, X6_3131, X7_3152, X8_3170, X9_3140, X10_3177, X11_3159, X12_3147, X13_3161, X14_3176, X15_3134, X16_3126, X17_3136, X18_3175, X19_3171, X20_3167, X21_3162, X22_3130, X23_3138, X24_3151, X25_3172, X26_3156, X27_3133, X28_3155, X29_3143, X30_3141, X31_3169, X32_3142, X33_3165, X34_3127, X35_3129, X36_3144, X37_3166, X38_3139) | ~ssPv5_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3137, V_3168, W_3132, X_3163, Y_3164, Z_3150, X1_3153, X2_3160, X3_3135, X4_3173, X5_3128, X6_3131, X7_3152, X8_3170, X9_3140, X10_3177, X11_3159, X12_3147, X13_3161, X14_3176, X15_3134, X16_3126, X17_3136, X18_3175, X19_3171, X20_3167, X21_3162, X22_3130, X23_3138, X24_3151, X25_3172, X26_3156, X27_3133, X28_3155, X29_3143, X30_3141, X31_3169, X32_3142, X33_3165, X34_3127, X35_3129, X36_3144, X37_3166, X38_3139, X39_3154, X40_3149, X41_3174, X42_3157, X43_3146, X44_3145, X45_3158, X46_3148)))). % 18.13/5.72 tff(c_5362, plain, (![X29_2214, U_2208, Z_2218, X22_2201, X1_2221, X7_2220, X15_2205, X_2229, X26_2224, X5_2199, X27_2204, X11_2225, X25_2238, X19_2237, X30_2212, X28_2223, X16_2197, X14_2241, X32_2213, X23_2209, X9_2211, X4_2239, X12_2216, X20_2233, Y_2230, X3_2206, W_2203, X24_2219, X21_2228, X18_2240, X17_2207, X10_2242, X2_2226, X31_2235, V_2234, X8_2236, X13_2227, X6_2202]: (ssPv52_5r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230) | ssPv48_9r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206) | ~ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197, X17_2207, X18_2240, X19_2237) | ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202) | ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197, X17_2207, X18_2240, X19_2237, X20_2233, X21_2228, X22_2201, X23_2209, X24_2219, X25_2238, X26_2224, X27_2204, X28_2223, X29_2214, X30_2212, X31_2235, X32_2213)))). % 18.13/5.72 tff(c_5104, plain, (![U_2928, X31_2958, X32_2933, X3_2926, X18_2964, X43_2937, X4_2962, X13_2950, X8_2959, X19_2960, X20_2956, X7_2942, X29_2934, X27_2924, X36_2935, X2_2949, X40_2939, X17_2927, X11_2948, X15_2925, X16_2917, X34_2918, X5_2919, X23_2929, Y_2953, Z_2940, X10_2966, X12_2938, X30_2932, X35_2920, X21_2951, X26_2946, V_2957, X38_2930, X28_2945, X9_2931, X1_2943, X6_2922, X22_2921, X44_2936, X14_2965, X37_2955, X42_2947, X24_2941, X_2952, X41_2963, X39_2944, X33_2954, W_2923, X25_2961]: (ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U_2928, V_2957, W_2923, X_2952, Y_2953, Z_2940, X1_2943, X2_2949, X3_2926, X4_2962, X5_2919, X6_2922) | ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2928, V_2957, W_2923, X_2952, Y_2953, Z_2940, X1_2943, X2_2949, X3_2926, X4_2962, X5_2919, X6_2922, X7_2942, X8_2959, X9_2931, X10_2966, X11_2948, X12_2938, X13_2950, X14_2965, X15_2925, X16_2917, X17_2927, X18_2964, X19_2960, X20_2956, X21_2951, X22_2921, X23_2929, X24_2941, X25_2961, X26_2946, X27_2924, X28_2945, X29_2934, X30_2932, X31_2958, X32_2933) | ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2928, V_2957, W_2923, X_2952, Y_2953, Z_2940, X1_2943, X2_2949, X3_2926, X4_2962, X5_2919, X6_2922, X7_2942, X8_2959, X9_2931, X10_2966, X11_2948, X12_2938, X13_2950, X14_2965, X15_2925, X16_2917, X17_2927, X18_2964, X19_2960, X20_2956, X21_2951, X22_2921, X23_2929, X24_2941, X25_2961, X26_2946, X27_2924, X28_2945, X29_2934, X30_2932, X31_2958, X32_2933, X33_2954, X34_2918, X35_2920, X36_2935, X37_2955, X38_2930, X39_2944, X40_2939, X41_2963, X42_2947, X43_2937, X44_2936) | ~ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2928, V_2957, W_2923, X_2952, Y_2953, Z_2940, X1_2943, X2_2949, X3_2926, X4_2962, X5_2919, X6_2922, X7_2942, X8_2959, X9_2931, X10_2966, X11_2948, X12_2938, X13_2950, X14_2965, X15_2925, X16_2917, X17_2927, X18_2964, X19_2960, X20_2956, X21_2951, X22_2921, X23_2929, X24_2941, X25_2961, X26_2946, X27_2924, X28_2945, X29_2934, X30_2932, X31_2958, X32_2933, X33_2954, X34_2918, X35_2920, X36_2935, X37_2955, X38_2930, X39_2944, X40_2939, X41_2963)))). % 18.13/5.73 tff(c_5166, plain, (![X22_3397, X24_3419, X9_3408, X40_3417, X25_3441, X46_3416, W_3399, X2_3429, X34_3394, X37_3435, X42_3425, X27_3400, X30_3409, X8_3439, U_3404, X19_3440, X14_3445, X45_3426, X48_3428, X36_3412, X20_3436, X32_3410, X41_3443, X43_3414, Y_3433, X6_3398, X16_3393, X23_3406, X47_3405, X11_3427, X7_3420, Z_3418, X_3432, X35_3396, X12_3415, X5_3395, X15_3401, X21_3431, X10_3446, X17_3403, X33_3434, X28_3423, V_3437, X26_3424, X44_3413, X3_3402, X39_3422, X38_3407, X18_3444, X13_3430, X29_3411, X1_3421, X31_3438, X4_3442]: (~ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3404, V_3437, W_3399, X_3432, Y_3433, Z_3418, X1_3421, X2_3429, X3_3402, X4_3442, X5_3395, X6_3398, X7_3420, X8_3439, X9_3408, X10_3446, X11_3427, X12_3415, X13_3430) | ~ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3404, V_3437, W_3399, X_3432, Y_3433, Z_3418, X1_3421, X2_3429, X3_3402, X4_3442, X5_3395, X6_3398, X7_3420, X8_3439, X9_3408, X10_3446, X11_3427, X12_3415, X13_3430, X14_3445, X15_3401, X16_3393, X17_3403, X18_3444, X19_3440, X20_3436, X21_3431, X22_3397, X23_3406, X24_3419) | ~ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3404, V_3437, W_3399, X_3432, Y_3433, Z_3418, X1_3421, X2_3429, X3_3402, X4_3442, X5_3395, X6_3398, X7_3420, X8_3439, X9_3408, X10_3446, X11_3427, X12_3415, X13_3430, X14_3445, X15_3401, X16_3393, X17_3403, X18_3444, X19_3440, X20_3436, X21_3431, X22_3397, X23_3406, X24_3419, X25_3441, X26_3424, X27_3400, X28_3423, X29_3411, X30_3409, X31_3438, X32_3410, X33_3434, X34_3394, X35_3396) | ~ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3404, V_3437, W_3399, X_3432, Y_3433, Z_3418, X1_3421, X2_3429, X3_3402, X4_3442, X5_3395, X6_3398, X7_3420, X8_3439, X9_3408, X10_3446, X11_3427, X12_3415, X13_3430, X14_3445, X15_3401, X16_3393, X17_3403, X18_3444, X19_3440, X20_3436, X21_3431, X22_3397, X23_3406, X24_3419, X25_3441, X26_3424, X27_3400, X28_3423, X29_3411, X30_3409, X31_3438, X32_3410, X33_3434, X34_3394, X35_3396, X36_3412, X37_3435, X38_3407, X39_3422, X40_3417, X41_3443, X42_3425, X43_3414, X44_3413, X45_3426, X46_3416, X47_3405, X48_3428)))). % 18.13/5.73 tff(c_5346, plain, (![Z_7092, Y_7093, X2_7090, W_7095, U_7089, V_7091, X_7087, X1_7088]: (ssPv52_5r1r1r1r1r1(U_7089, V_7091, W_7095, X_7087, Y_7093) | ~ssPv49_8r1r1r1r1r1r1r1r1(U_7089, V_7091, W_7095, X_7087, Y_7093, Z_7092, X1_7088, X2_7090)))). % 18.13/5.73 tff(c_5184, plain, (![X44_3467, X27_3454, X33_3490, X13_3485, X23_3460, X46_3470, X50_3487, V_3493, X31_3494, X41_3499, X5_3449, X39_3476, X14_3501, X16_3447, Y_3489, X19_3496, X45_3481, X9_3462, X18_3500, X3_3456, X1_3475, X42_3480, X37_3491, X6_3452, Z_3472, X26_3478, X7_3474, X11_3482, U_3458, X_3488, X28_3477, X38_3461, X25_3497, X8_3495, X29_3465, X21_3486, X35_3450, X48_3483, X20_3492, X40_3471, X2_3484, X12_3469, X24_3473, X43_3468, X34_3448, X47_3459, X36_3466, X49_3479, X32_3464, X4_3498, X17_3457, X10_3502, X30_3463, X15_3455, X22_3451, W_3453]: (~ssPv53_4r1r1r1r1(U_3458, V_3493, W_3453, X_3488) | ~ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3458, V_3493, W_3453, X_3488, Y_3489, Z_3472, X1_3475, X2_3484, X3_3456, X4_3498, X5_3449, X6_3452, X7_3474, X8_3495, X9_3462, X10_3502, X11_3482, X12_3469, X13_3485, X14_3501, X15_3455, X16_3447, X17_3457, X18_3500, X19_3496, X20_3492, X21_3486, X22_3451, X23_3460, X24_3473, X25_3497) | ~ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3458, V_3493, W_3453, X_3488, Y_3489, Z_3472, X1_3475, X2_3484, X3_3456, X4_3498, X5_3449, X6_3452, X7_3474, X8_3495, X9_3462, X10_3502, X11_3482, X12_3469, X13_3485, X14_3501, X15_3455, X16_3447, X17_3457, X18_3500, X19_3496, X20_3492, X21_3486, X22_3451, X23_3460, X24_3473, X25_3497, X26_3478, X27_3454, X28_3477, X29_3465, X30_3463, X31_3494, X32_3464, X33_3490, X34_3448, X35_3450, X36_3466, X37_3491, X38_3461, X39_3476, X40_3471, X41_3499, X42_3480) | ~ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3458, V_3493, W_3453, X_3488, Y_3489, Z_3472, X1_3475, X2_3484, X3_3456, X4_3498, X5_3449, X6_3452, X7_3474, X8_3495, X9_3462, X10_3502, X11_3482, X12_3469, X13_3485, X14_3501, X15_3455, X16_3447, X17_3457, X18_3500, X19_3496, X20_3492, X21_3486, X22_3451, X23_3460, X24_3473, X25_3497, X26_3478, X27_3454, X28_3477, X29_3465, X30_3463, X31_3494, X32_3464, X33_3490, X34_3448, X35_3450, X36_3466, X37_3491, X38_3461, X39_3476, X40_3471, X41_3499, X42_3480, X43_3468, X44_3467, X45_3481, X46_3470, X47_3459, X48_3483, X49_3479, X50_3487)))). % 18.13/5.73 tff(c_5098, plain, (![X9_2881, X43_2887, X7_2892, X24_2891, X18_2914, X8_2909, X11_2898, W_2873, X3_2876, X32_2883, X37_2905, X34_2868, X42_2897, X39_2894, X20_2906, X16_2867, X13_2900, X23_2879, X28_2895, X4_2912, V_2907, X41_2913, X6_2872, X15_2875, X_2902, X29_2884, X12_2888, Y_2903, X2_2899, X36_2885, X17_2877, X1_2893, X26_2896, X44_2886, X5_2869, X10_2916, X30_2882, X14_2915, X38_2880, X31_2908, X40_2889, X21_2901, X25_2911, X33_2904, Z_2890, X19_2910, U_2878, X35_2870, X27_2874, X22_2871]: (ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2878, V_2907, W_2873, X_2902, Y_2903, Z_2890, X1_2893, X2_2899, X3_2876, X4_2912, X5_2869, X6_2872, X7_2892, X8_2909, X9_2881, X10_2916, X11_2898, X12_2888, X13_2900, X14_2915, X15_2875, X16_2867, X17_2877, X18_2914, X19_2910, X20_2906, X21_2901, X22_2871, X23_2879, X24_2891, X25_2911, X26_2896, X27_2874, X28_2895, X29_2884, X30_2882, X31_2908, X32_2883, X33_2904, X34_2868, X35_2870, X36_2885, X37_2905, X38_2880, X39_2894, X40_2889, X41_2913, X42_2897, X43_2887, X44_2886) | ~ssPv49_8r1r1r1r1r1r1r1r1(U_2878, V_2907, W_2873, X_2902, Y_2903, Z_2890, X1_2893, X2_2899) | ~ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2878, V_2907, W_2873, X_2902, Y_2903, Z_2890, X1_2893, X2_2899, X3_2876, X4_2912, X5_2869, X6_2872, X7_2892, X8_2909, X9_2881, X10_2916, X11_2898, X12_2888, X13_2900, X14_2915, X15_2875, X16_2867, X17_2877, X18_2914, X19_2910, X20_2906, X21_2901, X22_2871, X23_2879) | ~ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2878, V_2907, W_2873, X_2902, Y_2903, Z_2890, X1_2893, X2_2899, X3_2876, X4_2912, X5_2869, X6_2872, X7_2892, X8_2909, X9_2881, X10_2916, X11_2898, X12_2888, X13_2900, X14_2915, X15_2875, X16_2867, X17_2877, X18_2914, X19_2910, X20_2906, X21_2901, X22_2871, X23_2879, X24_2891, X25_2911, X26_2896, X27_2874, X28_2895, X29_2884, X30_2882, X31_2908, X32_2883, X33_2904, X34_2868, X35_2870, X36_2885, X37_2905, X38_2880, X39_2894, X40_2889)))). % 18.13/5.73 tff(c_5174, plain, (![X30_3355, X38_3353, X35_3342, X11_3373, X45_3372, X16_3339, X14_3391, X44_3359, X32_3356, X17_3349, X5_3341, X15_3347, X21_3377, X47_3351, X3_3348, X1_3367, X7_3366, X9_3354, X43_3360, U_3350, X25_3387, X27_3346, X8_3385, X36_3358, X29_3357, Z_3364, X40_3363, X28_3369, X41_3389, X26_3370, X33_3380, W_3345, Y_3379, X2_3375, X18_3390, X6_3344, X31_3384, X48_3374, X24_3365, X4_3388, X39_3368, X10_3392, X22_3343, X19_3386, X42_3371, V_3383, X37_3381, X23_3352, X34_3340, X_3378, X12_3361, X20_3382, X46_3362, X13_3376]: (ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3350, V_3383, W_3345, X_3378, Y_3379, Z_3364, X1_3367, X2_3375, X3_3348, X4_3388, X5_3341, X6_3344, X7_3366, X8_3385, X9_3354, X10_3392, X11_3373, X12_3361, X13_3376, X14_3391, X15_3347, X16_3339, X17_3349, X18_3390, X19_3386, X20_3382, X21_3377, X22_3343, X23_3352, X24_3365) | ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3350, V_3383, W_3345, X_3378, Y_3379, Z_3364, X1_3367, X2_3375, X3_3348, X4_3388, X5_3341, X6_3344, X7_3366, X8_3385, X9_3354, X10_3392, X11_3373, X12_3361, X13_3376, X14_3391, X15_3347, X16_3339, X17_3349, X18_3390, X19_3386, X20_3382, X21_3377, X22_3343, X23_3352, X24_3365, X25_3387, X26_3370, X27_3346, X28_3369, X29_3357) | ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3350, V_3383, W_3345, X_3378, Y_3379, Z_3364, X1_3367, X2_3375, X3_3348, X4_3388, X5_3341, X6_3344, X7_3366, X8_3385, X9_3354, X10_3392, X11_3373, X12_3361, X13_3376, X14_3391, X15_3347, X16_3339, X17_3349, X18_3390, X19_3386, X20_3382, X21_3377, X22_3343, X23_3352, X24_3365, X25_3387, X26_3370, X27_3346, X28_3369, X29_3357, X30_3355, X31_3384, X32_3356, X33_3380, X34_3340, X35_3342, X36_3358, X37_3381, X38_3353, X39_3368, X40_3363, X41_3389, X42_3371, X43_3360, X44_3359, X45_3372, X46_3362, X47_3351, X48_3374) | ~ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3350, V_3383, W_3345, X_3378, Y_3379, Z_3364, X1_3367, X2_3375, X3_3348, X4_3388, X5_3341, X6_3344, X7_3366)))). % 18.13/5.73 tff(c_5160, plain, (![X17_3188, X33_3218, X38_3192, X36_3197, V_3221, X37_3219, X35_3181, X31_3222, X_3216, X22_3182, X46_3201, X6_3183, X23_3191, X42_3210, X10_3230, X2_3213, X47_3190, X3_3187, X32_3195, X7_3205, X12_3200, X43_3199, X28_3208, X11_3212, X21_3215, X27_3185, X1_3206, X8_3223, X5_3180, X9_3193, X14_3229, X41_3227, W_3184, X18_3228, X40_3202, X15_3186, X4_3226, X34_3179, X16_3178, X45_3211, U_3189, X24_3204, X39_3207, Y_3217, X20_3220, X13_3214, X44_3198, X30_3194, X19_3224, Z_3203, X29_3196, X25_3225, X26_3209]: (ssPv40_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3189, V_3221, W_3184, X_3216, Y_3217, Z_3203, X1_3206, X2_3213, X3_3187, X4_3226, X5_3180, X6_3183, X7_3205, X8_3223, X9_3193, X10_3230, X11_3212) | ~ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3189, V_3221, W_3184, X_3216, Y_3217, Z_3203, X1_3206, X2_3213, X3_3187, X4_3226, X5_3180, X6_3183, X7_3205, X8_3223, X9_3193, X10_3230) | ~ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3189, V_3221, W_3184, X_3216, Y_3217, Z_3203, X1_3206, X2_3213, X3_3187, X4_3226, X5_3180, X6_3183, X7_3205, X8_3223, X9_3193, X10_3230, X11_3212, X12_3200, X13_3214, X14_3229, X15_3186, X16_3178, X17_3188, X18_3228, X19_3224, X20_3220, X21_3215, X22_3182, X23_3191, X24_3204, X25_3225, X26_3209, X27_3185, X28_3208, X29_3196, X30_3194, X31_3222, X32_3195, X33_3218, X34_3179, X35_3181, X36_3197) | ~ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3189, V_3221, W_3184, X_3216, Y_3217, Z_3203, X1_3206, X2_3213, X3_3187, X4_3226, X5_3180, X6_3183, X7_3205, X8_3223, X9_3193, X10_3230, X11_3212, X12_3200, X13_3214, X14_3229, X15_3186, X16_3178, X17_3188, X18_3228, X19_3224, X20_3220, X21_3215, X22_3182, X23_3191, X24_3204, X25_3225, X26_3209, X27_3185, X28_3208, X29_3196, X30_3194, X31_3222, X32_3195, X33_3218, X34_3179, X35_3181, X36_3197, X37_3219, X38_3192, X39_3207, X40_3202, X41_3227, X42_3210, X43_3199, X44_3198, X45_3211, X46_3201, X47_3190)))). % 18.13/5.73 tff(c_5317, plain, (![X29_2214, U_2208, Z_2218, X22_2201, X1_2221, X7_2220, X15_2205, X_2229, X26_2224, X5_2199, X27_2204, X11_2225, X25_2238, X19_2237, X30_2212, X28_2223, X16_2197, X14_2241, X23_2209, X9_2211, X4_2239, X12_2216, X20_2233, Y_2230, X3_2206, W_2203, X24_2219, X21_2228, X18_2240, X17_2207, X10_2242, X2_2226, V_2234, X8_2236, X13_2227, X6_2202]: (ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197, X17_2207, X18_2240, X19_2237, X20_2233, X21_2228, X22_2201, X23_2209, X24_2219) | ~ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197, X17_2207, X18_2240, X19_2237, X20_2233, X21_2228, X22_2201, X23_2209, X24_2219, X25_2238, X26_2224, X27_2204, X28_2223, X29_2214) | ~ssPv21_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197, X17_2207, X18_2240, X19_2237, X20_2233, X21_2228, X22_2201, X23_2209, X24_2219, X25_2238, X26_2224, X27_2204, X28_2223, X29_2214, X30_2212)))). % 18.13/5.73 tff(c_5090, plain, (![X19_2759, X10_2765, X14_2764, X23_2729, X1_2742, X_2751, X29_2734, Y_2752, X2_2748, X36_2735, X34_2718, X33_2753, X15_2725, X6_2722, V_2756, X39_2743, X12_2737, U_2728, X17_2727, X35_2720, X9_2731, X20_2755, X21_2750, X22_2721, X40_2738, X30_2732, X26_2745, X42_2746, X41_2762, X16_2717, W_2723, Z_2739, X24_2740, X37_2754, X31_2757, X27_2724, X18_2763, X28_2744, X8_2758, X3_2726, X4_2761, X38_2730, X25_2760, X32_2733, X11_2747, X43_2736, X13_2749, X5_2719, X7_2741]: (ssPv54_3r1r1r1(U_2728, V_2756, W_2723) | ~ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2728, V_2756, W_2723, X_2751, Y_2752, Z_2739, X1_2742, X2_2748, X3_2726, X4_2761, X5_2719, X6_2722, X7_2741, X8_2758, X9_2731, X10_2765, X11_2747, X12_2737, X13_2749, X14_2764, X15_2725, X16_2717, X17_2727, X18_2763, X19_2759, X20_2755, X21_2750, X22_2721, X23_2729) | ~ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2728, V_2756, W_2723, X_2751, Y_2752, Z_2739, X1_2742, X2_2748, X3_2726, X4_2761, X5_2719, X6_2722, X7_2741, X8_2758, X9_2731, X10_2765, X11_2747, X12_2737, X13_2749, X14_2764, X15_2725, X16_2717, X17_2727, X18_2763, X19_2759, X20_2755, X21_2750, X22_2721, X23_2729, X24_2740, X25_2760, X26_2745, X27_2724, X28_2744, X29_2734, X30_2732, X31_2757, X32_2733, X33_2753, X34_2718, X35_2720, X36_2735, X37_2754) | ~ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2728, V_2756, W_2723, X_2751, Y_2752, Z_2739, X1_2742, X2_2748, X3_2726, X4_2761, X5_2719, X6_2722, X7_2741, X8_2758, X9_2731, X10_2765, X11_2747, X12_2737, X13_2749, X14_2764, X15_2725, X16_2717, X17_2727, X18_2763, X19_2759, X20_2755, X21_2750, X22_2721, X23_2729, X24_2740, X25_2760, X26_2745, X27_2724, X28_2744, X29_2734, X30_2732, X31_2757, X32_2733, X33_2753, X34_2718, X35_2720, X36_2735, X37_2754, X38_2730, X39_2743, X40_2738, X41_2762, X42_2746, X43_2736)))). % 18.13/5.73 tff(c_5310, plain, (![X21_6582, X29_6594, X30_6584, Y_6568, X11_6596, W_6588, X26_6602, X_6590, X10_6599, V_6561, X12_6574, X16_6585, X24_6560, X19_6586, X5_6566, X4_6576, X27_6572, X28_6559, X23_6564, X18_6575, X9_6591, X22_6569, X7_6600, X8_6573, U_6567, X14_6577, X15_6589, X2_6580, X6_6603, X17_6587, Z_6593, X1_6583, X3_6578, X13_6601, X20_6595, X25_6571, X31_6565]: (ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_6567, V_6561, W_6588, X_6590, Y_6568, Z_6593, X1_6583, X2_6580, X3_6578, X4_6576, X5_6566, X6_6603, X7_6600, X8_6573, X9_6591, X10_6599, X11_6596, X12_6574, X13_6601, X14_6577, X15_6589, X16_6585, X17_6587, X18_6575, X19_6586, X20_6595, X21_6582, X22_6569, X23_6564, X24_6560, X25_6571, X26_6602, X27_6572, X28_6559, X29_6594, X30_6584, X31_6565) | ~ssPv55_2r1r1(U_6567, V_6561) | ~ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_6567, V_6561, W_6588, X_6590, Y_6568, Z_6593, X1_6583, X2_6580, X3_6578, X4_6576, X5_6566, X6_6603, X7_6600, X8_6573, X9_6591, X10_6599, X11_6596, X12_6574, X13_6601, X14_6577, X15_6589, X16_6585, X17_6587, X18_6575, X19_6586, X20_6595, X21_6582, X22_6569, X23_6564)))). % 18.13/5.73 tff(c_4652, plain, (![X13_1660, X_1662, X25_1670, X10_1674, V_1666, X23_1646, X17_1644, X34_1636, X7_1654, X18_1672, X30_1648, U_1645, X22_1638, X11_1658, Z_1652, X28_1656, W_1640, X31_1667, X15_1642, X19_1669, X29_1650, X21_1661, X9_1647, X27_1641, X3_1643, X2_1659, X12_1651, Y_1663, X14_1673, X16_1635, X32_1649, X33_1664, X20_1665, X26_1657, X6_1639, X1_1655, X4_1671, X5_1637, X8_1668, X24_1653]: (ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1645, V_1666, W_1640, X_1662, Y_1663, Z_1652, X1_1655, X2_1659, X3_1643, X4_1671, X5_1637, X6_1639, X7_1654, X8_1668, X9_1647, X10_1674, X11_1658, X12_1651, X13_1660, X14_1673, X15_1642, X16_1635, X17_1644, X18_1672, X19_1669, X20_1665, X21_1661, X22_1638, X23_1646) | ~ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1645, V_1666, W_1640, X_1662, Y_1663, Z_1652, X1_1655, X2_1659, X3_1643, X4_1671, X5_1637, X6_1639, X7_1654, X8_1668, X9_1647, X10_1674) | ~ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1645, V_1666, W_1640, X_1662, Y_1663, Z_1652, X1_1655, X2_1659, X3_1643, X4_1671, X5_1637, X6_1639, X7_1654, X8_1668, X9_1647, X10_1674, X11_1658, X12_1651, X13_1660, X14_1673) | ~ssPv17_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1645, V_1666, W_1640, X_1662, Y_1663, Z_1652, X1_1655, X2_1659, X3_1643, X4_1671, X5_1637, X6_1639, X7_1654, X8_1668, X9_1647, X10_1674, X11_1658, X12_1651, X13_1660, X14_1673, X15_1642, X16_1635, X17_1644, X18_1672, X19_1669, X20_1665, X21_1661, X22_1638, X23_1646, X24_1653, X25_1670, X26_1657, X27_1641, X28_1656, X29_1650, X30_1648, X31_1667, X32_1649, X33_1664, X34_1636)))). % 18.13/5.73 tff(c_5303, plain, (![U_2208, Z_2218, X1_2221, X7_2220, X15_2205, X_2229, X5_2199, X11_2225, X16_2197, X14_2241, X9_2211, X4_2239, X12_2216, Y_2230, X3_2206, W_2203, X10_2242, X2_2226, V_2234, X8_2236, X13_2227, X6_2202]: (ssPv50_7r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221) | ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220) | ~ssPv35_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197)))). % 18.13/5.73 tff(c_5096, plain, (![X13_2799, X31_2807, X7_2791, X14_2814, X4_2811, X40_2788, X12_2787, X11_2797, X42_2796, X24_2790, X29_2783, X33_2803, X43_2786, X21_2800, X18_2813, X28_2794, X5_2768, X32_2782, Y_2802, X23_2778, X38_2779, X3_2775, X17_2776, V_2806, X34_2767, X6_2771, X9_2780, W_2772, X20_2805, X35_2769, X_2801, X44_2785, X2_2798, X1_2792, X26_2795, X15_2774, X25_2810, X37_2804, X30_2781, X16_2766, X27_2773, Z_2789, X22_2770, X39_2793, X10_2815, X41_2812, X8_2808, X36_2784, U_2777, X19_2809]: (ssPv52_5r1r1r1r1r1(U_2777, V_2806, W_2772, X_2801, Y_2802) | ssPv48_9r1r1r1r1r1r1r1r1r1(U_2777, V_2806, W_2772, X_2801, Y_2802, Z_2789, X1_2792, X2_2798, X3_2775) | ~ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2777, V_2806, W_2772, X_2801, Y_2802, Z_2789, X1_2792, X2_2798, X3_2775, X4_2811, X5_2768, X6_2771, X7_2791, X8_2808, X9_2780, X10_2815, X11_2797, X12_2787, X13_2799, X14_2814, X15_2774, X16_2766, X17_2776, X18_2813, X19_2809) | ~ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2777, V_2806, W_2772, X_2801, Y_2802, Z_2789, X1_2792, X2_2798, X3_2775, X4_2811, X5_2768, X6_2771, X7_2791, X8_2808, X9_2780, X10_2815, X11_2797, X12_2787, X13_2799, X14_2814, X15_2774, X16_2766, X17_2776, X18_2813, X19_2809, X20_2805, X21_2800, X22_2770, X23_2778, X24_2790, X25_2810, X26_2795, X27_2773, X28_2794, X29_2783, X30_2781, X31_2807, X32_2782, X33_2803, X34_2767, X35_2769, X36_2784, X37_2804, X38_2779, X39_2793, X40_2788, X41_2812, X42_2796, X43_2786, X44_2785)))). % 18.13/5.73 tff(c_5296, plain, (![Y_164, X_163, U_158, V_165, Z_159, W_156]: (~ssPv54_3r1r1r1(U_158, V_165, W_156) | ~ssPv51_6r1r1r1r1r1r1(U_158, V_165, W_156, X_163, Y_164, Z_159)))). % 18.13/5.73 tff(c_5178, plain, (![X26_3262, X37_3274, X29_3249, X10_3285, X19_3279, V_3276, X34_3232, X40_3255, X47_3243, X1_3259, X13_3269, X42_3264, X35_3234, X25_3280, X31_3277, X2_3268, X30_3247, X39_3260, Z_3256, X21_3270, U_3242, X14_3284, X18_3283, X24_3257, X15_3239, X27_3238, X11_3266, X28_3261, X49_3263, X43_3252, X8_3278, X32_3248, X5_3233, W_3237, X7_3258, X45_3265, X41_3282, X9_3246, Y_3272, X48_3267, X38_3245, X_3271, X4_3281, X46_3254, X20_3275, X33_3273, X36_3250, X22_3235, X23_3244, X16_3231, X12_3253, X44_3251, X6_3236, X3_3240, X17_3241]: (ssNder1_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3242, V_3276, W_3237, X_3271, Y_3272, Z_3256, X1_3259, X2_3268, X3_3240, X4_3281, X5_3233, X6_3236, X7_3258, X8_3278, X9_3246, X10_3285, X11_3266, X12_3253, X13_3269, X14_3284, X15_3239, X16_3231, X17_3241, X18_3283, X19_3279, X20_3275, X21_3270, X22_3235, X23_3244, X24_3257, X25_3280, X26_3262, X27_3238, X28_3261, X29_3249, X30_3247, X31_3277, X32_3248, X33_3273, X34_3232, X35_3234, X36_3250, X37_3274, X38_3245, X39_3260, X40_3255, X41_3282, X42_3264, X43_3252, X44_3251, X45_3265, X46_3254, X47_3243, X48_3267, X49_3263)))). % 18.13/5.73 tff(c_5168, plain, (![X41_3122, X35_3075, W_3078, X1_3100, X39_3101, X8_3118, X21_3110, X40_3096, X18_3123, X15_3080, X29_3090, X34_3073, X13_3109, X11_3106, X36_3091, X30_3088, X19_3119, X25_3120, X4_3121, X37_3114, X22_3076, X_3111, X46_3095, X38_3086, X20_3115, X23_3085, X16_3072, X42_3104, X44_3092, X7_3099, X6_3077, U_3083, X28_3102, X24_3098, X5_3074, Y_3112, X45_3105, X12_3094, X27_3079, X14_3124, X47_3084, X9_3087, X3_3081, X48_3107, V_3116, X17_3082, X26_3103, Z_3097, X43_3093, X10_3125, X32_3089, X33_3113, X31_3117, X2_3108]: (ssNder1_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3083, V_3116, W_3078, X_3111, Y_3112, Z_3097, X1_3100, X2_3108, X3_3081, X4_3121, X5_3074, X6_3077, X7_3099, X8_3118, X9_3087, X10_3125, X11_3106, X12_3094, X13_3109, X14_3124, X15_3080, X16_3072, X17_3082, X18_3123, X19_3119, X20_3115, X21_3110, X22_3076, X23_3085, X24_3098, X25_3120, X26_3103, X27_3079, X28_3102, X29_3090, X30_3088, X31_3117, X32_3089, X33_3113, X34_3073, X35_3075, X36_3091, X37_3114, X38_3086, X39_3101, X40_3096, X41_3122, X42_3104, X43_3093, X44_3092, X45_3105, X46_3095, X47_3084, X48_3107)))). % 18.13/5.73 tff(c_5162, plain, (![X42_3051, X18_3069, X16_3019, X10_3071, X5_3021, V_3062, X20_3061, X19_3065, X36_3038, X15_3027, X11_3053, Z_3044, X9_3034, X35_3022, X14_3070, X8_3064, X21_3056, X24_3045, X31_3063, X17_3029, X39_3048, X44_3039, X29_3037, X37_3060, X34_3020, X47_3031, X28_3049, X27_3026, X12_3041, U_3030, X38_3033, X22_3023, X25_3066, W_3025, X32_3036, X23_3032, X43_3040, X3_3028, X13_3055, X4_3067, X1_3047, X30_3035, X40_3043, X33_3059, X6_3024, X2_3054, X26_3050, X41_3068, X_3057, X7_3046, X46_3042, Y_3058, X45_3052]: (ssNder1_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_3030, V_3062, W_3025, X_3057, Y_3058, Z_3044, X1_3047, X2_3054, X3_3028, X4_3067, X5_3021, X6_3024, X7_3046, X8_3064, X9_3034, X10_3071, X11_3053, X12_3041, X13_3055, X14_3070, X15_3027, X16_3019, X17_3029, X18_3069, X19_3065, X20_3061, X21_3056, X22_3023, X23_3032, X24_3045, X25_3066, X26_3050, X27_3026, X28_3049, X29_3037, X30_3035, X31_3063, X32_3036, X33_3059, X34_3020, X35_3022, X36_3038, X37_3060, X38_3033, X39_3048, X40_3043, X41_3068, X42_3051, X43_3040, X44_3039, X45_3052, X46_3042, X47_3031)))). % 18.13/5.73 tff(c_5148, plain, (![X24_2992, X_3004, X37_3007, X42_2998, X14_3017, X2_3001, X23_2979, X36_2985, X38_2980, X13_3002, X4_3014, X46_2989, X16_2967, U_2978, W_2973, X39_2995, Y_3005, X33_3006, X19_3012, X41_3015, X40_2990, X22_2971, X35_2970, X44_2986, X18_3016, X30_2982, X9_2981, X26_2997, X32_2983, X5_2969, X28_2996, X17_2977, X34_2968, X15_2975, X20_3008, X29_2984, X6_2972, X31_3010, X1_2994, X27_2974, X43_2987, X7_2993, Z_2991, V_3009, X8_3011, X45_2999, X21_3003, X10_3018, X11_3000, X25_3013, X12_2988, X3_2976]: (ssNder1_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2978, V_3009, W_2973, X_3004, Y_3005, Z_2991, X1_2994, X2_3001, X3_2976, X4_3014, X5_2969, X6_2972, X7_2993, X8_3011, X9_2981, X10_3018, X11_3000, X12_2988, X13_3002, X14_3017, X15_2975, X16_2967, X17_2977, X18_3016, X19_3012, X20_3008, X21_3003, X22_2971, X23_2979, X24_2992, X25_3013, X26_2997, X27_2974, X28_2996, X29_2984, X30_2982, X31_3010, X32_2983, X33_3006, X34_2968, X35_2970, X36_2985, X37_3007, X38_2980, X39_2995, X40_2990, X41_3015, X42_2998, X43_2987, X44_2986, X45_2999, X46_2989)))). % 18.13/5.73 tff(c_5138, plain, (![X21_2851, X38_2829, X36_2834, X32_2832, X27_2823, X14_2865, X2_2849, X11_2848, X12_2837, Z_2839, X31_2858, X33_2854, X44_2835, X40_2838, X39_2843, X41_2863, X20_2856, Y_2853, X29_2833, X5_2818, X43_2836, X_2852, X3_2825, X13_2850, X28_2844, X16_2816, X6_2821, X9_2830, V_2857, X15_2824, X34_2817, X7_2841, X18_2864, X35_2819, X23_2828, X30_2831, X8_2859, U_2827, X1_2842, X17_2826, X42_2846, X26_2845, X24_2840, X22_2820, X25_2861, X45_2847, X37_2855, X19_2860, W_2822, X10_2866, X4_2862]: (ssNder1_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2827, V_2857, W_2822, X_2852, Y_2853, Z_2839, X1_2842, X2_2849, X3_2825, X4_2862, X5_2818, X6_2821, X7_2841, X8_2859, X9_2830, X10_2866, X11_2848, X12_2837, X13_2850, X14_2865, X15_2824, X16_2816, X17_2826, X18_2864, X19_2860, X20_2856, X21_2851, X22_2820, X23_2828, X24_2840, X25_2861, X26_2845, X27_2823, X28_2844, X29_2833, X30_2831, X31_2858, X32_2832, X33_2854, X34_2817, X35_2819, X36_2834, X37_2855, X38_2829, X39_2843, X40_2838, X41_2863, X42_2846, X43_2836, X44_2835, X45_2847)))). % 18.13/5.73 tff(c_5114, plain, (![X22_2671, X13_2700, X1_2693, X25_2711, X30_2682, X26_2696, X23_2679, X36_2685, X28_2695, U_2678, X15_2675, X18_2714, X43_2687, W_2673, X16_2667, X11_2698, X8_2709, X31_2708, X37_2705, X27_2674, X24_2691, X34_2668, X35_2670, X41_2713, Y_2703, X39_2694, Z_2690, X4_2712, X29_2684, X3_2676, X38_2680, X40_2689, X12_2688, X20_2706, X10_2716, X19_2710, X32_2683, V_2707, X21_2701, X44_2686, X6_2672, X42_2697, X17_2677, X2_2699, X9_2681, X_2702, X14_2715, X33_2704, X7_2692, X5_2669]: (ssNder1_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2678, V_2707, W_2673, X_2702, Y_2703, Z_2690, X1_2693, X2_2699, X3_2676, X4_2712, X5_2669, X6_2672, X7_2692, X8_2709, X9_2681, X10_2716, X11_2698, X12_2688, X13_2700, X14_2715, X15_2675, X16_2667, X17_2677, X18_2714, X19_2710, X20_2706, X21_2701, X22_2671, X23_2679, X24_2691, X25_2711, X26_2696, X27_2674, X28_2695, X29_2684, X30_2682, X31_2708, X32_2683, X33_2704, X34_2668, X35_2670, X36_2685, X37_2705, X38_2680, X39_2694, X40_2689, X41_2713, X42_2697, X43_2687, X44_2686)))). % 18.13/5.73 tff(c_5058, plain, (![X40_2592, W_2577, X6_2576, X16_2571, X38_2584, X13_2603, X35_2574, X42_2600, X26_2599, X10_2619, X25_2614, X15_2579, X39_2597, X19_2613, X21_2604, X43_2590, X4_2615, X3_2580, X18_2617, X37_2608, X41_2616, X33_2607, X8_2612, X5_2573, X36_2589, X34_2572, Z_2593, X23_2583, X20_2609, X32_2587, U_2582, X27_2578, V_2610, X17_2581, X_2605, X28_2598, X14_2618, X22_2575, Y_2606, X11_2601, X31_2611, X29_2588, X30_2586, X24_2594, X2_2602, X9_2585, X7_2595, X1_2596, X12_2591]: (ssNder1_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2582, V_2610, W_2577, X_2605, Y_2606, Z_2593, X1_2596, X2_2602, X3_2580, X4_2615, X5_2573, X6_2576, X7_2595, X8_2612, X9_2585, X10_2619, X11_2601, X12_2591, X13_2603, X14_2618, X15_2579, X16_2571, X17_2581, X18_2617, X19_2613, X20_2609, X21_2604, X22_2575, X23_2583, X24_2594, X25_2614, X26_2599, X27_2578, X28_2598, X29_2588, X30_2586, X31_2611, X32_2587, X33_2607, X34_2572, X35_2574, X36_2589, X37_2608, X38_2584, X39_2597, X40_2592, X41_2616, X42_2600, X43_2590)))). % 18.13/5.73 tff(c_4992, plain, (![X26_2410, X30_2398, X41_2426, W_2389, X38_2396, X15_2391, X18_2427, X6_2388, X19_2423, X22_2387, X16_2383, X3_2392, X13_2413, X7_2406, X36_2401, X35_2386, X14_2428, Y_2416, X10_2429, X27_2390, X40_2403, X21_2414, X32_2399, X5_2385, X33_2417, X39_2408, X2_2412, V_2420, X4_2425, X1_2407, X8_2422, U_2394, Z_2404, X_2415, X29_2400, X37_2418, X20_2419, X31_2421, X25_2424, X11_2411, X24_2405, X12_2402, X17_2393, X28_2409, X23_2395, X34_2384, X9_2397]: (~ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2394, V_2420, W_2389, X_2415, Y_2416, Z_2404, X1_2407, X2_2412, X3_2392, X4_2425, X5_2385, X6_2388, X7_2406, X8_2422, X9_2397, X10_2429, X11_2411, X12_2402, X13_2413, X14_2428, X15_2391, X16_2383, X17_2393, X18_2427, X19_2423, X20_2419, X21_2414, X22_2387, X23_2395, X24_2405, X25_2424, X26_2410, X27_2390, X28_2409, X29_2400, X30_2398, X31_2421, X32_2399, X33_2417, X34_2384, X35_2386, X36_2401, X37_2418, X38_2396, X39_2408, X40_2403, X41_2426, skc39)))). % 18.13/5.73 tff(c_5028, plain, (![X41_2567, X3_2532, X8_2563, X31_2562, X1_2547, X23_2535, X39_2548, X21_2555, W_2529, X28_2549, X34_2524, X40_2543, X38_2536, X4_2566, X14_2569, X_2556, V_2561, X19_2564, X18_2568, X33_2558, X35_2526, Z_2544, X29_2540, X13_2554, X2_2553, X6_2528, X37_2559, X32_2539, X24_2545, X11_2552, X15_2531, Y_2557, X16_2523, X9_2537, U_2534, X27_2530, X7_2546, X22_2527, X12_2542, X42_2551, X26_2550, X25_2565, X10_2570, X30_2538, X17_2533, X36_2541, X20_2560, X5_2525]: (ssNder1_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2534, V_2561, W_2529, X_2556, Y_2557, Z_2544, X1_2547, X2_2553, X3_2532, X4_2566, X5_2525, X6_2528, X7_2546, X8_2563, X9_2537, X10_2570, X11_2552, X12_2542, X13_2554, X14_2569, X15_2531, X16_2523, X17_2533, X18_2568, X19_2564, X20_2560, X21_2555, X22_2527, X23_2535, X24_2545, X25_2565, X26_2550, X27_2530, X28_2549, X29_2540, X30_2538, X31_2562, X32_2539, X33_2558, X34_2524, X35_2526, X36_2541, X37_2559, X38_2536, X39_2548, X40_2543, X41_2567, X42_2551)))). % 18.13/5.73 tff(c_4548, plain, (![X1_1492, X_1499, X27_1478, X14_1510, X10_1511, X5_1474, X26_1494, X24_1490, X16_1473, X19_1506, Z_1489, X23_1483, V_1503, X21_1498, X13_1497, X31_1504, X29_1487, X30_1485, X15_1479, X28_1493, X25_1507, X22_1475, X33_1501, X4_1508, X7_1491, W_1477, X11_1495, X3_1480, X18_1509, X32_1486, X9_1484, X8_1505, X6_1476, X12_1488, X2_1496, Y_1500, X20_1502, U_1482, X17_1481]: (ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1482, V_1503, W_1477, X_1499, Y_1500, Z_1489, X1_1492, X2_1496, X3_1480, X4_1508, X5_1474, X6_1476, X7_1491, X8_1505, X9_1484) | ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1482, V_1503, W_1477, X_1499, Y_1500, Z_1489, X1_1492, X2_1496, X3_1480, X4_1508, X5_1474, X6_1476, X7_1491, X8_1505, X9_1484, X10_1511, X11_1495, X12_1488, X13_1497, X14_1510, X15_1479, X16_1473, X17_1481, X18_1509, X19_1506, X20_1502, X21_1498, X22_1475, X23_1483, X24_1490, X25_1507, X26_1494, X27_1478, X28_1493) | ~ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1482, V_1503, W_1477, X_1499, Y_1500, Z_1489, X1_1492, X2_1496, X3_1480, X4_1508, X5_1474, X6_1476, X7_1491, X8_1505) | ~ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1482, V_1503, W_1477, X_1499, Y_1500, Z_1489, X1_1492, X2_1496, X3_1480, X4_1508, X5_1474, X6_1476, X7_1491, X8_1505, X9_1484, X10_1511, X11_1495, X12_1488, X13_1497, X14_1510, X15_1479, X16_1473, X17_1481, X18_1509, X19_1506, X20_1502, X21_1498, X22_1475, X23_1483, X24_1490, X25_1507, X26_1494, X27_1478, X28_1493, X29_1487, X30_1485, X31_1504, X32_1486, X33_1501)))). % 18.13/5.73 tff(c_5000, plain, (![X28_2362, X13_2366, X17_2346, X41_2379, X19_2376, X5_2338, X24_2358, X11_2364, X7_2359, X4_2378, X36_2354, X38_2349, Z_2357, X20_2372, X34_2337, X18_2380, V_2373, X29_2353, X22_2340, Y_2369, W_2342, X8_2375, X21_2367, X15_2344, X16_2336, X26_2363, X40_2356, X10_2382, X14_2381, X27_2343, X2_2365, X37_2371, X12_2355, X1_2360, X30_2351, X35_2339, U_2347, X39_2361, X23_2348, X3_2345, X25_2377, X31_2374, X_2368, X33_2370, X9_2350, X6_2341, X32_2352]: (ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2347, V_2373, W_2342, X_2368, Y_2369, Z_2357, X1_2360, X2_2365, X3_2345, X4_2378, X5_2338, X6_2341, X7_2359, X8_2375, X9_2350, X10_2382, X11_2364, X12_2355, X13_2366, X14_2381, X15_2344, X16_2336, X17_2346, X18_2380, X19_2376, X20_2372, X21_2367, X22_2340, X23_2348, X24_2358, X25_2377, X26_2363, X27_2343, X28_2362, X29_2353, X30_2351, X31_2374, X32_2352, X33_2370, X34_2337, X35_2339, X36_2354, X37_2371, X38_2349, X39_2361, X40_2356, X41_2379, skc38)))). % 18.13/5.73 tff(c_4982, plain, (![X3_2298, X35_2292, X38_2302, X23_2301, X15_2297, X32_2305, X_2321, X12_2308, Y_2322, X41_2332, X4_2331, X11_2317, Z_2310, X7_2312, X31_2327, X1_2313, X24_2311, X39_2314, X20_2325, X5_2291, X8_2328, X18_2333, V_2326, X16_2289, X34_2290, X21_2320, X36_2307, X17_2299, X27_2296, X14_2334, X13_2319, W_2295, X28_2315, X33_2323, X30_2304, X10_2335, U_2300, X9_2303, X19_2329, X22_2293, X29_2306, X40_2309, X25_2330, X37_2324, X6_2294, X26_2316, X2_2318]: (ssNder1_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2300, V_2326, W_2295, X_2321, Y_2322, Z_2310, X1_2313, X2_2318, X3_2298, X4_2331, X5_2291, X6_2294, X7_2312, X8_2328, X9_2303, X10_2335, X11_2317, X12_2308, X13_2319, X14_2334, X15_2297, X16_2289, X17_2299, X18_2333, X19_2329, X20_2325, X21_2320, X22_2293, X23_2301, X24_2311, X25_2330, X26_2316, X27_2296, X28_2315, X29_2306, X30_2304, X31_2327, X32_2305, X33_2323, X34_2290, X35_2292, X36_2307, X37_2324, X38_2302, X39_2314, X40_2309, X41_2332)))). % 18.13/5.73 tff(c_4956, plain, (![X34_2198, X35_2200, X39_2222, X29_2214, U_2208, Z_2218, X22_2201, X1_2221, X7_2220, X15_2205, X_2229, X26_2224, X5_2199, X27_2204, X11_2225, X25_2238, X19_2237, X30_2212, X40_2217, X28_2223, X16_2197, X14_2241, X32_2213, X23_2209, X9_2211, X4_2239, X12_2216, X20_2233, Y_2230, X3_2206, W_2203, X24_2219, X21_2228, X18_2240, X37_2232, X33_2231, X17_2207, X36_2215, X10_2242, X2_2226, X31_2235, X38_2210, V_2234, X8_2236, X13_2227, X6_2202]: (ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2208, V_2234, W_2203, X_2229, Y_2230, Z_2218, X1_2221, X2_2226, X3_2206, X4_2239, X5_2199, X6_2202, X7_2220, X8_2236, X9_2211, X10_2242, X11_2225, X12_2216, X13_2227, X14_2241, X15_2205, X16_2197, X17_2207, X18_2240, X19_2237, X20_2233, X21_2228, X22_2201, X23_2209, X24_2219, X25_2238, X26_2224, X27_2204, X28_2223, X29_2214, X30_2212, X31_2235, X32_2213, X33_2231, X34_2198, X35_2200, X36_2215, X37_2232, X38_2210, X39_2222, X40_2217, skc40)))). % 18.13/5.73 tff(c_4968, plain, (![X9_2257, X23_2255, X40_2263, X19_2283, X24_2265, X27_2250, X1_2267, X15_2251, X25_2284, X22_2247, X6_2248, W_2249, X29_2260, X11_2271, X10_2288, X13_2273, X34_2244, X20_2279, X39_2268, X18_2286, V_2280, X36_2261, U_2254, X5_2245, X7_2266, X33_2277, X38_2256, X17_2253, X30_2258, X16_2243, X4_2285, X14_2287, X8_2282, X2_2272, X_2275, X32_2259, X28_2269, X31_2281, Y_2276, Z_2264, X3_2252, X12_2262, X21_2274, X35_2246, X37_2278, X26_2270]: (~ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2254, V_2280, W_2249, X_2275, Y_2276, Z_2264, X1_2267, X2_2272, X3_2252, X4_2285, X5_2245, X6_2248, X7_2266, X8_2282, X9_2257, X10_2288, X11_2271, X12_2262, X13_2273, X14_2287, X15_2251, X16_2243, X17_2253, X18_2286, X19_2283, X20_2279, X21_2274, X22_2247, X23_2255, X24_2265, X25_2284, X26_2270, X27_2250, X28_2269, X29_2260, X30_2258, X31_2281, X32_2259, X33_2277, X34_2244, X35_2246, X36_2261, X37_2278, X38_2256, X39_2268, X40_2263, skc41)))). % 18.13/5.73 tff(c_4918, plain, (![X_2183, X24_2173, X23_2163, X38_2164, X7_2174, V_2188, X19_2191, X37_2186, X13_2181, W_2157, X11_2179, X20_2187, X21_2182, Y_2184, X18_2194, X27_2158, X17_2161, X28_2177, X32_2167, X33_2185, X35_2154, X26_2178, X15_2159, X3_2160, X40_2171, X16_2151, X12_2170, X36_2169, X6_2156, X25_2192, U_2162, X5_2153, X9_2165, X39_2176, X34_2152, X10_2196, X29_2168, X4_2193, X22_2155, X14_2195, X8_2190, X31_2189, X1_2175, X2_2180, Z_2172, X30_2166]: (ssNder1_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2162, V_2188, W_2157, X_2183, Y_2184, Z_2172, X1_2175, X2_2180, X3_2160, X4_2193, X5_2153, X6_2156, X7_2174, X8_2190, X9_2165, X10_2196, X11_2179, X12_2170, X13_2181, X14_2195, X15_2159, X16_2151, X17_2161, X18_2194, X19_2191, X20_2187, X21_2182, X22_2155, X23_2163, X24_2173, X25_2192, X26_2178, X27_2158, X28_2177, X29_2168, X30_2166, X31_2189, X32_2167, X33_2185, X34_2152, X35_2154, X36_2169, X37_2186, X38_2164, X39_2176, X40_2171)))). % 18.13/5.73 tff(c_4896, plain, (![X39_2085, X38_2074, X19_2100, X33_2094, X_2092, X25_2101, X20_2096, Y_2093, X34_2062, X26_2087, X28_2086, X35_2064, X36_2079, X37_2095, X10_2105, U_2072, X24_2082, V_2097, X29_2078, X3_2070, X23_2073, X15_2069, X4_2102, X31_2098, X22_2065, X30_2076, X1_2084, X32_2077, X16_2061, X5_2063, X21_2091, X27_2068, X17_2071, X9_2075, X6_2066, X14_2104, X13_2090, X18_2103, X12_2080, X7_2083, X11_2088, W_2067, X8_2099, X2_2089, Z_2081]: (ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2072, V_2097, W_2067, X_2092, Y_2093, Z_2081, X1_2084, X2_2089, X3_2070, X4_2102, X5_2063, X6_2066, X7_2083, X8_2099, X9_2075, X10_2105, X11_2088, X12_2080, X13_2090, X14_2104, X15_2069, X16_2061, X17_2071, X18_2103, X19_2100, X20_2096, X21_2091, X22_2065, X23_2073, X24_2082, X25_2101, X26_2087, X27_2068, X28_2086, X29_2078, X30_2076, X31_2098, X32_2077, X33_2094, X34_2062, X35_2064, X36_2079, X37_2095, X38_2074, X39_2085, skc42)))). % 18.13/5.73 tff(c_4946, plain, (![X13_2135, X29_2123, X22_2110, X1_2129, X7_2128, X35_2109, X27_2113, X28_2131, X24_2127, X11_2133, X4_2147, X19_2145, X39_2130, X33_2139, X36_2124, Y_2138, X_2137, V_2142, X8_2144, X37_2140, Z_2126, X5_2108, X14_2149, X20_2141, X10_2150, X18_2148, X6_2111, U_2117, X32_2122, X25_2146, X21_2136, X9_2120, X15_2114, W_2112, X34_2107, X31_2143, X12_2125, X17_2116, X3_2115, X16_2106, X23_2118, X26_2132, X2_2134, X38_2119, X30_2121]: (~ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2117, V_2142, W_2112, X_2137, Y_2138, Z_2126, X1_2129, X2_2134, X3_2115, X4_2147, X5_2108, X6_2111, X7_2128, X8_2144, X9_2120, X10_2150, X11_2133, X12_2125, X13_2135, X14_2149, X15_2114, X16_2106, X17_2116, X18_2148, X19_2145, X20_2141, X21_2136, X22_2110, X23_2118, X24_2127, X25_2146, X26_2132, X27_2113, X28_2131, X29_2123, X30_2121, X31_2143, X32_2122, X33_2139, X34_2107, X35_2109, X36_2124, X37_2140, X38_2119, X39_2130, skc43)))). % 18.13/5.74 tff(c_4910, plain, (![X28_2041, X31_2053, X39_2040, X4_2057, X13_2045, X22_2020, X26_2042, Y_2048, X7_2038, X1_2039, X24_2037, X33_2049, W_2022, Z_2036, X20_2051, X9_2030, X_2047, X5_2018, X2_2044, X16_2016, X3_2025, X8_2054, X32_2032, X38_2029, X6_2021, X17_2026, X19_2055, U_2027, X35_2019, X37_2050, X10_2060, X12_2035, X18_2058, V_2052, X36_2034, X23_2028, X27_2023, X15_2024, X11_2043, X21_2046, X30_2031, X25_2056, X34_2017, X29_2033, X14_2059]: (ssNder1_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_2027, V_2052, W_2022, X_2047, Y_2048, Z_2036, X1_2039, X2_2044, X3_2025, X4_2057, X5_2018, X6_2021, X7_2038, X8_2054, X9_2030, X10_2060, X11_2043, X12_2035, X13_2045, X14_2059, X15_2024, X16_2016, X17_2026, X18_2058, X19_2055, X20_2051, X21_2046, X22_2020, X23_2028, X24_2037, X25_2056, X26_2042, X27_2023, X28_2041, X29_2033, X30_2031, X31_2053, X32_2032, X33_2049, X34_2017, X35_2019, X36_2034, X37_2050, X38_2029, X39_2040)))). % 18.13/5.74 tff(c_4792, plain, (![X35_1932, X15_1937, X21_1957, X_1958, X6_1934, X36_1946, X24_1949, X30_1943, X8_1965, U_1940, X12_1947, X20_1962, X32_1944, X11_1954, X28_1952, X25_1967, X9_1942, X19_1966, X31_1964, X3_1938, X37_1961, Z_1948, X26_1953, X29_1945, X7_1950, X1_1951, X17_1939, V_1963, X4_1968, X22_1933, X16_1929, X5_1931, X33_1960, X27_1936, X10_1971, X23_1941, X13_1956, X34_1930, W_1935, X18_1969, Y_1959, X14_1970, X2_1955]: (~ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1940, V_1963, W_1935, X_1958, Y_1959, Z_1948, X1_1951, X2_1955, X3_1938, X4_1968, X5_1931, X6_1934, X7_1950, X8_1965, X9_1942, X10_1971, X11_1954, X12_1947, X13_1956, X14_1970, X15_1937, X16_1929, X17_1939, X18_1969, X19_1966, X20_1962, X21_1957, X22_1933, X23_1941, X24_1949, X25_1967, X26_1953, X27_1936, X28_1952, X29_1945, X30_1943, X31_1964, X32_1944, X33_1960, X34_1930, X35_1932, X36_1946, X37_1961, skc45)))). % 18.13/5.74 tff(c_4208, plain, (![X25_1198, X7_1184, X4_1199, X8_1196, X2_1189, X15_1174, X18_1200, X10_1202, X27_1173, W_1172, Y_1193, X12_1181, X3_1175, X26_1187, X28_1186, X14_1201, U_1177, X24_1183, X6_1171, X9_1179, X29_1180, X20_1194, X23_1178, X_1192, X19_1197, X16_1168, X22_1170, X5_1169, X17_1176, X1_1185, V_1195, X21_1191, X13_1190, X11_1188, Z_1182]: (ssPv48_9r1r1r1r1r1r1r1r1r1(U_1177, V_1195, W_1172, X_1192, Y_1193, Z_1182, X1_1185, X2_1189, X3_1175) | ssPv31_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1177, V_1195, W_1172, X_1192, Y_1193, Z_1182, X1_1185, X2_1189, X3_1175, X4_1199, X5_1169, X6_1171, X7_1184, X8_1196, X9_1179, X10_1202, X11_1188, X12_1181, X13_1190, X14_1201, X15_1174, X16_1168, X17_1176, X18_1200, X19_1197, X20_1194) | ~ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1177, V_1195, W_1172, X_1192, Y_1193, Z_1182, X1_1185, X2_1189, X3_1175, X4_1199, X5_1169, X6_1171, X7_1184, X8_1196, X9_1179, X10_1202, X11_1188, X12_1181, X13_1190) | ~ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1177, V_1195, W_1172, X_1192, Y_1193, Z_1182, X1_1185, X2_1189, X3_1175, X4_1199, X5_1169, X6_1171, X7_1184, X8_1196, X9_1179, X10_1202, X11_1188, X12_1181, X13_1190, X14_1201, X15_1174, X16_1168, X17_1176, X18_1200, X19_1197, X20_1194, X21_1191, X22_1170, X23_1178, X24_1183, X25_1198, X26_1187, X27_1173, X28_1186, X29_1180)))). % 18.13/5.74 tff(c_4810, plain, (![X12_1904, X33_1917, X30_1900, X16_1886, X22_1890, X9_1899, X3_1895, U_1897, X28_1909, X27_1893, X4_1925, X37_1918, X13_1913, X23_1898, W_1892, Z_1905, X2_1912, X29_1902, X11_1911, X21_1914, X10_1928, X25_1924, X32_1901, X34_1887, X1_1908, V_1920, X35_1889, X24_1906, X36_1903, X31_1921, Y_1916, X8_1922, X14_1927, X18_1926, X20_1919, X19_1923, X_1915, X17_1896, X15_1894, X26_1910, X7_1907, X5_1888, X6_1891]: (ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1897, V_1920, W_1892, X_1915, Y_1916, Z_1905, X1_1908, X2_1912, X3_1895, X4_1925, X5_1888, X6_1891, X7_1907, X8_1922, X9_1899, X10_1928, X11_1911, X12_1904, X13_1913, X14_1927, X15_1894, X16_1886, X17_1896, X18_1926, X19_1923, X20_1919, X21_1914, X22_1890, X23_1898, X24_1906, X25_1924, X26_1910, X27_1893, X28_1909, X29_1902, X30_1900, X31_1921, X32_1901, X33_1917, X34_1887, X35_1889, X36_1903, X37_1918, skc44)))). % 18.13/5.74 tff(c_4876, plain, (![X21_2001, X26_1997, X18_2013, X12_1991, X13_2000, X16_1972, X3_1981, X14_2014, X31_2008, X25_2011, X30_1987, Z_1992, X7_1994, X37_2005, X32_1988, X10_2015, X23_1984, X35_1975, X11_1998, X9_1986, X36_1990, X2_1999, X29_1989, Y_2003, X33_2004, X6_1977, X38_1985, U_1983, X27_1979, X22_1976, X_2002, V_2007, X20_2006, X19_2010, X24_1993, X17_1982, X15_1980, X28_1996, W_1978, X4_2012, X1_1995, X8_2009, X34_1973, X5_1974]: (ssNder1_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1983, V_2007, W_1978, X_2002, Y_2003, Z_1992, X1_1995, X2_1999, X3_1981, X4_2012, X5_1974, X6_1977, X7_1994, X8_2009, X9_1986, X10_2015, X11_1998, X12_1991, X13_2000, X14_2014, X15_1980, X16_1972, X17_1982, X18_2013, X19_2010, X20_2006, X21_2001, X22_1976, X23_1984, X24_1993, X25_2011, X26_1997, X27_1979, X28_1996, X29_1989, X30_1987, X31_2008, X32_1988, X33_2004, X34_1973, X35_1975, X36_1990, X37_2005, X38_1985)))). % 18.13/5.74 tff(c_4764, plain, (![X13_1870, X30_1857, X26_1867, X35_1846, X17_1853, X6_1848, Z_1862, W_1849, X27_1850, X15_1851, X8_1879, X16_1843, X25_1881, X9_1856, X31_1878, X1_1865, X21_1871, X7_1864, X18_1883, X22_1847, X36_1860, X28_1866, X23_1855, X34_1844, X19_1880, X24_1863, X5_1845, X12_1861, X11_1868, X37_1875, X32_1858, X20_1876, X33_1874, X14_1884, X10_1885, X4_1882, Y_1873, V_1877, X29_1859, U_1854, X3_1852, X_1872, X2_1869]: (ssNder1_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1854, V_1877, W_1849, X_1872, Y_1873, Z_1862, X1_1865, X2_1869, X3_1852, X4_1882, X5_1845, X6_1848, X7_1864, X8_1879, X9_1856, X10_1885, X11_1868, X12_1861, X13_1870, X14_1884, X15_1851, X16_1843, X17_1853, X18_1883, X19_1880, X20_1876, X21_1871, X22_1847, X23_1855, X24_1863, X25_1881, X26_1867, X27_1850, X28_1866, X29_1859, X30_1857, X31_1878, X32_1858, X33_1874, X34_1844, X35_1846, X36_1860, X37_1875)))). % 18.13/5.74 tff(c_4808, plain, (![X14_1757, X3_1726, Z_1736, X2_1743, X20_1749, X15_1725, X13_1744, X29_1733, X17_1727, X24_1737, X27_1724, X16_1717, X26_1741, X30_1731, U_1728, V_1750, X1_1739, X23_1729, X8_1752, X4_1755, X5_1719, X33_1748, X34_1718, X6_1722, W_1723, X25_1754, X31_1751, X9_1730, X36_1734, X19_1753, X32_1732, X_1746, Y_1747, X21_1745, X18_1756, X11_1742, X10_1758, X7_1738, X12_1735, X35_1720, X28_1740, X22_1721]: (ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1728, V_1750, W_1723, X_1746, Y_1747, Z_1736, X1_1739, X2_1743, X3_1726, X4_1755, X5_1719, X6_1722, X7_1738, X8_1752, X9_1730, X10_1758, X11_1742, X12_1735, X13_1744, X14_1757, X15_1725, X16_1717, X17_1727, X18_1756, X19_1753, X20_1749, X21_1745, X22_1721, X23_1729, X24_1737, X25_1754, X26_1741, X27_1724, X28_1740, X29_1733, X30_1731, X31_1751, X32_1732, X33_1748, X34_1718, X35_1720, X36_1734, skc46)))). % 18.13/5.74 tff(c_4750, plain, (![X25_1796, X22_1763, X_1788, X10_1800, X2_1785, X18_1798, X32_1774, U_1770, Y_1789, X28_1782, X7_1780, X13_1786, X3_1768, X6_1764, X8_1794, X11_1784, X33_1790, X17_1769, X29_1775, X36_1776, X30_1773, X34_1760, X15_1767, X19_1795, X4_1797, X31_1793, X14_1799, X16_1759, Z_1778, X26_1783, X1_1781, X27_1766, X24_1779, X35_1762, X20_1791, W_1765, V_1792, X12_1777, X9_1772, X5_1761, X21_1787, X23_1771]: (~ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1770, V_1792, W_1765, X_1788, Y_1789, Z_1778, X1_1781, X2_1785, X3_1768, X4_1797, X5_1761, X6_1764, X7_1780, X8_1794, X9_1772, X10_1800, X11_1784, X12_1777, X13_1786, X14_1799, X15_1767, X16_1759, X17_1769, X18_1798, X19_1795, X20_1791, X21_1787, X22_1763, X23_1771, X24_1779, X25_1796, X26_1783, X27_1766, X28_1782, X29_1775, X30_1773, X31_1793, X32_1774, X33_1790, X34_1760, X35_1762, X36_1776, skc47)))). % 18.13/5.74 tff(c_4688, plain, (![X1_1574, X7_1573, X23_1565, X29_1569, X26_1576, X8_1587, X28_1575, X15_1561, X19_1588, X32_1568, X20_1584, X9_1566, U_1564, X6_1558, X17_1563, X_1581, X12_1570, Y_1582, X4_1590, X24_1572, X2_1578, X31_1586, X14_1592, X3_1562, X16_1553, X35_1556, X10_1593, X25_1589, X5_1555, X13_1579, W_1559, X34_1554, V_1585, X27_1560, X11_1577, Z_1571, X33_1583, X18_1591, X30_1567, X21_1580, X22_1557]: (ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1564, V_1585, W_1559, X_1581, Y_1582, Z_1571, X1_1574, X2_1578, X3_1562, X4_1590, X5_1555, X6_1558, X7_1573, X8_1587, X9_1566, X10_1593, X11_1577, X12_1570, X13_1579, X14_1592, X15_1561, X16_1553, X17_1563, X18_1591, X19_1588, X20_1584, X21_1580, X22_1557, X23_1565, X24_1572, X25_1589, X26_1576, X27_1560, X28_1575, X29_1569, X30_1567, X31_1586, X32_1568, X33_1583, X34_1554, X35_1556, skc48)))). % 18.13/5.74 tff(c_4754, plain, (![X31_1709, X26_1699, X30_1689, X28_1698, X36_1692, X2_1701, X5_1677, X11_1700, X29_1691, X27_1682, X3_1684, X12_1693, X8_1710, V_1708, X18_1714, X35_1678, X20_1707, X1_1697, X15_1683, X33_1706, X9_1688, X4_1713, X10_1716, X25_1712, X7_1696, X24_1695, X17_1685, U_1686, W_1681, X6_1680, Y_1705, X13_1702, X22_1679, Z_1694, X_1704, X21_1703, X19_1711, X23_1687, X16_1675, X14_1715, X32_1690, X34_1676]: (ssNder1_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1686, V_1708, W_1681, X_1704, Y_1705, Z_1694, X1_1697, X2_1701, X3_1684, X4_1713, X5_1677, X6_1680, X7_1696, X8_1710, X9_1688, X10_1716, X11_1700, X12_1693, X13_1702, X14_1715, X15_1683, X16_1675, X17_1685, X18_1714, X19_1711, X20_1707, X21_1703, X22_1679, X23_1687, X24_1695, X25_1712, X26_1699, X27_1682, X28_1698, X29_1691, X30_1689, X31_1709, X32_1690, X33_1706, X34_1676, X35_1678, X36_1692)))). % 18.13/5.74 tff(c_4700, plain, (![X10_1634, X29_1610, X4_1631, X34_1595, X15_1602, X19_1629, X3_1603, X17_1604, X14_1633, X25_1630, X27_1601, U_1605, X23_1606, W_1600, X7_1614, X32_1609, X13_1620, X1_1615, Z_1612, X31_1627, X11_1618, X18_1632, V_1626, X35_1597, X8_1628, X12_1611, X16_1594, X26_1617, X21_1621, X9_1607, X5_1596, X30_1608, X22_1598, X24_1613, Y_1623, X28_1616, X6_1599, X_1622, X2_1619, X33_1624, X20_1625]: (~ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1605, V_1626, W_1600, X_1622, Y_1623, Z_1612, X1_1615, X2_1619, X3_1603, X4_1631, X5_1596, X6_1599, X7_1614, X8_1628, X9_1607, X10_1634, X11_1618, X12_1611, X13_1620, X14_1633, X15_1602, X16_1594, X17_1604, X18_1632, X19_1629, X20_1625, X21_1621, X22_1598, X23_1606, X24_1613, X25_1630, X26_1617, X27_1601, X28_1616, X29_1610, X30_1608, X31_1627, X32_1609, X33_1624, X34_1595, X35_1597, skc49)))). % 18.13/5.74 tff(c_4650, plain, (![V_1424, X7_1412, X13_1418, X12_1409, X10_1432, X18_1430, X3_1401, X26_1415, X23_1404, X4_1429, X14_1431, Z_1410, X2_1417, X31_1425, X11_1416, U_1403, X24_1411, X28_1414, X15_1400, W_1398, X27_1399, X17_1402, X25_1428, X9_1405, X33_1422, X22_1396, X5_1395, Y_1421, X30_1406, X29_1408, X20_1423, X32_1407, X21_1419, X_1420, X34_1394, X19_1427, X8_1426, X1_1413, X16_1393, X6_1397]: (ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1403, V_1424, W_1398, X_1420, Y_1421, Z_1410, X1_1413, X2_1417, X3_1401, X4_1429, X5_1395, X6_1397, X7_1412, X8_1426, X9_1405, X10_1432, X11_1416, X12_1409, X13_1418, X14_1431, X15_1400, X16_1393, X17_1402, X18_1430, X19_1427, X20_1423, X21_1419, X22_1396, X23_1404, X24_1411, X25_1428, X26_1415, X27_1399, X28_1414, X29_1408, X30_1406, X31_1425, X32_1407, X33_1422, X34_1394, skc50)))). % 18.13/5.74 tff(c_4386, plain, (![X20_1230, X18_1236, X23_1213, X16_1203, Z_1218, W_1207, X26_1223, X11_1224, X28_1222, X27_1208, X_1228, X9_1214, Y_1229, V_1231, X10_1238, X5_1204, X30_1215, X25_1234, X22_1205, X19_1233, X14_1237, X8_1232, X4_1235, X7_1220, X15_1209, X13_1226, X12_1217, U_1212, X24_1219, X2_1225, X1_1221, X21_1227, X3_1210, X6_1206, X17_1211, X29_1216]: (ssPv54_3r1r1r1(U_1212, V_1231, W_1207) | ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1212, V_1231, W_1207, X_1228, Y_1229, Z_1218, X1_1221, X2_1225, X3_1210, X4_1235, X5_1204, X6_1206, X7_1220, X8_1232) | ~ssPv48_9r1r1r1r1r1r1r1r1r1(U_1212, V_1231, W_1207, X_1228, Y_1229, Z_1218, X1_1221, X2_1225, X3_1210) | ~ssPv21_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1212, V_1231, W_1207, X_1228, Y_1229, Z_1218, X1_1221, X2_1225, X3_1210, X4_1235, X5_1204, X6_1206, X7_1220, X8_1232, X9_1214, X10_1238, X11_1224, X12_1217, X13_1226, X14_1237, X15_1209, X16_1203, X17_1211, X18_1236, X19_1233, X20_1230, X21_1227, X22_1205, X23_1213, X24_1219, X25_1234, X26_1223, X27_1208, X28_1222, X29_1216, X30_1215)))). % 18.13/5.74 tff(c_4696, plain, (![X27_1519, X1_1533, X24_1531, X32_1527, X31_1545, X8_1546, V_1544, X14_1551, Z_1530, X7_1532, X10_1552, X6_1517, X3_1521, X17_1522, X19_1547, X18_1550, X34_1513, X2_1537, X12_1529, X29_1528, X23_1524, X5_1514, X16_1512, X30_1526, X15_1520, Y_1541, X26_1535, X28_1534, X21_1539, X33_1542, W_1518, X20_1543, X11_1536, X13_1538, X4_1549, X_1540, X9_1525, X35_1515, U_1523, X22_1516, X25_1548]: (ssNder1_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1523, V_1544, W_1518, X_1540, Y_1541, Z_1530, X1_1533, X2_1537, X3_1521, X4_1549, X5_1514, X6_1517, X7_1532, X8_1546, X9_1525, X10_1552, X11_1536, X12_1529, X13_1538, X14_1551, X15_1520, X16_1512, X17_1522, X18_1550, X19_1547, X20_1543, X21_1539, X22_1516, X23_1524, X24_1531, X25_1548, X26_1535, X27_1519, X28_1534, X29_1528, X30_1526, X31_1545, X32_1527, X33_1542, X34_1513, X35_1515)))). % 18.13/5.74 tff(c_4602, plain, (![X_1460, X25_1468, X31_1465, Y_1461, X24_1451, X2_1457, X14_1471, X3_1441, X23_1444, X4_1469, Z_1450, X11_1456, U_1443, X28_1454, X33_1462, X27_1439, X30_1446, V_1464, X5_1435, X13_1458, X18_1470, X7_1452, X26_1455, X1_1453, X34_1434, X21_1459, X32_1447, X20_1463, X22_1436, X8_1466, X29_1448, X15_1440, W_1438, X9_1445, X19_1467, X10_1472, X6_1437, X16_1433, X17_1442, X12_1449]: (~ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1443, V_1464, W_1438, X_1460, Y_1461, Z_1450, X1_1453, X2_1457, X3_1441, X4_1469, X5_1435, X6_1437, X7_1452, X8_1466, X9_1445, X10_1472, X11_1456, X12_1449, X13_1458, X14_1471, X15_1440, X16_1433, X17_1442, X18_1470, X19_1467, X20_1463, X21_1459, X22_1436, X23_1444, X24_1451, X25_1468, X26_1455, X27_1439, X28_1454, X29_1448, X30_1446, X31_1465, X32_1447, X33_1462, X34_1434, skc51)))). % 18.13/5.74 tff(c_4570, plain, (![X25_1388, X2_1377, X13_1378, X23_1364, X16_1353, Y_1381, X3_1361, X5_1355, X20_1383, X26_1375, X19_1387, X32_1367, X1_1373, X8_1386, X_1380, X15_1360, X21_1379, U_1363, X27_1359, V_1384, X4_1389, X18_1390, X28_1374, X14_1391, X22_1356, X30_1366, X7_1372, X33_1382, X34_1354, W_1358, X29_1368, X11_1376, X24_1371, X9_1365, X17_1362, X12_1369, X10_1392, Z_1370, X6_1357, X31_1385]: (ssNder1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1363, V_1384, W_1358, X_1380, Y_1381, Z_1370, X1_1373, X2_1377, X3_1361, X4_1389, X5_1355, X6_1357, X7_1372, X8_1386, X9_1365, X10_1392, X11_1376, X12_1369, X13_1378, X14_1391, X15_1360, X16_1353, X17_1362, X18_1390, X19_1387, X20_1383, X21_1379, X22_1356, X23_1364, X24_1371, X25_1388, X26_1375, X27_1359, X28_1374, X29_1368, X30_1366, X31_1385, X32_1367, X33_1382, X34_1354)))). % 18.13/5.74 tff(c_4562, plain, (![X5_1315, X18_1350, V_1344, X9_1325, X12_1329, X26_1335, X3_1321, W_1318, X14_1351, X28_1334, X4_1349, X7_1332, X22_1316, X11_1336, X20_1343, X19_1347, X24_1331, X31_1345, X10_1352, X27_1319, X_1340, X33_1342, X30_1326, X13_1338, X25_1348, Y_1341, U_1323, X2_1337, X21_1339, Z_1330, X16_1314, X23_1324, X15_1320, X1_1333, X29_1328, X6_1317, X8_1346, X17_1322, X32_1327]: (ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1323, V_1344, W_1318, X_1340, Y_1341, Z_1330, X1_1333, X2_1337, X3_1321, X4_1349, X5_1315, X6_1317, X7_1332, X8_1346, X9_1325, X10_1352, X11_1336, X12_1329, X13_1338, X14_1351, X15_1320, X16_1314, X17_1322, X18_1350, X19_1347, X20_1343, X21_1339, X22_1316, X23_1324, X24_1331, X25_1348, X26_1335, X27_1319, X28_1334, X29_1328, X30_1326, X31_1345, X32_1327, X33_1342)))). % 18.13/5.74 tff(c_4484, plain, (![X21_1301, X19_1308, X8_1307, X2_1299, X10_1313, X28_1296, X14_1312, X32_1289, X20_1304, X22_1278, V_1305, X12_1291, X7_1294, X5_1277, X16_1276, X1_1295, X17_1284, X29_1290, X4_1310, W_1280, X27_1281, Z_1292, X25_1309, X11_1298, X_1302, X24_1293, X31_1306, Y_1303, U_1285, X6_1279, X9_1287, X13_1300, X3_1283, X15_1282, X23_1286, X26_1297, X30_1288, X18_1311]: (ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1285, V_1305, W_1280, X_1302, Y_1303, Z_1292, X1_1295, X2_1299, X3_1283, X4_1310, X5_1277, X6_1279, X7_1294, X8_1307, X9_1287, X10_1313, X11_1298, X12_1291, X13_1300, X14_1312, X15_1282, X16_1276, X17_1284, X18_1311, X19_1308, X20_1304, X21_1301, X22_1278, X23_1286, X24_1293, X25_1309, X26_1297, X27_1281, X28_1296, X29_1290, X30_1288, X31_1306, X32_1289)))). % 18.13/5.74 tff(c_4418, plain, (![X6_1242, X18_1273, X24_1255, X27_1244, W_1243, X23_1249, X10_1275, U_1248, X21_1263, X30_1251, X29_1252, X25_1271, Z_1254, X8_1269, X12_1253, V_1267, X13_1262, X26_1259, X9_1250, X14_1274, X15_1245, X31_1268, X4_1272, X17_1247, X28_1258, X_1264, X7_1256, X22_1241, Y_1265, X1_1257, X3_1246, X16_1239, X11_1260, X2_1261, X20_1266, X19_1270, X5_1240]: (ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1248, V_1267, W_1243, X_1264, Y_1265, Z_1254, X1_1257, X2_1261, X3_1246, X4_1272, X5_1240, X6_1242, X7_1256, X8_1269, X9_1250, X10_1275, X11_1260, X12_1253, X13_1262, X14_1274, X15_1245, X16_1239, X17_1247, X18_1273, X19_1270, X20_1266, X21_1263, X22_1241, X23_1249, X24_1255, X25_1271, X26_1259, X27_1244, X28_1258, X29_1252, X30_1251, X31_1268)))). % 18.13/5.74 tff(c_4334, plain, (![X7_1149, X26_1152, Z_1147, X29_1145, X12_1146, X6_1135, Y_1158, X_1157, W_1136, X23_1142, X24_1148, X2_1154, X22_1134, X3_1139, X1_1150, X16_1132, X21_1156, X11_1153, X8_1161, X10_1167, X4_1164, V_1160, X17_1140, X28_1151, X14_1166, X15_1138, X25_1163, X20_1159, X9_1143, X13_1155, X27_1137, X5_1133, X18_1165, X19_1162, X30_1144, U_1141]: (ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1141, V_1160, W_1136, X_1157, Y_1158, Z_1147, X1_1150, X2_1154, X3_1139, X4_1164, X5_1133, X6_1135, X7_1149, X8_1161, X9_1143, X10_1167, X11_1153, X12_1146, X13_1155, X14_1166, X15_1138, X16_1132, X17_1140, X18_1165, X19_1162, X20_1159, X21_1156, X22_1134, X23_1142, X24_1148, X25_1163, X26_1152, X27_1137, X28_1151, X29_1145, X30_1144)))). % 18.13/5.74 tff(c_5247, plain, (![X8_4651, Z_4644, X13_4639, X12_4634, Y_4646, W_4636, X_4642, V_4626, X7_4627, X1_4635, X11_4649, X2_4654, X5_4631, X6_4652, X9_4648, X10_4645, X4_4630, X14_4643, U_4641, X3_4637]: (ssPv56_1r1(U_4641) | ~ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U_4641, V_4626, W_4636, X_4642, Y_4646, Z_4644, X1_4635, X2_4654, X3_4637, X4_4630, X5_4631, X6_4652) | ~ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_4641, V_4626, W_4636, X_4642, Y_4646, Z_4644, X1_4635, X2_4654, X3_4637, X4_4630, X5_4631, X6_4652, X7_4627, X8_4651, X9_4648, X10_4645, X11_4649, X12_4634, X13_4639, X14_4643)))). % 18.13/5.74 tff(c_4186, plain, (![X5_1098, X12_1110, X27_1102, V_1124, X11_1117, X15_1103, U_1106, X29_1109, X23_1107, X10_1131, X14_1130, X20_1123, X28_1115, X26_1116, X4_1128, X8_1125, X19_1126, W_1101, X7_1113, X21_1120, X18_1129, X3_1104, X25_1127, X1_1114, X16_1097, X2_1118, X24_1112, Z_1111, X9_1108, X13_1119, Y_1122, X17_1105, X22_1099, X_1121, X6_1100]: (ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1106, V_1124, W_1101, X_1121, Y_1122, Z_1111, X1_1114, X2_1118, X3_1104, X4_1128, X5_1098, X6_1100, X7_1113, X8_1125, X9_1108, X10_1131, X11_1117, X12_1110, X13_1119, X14_1130, X15_1103, X16_1097, X17_1105, X18_1129, X19_1126, X20_1123, X21_1120, X22_1099, X23_1107, X24_1112, X25_1127, X26_1116, X27_1102, X28_1115, X29_1109)))). % 18.13/5.74 tff(c_4138, plain, (![X_1086, X10_1096, V_1089, U_1072, X22_1065, X5_1064, X2_1083, X12_1075, X15_1069, X14_1095, X8_1090, X27_1068, X26_1081, X16_1063, W_1067, X21_1085, Z_1076, X23_1073, X19_1091, X9_1074, X7_1078, Y_1087, X17_1071, X1_1079, X6_1066, X25_1092, X24_1077, X3_1070, X13_1084, X11_1082, X4_1093, X28_1080, X20_1088, X18_1094]: (ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1072, V_1089, W_1067, X_1086, Y_1087, Z_1076, X1_1079, X2_1083, X3_1070, X4_1093, X5_1064, X6_1066, X7_1078, X8_1090, X9_1074, X10_1096, X11_1082, X12_1075, X13_1084, X14_1095, X15_1069, X16_1063, X17_1071, X18_1094, X19_1091, X20_1088, X21_1085, X22_1065, X23_1073, X24_1077, X25_1092, X26_1081, X27_1068, X28_1080)))). % 18.13/5.74 tff(c_4074, plain, (![Y_1053, X5_1031, X14_1061, X12_1042, U_1039, X15_1036, X22_1032, X26_1047, X8_1056, X_1052, X16_1030, X27_1035, X21_1051, W_1034, X7_1045, X17_1038, X1_1046, X3_1037, X9_1041, X2_1049, X24_1044, X18_1060, X11_1048, Z_1043, X13_1050, X23_1040, X6_1033, V_1055, X20_1054, X10_1062, X19_1057, X4_1059, X25_1058]: (ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_1039, V_1055, W_1034, X_1052, Y_1053, Z_1043, X1_1046, X2_1049, X3_1037, X4_1059, X5_1031, X6_1033, X7_1045, X8_1056, X9_1041, X10_1062, X11_1048, X12_1042, X13_1050, X14_1061, X15_1036, X16_1030, X17_1038, X18_1060, X19_1057, X20_1054, X21_1051, X22_1032, X23_1040, X24_1044, X25_1058, X26_1047, X27_1035)))). % 18.13/5.74 tff(c_4002, plain, (![X8_992, W_971, X12_978, X19_993, X22_969, Y_989, X11_984, X23_976, X3_973, X2_985, X16_967, X26_983, X9_977, X14_997, X18_996, X21_987, V_991, Z_979, X5_968, X10_998, X15_972, X20_990, U_975, X13_986, X_988, X4_995, X7_981, X25_994, X1_982, X24_980, X6_970, X17_974]: (ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_975, V_991, W_971, X_988, Y_989, Z_979, X1_982, X2_985, X3_973, X4_995, X5_968, X6_970, X7_981, X8_992, X9_977, X10_998, X11_984, X12_978, X13_986, X14_997, X15_972, X16_967, X17_974, X18_996, X19_993, X20_990, X21_987, X22_969, X23_976, X24_980, X25_994, X26_983)))). % 18.13/5.74 tff(c_3906, plain, (![X8_930, X5_907, X16_906, X15_911, X9_916, X3_912, X23_915, X_926, W_910, X11_922, X6_909, X22_908, X20_928, X18_933, X12_917, X17_913, X24_919, X2_923, Y_927, X19_931, X1_921, X4_932, X10_935, X21_925, X13_924, Z_918, X14_934, U_914, X7_920, V_929]: (~ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_914, V_929, W_910, X_926, Y_927, Z_918, X1_921, X2_923, X3_912, X4_932, X5_907, X6_909, X7_920, X8_930, X9_916, X10_935, X11_922, X12_917, X13_924, X14_934, X15_911, X16_906, X17_913, X18_933, X19_931, X20_928, X21_925, X22_908, X23_915, X24_919, skc53)))). % 18.13/5.74 tff(c_3960, plain, (![X10_966, X23_945, X7_950, U_944, X14_965, X_956, X6_939, X18_964, X17_943, X4_963, X2_953, X22_938, X16_936, X3_942, X24_949, X21_955, X1_951, X5_937, X15_941, X12_947, X13_954, X20_958, X19_961, W_940, X11_952, Z_948, X8_960, V_959, X9_946, X25_962, Y_957]: (ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_944, V_959, W_940, X_956, Y_957, Z_948, X1_951, X2_953, X3_942, X4_963, X5_937, X6_939, X7_950, X8_960, X9_946, X10_966, X11_952, X12_947, X13_954, X14_965, X15_941, X16_936, X17_943, X18_964, X19_961, X20_958, X21_955, X22_938, X23_945, X24_949, X25_962)))). % 18.13/5.74 tff(c_3802, plain, (![X2_893, U_884, X10_905, X20_898, X13_894, X15_881, X19_901, X16_876, W_880, X8_900, X18_903, X6_879, X3_882, X21_895, X11_892, X7_890, X4_902, X14_904, X17_883, X12_887, X9_886, X_896, V_899, X23_885, Y_897, X24_889, X1_891, Z_888, X22_878, X5_877]: (ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_884, V_899, W_880, X_896, Y_897, Z_888, X1_891, X2_893, X3_882, X4_902, X5_877, X6_879, X7_890, X8_900, X9_886, X10_905, X11_892, X12_887, X13_894, X14_904, X15_881, X16_876, X17_883, X18_903, X19_901, X20_898, X21_895, X22_878, X23_885, X24_889, skc52)))). % 18.13/5.74 tff(c_3796, plain, (![X17_853, X_866, X10_875, X5_847, X4_872, U_854, X6_849, X21_865, X15_851, X7_860, X19_871, X18_873, X2_863, X20_868, X23_855, Y_867, X9_856, W_850, X1_861, X22_848, X3_852, X13_864, X16_846, Z_858, X11_862, X8_870, X24_859, X12_857, X14_874, V_869]: (ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_854, V_869, W_850, X_866, Y_867, Z_858, X1_861, X2_863, X3_852, X4_872, X5_847, X6_849, X7_860, X8_870, X9_856, X10_875, X11_862, X12_857, X13_864, X14_874, X15_851, X16_846, X17_853, X18_873, X19_871, X20_868, X21_865, X22_848, X23_855, X24_859)))). % 18.13/5.74 tff(c_3660, plain, (![X12_799, U_796, V_810, X20_809, X5_789, W_792, Y_808, X17_795, X22_790, X15_793, X11_803, X14_815, X9_798, X_807, X18_814, X2_804, Z_800, X10_816, X19_812, X8_811, X23_797, X4_813, X6_791, X16_788, X13_805, X7_801, X1_802, X3_794, X21_806]: (ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_796, V_810, W_792, X_807, Y_808, Z_800, X1_802, X2_804, X3_794, X4_813, X5_789, X6_791, X7_801, X8_811, X9_798, X10_816, X11_803, X12_799, X13_805, X14_815, X15_793, X16_788, X17_795, X18_814, X19_812, X20_809, X21_806, X22_790, X23_797, skc54)))). % 18.13/5.74 tff(c_3734, plain, (![X17_824, X18_843, X_836, X1_831, X16_817, X11_832, X20_838, X21_835, X6_820, X2_833, X8_840, X14_844, U_825, X12_828, X4_842, X9_827, X15_822, V_839, X10_845, X3_823, Z_829, X5_818, X22_819, W_821, Y_837, X23_826, X19_841, X7_830, X13_834]: (~ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_825, V_839, W_821, X_836, Y_837, Z_829, X1_831, X2_833, X3_823, X4_842, X5_818, X6_820, X7_830, X8_840, X9_827, X10_845, X11_832, X12_828, X13_834, X14_844, X15_822, X16_817, X17_824, X18_843, X19_841, X20_838, X21_835, X22_819, X23_826, skc55)))). % 18.13/5.74 tff(c_3596, plain, (![X14_757, X5_732, X22_733, X15_736, X19_754, X4_755, X13_747, X17_738, V_752, X20_751, X1_744, X8_753, Y_750, X2_746, X12_741, X16_731, X9_740, X_749, W_735, X6_734, X10_758, X11_745, X21_748, U_739, X3_737, X7_743, X18_756, Z_742]: (~ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_739, V_752, W_735, X_749, Y_750, Z_742, X1_744, X2_746, X3_737, X4_755, X5_732, X6_734, X7_743, X8_753, X9_740, X10_758, X11_745, X12_741, X13_747, X14_757, X15_736, X16_731, X17_738, X18_756, X19_754, X20_751, X21_748, X22_733, skc57)))). % 18.13/5.74 tff(c_3520, plain, (![V_724, X15_708, X8_725, X22_705, X14_729, X2_718, X3_709, X5_704, X21_720, W_707, X13_719, Z_714, X9_712, X11_717, X18_728, X_721, X20_723, X1_716, Y_722, X6_706, X10_730, X16_703, X7_715, X17_710, X12_713, U_711, X4_727, X19_726]: (ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_711, V_724, W_707, X_721, Y_722, Z_714, X1_716, X2_718, X3_709, X4_727, X5_704, X6_706, X7_715, X8_725, X9_712, X10_730, X11_717, X12_713, X13_719, X14_729, X15_708, X16_703, X17_710, X18_728, X19_726, X20_723, X21_720, X22_705, skc56)))). % 18.13/5.74 tff(c_3724, plain, (![X9_769, X18_785, X1_773, X12_770, X19_783, X14_786, X22_761, X16_759, X10_787, X8_782, X11_774, W_763, X5_760, X6_762, X3_765, U_767, X21_777, X_778, X17_766, Y_779, X15_764, X7_772, X13_776, X4_784, X23_768, V_781, X2_775, Z_771, X20_780]: (ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_767, V_781, W_763, X_778, Y_779, Z_771, X1_773, X2_775, X3_765, X4_784, X5_760, X6_762, X7_772, X8_782, X9_769, X10_787, X11_774, X12_770, X13_776, X14_786, X15_764, X16_759, X17_766, X18_785, X19_783, X20_780, X21_777, X22_761, X23_768)))). % 18.13/5.74 tff(c_3528, plain, (![X19_698, X21_692, X17_682, X10_702, X4_699, X7_687, X13_691, X15_680, X8_697, X2_690, W_679, X12_685, X18_700, Z_686, X11_689, X_693, X20_695, X16_675, X22_677, U_683, X14_701, X1_688, X5_676, V_696, X6_678, Y_694, X9_684, X3_681]: (ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_683, V_696, W_679, X_693, Y_694, Z_686, X1_688, X2_690, X3_681, X4_699, X5_676, X6_678, X7_687, X8_697, X9_684, X10_702, X11_689, X12_685, X13_691, X14_701, X15_680, X16_675, X17_682, X18_700, X19_698, X20_695, X21_692, X22_677)))). % 18.13/5.74 tff(c_3442, plain, (![X14_673, X20_667, X5_649, Y_666, X_665, X7_659, X10_674, X18_672, W_651, V_668, Z_658, X16_648, X19_670, X15_652, X12_657, X2_662, U_655, X21_664, X8_669, X11_661, X4_671, X3_653, X6_650, X17_654, X9_656, X13_663, X1_660]: (ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_655, V_668, W_651, X_665, Y_666, Z_658, X1_660, X2_662, X3_653, X4_671, X5_649, X6_650, X7_659, X8_669, X9_656, X10_674, X11_661, X12_657, X13_663, X14_673, X15_652, X16_648, X17_654, X18_672, X19_670, X20_667, X21_664)))). % 18.13/5.74 tff(c_3238, plain, (![X6_598, X9_604, X19_617, X3_601, X20_614, X2_610, X14_620, X18_619, W_599, X17_602, X8_616, Z_606, U_603, X5_597, X15_600, X13_611, X10_621, X4_618, X16_596, V_615, X11_609, X1_608, X7_607, Y_613, X12_605, X_612]: (ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_603, V_615, W_599, X_612, Y_613, Z_606, X1_608, X2_610, X3_601, X4_618, X5_597, X6_598, X7_607, X8_616, X9_604, X10_621, X11_609, X12_605, X13_611, X14_620, X15_600, X16_596, X17_602, X18_619, X19_617, X20_614, skc58)))). % 18.13/5.74 tff(c_3376, plain, (![V_641, X9_630, X3_627, X11_635, Y_639, X10_647, U_629, X7_633, X14_646, X19_643, Z_632, X15_626, X13_637, X8_642, X2_636, X12_631, X16_622, X5_623, X18_645, X1_634, X17_628, W_625, X20_640, X_638, X4_644, X6_624]: (~ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_629, V_641, W_625, X_638, Y_639, Z_632, X1_634, X2_636, X3_627, X4_644, X5_623, X6_624, X7_633, X8_642, X9_630, X10_647, X11_635, X12_631, X13_637, X14_646, X15_626, X16_622, X17_628, X18_645, X19_643, X20_640, skc59)))). % 18.13/5.74 tff(c_3378, plain, (![W_573, V_589, X3_575, U_577, X_586, X10_595, X7_581, Y_587, X11_583, X4_592, X8_590, X14_594, X9_578, X1_582, X20_588, X19_591, X18_593, X16_570, X13_585, X15_574, X5_571, X12_579, X2_584, X6_572, Z_580, X17_576]: (ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_577, V_589, W_573, X_586, Y_587, Z_580, X1_582, X2_584, X3_575, X4_592, X5_571, X6_572, X7_581, X8_590, X9_578, X10_595, X11_583, X12_579, X13_585, X14_594, X15_574, X16_570, X17_576, X18_593, X19_591, X20_588)))). % 18.13/5.74 tff(c_3322, plain, (![X1_557, X7_556, V_563, Y_562, X12_554, X9_553, X11_558, X15_549, X8_564, X3_550, X_561, X4_566, X6_547, X18_567, W_548, X17_551, X19_565, X14_568, Z_555, X13_560, U_552, X16_545, X10_569, X2_559, X5_546]: (~ssPv31_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_552, V_563, W_548, X_561, Y_562, Z_555, X1_557, X2_559, X3_550, X4_566, X5_546, X6_547, X7_556, X8_564, X9_553, X10_569, X11_558, X12_554, X13_560, X14_568, X15_549, X16_545, X17_551, X18_567, X19_565, skc61)))). % 18.13/5.74 tff(c_3232, plain, (![X_463, X3_452, V_465, X6_449, X12_456, U_454, X18_468, X9_455, X4_467, Y_464, Z_457, X8_466, X11_460, X1_459, W_450, X5_448, X16_447, X14_469, X15_451, X7_458, X13_462, X17_453, X2_461, X10_470]: (ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_454, V_465, W_450, X_463, Y_464, Z_457, X1_459, X2_461, X3_452, X4_467, X5_448, X6_449, X7_458, X8_466, X9_455, X10_470, X11_460, X12_456, X13_462, X14_469, X15_451, X16_447, X17_453, X18_468, skc62)))). % 18.13/5.74 tff(c_3514, plain, (![X11_533, X10_544, Z_530, X5_521, X14_543, X2_534, X9_528, X18_542, X3_525, X17_526, Y_537, X16_520, U_527, W_523, X12_529, X_536, X13_535, V_538, X4_541, X6_522, X15_524, X1_532, X8_539, X19_540, X7_531]: (ssPv31_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_527, V_538, W_523, X_536, Y_537, Z_530, X1_532, X2_534, X3_525, X4_541, X5_521, X6_522, X7_531, X8_539, X9_528, X10_544, X11_533, X12_529, X13_535, X14_543, X15_524, X16_520, X17_526, X18_542, X19_540, skc60)))). % 18.13/5.74 tff(c_3236, plain, (![X1_507, X15_499, X10_519, X4_516, X14_518, X3_500, X12_504, X5_496, U_502, X13_510, X9_503, W_498, Z_505, X16_495, X8_514, X2_509, X17_501, X19_515, X11_508, X18_517, V_513, Y_512, X_511, X7_506, X6_497]: (ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_502, V_513, W_498, X_511, Y_512, Z_505, X1_507, X2_509, X3_500, X4_516, X5_496, X6_497, X7_506, X8_514, X9_503, X10_519, X11_508, X12_504, X13_510, X14_518, X15_499, X16_495, X17_501, X18_517, X19_515)))). % 18.13/5.74 tff(c_3256, plain, (![X12_480, Z_481, X5_472, X16_471, X14_493, Y_488, X4_491, X10_494, X7_482, X6_473, X13_486, U_478, X3_476, X1_483, V_489, X17_477, X_487, X18_492, X11_484, X8_490, X2_485, X9_479, X15_475, W_474]: (~ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_478, V_489, W_474, X_487, Y_488, Z_481, X1_483, X2_485, X3_476, X4_491, X5_472, X6_473, X7_482, X8_490, X9_479, X10_494, X11_484, X12_480, X13_486, X14_493, X15_475, X16_471, X17_477, X18_492, skc63)))). % 18.13/5.74 tff(c_3228, plain, (![X8_442, X5_424, X2_437, U_430, X16_423, X6_425, Z_433, X1_435, X7_434, X13_438, X3_428, Y_440, X14_445, X12_432, X4_443, X_439, W_426, X18_444, V_441, X10_446, X17_429, X11_436, X9_431, X15_427]: (ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_430, V_441, W_426, X_439, Y_440, Z_433, X1_435, X2_437, X3_428, X4_443, X5_424, X6_425, X7_434, X8_442, X9_431, X10_446, X11_436, X12_432, X13_438, X14_445, X15_427, X16_423, X17_429, X18_444)))). % 18.13/5.74 tff(c_3068, plain, (![X9_408, Z_410, X4_420, W_403, Y_417, X17_406, X10_422, X8_419, X_416, X11_413, X7_411, X3_405, X2_414, X1_412, X14_421, X16_400, U_407, X6_402, X5_401, V_418, X12_409, X13_415, X15_404]: (ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_407, V_418, W_403, X_416, Y_417, Z_410, X1_412, X2_414, X3_405, X4_420, X5_401, X6_402, X7_411, X8_419, X9_408, X10_422, X11_413, X12_409, X13_415, X14_421, X15_404, X16_400, X17_406)))). % 18.13/5.74 tff(c_2942, plain, (![X_393, Y_394, X5_379, X13_392, X4_397, X3_383, X1_389, X11_390, X14_398, X12_386, Z_387, X6_380, X8_396, X15_382, V_395, X16_378, X7_388, U_384, X9_385, W_381, X2_391, X10_399]: (ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_384, V_395, W_381, X_393, Y_394, Z_387, X1_389, X2_391, X3_383, X4_397, X5_379, X6_380, X7_388, X8_396, X9_385, X10_399, X11_390, X12_386, X13_392, X14_398, X15_382, X16_378)))). % 18.13/5.74 tff(c_2896, plain, (![V_373, Z_365, X3_361, X2_369, Y_372, U_362, X5_357, X4_375, X1_367, X13_370, X12_364, X6_358, X15_360, X14_376, W_359, X7_366, X_371, X10_377, X11_368, X8_374, X9_363]: (ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_362, V_373, W_359, X_371, Y_372, Z_365, X1_367, X2_369, X3_361, X4_375, X5_357, X6_358, X7_366, X8_374, X9_363, X10_377, X11_368, X12_364, X13_370, X14_376, X15_360)))). % 18.13/5.74 tff(c_2826, plain, (![X1_346, X4_354, Y_351, X5_337, X3_340, X7_345, X10_356, X13_349, X8_353, W_339, X11_347, X9_342, X14_355, X_350, X2_348, X6_338, V_352, Z_344, X12_343, U_341]: (ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_341, V_352, W_339, X_350, Y_351, Z_344, X1_346, X2_348, X3_340, X4_354, X5_337, X6_338, X7_345, X8_353, X9_342, X10_356, X11_347, X12_343, X13_349, X14_355)))). % 18.13/5.74 tff(c_2798, plain, (![X5_318, X8_334, X11_328, X7_326, X10_336, V_333, U_322, Y_332, X3_321, X13_330, W_320, X2_329, X4_335, X12_324, X_331, X6_319, X9_323, Z_325, X1_327]: (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_322, V_333, W_320, X_331, Y_332, Z_325, X1_327, X2_329, X3_321, X4_335, X5_318, X6_319, X7_326, X8_334, X9_323, X10_336, X11_328, X12_324, X13_330)))). % 18.13/5.74 tff(c_2538, plain, (![X_312, X7_308, Y_313, X8_315, V_314, X12_306, W_302, U_304, X4_316, Z_307, X2_311, X1_309, X3_303, X5_300, X10_317, X11_310, X6_301, X9_305]: (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_304, V_314, W_302, X_312, Y_313, Z_307, X1_309, X2_311, X3_303, X4_316, X5_300, X6_301, X7_308, X8_315, X9_305, X10_317, X11_310, X12_306)))). % 18.13/5.75 tff(c_2382, plain, (![X8_297, U_287, X6_284, X7_290, W_285, X2_293, V_296, X11_292, X10_299, X_294, Y_295, X3_286, X1_291, X4_298, Z_289, X9_288, X5_283]: (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_287, V_296, W_285, X_294, Y_295, Z_289, X1_291, X2_293, X3_286, X4_298, X5_283, X6_284, X7_290, X8_297, X9_288, X10_299, X11_292)))). % 18.13/5.75 tff(c_2046, plain, (![X3_255, X8_265, X7_259, X9_257, V_264, X4_266, Y_263, W_254, X6_253, X1_260, X5_252, X2_261, U_256, X_262, Z_258]: (~ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_256, V_264, W_254, X_262, Y_263, Z_258, X1_260, X2_261, X3_255, X4_266, X5_252, X6_253, X7_259, X8_265, X9_257, skc65)))). % 18.13/5.75 tff(c_2048, plain, (![X9_242, V_249, X1_245, X_247, X8_250, Y_248, X7_244, X4_251, X6_238, U_241, X3_240, X2_246, Z_243, W_239, X5_237]: (ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_241, V_249, W_239, X_247, Y_248, Z_243, X1_245, X2_246, X3_240, X4_251, X5_237, X6_238, X7_244, X8_250, X9_242, skc64)))). % 18.13/5.75 tff(c_2208, plain, (![V_279, U_271, X8_280, X3_270, X9_272, X4_281, Z_273, X6_268, W_269, X10_282, Y_278, X_277, X7_274, X2_276, X5_267, X1_275]: (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_271, V_279, W_269, X_277, Y_278, Z_273, X1_275, X2_276, X3_270, X4_281, X5_267, X6_268, X7_274, X8_280, X9_272, X10_282)))). % 18.13/5.75 tff(c_2050, plain, (![X8_235, X_232, X7_229, X1_230, X4_236, X3_225, X6_223, Z_228, U_226, W_224, X5_222, V_234, X9_227, X2_231, Y_233]: (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_226, V_234, W_224, X_232, Y_233, Z_228, X1_230, X2_231, X3_225, X4_236, X5_222, X6_223, X7_229, X8_235, X9_227)))). % 18.13/5.75 tff(c_1868, plain, (![Z_213, V_219, X_217, X2_216, X1_215, X6_209, U_212, X8_220, X7_214, X5_208, Y_218, X4_221, X3_211, W_210]: (~ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_212, V_219, W_210, X_217, Y_218, Z_213, X1_215, X2_216, X3_211, X4_221, X5_208, X6_209, X7_214, X8_220, skc67)))). % 18.13/5.75 tff(c_1882, plain, (![U_198, X3_197, X4_207, V_205, W_196, X6_195, X1_201, Y_204, X8_206, X7_200, X5_194, Z_199, X_203, X2_202]: (ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_198, V_205, W_196, X_203, Y_204, Z_199, X1_201, X2_202, X3_197, X4_207, X5_194, X6_195, X7_200, X8_206, skc66)))). % 18.13/5.75 tff(c_2014, plain, (![V_191, X5_180, X7_186, X2_188, X_189, Z_185, X6_181, W_182, U_184, X4_193, X1_187, X8_192, Y_190, X3_183]: (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_184, V_191, W_182, X_189, Y_190, Z_185, X1_187, X2_188, X3_183, X4_193, X5_180, X6_181, X7_186, X8_192)))). % 18.13/5.75 tff(c_1986, plain, (![Y_164, X1_161, X7_160, X4_166, X2_162, X3_157, X_163, U_158, X6_155, V_165, Z_159, X5_154, W_156]: (ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_158, V_165, W_156, X_163, Y_164, Z_159, X1_161, X2_162, X3_157, X4_166, X5_154, X6_155, X7_160, skc68)))). % 18.13/5.75 tff(c_1782, plain, (![Z_172, V_178, X_176, W_169, X5_167, X3_170, X1_174, Y_177, X7_173, X2_175, U_171, X6_168, X4_179]: (~ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_171, V_178, W_169, X_176, Y_177, Z_172, X1_174, X2_175, X3_170, X4_179, X5_167, X6_168, X7_173, skc69)))). % 18.13/5.75 tff(c_1566, plain, (![X2_124, X3_120, X_125, Z_122, X5_117, X4_128, X6_118, V_127, W_119, U_121, Y_126, X1_123]: (ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_121, V_127, W_119, X_125, Y_126, Z_122, X1_123, X2_124, X3_120, X4_128, X5_117, X6_118, skc70)))). % 18.13/5.75 tff(c_1640, plain, (![X_137, X3_132, W_131, X5_129, Z_134, X4_140, U_133, X1_135, V_139, X6_130, Y_138, X2_136]: (~ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_133, V_139, W_131, X_137, Y_138, Z_134, X1_135, X2_136, X3_132, X4_140, X5_129, X6_130, skc71)))). % 18.13/5.75 tff(c_1832, plain, (![W_143, Z_146, V_152, X2_149, X7_147, U_145, X5_141, X4_153, X6_142, X_150, Y_151, X3_144, X1_148]: (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_145, V_152, W_143, X_150, Y_151, Z_146, X1_148, X2_149, X3_144, X4_153, X5_141, X6_142, X7_147)))). % 18.13/5.75 tff(c_1372, plain, (![X5_83, Z_87, U_86, X4_93, X1_88, X2_89, Y_91, W_84, X3_85, V_92, X_90]: (ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U_86, V_92, W_84, X_90, Y_91, Z_87, X1_88, X2_89, X3_85, X4_93, X5_83, skc72)))). % 18.13/5.75 tff(c_1394, plain, (![V_103, X5_94, Z_98, U_97, X1_99, Y_102, X4_104, W_95, X2_100, X_101, X3_96]: (~ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U_97, V_103, W_95, X_101, Y_102, Z_98, X1_99, X2_100, X3_96, X4_104, X5_94, skc73)))). % 18.13/5.75 tff(c_1588, plain, (![U_109, X5_105, V_115, X1_111, Y_114, W_107, Z_110, X2_112, X_113, X4_116, X3_108, X6_106]: (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U_109, V_115, W_107, X_113, Y_114, Z_110, X1_111, X2_112, X3_108, X4_116, X5_105, X6_106)))). % 18.13/5.75 tff(c_1382, plain, (![X4_82, X_79, Z_76, X5_72, U_75, X1_77, W_73, Y_80, X2_78, V_81, X3_74]: (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U_75, V_81, W_73, X_79, Y_80, Z_76, X1_77, X2_78, X3_74, X4_82, X5_72)))). % 18.13/5.75 tff(c_1178, plain, (![X4_71, Z_65, Y_69, X_68, U_64, X1_66, V_70, X2_67, W_62, X3_63]: (ssNder1_10r1r1r1r1r1r1r1r1r1r1(U_64, V_70, W_62, X_68, Y_69, Z_65, X1_66, X2_67, X3_63, X4_71)))). % 18.13/5.75 tff(c_1158, plain, (![W_53, X2_58, X_59, Y_60, X3_54, X1_57, V_61, Z_56, U_55]: (ssNder1_9r1r1r1r1r1r1r1r1r1(U_55, V_61, W_53, X_59, Y_60, Z_56, X1_57, X2_58, X3_54)))). % 18.13/5.75 tff(c_942, plain, (![X2_49, U_46, Z_47, V_52, X1_48, Y_51, X_50, W_45]: (~ssPv48_9r1r1r1r1r1r1r1r1r1(U_46, V_52, W_45, X_50, Y_51, Z_47, X1_48, X2_49, skc75)))). % 18.13/5.75 tff(c_976, plain, (![Y_43, X2_41, Z_39, X_42, X1_40, V_44, W_37, U_38]: (ssPv48_9r1r1r1r1r1r1r1r1r1(U_38, V_44, W_37, X_42, Y_43, Z_39, X1_40, X2_41, skc74)))). % 18.13/5.75 tff(c_950, plain, (![W_29, Z_31, V_36, X2_33, X1_32, U_30, X_34, Y_35]: (ssNder1_8r1r1r1r1r1r1r1r1(U_30, V_36, W_29, X_34, Y_35, Z_31, X1_32, X2_33)))). % 18.13/5.75 tff(c_930, plain, (![V_28, X_26, Z_24, Y_27, U_23, W_22, X1_25]: (ssNder1_7r1r1r1r1r1r1r1(U_23, V_28, W_22, X_26, Y_27, Z_24, X1_25)))). % 18.13/5.75 tff(c_912, plain, (![V_21, W_16, U_17, X_19, Z_18, Y_20]: (ssNder1_6r1r1r1r1r1r1(U_17, V_21, W_16, X_19, Y_20, Z_18)))). % 18.13/5.75 tff(c_706, plain, (![Y_14, V_15, U_12, X_13, W_11]: (ssNder1_5r1r1r1r1r1(U_12, V_15, W_11, X_13, Y_14)))). % 18.13/5.75 tff(c_488, plain, (![U_7, V_8, W_9, X_10]: (ssNder1_4r1r1r1r1(U_7, V_8, W_9, X_10)))). % 18.13/5.75 tff(c_468, plain, (![U_4, V_5, W_6]: (ssNder1_3r1r1r1(U_4, V_5, W_6)))). % 18.13/5.75 tff(c_458, plain, (![U_2, V_3]: (ssNder1_2r1r1(U_2, V_3)))). % 18.13/5.75 tff(c_230, plain, (![U_1]: (ssNder1_1r1(U_1)))). % 18.13/5.75 tff(c_2, plain, (ssNder1_0)). % 18.13/5.75 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.13/5.75 %------------------------------------------------------------------------------