%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN868-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 : n023.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 9.32s 3.02s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.09 % Problem : SYN868-1 : TPTP v9.0.0. Released v2.5.0. % 0.09/0.10 % 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.10/0.29 % Computer : n023.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 300 % 0.10/0.29 % DateTime : Wed Apr 9 08:33:39 EDT 2025 % 0.10/0.29 % CPUTime : % 9.32/3.02 % 9.32/3.02 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.32/3.02 % 9.32/3.02 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.32/3.04 %$ ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv18_11r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 > ssPv19_10r1r1r1r1r1r1r1r1r1r1 > ssNder1_10r1r1r1r1r1r1r1r1r1r1 > ssNder1_9r1r1r1r1r1r1r1r1r1 > ssPv21_8r1r1r1r1r1r1r1r1 > ssNder1_8r1r1r1r1r1r1r1r1 > ssPv22_7r1r1r1r1r1r1r1 > ssNder1_7r1r1r1r1r1r1r1 > ssNder1_6r1r1r1r1r1r1 > ssPv24_5r1r1r1r1r1 > ssNder1_5r1r1r1r1r1 > ssPv25_4r1r1r1r1 > ssNder1_4r1r1r1r1 > ssPv26_3r1r1r1 > ssNder1_3r1r1r1 > ssNder1_2r1r1 > ssPv28_1r1 > ssNder1_1r1 > #nlpp > ssNder1_0 > skc35 > skc34 > skc33 > skc32 > skc31 > skc30 > skc29 > skc28 > skc27 > skc26 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 % 9.32/3.04 % 9.32/3.04 %Foreground sorts: % 9.32/3.04 % 9.32/3.04 % 9.32/3.04 %Background operators: % 9.32/3.04 % 9.32/3.04 % 9.32/3.04 %Foreground operators: % 9.32/3.04 tff(ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc34, type, skc34: $i). % 9.32/3.04 tff(ssPv26_3r1r1r1, type, ssPv26_3r1r1r1: ($i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_7r1r1r1r1r1r1r1, type, ssNder1_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv19_10r1r1r1r1r1r1r1r1r1r1, type, ssPv19_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc18, type, skc18: $i). % 9.32/3.04 tff(skc29, type, skc29: $i). % 9.32/3.04 tff(skc25, type, skc25: $i). % 9.32/3.04 tff(ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 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). % 9.32/3.04 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). % 9.32/3.04 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). % 9.32/3.04 tff(ssNder1_10r1r1r1r1r1r1r1r1r1r1, type, ssNder1_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv21_8r1r1r1r1r1r1r1r1, type, ssPv21_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv28_1r1, type, ssPv28_1r1: $i > $o). % 9.32/3.04 tff(ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 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). % 9.32/3.04 tff(skc26, type, skc26: $i). % 9.32/3.04 tff(skc24, type, skc24: $i). % 9.32/3.04 tff(ssNder1_2r1r1, type, ssNder1_2r1r1: ($i * $i) > $o). % 9.32/3.04 tff(skc32, type, skc32: $i). % 9.32/3.04 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). % 9.32/3.04 tff(ssPv18_11r1r1r1r1r1r1r1r1r1r1r1, type, ssPv18_11r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc20, type, skc20: $i). % 9.32/3.04 tff(ssPv22_7r1r1r1r1r1r1r1, type, ssPv22_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 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). % 9.32/3.04 tff(skc23, type, skc23: $i). % 9.32/3.04 tff(ssNder1_0, type, ssNder1_0: $o). % 9.32/3.04 tff(skc21, type, skc21: $i). % 9.32/3.04 tff(ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc22, type, skc22: $i). % 9.32/3.04 tff(ssNder1_11r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_11r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc27, type, skc27: $i). % 9.32/3.04 tff(ssNder1_8r1r1r1r1r1r1r1r1, type, ssNder1_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_5r1r1r1r1r1, type, ssNder1_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_9r1r1r1r1r1r1r1r1r1, type, ssNder1_9r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_3r1r1r1, type, ssNder1_3r1r1r1: ($i * $i * $i) > $o). % 9.32/3.04 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). % 9.32/3.04 tff(skc31, type, skc31: $i). % 9.32/3.04 tff(ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_6r1r1r1r1r1r1, type, ssNder1_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc35, type, skc35: $i). % 9.32/3.04 tff(ssNder1_4r1r1r1r1, type, ssNder1_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 9.32/3.04 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). % 9.32/3.04 tff(ssPv24_5r1r1r1r1r1, type, ssPv24_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc30, type, skc30: $i). % 9.32/3.04 tff(ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc19, type, skc19: $i). % 9.32/3.04 tff(ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(skc33, type, skc33: $i). % 9.32/3.04 tff(ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv2_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). % 9.32/3.04 tff(ssPv25_4r1r1r1r1, type, ssPv25_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 9.32/3.04 tff(ssNder1_1r1, type, ssNder1_1r1: $i > $o). % 9.32/3.04 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). % 9.32/3.04 tff(skc28, type, skc28: $i). % 9.32/3.04 % 9.32/3.04 %Saturated clause set: % 9.32/3.04 tff(c_1400, plain, (![X1_795, X10_809, X17_789, X5_784, X11_796, W_786, X12_792, X14_808, X13_798, X16_783, X15_787, X9_791, U_790, X8_804, X6_785, V_803, X2_797, X21_799, X4_806, Z_793, X20_802, X3_788, X18_807, X7_794, X19_805, Y_801, X_800]: (ssPv19_10r1r1r1r1r1r1r1r1r1r1(U_790, V_803, W_786, X_800, Y_801, Z_793, X1_795, X2_797, X3_788, X4_806) | ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_790, V_803, W_786, X_800, Y_801, Z_793, X1_795, X2_797, X3_788, X4_806, X5_784, X6_785, X7_794, X8_804, X9_791, X10_809, X11_796, X12_792, X13_798, X14_808, X15_787, X16_783, X17_789, X18_807) | ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_790, V_803, W_786, X_800, Y_801, Z_793, X1_795, X2_797, X3_788, X4_806, X5_784, X6_785, X7_794, X8_804, X9_791, X10_809, X11_796, X12_792, X13_798, X14_808, X15_787, X16_783, X17_789, X18_807, X19_805, X20_802, X21_799) | ~ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_790, V_803, W_786, X_800, Y_801, Z_793, X1_795, X2_797, X3_788, X4_806, X5_784, X6_785, X7_794, X8_804, X9_791, X10_809, X11_796, X12_792, X13_798, X14_808, X15_787, X16_783)))). % 9.32/3.05 tff(c_1392, plain, (![W_760, X17_763, X7_768, X20_775, X12_766, X11_770, X3_762, X13_772, X16_757, X10_782, Z_767, X1_769, X14_781, X4_779, X15_761, X9_765, X18_780, Y_774, X2_771, X6_759, X_773, V_776, X8_777, U_764, X5_758, X19_778]: (ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_764, V_776, W_760, X_773, Y_774, Z_767, X1_769, X2_771, X3_762, X4_779, X5_758, X6_759, X7_768, X8_777, X9_765) | ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_764, V_776, W_760, X_773, Y_774, Z_767, X1_769, X2_771, X3_762, X4_779, X5_758, X6_759, X7_768, X8_777, X9_765, X10_782, X11_770, X12_766, X13_772, X14_781, X15_761, X16_757, X17_763, X18_780, X19_778, X20_775) | ~ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(U_764, V_776, W_760, X_773, Y_774, Z_767, X1_769, X2_771, X3_762, X4_779, X5_758, X6_759) | ~ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_764, V_776, W_760, X_773, Y_774, Z_767, X1_769, X2_771, X3_762, X4_779, X5_758, X6_759, X7_768, X8_777, X9_765, X10_782, X11_770, X12_766, X13_772, X14_781, X15_761, X16_757)))). % 9.32/3.05 tff(c_1404, plain, (![X5_732, X9_739, X7_742, U_738, Y_748, X13_746, X15_735, X20_749, X1_743, X_747, X18_754, X16_731, X14_755, W_734, X11_744, Z_741, X12_740, X19_752, X3_736, X4_753, X2_745, X6_733, X17_737, V_750, X8_751, X10_756]: (ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_738, V_750, W_734, X_747, Y_748, Z_741, X1_743, X2_745, X3_736, X4_753, X5_732, X6_733, X7_742) | ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_738, V_750, W_734, X_747, Y_748, Z_741, X1_743, X2_745, X3_736, X4_753, X5_732, X6_733, X7_742, X8_751, X9_739, X10_756, X11_744, X12_740, X13_746, X14_755, X15_735, X16_731, X17_737, X18_754, X19_752, X20_749) | ~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_738, V_750, W_734, X_747, Y_748, Z_741, X1_743, X2_745, X3_736, X4_753, X5_732, X6_733, X7_742, X8_751, X9_739) | ~ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_738, V_750, W_734, X_747, Y_748, Z_741, X1_743, X2_745, X3_736, X4_753, X5_732, X6_733, X7_742, X8_751, X9_739, X10_756, X11_744, X12_740, X13_746, X14_755)))). % 9.32/3.05 tff(c_1402, plain, (![X2_719, X5_706, X1_717, V_724, X7_716, X3_710, X8_725, X16_705, X12_714, W_708, X14_729, U_712, X9_713, Z_715, X6_707, X18_728, X13_720, X_721, X17_711, X20_723, Y_722, X10_730, X15_709, X11_718, X4_727, X19_726]: (ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(U_712, V_724, W_708, X_721, Y_722, Z_715, X1_717, X2_719, X3_710, X4_727, X5_706, X6_707) | ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_712, V_724, W_708, X_721, Y_722, Z_715, X1_717, X2_719, X3_710, X4_727, X5_706, X6_707, X7_716, X8_725, X9_713, X10_730, X11_718, X12_714, X13_720, X14_729, X15_709, X16_705, X17_711, X18_728, X19_726, X20_723) | ~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_712, V_724, W_708, X_721, Y_722, Z_715, X1_717, X2_719, X3_710, X4_727, X5_706, X6_707, X7_716, X8_725, X9_713) | ~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_712, V_724, W_708, X_721, Y_722, Z_715, X1_717, X2_719, X3_710, X4_727, X5_706, X6_707, X7_716, X8_725, X9_713, X10_730)))). % 9.32/3.05 tff(c_1394, plain, (![X9_687, X20_697, X1_691, X8_699, X12_688, X6_681, V_698, Y_696, Z_689, X_695, X3_684, X14_703, X17_685, U_686, W_682, X10_704, X18_702, X4_701, X13_694, X15_683, X5_680, X11_692, X19_700, X2_693, X16_679, X7_690]: (ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_686, V_698, W_682, X_695, Y_696, Z_689, X1_691, X2_693, X3_684, X4_701, X5_680, X6_681, X7_690) | ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_686, V_698, W_682, X_695, Y_696, Z_689, X1_691, X2_693, X3_684, X4_701, X5_680, X6_681, X7_690, X8_699, X9_687, X10_704, X11_692, X12_688, X13_694) | ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_686, V_698, W_682, X_695, Y_696, Z_689, X1_691, X2_693, X3_684, X4_701, X5_680, X6_681, X7_690, X8_699, X9_687, X10_704, X11_692, X12_688, X13_694, X14_703, X15_683, X16_679, X17_685, X18_702, X19_700, X20_697) | ~ssPv24_5r1r1r1r1r1(U_686, V_698, W_682, X_695, Y_696)))). % 9.32/3.05 tff(c_1380, plain, (![V_672, X10_678, X1_666, X7_665, X_670, X8_673, X5_655, W_657, X18_676, X3_659, X12_663, X11_667, Z_664, X13_669, X4_675, Y_671, U_661, X14_677, X2_668, X16_654, X17_660, X15_658, X6_656, X9_662, X19_674]: (~ssPv25_4r1r1r1r1(U_661, V_672, W_657, X_670) | ~ssPv22_7r1r1r1r1r1r1r1(U_661, V_672, W_657, X_670, Y_671, Z_664, X1_666) | ~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_661, V_672, W_657, X_670, Y_671, Z_664, X1_666, X2_668, X3_659, X4_675, X5_655, X6_656, X7_665, X8_673) | ~ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_661, V_672, W_657, X_670, Y_671, Z_664, X1_666, X2_668, X3_659, X4_675, X5_655, X6_656, X7_665, X8_673, X9_662, X10_678, X11_667, X12_663, X13_669, X14_677, X15_658, X16_654, X17_660, X18_676, X19_674)))). % 9.32/3.05 tff(c_1466, plain, (![X2_169, X4_173, Y_171, X_170, X1_168, X3_164, V_172, W_163, Z_166, U_165]: (~ssPv26_3r1r1r1(U_165, V_172, W_163) | ~ssPv19_10r1r1r1r1r1r1r1r1r1r1(U_165, V_172, W_163, X_170, Y_171, Z_166, X1_168, X2_169, X3_164, X4_173)))). % 9.32/3.05 tff(c_1455, plain, (![X6_403, X9_408, Z_410, X5_402, X4_420, Y_417, X10_422, X8_419, X3_406, X_416, X11_413, X7_411, W_404, X2_414, X1_412, X14_421, U_407, V_418, X12_409, X13_415]: (ssPv28_1r1(U_407) | ssPv24_5r1r1r1r1r1(U_407, V_418, W_404, X_416, Y_417) | ~ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_407, V_418, W_404, X_416, Y_417, Z_410, X1_412, X2_414, X3_406, X4_420, X5_402, X6_403, X7_411, X8_419, X9_408, X10_422, X11_413, X12_409, X13_415, X14_421)))). % 9.32/3.05 tff(c_1398, plain, (![X18_651, X13_643, X17_634, X10_653, X8_648, X11_641, X20_646, X_644, X12_637, U_635, X2_642, Y_645, X4_650, V_647, X19_649, X9_636, W_631, X15_632, X16_628, X7_639, X3_633, X6_630, X14_652, X1_640, Z_638, X5_629]: (ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_635, V_647, W_631, X_644, Y_645, Z_638, X1_640, X2_642, X3_633, X4_650, X5_629, X6_630, X7_639, X8_648, X9_636, X10_653, X11_641, X12_637, X13_643, X14_652, X15_632, X16_628, X17_634, X18_651, X19_649, X20_646)))). % 9.32/3.05 tff(c_1390, plain, (![X8_622, Y_620, X18_625, X14_626, X12_612, X17_609, X2_617, W_606, X3_608, X4_624, X11_616, X_619, U_610, X16_603, V_621, Z_613, X6_605, X7_614, X9_611, X15_607, X5_604, X19_623, X10_627, X1_615, X13_618]: (ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_610, V_621, W_606, X_619, Y_620, Z_613, X1_615, X2_617, X3_608, X4_624, X5_604, X6_605, X7_614, X8_622, X9_611, X10_627, X11_616, X12_612, X13_618, X14_626, X15_607, X16_603, X17_609, X18_625, X19_623)))). % 9.32/3.06 tff(c_1342, plain, (![X14_533, X12_521, X13_527, X15_516, Z_522, X6_514, X1_524, X11_525, X17_518, Y_529, X_528, X10_534, X3_517, X8_531, X2_526, X16_512, X7_523, W_515, X4_532, X5_513, U_519, V_530, X9_520]: (~ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_519, V_530, W_515, X_528, Y_529, Z_522, X1_524, X2_526, X3_517, X4_532, X5_513, X6_514, X7_523, X8_531, X9_520, X10_534, X11_525, X12_521, X13_527, X14_533, X15_516, X16_512, X17_518, skc19)))). % 9.32/3.06 tff(c_1364, plain, (![X16_579, X13_594, X2_593, U_586, X17_585, X15_583, X6_581, V_597, Y_596, X4_599, X7_590, X11_592, X5_580, X1_591, W_582, X3_584, X18_600, X12_588, X10_602, X_595, X14_601, X9_587, Z_589, X8_598]: (ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_586, V_597, W_582, X_595, Y_596, Z_589, X1_591, X2_593, X3_584, X4_599, X5_580, X6_581, X7_590, X8_598, X9_587, X10_602, X11_592, X12_588, X13_594, X14_601, X15_583, X16_579, X17_585, X18_600)))). % 9.32/3.06 tff(c_1346, plain, (![X10_511, X14_510, X16_489, X7_500, X5_490, Z_499, X_505, X15_493, X13_504, X12_498, X1_501, X4_509, X8_508, X3_494, Y_506, X9_497, X11_502, W_492, V_507, X6_491, X2_503, U_496, X17_495]: (ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_496, V_507, W_492, X_505, Y_506, Z_499, X1_501, X2_503, X3_494, X4_509, X5_490, X6_491, X7_500, X8_508, X9_497, X10_511, X11_502, X12_498, X13_504, X14_510, X15_493, X16_489, X17_495, skc18)))). % 9.32/3.06 tff(c_1336, plain, (![X11_479, X_482, W_469, X9_474, X17_472, V_484, U_473, X12_475, Z_476, Y_483, X15_470, X4_486, X3_471, X14_487, X6_468, X5_467, X8_485, X13_481, X16_466, X7_477, X10_488, X2_480, X1_478]: (ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_473, V_484, W_469, X_482, Y_483, Z_476, X1_478, X2_480, X3_471, X4_486, X5_467, X6_468, X7_477, X8_485, X9_474, X10_488, X11_479, X12_475, X13_481, X14_487, X15_470, X16_466, X17_472)))). % 9.32/3.06 tff(c_1286, plain, (![X15_405, X6_403, X9_408, Z_410, X5_402, X4_420, Y_417, X10_422, X8_419, X3_406, X_416, X11_413, X7_411, W_404, X2_414, X1_412, X14_421, U_407, V_418, X12_409, X13_415]: (ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_407, V_418, W_404, X_416, Y_417, Z_410, X1_412, X2_414, X3_406, X4_420, X5_402, X6_403, X7_411, X8_419, X9_408, X10_422, X11_413, X12_409, X13_415, X14_421, X15_405, skc20)))). % 9.32/3.06 tff(c_1166, plain, (![X6_326, X7_332, X10_341, X3_328, W_327, X11_334, X2_335, X_336, Y_337, X8_339, X5_325, U_329, V_338, X9_330, X1_333, Z_331, X4_340]: (ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_329, V_338, W_327, X_336, Y_337, Z_331, X1_333, X2_335, X3_328, X4_340, X5_325, X6_326, X7_332, X8_339, X9_330, X10_341, X11_334) | ~ssPv28_1r1(U_329) | ~ssPv21_8r1r1r1r1r1r1r1r1(U_329, V_338, W_327, X_336, Y_337, Z_331, X1_333, X2_335) | ~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_329, V_338, W_327, X_336, Y_337, Z_331, X1_333, X2_335, X3_328, X4_340, X5_325, X6_326, X7_332)))). % 9.32/3.06 tff(c_1298, plain, (![X9_429, V_439, X4_441, X14_442, X10_443, U_428, W_425, X_437, X8_440, X2_435, X11_434, Y_438, X3_427, X13_436, X1_433, X12_430, X6_424, X5_423, X7_432, X15_426, Z_431]: (~ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_428, V_439, W_425, X_437, Y_438, Z_431, X1_433, X2_435, X3_427, X4_441, X5_423, X6_424, X7_432, X8_440, X9_429, X10_443, X11_434, X12_430, X13_436, X14_442, X15_426, skc21)))). % 9.32/3.06 tff(c_1320, plain, (![X10_465, Z_453, X12_452, X8_462, Y_460, W_447, X_459, X9_451, U_450, X15_448, X2_457, V_461, X6_446, X13_458, X3_449, X1_455, X11_456, X4_463, X7_454, X14_464, X5_445, X16_444]: (ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_450, V_461, W_447, X_459, Y_460, Z_453, X1_455, X2_457, X3_449, X4_463, X5_445, X6_446, X7_454, X8_462, X9_451, X10_465, X11_456, X12_452, X13_458, X14_464, X15_448, X16_444)))). % 9.32/3.06 tff(c_1302, plain, (![X15_384, X5_381, V_397, X9_387, W_383, X6_382, X1_391, X8_398, X2_393, X_395, X14_400, U_386, X4_399, X3_385, X10_401, X12_388, X13_394, X7_390, X11_392, Z_389, Y_396]: (ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_386, V_397, W_383, X_395, Y_396, Z_389, X1_391, X2_393, X3_385, X4_399, X5_381, X6_382, X7_390, X8_398, X9_387, X10_401, X11_392, X12_388, X13_394, X14_400, X15_384)))). % 9.32/3.06 tff(c_1268, plain, (![X8_377, X5_361, V_376, Z_368, X_374, X4_378, X9_366, X3_364, U_365, X13_373, X2_372, Y_375, X11_371, X12_367, X6_362, X7_369, X10_380, W_363, X1_370, X14_379]: (ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_365, V_376, W_363, X_374, Y_375, Z_368, X1_370, X2_372, X3_364, X4_378, X5_361, X6_362, X7_369, X8_377, X9_366, X10_380, X11_371, X12_367, X13_373, X14_379)))). % 9.32/3.06 tff(c_1252, plain, (![X7_350, X11_352, X_355, X13_354, X3_345, X2_353, X12_348, X9_347, X4_359, X6_343, X8_358, Z_349, X10_360, W_344, X5_342, X1_351, Y_356, V_357, U_346]: (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_346, V_357, W_344, X_355, Y_356, Z_349, X1_351, X2_353, X3_345, X4_359, X5_342, X6_343, X7_350, X8_358, X9_347, X10_360, X11_352, X12_348, X13_354)))). % 9.32/3.06 tff(c_1228, plain, (![Y_320, X5_307, X_319, X11_317, X3_310, X10_324, X7_315, X4_323, X8_322, V_321, U_311, X2_318, X12_313, W_309, Z_314, X1_316, X6_308, X9_312]: (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_311, V_321, W_309, X_319, Y_320, Z_314, X1_316, X2_318, X3_310, X4_323, X5_307, X6_308, X7_315, X8_322, X9_312, X10_324, X11_317, X12_313)))). % 9.32/3.06 tff(c_1192, plain, (![X_301, X9_295, X10_306, W_292, V_303, X3_293, Y_302, X4_305, U_294, X5_290, X8_304, Z_296, X1_298, X2_300, X7_297, X6_291, X11_299]: (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_294, V_303, W_292, X_301, Y_302, Z_296, X1_298, X2_300, X3_293, X4_305, X5_290, X6_291, X7_297, X8_304, X9_295, X10_306, X11_299)))). % 9.32/3.06 tff(c_1048, plain, (![X_254, Z_250, X8_257, X1_252, X4_258, X7_251, X9_249, X3_247, X6_245, X5_244, U_248, W_246, V_256, Y_255, X2_253]: (ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_248, V_256, W_246, X_254, Y_255, Z_250, X1_252, X2_253, X3_247, X4_258, X5_244, X6_245, X7_251, X8_257, X9_249, skc22)))). % 9.32/3.06 tff(c_1100, plain, (![X3_277, X2_283, Z_280, X5_274, X8_287, W_276, X10_289, X9_279, X6_275, V_286, X7_281, Y_285, X1_282, X_284, U_278, X4_288]: (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_278, V_286, W_276, X_284, Y_285, Z_280, X1_282, X2_283, X3_277, X4_288, X5_274, X6_275, X7_281, X8_287, X9_279, X10_289)))). % 9.32/3.06 tff(c_1094, plain, (![Z_265, X8_272, X6_260, X2_268, V_271, X9_264, U_263, X7_266, X3_262, W_261, Y_270, X5_259, X4_273, X_269, X1_267]: (~ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_263, V_271, W_261, X_269, Y_270, Z_265, X1_267, X2_268, X3_262, X4_273, X5_259, X6_260, X7_266, X8_272, X9_264, skc23)))). % 9.32/3.06 tff(c_986, plain, (![Z_220, X7_221, X5_215, X1_222, X3_218, X8_227, X6_216, Y_225, U_219, W_217, X_224, X4_228, V_226, X2_223]: (~ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_219, V_226, W_217, X_224, Y_225, Z_220, X1_222, X2_223, X3_218, X4_228, X5_215, X6_216, X7_221, X8_227, skc25)))). % 9.32/3.06 tff(c_1040, plain, (![U_205, X7_207, X4_214, X_210, X3_204, X2_209, X6_202, X5_201, Z_206, X8_213, W_203, V_212, Y_211, X1_208]: (ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_205, V_212, W_203, X_210, Y_211, Z_206, X1_208, X2_209, X3_204, X4_214, X5_201, X6_202, X7_207, X8_213, skc24)))). % 9.32/3.06 tff(c_1076, plain, (![X6_230, X5_229, X_239, Z_235, X2_238, X1_237, V_241, X3_232, X8_242, X7_236, Y_240, X9_234, W_231, U_233, X4_243]: (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_233, V_241, W_231, X_239, Y_240, Z_235, X1_237, X2_238, X3_232, X4_243, X5_229, X6_230, X7_236, X8_242, X9_234)))). % 9.32/3.06 tff(c_1042, plain, (![X7_193, X6_188, X3_190, W_189, X2_195, Y_197, V_198, X_196, X4_200, Z_192, U_191, X8_199, X1_194, X5_187]: (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_191, V_198, W_189, X_196, Y_197, Z_192, X1_194, X2_195, X3_190, X4_200, X5_187, X6_188, X7_193, X8_199)))). % 9.32/3.06 tff(c_918, plain, (![X2_169, X4_173, Y_171, X_170, X1_168, X3_164, V_172, W_163, X7_167, X5_161, Z_166, X6_162, U_165]: (ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_165, V_172, W_163, X_170, Y_171, Z_166, X1_168, X2_169, X3_164, X4_173, X5_161, X6_162, X7_167, skc26)))). % 9.32/3.06 tff(c_932, plain, (![X6_175, U_178, Z_179, V_185, X1_181, W_176, X7_180, X5_174, X2_182, X4_186, X3_177, X_183, Y_184]: (~ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_178, V_185, W_176, X_183, Y_184, Z_179, X1_181, X2_182, X3_177, X4_186, X5_174, X6_175, X7_180, skc27)))). % 9.32/3.06 tff(c_850, plain, (![X5_113, W_115, X3_116, U_117, X2_120, V_123, Z_118, X_121, X4_124, Y_122, X6_114, X1_119]: (ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_117, V_123, W_115, X_121, Y_122, Z_118, X1_119, X2_120, X3_116, X4_124, X5_113, X6_114, skc28)))). % 9.32/3.06 tff(c_924, plain, (![X2_156, X3_151, V_159, X5_148, Y_158, U_152, X6_149, Z_153, X7_154, X_157, X1_155, X4_160, W_150]: (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_152, V_159, W_150, X_157, Y_158, Z_153, X1_155, X2_156, X3_151, X4_160, X5_148, X6_149, X7_154)))). % 9.32/3.06 tff(c_926, plain, (![X2_132, Z_130, X_133, X3_128, Y_134, U_129, X6_126, V_135, X4_136, X5_125, X1_131, W_127]: (~ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_129, V_135, W_127, X_133, Y_134, Z_130, X1_131, X2_132, X3_128, X4_136, X5_125, X6_126, skc29)))). % 9.32/3.06 tff(c_774, plain, (![X4_147, X_144, Y_145, Z_141, X3_139, X5_137, U_140, X1_142, V_146, X2_143, W_138]: (ssPv26_3r1r1r1(U_140, V_146, W_138) | ssPv21_8r1r1r1r1r1r1r1r1(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143) | ~ssPv22_7r1r1r1r1r1r1r1(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142) | ~ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143, X3_139, X4_147, X5_137)))). % 9.32/3.06 tff(c_916, plain, (![X6_102, U_105, V_111, W_103, X_109, X5_101, X2_108, X1_107, X4_112, Z_106, Y_110, X3_104]: (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U_105, V_111, W_103, X_109, Y_110, Z_106, X1_107, X2_108, X3_104, X4_112, X5_101, X6_102)))). % 9.32/3.06 tff(c_778, plain, (![Y_98, X5_90, X_97, X4_100, W_91, X3_92, Z_94, X1_95, U_93, V_99, X2_96]: (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U_93, V_99, W_91, X_97, Y_98, Z_94, X1_95, X2_96, X3_92, X4_100, X5_90)))). % 9.32/3.06 tff(c_710, plain, (![Y_87, X_86, W_80, X3_81, Z_83, X4_89, U_82, V_88, X2_85, X1_84]: (ssNder1_10r1r1r1r1r1r1r1r1r1r1(U_82, V_88, W_80, X_86, Y_87, Z_83, X1_84, X2_85, X3_81, X4_89)))). % 9.32/3.06 tff(c_618, plain, (![U_73, V_79, X1_75, X2_76, Y_78, Z_74, X3_72, X_77, W_71]: (ssNder1_9r1r1r1r1r1r1r1r1r1(U_73, V_79, W_71, X_77, Y_78, Z_74, X1_75, X2_76, X3_72)))). % 9.32/3.06 tff(c_540, plain, (![Z_65, Y_69, X_68, U_64, X1_66, V_70, X2_67, W_63]: (ssNder1_8r1r1r1r1r1r1r1r1(U_64, V_70, W_63, X_68, Y_69, Z_65, X1_66, X2_67)))). % 9.32/3.06 tff(c_510, plain, (![X1_52, Z_51, Y_54, U_50, X_53, V_55, W_49]: (ssPv21_8r1r1r1r1r1r1r1r1(U_50, V_55, W_49, X_53, Y_54, Z_51, X1_52, skc30)))). % 9.32/3.06 tff(c_358, plain, (![V_41, W_36, U_37, Y_40, X_39, Z_38]: (~ssPv22_7r1r1r1r1r1r1r1(U_37, V_41, W_36, X_39, Y_40, Z_38, skc33)))). % 9.32/3.06 tff(c_350, plain, (![X_33, V_35, U_31, Z_32, W_30, Y_34]: (ssPv22_7r1r1r1r1r1r1r1(U_31, V_35, W_30, X_33, Y_34, Z_32, skc32)))). % 9.32/3.06 tff(c_450, plain, (![Y_47, X1_45, W_42, X_46, U_43, Z_44, V_48]: (ssNder1_7r1r1r1r1r1r1r1(U_43, V_48, W_42, X_46, Y_47, Z_44, X1_45)))). % 9.32/3.06 tff(c_454, plain, (![X_60, Z_58, U_57, Y_61, W_56, X1_59, V_62]: (~ssPv21_8r1r1r1r1r1r1r1r1(U_57, V_62, W_56, X_60, Y_61, Z_58, X1_59, skc31)))). % 9.32/3.06 tff(c_354, plain, (![W_24, U_25, Z_26, V_29, Y_28, X_27]: (ssNder1_6r1r1r1r1r1r1(U_25, V_29, W_24, X_27, Y_28, Z_26)))). % 9.32/3.06 tff(c_286, plain, (![U_11, V_12, W_13, X_14]: (ssPv24_5r1r1r1r1r1(U_11, V_12, W_13, X_14, skc34)))). % 9.32/3.06 tff(c_288, plain, (![U_15, V_16, W_17, X_18]: (~ssPv24_5r1r1r1r1r1(U_15, V_16, W_17, X_18, skc35)))). % 9.32/3.06 tff(c_250, plain, (![U_20, X_21, Y_22, W_19, V_23]: (ssNder1_5r1r1r1r1r1(U_20, V_23, W_19, X_21, Y_22)))). % 9.32/3.07 tff(c_248, plain, (![U_7, V_8, W_9, X_10]: (ssNder1_4r1r1r1r1(U_7, V_8, W_9, X_10)))). % 9.32/3.07 tff(c_230, plain, (![U_4, V_5, W_6]: (ssNder1_3r1r1r1(U_4, V_5, W_6)))). % 9.32/3.07 tff(c_222, plain, (![U_2, V_3]: (ssNder1_2r1r1(U_2, V_3)))). % 9.32/3.07 tff(c_112, plain, (![U_1]: (ssNder1_1r1(U_1)))). % 9.32/3.07 tff(c_2, plain, (ssNder1_0)). % 9.32/3.07 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.32/3.07 %------------------------------------------------------------------------------