%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN772-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 : n021.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:04:53 PM UTC 2025 % Result : Satisfiable 12.51s 4.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN772-1 : TPTP v9.0.0. Released v2.5.0. % 0.03/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.35 % Computer : n021.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Apr 9 08:18:59 EDT 2025 % 0.13/0.35 % CPUTime : % 12.51/4.95 % 12.51/4.96 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.51/4.96 % 12.51/4.96 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.51/4.97 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf3 > skf2 % 12.51/4.97 % 12.51/4.97 %Foreground sorts: % 12.51/4.97 % 12.51/4.97 % 12.51/4.97 %Background operators: % 12.51/4.97 % 12.51/4.97 % 12.51/4.97 %Foreground operators: % 12.51/4.97 tff(skf3, type, skf3: $i > $i). % 12.51/4.97 tff(ssPv1, type, ssPv1: $i > $o). % 12.51/4.97 tff(ssPv3, type, ssPv3: $i > $o). % 12.51/4.97 tff(ssPv7, type, ssPv7: $i > $o). % 12.51/4.97 tff(ssPv6, type, ssPv6: $i > $o). % 12.51/4.97 tff(ssPv5, type, ssPv5: $i > $o). % 12.51/4.97 tff(skf2, type, skf2: $i > $i). % 12.51/4.97 tff(ssRr, type, ssRr: ($i * $i) > $o). % 12.51/4.97 tff(ssPv4, type, ssPv4: $i > $o). % 12.51/4.97 tff(ssPv2, type, ssPv2: $i > $o). % 12.51/4.97 tff(ssPv8, type, ssPv8: $i > $o). % 12.51/4.97 % 12.51/4.97 %Saturated clause set: % 12.51/4.97 tff(c_6591, plain, (![U_574]: (ssPv5(skf3(skf3(U_574))) | ssPv2(skf3(skf3(U_574))) | ~ssPv3(skf3(skf3(U_574))) | ssPv6(skf3(skf3(U_574))) | ssPv1(skf3(skf3(U_574))) | ~ssPv7(skf3(skf3(U_574))) | ssPv1(skf3(U_574)) | ssPv1(skf2(skf3(U_574))) | ~ssPv4(skf2(skf3(U_574))) | ~ssPv5(skf2(skf3(U_574))) | ssPv2(skf2(skf3(U_574))) | ~ssPv3(skf2(skf3(U_574))) | ssPv6(skf2(skf3(U_574))) | ~ssPv8(skf3(U_574)) | ~ssPv7(skf3(U_574)) | ~ssPv5(skf3(U_574)) | ~ssPv6(U_574)))). % 12.51/4.97 tff(c_6613, plain, (![U_577]: (ssPv5(skf3(skf3(U_577))) | ssPv2(skf3(skf3(U_577))) | ~ssPv3(skf3(skf3(U_577))) | ssPv6(skf3(skf3(U_577))) | ssPv1(skf3(skf3(U_577))) | ~ssPv7(skf3(skf3(U_577))) | ssPv1(skf3(U_577)) | ssPv1(skf2(skf3(U_577))) | ~ssPv4(skf2(skf3(U_577))) | ssPv6(skf2(skf3(U_577))) | ~ssPv5(skf2(skf3(U_577))) | ssPv2(skf2(skf3(U_577))) | ~ssPv3(skf2(skf3(U_577))) | ~ssPv3(skf3(U_577)) | ~ssPv7(skf3(U_577)) | ~ssPv5(skf3(U_577)) | ~ssPv6(U_577)))). % 12.51/4.97 tff(c_6504, plain, (![U_570]: (ssPv5(skf3(skf3(U_570))) | ssPv2(skf3(skf3(U_570))) | ~ssPv3(skf3(skf3(U_570))) | ssPv6(skf3(skf3(U_570))) | ssPv1(skf3(skf3(U_570))) | ~ssPv7(skf3(skf3(U_570))) | ssPv1(skf3(U_570)) | ~ssPv5(skf2(skf3(U_570))) | ssPv6(skf2(skf3(U_570))) | ssPv3(skf3(U_570)) | ssPv2(skf2(skf3(U_570))) | ssPv3(skf2(skf3(U_570))) | ~ssPv1(skf2(skf3(U_570))) | ~ssPv6(skf3(U_570)) | ~ssPv7(skf3(U_570)) | ~ssPv5(skf3(U_570)) | ~ssPv6(U_570)))). % 12.51/4.97 tff(c_7066, plain, (![U_584]: (ssPv2(skf3(skf3(U_584))) | ~ssPv6(skf3(skf3(U_584))) | ssPv3(skf3(skf3(U_584))) | ssPv1(skf3(U_584)) | ~ssPv5(skf2(skf3(U_584))) | ssPv6(skf2(skf3(U_584))) | ssPv2(skf2(skf3(U_584))) | ssPv3(skf2(skf3(U_584))) | ~ssPv1(skf2(skf3(U_584))) | ~ssPv6(skf3(U_584)) | ~ssPv7(skf3(U_584)) | ~ssPv5(skf3(U_584)) | ~ssPv6(U_584) | ssPv3(skf3(U_584)) | ~ssPv5(skf3(skf3(U_584))) | ~ssPv4(skf3(U_584))))). % 12.51/4.97 tff(c_6616, plain, (![U_577]: (ssPv2(skf3(skf3(U_577))) | ~ssPv3(skf3(skf3(U_577))) | ~ssPv4(skf3(U_577)) | ssPv1(skf3(U_577)) | ssPv1(skf2(skf3(U_577))) | ~ssPv4(skf2(skf3(U_577))) | ssPv6(skf2(skf3(U_577))) | ~ssPv5(skf2(skf3(U_577))) | ssPv2(skf2(skf3(U_577))) | ~ssPv3(skf2(skf3(U_577))) | ~ssPv3(skf3(U_577)) | ~ssPv7(skf3(U_577)) | ~ssPv5(skf3(U_577)) | ~ssPv6(U_577)))). % 12.51/4.97 tff(c_6594, plain, (![U_574]: (ssPv2(skf3(skf3(U_574))) | ~ssPv3(skf3(skf3(U_574))) | ~ssPv4(skf3(U_574)) | ssPv1(skf3(U_574)) | ssPv1(skf2(skf3(U_574))) | ~ssPv4(skf2(skf3(U_574))) | ~ssPv5(skf2(skf3(U_574))) | ssPv2(skf2(skf3(U_574))) | ~ssPv3(skf2(skf3(U_574))) | ssPv6(skf2(skf3(U_574))) | ~ssPv8(skf3(U_574)) | ~ssPv7(skf3(U_574)) | ~ssPv5(skf3(U_574)) | ~ssPv6(U_574)))). % 12.51/4.97 tff(c_6507, plain, (![U_570]: (ssPv2(skf3(skf3(U_570))) | ~ssPv3(skf3(skf3(U_570))) | ~ssPv4(skf3(U_570)) | ssPv1(skf3(U_570)) | ~ssPv5(skf2(skf3(U_570))) | ssPv6(skf2(skf3(U_570))) | ssPv3(skf3(U_570)) | ssPv2(skf2(skf3(U_570))) | ssPv3(skf2(skf3(U_570))) | ~ssPv1(skf2(skf3(U_570))) | ~ssPv6(skf3(U_570)) | ~ssPv7(skf3(U_570)) | ~ssPv5(skf3(U_570)) | ~ssPv6(U_570)))). % 12.51/4.97 tff(c_6593, plain, (![U_574]: (ssPv6(skf3(U_574)) | ssPv3(skf3(skf3(U_574))) | ssPv1(skf3(U_574)) | ssPv1(skf2(skf3(U_574))) | ~ssPv4(skf2(skf3(U_574))) | ~ssPv5(skf2(skf3(U_574))) | ssPv2(skf2(skf3(U_574))) | ~ssPv3(skf2(skf3(U_574))) | ssPv6(skf2(skf3(U_574))) | ~ssPv8(skf3(U_574)) | ~ssPv7(skf3(U_574)) | ~ssPv5(skf3(U_574)) | ~ssPv6(U_574)))). % 12.51/4.98 tff(c_5074, plain, (![U_505]: (ssPv5(skf3(U_505)) | ssPv2(skf3(U_505)) | ~ssPv3(skf3(U_505)) | ssPv6(skf3(U_505)) | ssPv1(skf3(U_505)) | ~ssPv7(skf3(U_505)) | ssPv1(U_505) | ~ssPv7(U_505) | ssPv1(skf2(U_505)) | ~ssPv4(skf2(U_505)) | ssPv6(skf2(U_505)) | ~ssPv5(skf2(U_505)) | ~ssPv3(skf2(U_505)) | ssPv4(U_505) | ssPv2(skf2(U_505)) | ~ssPv3(U_505)))). % 12.51/4.98 tff(c_5076, plain, (![U_201]: (ssPv6(skf2(U_201)) | ssPv3(U_201) | ~ssPv8(skf2(U_201)) | ssPv1(skf2(U_201)) | ~ssPv7(skf2(U_201)) | ssPv1(skf2(skf2(U_201))) | ~ssPv4(skf2(skf2(U_201))) | ssPv6(skf2(skf2(U_201))) | ~ssPv5(skf2(skf2(U_201))) | ~ssPv3(skf2(skf2(U_201))) | ssPv4(skf2(U_201)) | ssPv2(skf2(skf2(U_201))) | ~ssPv3(skf2(U_201))))). % 12.51/4.98 tff(c_6599, plain, (![U_575]: (ssPv1(skf3(U_575)) | ssPv8(skf3(skf3(U_575))) | ssPv1(skf2(skf3(U_575))) | ~ssPv4(skf2(skf3(U_575))) | ssPv6(skf2(skf3(U_575))) | ~ssPv5(skf2(skf3(U_575))) | ssPv2(skf2(skf3(U_575))) | ~ssPv3(skf2(skf3(U_575))) | ~ssPv3(skf3(U_575)) | ~ssPv7(skf3(U_575)) | ~ssPv5(skf3(U_575)) | ~ssPv6(U_575)))). % 12.51/4.98 tff(c_6380, plain, (![U_561, U_120]: (ssPv1(skf3(U_561)) | ssPv8(U_120) | ~ssRr(U_120, skf3(U_561)) | ssPv1(skf2(skf3(U_561))) | ~ssPv4(skf2(skf3(U_561))) | ssPv6(skf2(skf3(U_561))) | ~ssPv5(skf2(skf3(U_561))) | ssPv2(skf2(skf3(U_561))) | ~ssPv3(skf2(skf3(U_561))) | ~ssPv3(skf3(U_561)) | ~ssPv7(skf3(U_561)) | ~ssPv5(skf3(U_561)) | ~ssPv6(U_561)))). % 12.51/4.98 tff(c_6577, plain, (![U_572]: (ssPv1(skf3(U_572)) | ssPv8(skf3(skf3(U_572))) | ssPv1(skf2(skf3(U_572))) | ~ssPv4(skf2(skf3(U_572))) | ~ssPv5(skf2(skf3(U_572))) | ssPv2(skf2(skf3(U_572))) | ~ssPv3(skf2(skf3(U_572))) | ssPv6(skf2(skf3(U_572))) | ~ssPv8(skf3(U_572)) | ~ssPv7(skf3(U_572)) | ~ssPv5(skf3(U_572)) | ~ssPv6(U_572)))). % 12.51/4.98 tff(c_6400, plain, (![U_562, U_120]: (ssPv1(skf3(U_562)) | ssPv8(U_120) | ~ssRr(U_120, skf3(U_562)) | ssPv1(skf2(skf3(U_562))) | ~ssPv4(skf2(skf3(U_562))) | ~ssPv5(skf2(skf3(U_562))) | ssPv2(skf2(skf3(U_562))) | ~ssPv3(skf2(skf3(U_562))) | ssPv6(skf2(skf3(U_562))) | ~ssPv8(skf3(U_562)) | ~ssPv7(skf3(U_562)) | ~ssPv5(skf3(U_562)) | ~ssPv6(U_562)))). % 12.51/4.98 tff(c_4014, plain, (![U_2]: (ssPv5(skf3(skf2(U_2))) | ssPv2(skf3(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2))) | ssPv6(skf3(skf2(U_2))) | ssPv1(skf3(skf2(U_2))) | ~ssPv7(skf2(U_2)) | ssPv8(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv6(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.51/4.98 tff(c_6490, plain, (![U_568]: (ssPv1(skf3(U_568)) | ssPv8(skf3(skf3(U_568))) | ~ssPv5(skf2(skf3(U_568))) | ssPv6(skf2(skf3(U_568))) | ssPv3(skf3(U_568)) | ssPv2(skf2(skf3(U_568))) | ssPv3(skf2(skf3(U_568))) | ~ssPv1(skf2(skf3(U_568))) | ~ssPv6(skf3(U_568)) | ~ssPv7(skf3(U_568)) | ~ssPv5(skf3(U_568)) | ~ssPv6(U_568)))). % 12.51/4.98 tff(c_6280, plain, (![U_556, U_120]: (ssPv1(skf3(U_556)) | ssPv8(U_120) | ~ssRr(U_120, skf3(U_556)) | ~ssPv5(skf2(skf3(U_556))) | ssPv6(skf2(skf3(U_556))) | ssPv3(skf3(U_556)) | ssPv2(skf2(skf3(U_556))) | ssPv3(skf2(skf3(U_556))) | ~ssPv1(skf2(skf3(U_556))) | ~ssPv6(skf3(U_556)) | ~ssPv7(skf3(U_556)) | ~ssPv5(skf3(U_556)) | ~ssPv6(U_556)))). % 12.51/4.98 tff(c_6479, plain, (![U_566]: (ssPv2(skf3(skf3(U_566))) | ~ssPv6(skf3(skf3(U_566))) | ~ssPv5(skf3(U_566)) | ssPv3(skf3(skf3(U_566))) | ssPv1(skf3(U_566)) | ~ssPv7(skf3(U_566)) | ~ssPv6(skf3(U_566)) | ~ssPv4(skf2(skf3(U_566))) | ~ssPv5(U_566) | ssPv3(skf3(U_566)) | ~ssPv5(skf3(skf3(U_566))) | ~ssPv4(skf3(U_566))))). % 12.51/4.98 tff(c_2655, plain, (![U_352]: (ssPv2(skf3(skf3(U_352))) | ~ssPv6(skf3(skf3(U_352))) | ~ssPv4(skf3(U_352)) | ~ssPv5(skf3(U_352)) | ssPv3(skf3(skf3(U_352))) | ~ssPv7(skf3(skf3(U_352))) | ~ssPv5(skf3(skf3(U_352))) | ssPv1(skf3(U_352)) | ~ssPv7(skf3(U_352)) | ~ssPv6(skf3(U_352)) | ~ssPv4(skf2(skf3(U_352))) | ~ssPv5(U_352)))). % 12.51/4.98 tff(c_6354, plain, (![U_559]: (ssPv2(skf3(skf3(U_559))) | ~ssPv6(skf3(skf3(U_559))) | ~ssPv5(skf3(U_559)) | ssPv3(skf3(skf3(U_559))) | ssPv1(skf3(U_559)) | ~ssPv7(skf3(U_559)) | ~ssPv6(skf3(U_559)) | ~ssPv4(U_559) | ~ssPv5(skf2(skf3(U_559))) | ssPv3(skf3(U_559)) | ~ssPv5(skf3(skf3(U_559))) | ~ssPv4(skf3(U_559))))). % 12.51/4.98 tff(c_3890, plain, (![U_355]: (ssPv5(skf3(skf3(U_355))) | ssPv2(skf3(skf3(U_355))) | ~ssPv3(skf3(skf3(U_355))) | ssPv6(skf3(skf3(U_355))) | ssPv1(skf3(skf3(U_355))) | ~ssPv7(skf3(skf3(U_355))) | ssPv1(skf3(U_355)) | ~ssPv7(skf3(U_355)) | ~ssPv6(skf3(U_355)) | ~ssPv4(U_355) | ~ssPv5(skf2(skf3(U_355)))))). % 12.51/4.98 tff(c_3891, plain, (![U_352]: (ssPv5(skf3(skf3(U_352))) | ssPv2(skf3(skf3(U_352))) | ~ssPv3(skf3(skf3(U_352))) | ssPv6(skf3(skf3(U_352))) | ssPv1(skf3(skf3(U_352))) | ~ssPv7(skf3(skf3(U_352))) | ssPv1(skf3(U_352)) | ~ssPv7(skf3(U_352)) | ~ssPv6(skf3(U_352)) | ~ssPv4(skf2(skf3(U_352))) | ~ssPv5(U_352)))). % 12.51/4.98 tff(c_3721, plain, (![U_1]: (ssPv1(skf2(skf3(U_1))) | ~ssPv4(skf2(skf3(U_1))) | ssPv7(skf2(skf3(U_1))) | ~ssPv5(skf2(skf3(U_1))) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv6(skf2(skf3(U_1))) | ~ssPv8(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.51/4.98 tff(c_3772, plain, (![U_1]: (ssPv1(skf2(skf3(U_1))) | ~ssPv4(skf2(skf3(U_1))) | ssPv6(skf2(skf3(U_1))) | ssPv7(skf2(skf3(U_1))) | ~ssPv5(skf2(skf3(U_1))) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.51/4.98 tff(c_6329, plain, (![U_558]: (ssPv2(skf3(skf3(U_558))) | ~ssPv6(skf3(skf3(U_558))) | ~ssPv5(skf3(U_558)) | ssPv3(skf3(skf3(U_558))) | ssPv1(skf3(U_558)) | ~ssPv7(skf3(U_558)) | ~ssPv6(skf3(U_558)) | ~ssPv4(U_558) | ~ssPv5(U_558) | ssPv3(skf3(U_558)) | ~ssPv5(skf3(skf3(U_558))) | ~ssPv4(skf3(U_558))))). % 12.51/4.98 tff(c_2654, plain, (![U_355]: (ssPv2(skf3(skf3(U_355))) | ~ssPv6(skf3(skf3(U_355))) | ~ssPv4(skf3(U_355)) | ~ssPv5(skf3(U_355)) | ssPv3(skf3(skf3(U_355))) | ~ssPv7(skf3(skf3(U_355))) | ~ssPv5(skf3(skf3(U_355))) | ssPv1(skf3(U_355)) | ~ssPv7(skf3(U_355)) | ~ssPv6(skf3(U_355)) | ~ssPv4(U_355) | ~ssPv5(skf2(skf3(U_355)))))). % 12.51/4.98 tff(c_2657, plain, (![U_331]: (ssPv2(skf3(skf3(U_331))) | ~ssPv6(skf3(skf3(U_331))) | ~ssPv4(skf3(U_331)) | ~ssPv5(skf3(U_331)) | ssPv3(skf3(skf3(U_331))) | ~ssPv7(skf3(skf3(U_331))) | ~ssPv5(skf3(skf3(U_331))) | ssPv1(skf3(U_331)) | ~ssPv7(skf3(U_331)) | ~ssPv6(skf3(U_331)) | ~ssPv4(U_331) | ~ssPv5(U_331)))). % 12.51/4.98 tff(c_3892, plain, (![U_341]: (ssPv5(skf3(skf3(U_341))) | ssPv2(skf3(skf3(U_341))) | ~ssPv3(skf3(skf3(U_341))) | ssPv6(skf3(skf3(U_341))) | ssPv1(skf3(skf3(U_341))) | ~ssPv7(skf3(skf3(U_341))) | ssPv1(skf3(U_341)) | ~ssPv7(skf3(U_341)) | ssPv8(skf3(U_341)) | ~ssPv5(skf3(U_341)) | ~ssPv5(U_341)))). % 12.51/4.98 tff(c_3026, plain, (![U_1]: (ssPv7(skf2(skf3(U_1))) | ~ssPv5(skf2(skf3(U_1))) | ssPv6(skf2(skf3(U_1))) | ssPv3(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ssPv3(skf2(skf3(U_1))) | ~ssPv1(skf2(skf3(U_1))) | ~ssPv6(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.51/4.98 tff(c_3893, plain, (![U_331]: (ssPv5(skf3(skf3(U_331))) | ssPv2(skf3(skf3(U_331))) | ~ssPv3(skf3(skf3(U_331))) | ssPv6(skf3(skf3(U_331))) | ssPv1(skf3(skf3(U_331))) | ~ssPv7(skf3(skf3(U_331))) | ssPv1(skf3(U_331)) | ~ssPv7(skf3(U_331)) | ~ssPv6(skf3(U_331)) | ~ssPv4(U_331) | ~ssPv5(U_331)))). % 12.51/4.98 tff(c_6229, plain, (![U_553]: (ssPv2(skf3(skf3(U_553))) | ~ssPv6(skf3(skf3(U_553))) | ~ssPv5(skf3(U_553)) | ssPv3(skf3(skf3(U_553))) | ~ssPv6(skf3(U_553)) | ssPv1(skf3(U_553)) | ~ssPv7(skf3(U_553)) | ~ssPv7(U_553) | ssPv3(skf3(U_553)) | ~ssPv5(skf3(skf3(U_553))) | ~ssPv4(skf3(U_553))))). % 12.51/4.98 tff(c_2665, plain, (![U_189]: (ssPv2(skf3(skf3(U_189))) | ~ssPv6(skf3(skf3(U_189))) | ~ssPv4(skf3(U_189)) | ~ssPv5(skf3(U_189)) | ssPv3(skf3(skf3(U_189))) | ~ssPv7(skf3(skf3(U_189))) | ~ssPv5(skf3(skf3(U_189))) | ~ssPv6(skf3(U_189)) | ssPv1(skf3(U_189)) | ~ssPv7(skf3(U_189)) | ~ssPv7(U_189)))). % 12.51/4.98 tff(c_5498, plain, (![U_525]: (ssPv2(skf3(U_525)) | ssPv4(skf3(U_525)) | ssPv2(U_525) | ~ssPv3(skf3(U_525)) | ~ssPv4(skf2(skf3(U_525))) | ssPv7(skf3(U_525)) | ssPv4(skf3(skf3(U_525))) | ~ssPv3(skf2(skf3(U_525))) | ssPv8(skf3(U_525)) | ~ssPv6(skf3(U_525)) | ~ssPv1(skf2(skf3(U_525)))))). % 12.51/4.98 tff(c_5523, plain, (![U_526]: (ssPv2(skf3(U_526)) | ssPv4(skf3(U_526)) | ssPv2(skf2(skf3(U_526))) | ~ssPv3(skf3(U_526)) | ~ssPv4(skf2(skf3(U_526))) | ssPv7(skf3(U_526)) | ssPv4(skf3(skf3(U_526))) | ~ssPv3(U_526) | ssPv8(skf3(U_526)) | ~ssPv6(skf3(U_526)) | ~ssPv1(skf2(skf3(U_526)))))). % 12.51/4.98 tff(c_3899, plain, (![U_208]: (ssPv5(skf3(skf3(U_208))) | ssPv2(skf3(skf3(U_208))) | ~ssPv3(skf3(skf3(U_208))) | ssPv6(skf3(skf3(U_208))) | ssPv1(skf3(skf3(U_208))) | ~ssPv7(skf3(skf3(U_208))) | ~ssPv7(skf3(U_208)) | ssPv8(skf3(U_208)) | ssPv4(skf3(U_208)) | ssPv6(U_208)))). % 12.51/4.99 tff(c_5167, plain, (![U_510]: (ssPv2(skf3(U_510)) | ssPv5(skf3(U_510)) | ~ssPv4(skf3(U_510)) | ~ssPv3(skf3(U_510)) | ~ssPv4(skf2(skf3(U_510))) | ssPv7(skf3(U_510)) | ssPv4(skf3(skf3(U_510))) | ~ssPv3(U_510) | ssPv8(skf3(U_510)) | ~ssPv6(skf3(U_510)) | ~ssPv1(skf2(skf3(U_510)))))). % 12.51/4.99 tff(c_2754, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_5227, plain, (![U_514]: (ssPv2(skf3(U_514)) | ssPv4(skf3(U_514)) | ssPv2(skf2(skf3(U_514))) | ~ssPv3(skf3(U_514)) | ~ssPv5(skf3(U_514)) | ssPv7(skf3(U_514)) | ssPv4(skf3(skf3(U_514))) | ~ssPv3(U_514) | ssPv8(skf3(U_514)) | ~ssPv6(skf3(U_514)) | ~ssPv1(skf2(skf3(U_514)))))). % 12.51/4.99 tff(c_5181, plain, (![U_512]: (ssPv2(skf2(U_512)) | ssPv5(skf2(U_512)) | ~ssPv4(skf2(U_512)) | ~ssPv3(skf2(U_512)) | ~ssPv4(skf2(skf2(U_512))) | ssPv7(skf2(U_512)) | ssPv4(U_512) | ~ssPv3(skf2(skf2(U_512))) | ssPv8(skf2(U_512)) | ~ssPv6(skf2(U_512)) | ~ssPv1(skf2(skf2(U_512)))))). % 12.51/4.99 tff(c_5045, plain, (![U_501]: (ssPv2(skf3(U_501)) | ssPv5(skf3(U_501)) | ~ssPv4(skf3(U_501)) | ~ssPv3(skf3(U_501)) | ~ssPv4(U_501) | ssPv7(skf3(U_501)) | ssPv4(skf3(skf3(U_501))) | ~ssPv3(skf2(skf3(U_501))) | ssPv8(skf3(U_501)) | ~ssPv6(skf3(U_501)) | ~ssPv1(skf2(skf3(U_501)))))). % 12.51/4.99 tff(c_3938, plain, (![U_2]: (ssPv2(skf3(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2))) | ssPv6(skf3(skf2(U_2))) | ssPv1(skf3(skf2(U_2))) | ~ssPv7(skf2(U_2)) | ssPv5(skf3(skf2(U_2))) | ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.51/4.99 tff(c_4758, plain, (![U_490]: (ssPv2(skf3(U_490)) | ssPv4(skf3(U_490)) | ssPv2(U_490) | ~ssPv3(skf3(U_490)) | ~ssPv4(skf2(skf3(U_490))) | ssPv7(skf3(U_490)) | ssPv4(skf3(skf3(U_490))) | ~ssPv3(U_490) | ssPv8(skf3(U_490)) | ~ssPv6(skf3(U_490)) | ~ssPv1(skf2(skf3(U_490)))))). % 12.51/4.99 tff(c_4800, plain, (![U_492]: (ssPv2(skf3(U_492)) | ssPv4(skf3(U_492)) | ssPv2(U_492) | ~ssPv3(skf3(U_492)) | ~ssPv4(U_492) | ssPv7(skf3(U_492)) | ssPv4(skf3(skf3(U_492))) | ~ssPv3(skf2(skf3(U_492))) | ssPv8(skf3(U_492)) | ~ssPv6(skf3(U_492)) | ~ssPv1(skf2(skf3(U_492)))))). % 12.51/4.99 tff(c_5497, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_4779, plain, (![U_491]: (ssPv2(skf3(U_491)) | ssPv4(skf3(U_491)) | ssPv2(skf2(skf3(U_491))) | ~ssPv3(skf3(U_491)) | ~ssPv4(U_491) | ssPv7(skf3(U_491)) | ssPv4(skf3(skf3(U_491))) | ~ssPv3(U_491) | ssPv8(skf3(U_491)) | ~ssPv6(skf3(U_491)) | ~ssPv1(skf2(skf3(U_491)))))). % 12.51/4.99 tff(c_5522, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_3668, plain, (![U_441]: (ssPv2(skf3(skf3(U_441))) | ~ssPv3(skf3(skf3(U_441))) | ~ssPv4(skf3(U_441)) | ssPv1(skf3(U_441)) | ~ssPv7(skf3(U_441)) | ~ssPv6(skf3(U_441)) | ~ssPv4(U_441) | ssPv2(skf2(skf3(U_441))) | ~ssPv3(skf2(skf3(U_441))) | ~ssPv3(skf3(U_441))))). % 12.51/4.99 tff(c_5077, plain, (![U_505]: (ssPv6(U_505) | ssPv3(skf3(U_505)) | ~ssPv8(U_505) | ssPv1(U_505) | ~ssPv7(U_505) | ssPv1(skf2(U_505)) | ~ssPv4(skf2(U_505)) | ssPv6(skf2(U_505)) | ~ssPv5(skf2(U_505)) | ~ssPv3(skf2(U_505)) | ssPv4(U_505) | ssPv2(skf2(U_505)) | ~ssPv3(U_505)))). % 12.51/4.99 tff(c_5718, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv5(U_1) | ssPv3(skf3(U_1)) | ~ssPv6(U_1) | ssPv1(U_1) | ~ssPv7(U_1) | ssPv6(skf2(U_1)) | ssPv1(skf2(U_1)) | ~ssPv2(U_1) | ssPv3(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.51/4.99 tff(c_2661, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1) | ssPv1(U_1) | ~ssPv7(U_1) | ssPv6(skf2(U_1)) | ssPv1(skf2(U_1)) | ~ssPv2(U_1)))). % 12.51/4.99 tff(c_5226, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_4446, plain, (![U_478]: (ssPv2(skf3(U_478)) | ssPv5(skf3(U_478)) | ~ssPv4(skf3(U_478)) | ~ssPv3(skf3(U_478)) | ~ssPv4(U_478) | ssPv7(skf3(U_478)) | ssPv4(skf3(skf3(U_478))) | ~ssPv3(U_478) | ssPv8(skf3(U_478)) | ~ssPv6(skf3(U_478)) | ~ssPv1(skf2(skf3(U_478)))))). % 12.51/4.99 tff(c_4370, plain, (![U_474]: (ssPv2(skf3(U_474)) | ssPv4(skf3(U_474)) | ssPv2(U_474) | ~ssPv3(skf3(U_474)) | ~ssPv5(skf3(U_474)) | ssPv7(skf3(U_474)) | ssPv4(skf3(skf3(U_474))) | ~ssPv3(U_474) | ssPv8(skf3(U_474)) | ~ssPv6(skf3(U_474)) | ~ssPv1(skf2(skf3(U_474)))))). % 12.51/4.99 tff(c_5044, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_5166, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_5559, plain, (![U_528]: (ssPv2(skf2(U_528)) | ssPv4(skf2(U_528)) | ~ssPv6(skf2(U_528)) | ~ssPv4(skf2(skf2(U_528))) | ssPv7(skf2(U_528)) | ssPv4(U_528) | ssPv2(skf2(skf2(U_528))) | ~ssPv3(skf2(skf2(U_528))) | ~ssPv3(skf2(U_528))))). % 12.51/4.99 tff(c_5496, plain, (![U_525]: (ssPv2(skf3(U_525)) | ssPv4(skf3(U_525)) | ssPv2(U_525) | ~ssPv6(skf3(U_525)) | ~ssPv4(skf2(skf3(U_525))) | ssPv7(skf3(U_525)) | ssPv4(skf3(skf3(U_525))) | ~ssPv3(skf2(skf3(U_525))) | ~ssPv3(skf3(U_525)) | ~ssPv5(skf3(U_525))))). % 12.51/4.99 tff(c_1964, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(skf2(skf3(U_243))) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(skf2(skf3(U_243))) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/4.99 tff(c_3377, plain, (![U_429]: (ssPv2(skf3(U_429)) | ssPv4(skf3(U_429)) | ssPv2(U_429) | ~ssPv3(skf3(U_429)) | ~ssPv6(skf3(U_429)) | ~ssPv4(skf2(skf3(U_429))) | ~ssPv5(skf2(skf3(U_429))) | ssPv7(skf3(U_429)) | ssPv4(skf3(skf3(U_429))) | ~ssPv3(skf2(skf3(U_429)))))). % 12.51/4.99 tff(c_3901, plain, (![U_189]: (ssPv5(skf3(skf3(U_189))) | ssPv2(skf3(skf3(U_189))) | ~ssPv3(skf3(skf3(U_189))) | ssPv6(skf3(skf3(U_189))) | ssPv1(skf3(skf3(U_189))) | ~ssPv7(skf3(skf3(U_189))) | ssPv1(skf3(U_189)) | ~ssPv7(skf3(U_189)) | ~ssPv7(U_189)))). % 12.51/4.99 tff(c_3669, plain, (![U_441]: (ssPv2(skf3(skf3(U_441))) | ~ssPv3(skf3(skf3(U_441))) | ~ssPv4(skf3(U_441)) | ssPv1(skf3(U_441)) | ~ssPv7(skf3(U_441)) | ~ssPv6(skf3(U_441)) | ~ssPv4(U_441) | ~ssPv3(skf2(skf3(U_441))) | ~ssPv3(skf3(U_441)) | ~ssPv5(skf3(U_441))))). % 12.51/4.99 tff(c_4799, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_4757, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_4289, plain, (![U_469]: (ssPv2(skf3(U_469)) | ssPv4(skf3(U_469)) | ssPv2(U_469) | ~ssPv3(skf3(U_469)) | ~ssPv4(U_469) | ssPv7(skf3(U_469)) | ssPv4(skf3(skf3(U_469))) | ~ssPv3(U_469) | ssPv8(skf3(U_469)) | ~ssPv6(skf3(U_469)) | ~ssPv1(skf2(skf3(U_469)))))). % 12.51/4.99 tff(c_5324, plain, (![U_518]: (ssPv2(skf3(U_518)) | ssPv4(skf3(U_518)) | ~ssPv6(skf3(U_518)) | ~ssPv4(U_518) | ssPv7(skf3(U_518)) | ssPv4(skf3(skf3(U_518))) | ssPv2(skf2(skf3(U_518))) | ~ssPv3(skf2(skf3(U_518))) | ~ssPv3(skf3(U_518))))). % 12.51/4.99 tff(c_4778, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/4.99 tff(c_5250, plain, (![U_515]: (ssPv2(skf3(U_515)) | ssPv4(skf3(U_515)) | ssPv2(U_515) | ssPv8(skf3(U_515)) | ssPv7(skf3(U_515)) | ssPv4(skf3(skf3(U_515))) | ~ssPv3(skf2(skf3(U_515))) | ~ssPv3(skf3(U_515)) | ~ssPv5(skf3(U_515))))). % 12.51/4.99 tff(c_1834, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(skf2(skf3(U_243))) | ~ssPv3(skf3(U_243)) | ssPv8(skf3(U_243)) | ~ssPv5(skf3(U_243)) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/4.99 tff(c_5057, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv8(U_2) | ~ssPv7(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv4(skf2(skf2(U_2))) | ssPv6(skf2(skf2(U_2))) | ~ssPv5(skf2(skf2(U_2))) | ~ssPv3(skf2(skf2(U_2))) | ssPv4(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2))))). % 12.51/4.99 tff(c_1702, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv5(skf2(U_2)) | ~ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv6(skf2(U_2)) | ~ssPv4(skf2(skf2(U_2))) | ~ssPv5(skf2(skf2(U_2))) | ssPv7(skf2(U_2)) | ssPv4(U_2) | ~ssPv3(skf2(skf2(U_2)))))). % 12.51/4.99 tff(c_5141, plain, (![U_509]: (ssPv2(skf2(U_509)) | ssPv4(skf2(U_509)) | ssPv8(skf2(U_509)) | ~ssPv5(skf2(U_509)) | ssPv4(U_509) | ssPv2(skf2(skf2(U_509))) | ~ssPv3(skf2(U_509)) | ssPv7(skf2(U_509)) | ~ssPv1(skf2(skf2(U_509))) | ~ssPv6(skf2(U_509))))). % 12.51/4.99 tff(c_1701, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv5(skf3(U_243)) | ~ssPv4(skf3(U_243)) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(skf2(skf3(U_243))) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/4.99 tff(c_5131, plain, (![U_508]: (ssPv2(skf2(U_508)) | ssPv4(skf2(U_508)) | ssPv8(skf2(U_508)) | ~ssPv5(skf2(U_508)) | ssPv7(skf2(U_508)) | ssPv4(U_508) | ssPv2(skf2(skf2(U_508))) | ~ssPv3(skf2(skf2(U_508))) | ~ssPv3(skf2(U_508))))). % 12.51/4.99 tff(c_1786, plain, (![U_330]: (~ssPv3(skf2(U_330)) | ssPv6(skf2(U_330)) | ~ssPv8(skf2(U_330)) | ~ssPv8(U_330) | ssPv2(skf3(skf2(U_330))) | ~ssPv3(skf3(skf2(U_330))) | ~ssPv4(skf2(U_330)) | ssPv5(skf2(U_330)) | ~ssPv4(skf3(skf2(U_330))) | ~ssPv1(skf2(U_330))))). % 12.51/4.99 tff(c_2950, plain, (![U_406]: (ssPv2(skf3(U_406)) | ssPv5(skf3(U_406)) | ~ssPv4(skf3(U_406)) | ~ssPv3(skf3(U_406)) | ~ssPv6(skf3(U_406)) | ~ssPv4(skf2(skf3(U_406))) | ~ssPv5(U_406) | ssPv7(skf3(U_406)) | ssPv4(skf3(skf3(U_406))) | ~ssPv3(skf2(skf3(U_406)))))). % 12.51/4.99 tff(c_5056, plain, (![U_1]: (ssPv1(U_1) | ssPv8(skf3(U_1)) | ~ssPv7(U_1) | ssPv1(skf2(U_1)) | ~ssPv4(skf2(U_1)) | ssPv6(skf2(U_1)) | ~ssPv5(skf2(U_1)) | ~ssPv3(skf2(U_1)) | ssPv4(U_1) | ssPv2(skf2(U_1)) | ~ssPv3(U_1)))). % 12.51/4.99 tff(c_3795, plain, (![U_450, U_120]: (ssPv1(U_450) | ssPv8(U_120) | ~ssPv7(U_450) | ~ssRr(U_120, U_450) | ssPv1(skf2(U_450)) | ~ssPv4(skf2(U_450)) | ssPv6(skf2(U_450)) | ~ssPv5(skf2(U_450)) | ~ssPv3(skf2(U_450)) | ssPv4(U_450) | ssPv2(skf2(U_450)) | ~ssPv3(U_450)))). % 12.51/5.00 tff(c_4205, plain, (![U_192]: (ssPv2(skf3(skf3(U_192))) | ~ssPv4(skf3(U_192)) | ssPv8(U_192) | ~ssPv5(skf3(U_192)) | ssPv6(skf3(U_192)) | ~ssPv8(skf3(U_192)) | ssPv1(skf3(U_192)) | ~ssPv7(skf3(U_192)) | ssPv1(skf2(skf3(U_192))) | ~ssPv2(skf3(U_192))))). % 12.51/5.00 tff(c_2900, plain, (![U_404]: (ssPv2(skf3(U_404)) | ssPv5(skf3(U_404)) | ~ssPv4(skf3(U_404)) | ~ssPv3(skf3(U_404)) | ~ssPv6(skf3(U_404)) | ~ssPv4(U_404) | ~ssPv5(skf2(skf3(U_404))) | ssPv7(skf3(U_404)) | ssPv4(skf3(skf3(U_404))) | ~ssPv3(skf2(skf3(U_404)))))). % 12.51/5.00 tff(c_2468, plain, (![U_380]: (ssPv2(skf3(U_380)) | ~ssPv6(skf3(U_380)) | ~ssPv4(skf2(skf3(U_380))) | ~ssPv5(U_380) | ssPv5(skf2(skf3(U_380))) | ~ssPv3(skf2(skf3(U_380))) | ~ssPv8(skf3(U_380)) | ~ssPv7(skf3(U_380)) | ~ssPv5(skf3(U_380)) | ~ssPv6(U_380)))). % 12.51/5.00 tff(c_4445, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/5.00 tff(c_4881, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv5(U_1) | ssPv3(skf3(U_1)) | ssPv1(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv4(skf2(U_1)) | ~ssPv5(skf2(U_1)) | ssPv3(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.51/5.00 tff(c_2658, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ssPv1(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv4(skf2(U_1)) | ~ssPv5(skf2(U_1))))). % 12.51/5.00 tff(c_4369, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/5.00 tff(c_4798, plain, (![U_492]: (ssPv2(skf3(U_492)) | ssPv4(skf3(U_492)) | ssPv2(U_492) | ~ssPv6(skf3(U_492)) | ~ssPv4(U_492) | ssPv7(skf3(U_492)) | ssPv4(skf3(skf3(U_492))) | ~ssPv3(skf2(skf3(U_492))) | ~ssPv3(skf3(U_492)) | ~ssPv5(skf3(U_492))))). % 12.51/5.00 tff(c_2588, plain, (![U_384]: (ssPv2(skf3(U_384)) | ssPv4(skf3(U_384)) | ssPv2(U_384) | ~ssPv3(skf3(U_384)) | ~ssPv6(skf3(U_384)) | ~ssPv4(U_384) | ~ssPv5(skf2(skf3(U_384))) | ssPv7(skf3(U_384)) | ssPv4(skf3(skf3(U_384))) | ~ssPv3(skf2(skf3(U_384)))))). % 12.51/5.00 tff(c_3350, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(skf2(skf3(U_243))) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(U_243) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_3376, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(U_243) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(skf2(skf3(U_243))) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_3007, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(skf2(skf3(U_243))) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(skf2(skf3(U_243))) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_2563, plain, (![U_383]: (ssPv2(skf3(U_383)) | ssPv4(skf3(U_383)) | ssPv2(U_383) | ~ssPv3(skf3(U_383)) | ~ssPv6(skf3(U_383)) | ~ssPv4(skf2(skf3(U_383))) | ~ssPv5(U_383) | ssPv7(skf3(U_383)) | ssPv4(skf3(skf3(U_383))) | ~ssPv3(skf2(skf3(U_383)))))). % 12.51/5.00 tff(c_3894, plain, (![U_1]: (ssPv5(skf3(U_1)) | ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv6(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ssPv1(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv4(skf2(U_1)) | ~ssPv5(skf2(U_1))))). % 12.51/5.00 tff(c_3897, plain, (![U_1]: (ssPv5(skf3(U_1)) | ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv6(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ssPv1(U_1) | ~ssPv7(U_1) | ssPv6(skf2(U_1)) | ssPv1(skf2(U_1)) | ~ssPv2(U_1)))). % 12.51/5.00 tff(c_4288, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(skf3(U_1)) | ssPv4(skf3(skf3(U_1))) | ~ssPv3(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/5.00 tff(c_2415, plain, (![U_378]: (ssPv2(skf3(U_378)) | ssPv5(skf3(U_378)) | ~ssPv4(skf3(U_378)) | ~ssPv3(skf3(U_378)) | ~ssPv6(skf3(U_378)) | ~ssPv4(U_378) | ~ssPv5(U_378) | ssPv7(skf3(U_378)) | ssPv4(skf3(skf3(U_378))) | ~ssPv3(skf2(skf3(U_378)))))). % 12.51/5.00 tff(c_2924, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(skf2(skf3(U_243))) | ~ssPv3(skf3(U_243)) | ssPv8(skf3(U_243)) | ~ssPv5(skf3(U_243)) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_2949, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv5(skf3(U_243)) | ~ssPv4(skf3(U_243)) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(skf2(skf3(U_243))) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_2899, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv5(skf3(U_243)) | ~ssPv4(skf3(U_243)) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(U_243) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_3896, plain, (![U_1]: (ssPv5(skf3(U_1)) | ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv6(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ssPv1(U_1) | ~ssPv7(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv5(skf2(U_1))))). % 12.51/5.00 tff(c_3671, plain, (![U_441]: (ssPv2(skf3(skf3(U_441))) | ~ssPv3(skf3(skf3(U_441))) | ~ssPv4(skf3(U_441)) | ssPv1(skf3(U_441)) | ~ssPv7(skf3(U_441)) | ~ssPv4(U_441) | ssPv8(skf3(U_441)) | ~ssPv6(skf3(U_441)) | ~ssPv1(skf2(skf3(U_441)))))). % 12.51/5.00 tff(c_2066, plain, (![U_1]: (ssPv2(skf3(skf3(U_1))) | ~ssPv3(skf3(skf3(U_1))) | ~ssPv4(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/5.00 tff(c_2874, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(U_243) | ~ssPv3(skf3(U_243)) | ssPv8(skf3(U_243)) | ~ssPv5(skf3(U_243)) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_2470, plain, (![U_380]: (ssPv2(skf3(U_380)) | ~ssPv6(skf3(U_380)) | ~ssPv4(U_380) | ~ssPv5(U_380) | ssPv5(skf2(skf3(U_380))) | ~ssPv3(skf2(skf3(U_380))) | ~ssPv8(skf3(U_380)) | ~ssPv7(skf3(U_380)) | ~ssPv5(skf3(U_380)) | ~ssPv6(U_380)))). % 12.51/5.00 tff(c_1449, plain, (![U_311]: (ssPv2(skf3(skf3(U_311))) | ~ssPv3(skf3(skf3(U_311))) | ~ssPv4(skf3(U_311)) | ~ssPv5(skf3(U_311)) | ~ssPv1(skf3(U_311)) | ssPv6(U_311) | ssPv7(skf3(U_311)) | ~ssPv1(skf2(skf3(U_311))) | ~ssPv6(skf3(U_311))))). % 12.51/5.00 tff(c_4245, plain, (![U_467]: (ssPv2(skf2(U_467)) | ~ssPv6(skf2(U_467)) | ~ssPv4(skf2(skf2(U_467))) | ssPv8(skf2(U_467)) | ssPv4(skf2(U_467)) | ssPv8(U_467) | ssPv2(skf2(skf2(U_467))) | ~ssPv3(skf2(skf2(U_467))) | ~ssPv3(skf2(U_467))))). % 12.51/5.00 tff(c_4247, plain, (![U_467]: (ssPv2(skf2(U_467)) | ssPv2(skf2(skf2(U_467))) | ~ssPv3(skf2(U_467)) | ~ssPv4(skf2(skf2(U_467))) | ssPv4(skf2(U_467)) | ssPv8(U_467) | ssPv8(skf2(U_467)) | ~ssPv6(skf2(U_467)) | ~ssPv1(skf2(skf2(U_467)))))). % 12.51/5.00 tff(c_2587, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(U_243) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(U_243) | ~ssPv5(skf2(skf3(U_243))) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_2562, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(U_243) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(skf2(skf3(U_243))) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_1967, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv6(skf2(U_2)) | ~ssPv4(skf2(skf2(U_2))) | ~ssPv5(skf2(skf2(U_2))) | ssPv8(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv8(U_2)))). % 12.51/5.00 tff(c_2501, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(skf2(skf3(U_243))) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(U_243) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_2029, plain, (![U_192]: (ssPv8(U_192) | ~ssPv5(skf3(U_192)) | ssPv2(skf3(skf3(U_192))) | ~ssPv3(skf3(skf3(U_192))) | ~ssPv4(skf3(U_192)) | ssPv1(skf3(U_192)) | ~ssPv7(skf3(U_192)) | ssPv1(skf2(skf3(U_192))) | ~ssPv2(skf3(U_192))))). % 12.51/5.00 tff(c_2286, plain, (![U_369]: (ssPv2(skf3(U_369)) | ssPv4(skf3(U_369)) | ssPv2(U_369) | ~ssPv3(skf3(U_369)) | ~ssPv6(skf3(U_369)) | ~ssPv4(U_369) | ~ssPv5(U_369) | ssPv7(skf3(U_369)) | ssPv4(skf3(skf3(U_369))) | ~ssPv3(skf2(skf3(U_369)))))). % 12.51/5.00 tff(c_3042, plain, (![U_410]: (ssPv2(skf2(U_410)) | ssPv2(skf2(skf2(U_410))) | ~ssPv3(skf2(U_410)) | ~ssPv5(skf2(U_410)) | ssPv4(skf2(U_410)) | ssPv8(U_410) | ssPv8(skf2(U_410)) | ~ssPv6(skf2(U_410)) | ~ssPv1(skf2(skf2(U_410)))))). % 12.51/5.00 tff(c_1853, plain, (![U_1]: (ssPv2(skf3(skf3(U_1))) | ~ssPv3(skf3(skf3(U_1))) | ~ssPv4(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/5.00 tff(c_1302, plain, (![U_299]: (ssPv2(skf3(U_299)) | ~ssPv6(skf3(U_299)) | ~ssPv4(skf2(skf3(U_299))) | ~ssPv5(skf2(skf3(U_299))) | ssPv3(skf3(U_299)) | ~ssPv8(skf3(U_299)) | ~ssPv7(skf3(U_299)) | ~ssPv5(skf3(U_299)) | ~ssPv6(U_299)))). % 12.51/5.00 tff(c_1725, plain, (![U_192]: (ssPv8(U_192) | ~ssPv5(skf3(U_192)) | ssPv6(skf3(U_192)) | ssPv3(skf3(skf3(U_192))) | ~ssPv8(skf3(U_192)) | ssPv1(skf3(U_192)) | ~ssPv7(skf3(U_192)) | ssPv1(skf2(skf3(U_192))) | ~ssPv2(skf3(U_192))))). % 12.51/5.00 tff(c_2393, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(U_243) | ~ssPv3(skf3(U_243)) | ssPv8(skf3(U_243)) | ~ssPv5(skf3(U_243)) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_3904, plain, (![U_1]: (ssPv5(skf3(U_1)) | ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv6(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ssPv6(skf2(U_1))))). % 12.51/5.00 tff(c_3670, plain, (![U_1]: (ssPv2(skf3(skf3(U_1))) | ~ssPv3(skf3(skf3(U_1))) | ~ssPv4(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv4(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.51/5.00 tff(c_1448, plain, (![U_311]: (ssPv8(skf3(U_311)) | ssPv3(skf3(U_311)) | ~ssPv4(skf3(U_311)) | ~ssPv5(skf3(U_311)) | ~ssPv1(skf3(U_311)) | ssPv6(U_311) | ssPv7(skf3(U_311)) | ~ssPv1(skf2(skf3(U_311))) | ~ssPv6(skf3(U_311))))). % 12.51/5.00 tff(c_2414, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv5(skf3(U_243)) | ~ssPv4(skf3(U_243)) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(U_243) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_3905, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv6(skf3(U_1)) | ssPv1(skf3(U_1)) | ~ssPv7(U_1) | ssPv5(skf3(U_1)) | ssPv2(U_1) | ~ssPv7(skf3(U_1))))). % 12.51/5.00 tff(c_3828, plain, (![U_191]: (ssPv5(skf3(U_191)) | ssPv2(skf3(U_191)) | ~ssPv3(skf3(U_191)) | ssPv6(skf3(U_191)) | ~ssPv8(skf3(U_191)) | ssPv1(skf3(U_191)) | ~ssPv7(skf3(U_191)) | ~ssPv7(U_191)))). % 12.51/5.00 tff(c_2979, plain, (![U_407]: (ssPv7(skf2(U_407)) | ~ssPv5(skf2(U_407)) | ssPv6(skf2(U_407)) | ssPv3(U_407) | ~ssPv8(skf2(U_407)) | ssPv2(skf2(U_407)) | ssPv3(skf2(U_407)) | ~ssPv4(skf3(skf2(U_407))) | ~ssPv1(skf2(U_407))))). % 12.51/5.00 tff(c_3774, plain, (![U_2]: (ssPv1(skf2(U_2)) | ~ssPv4(skf2(U_2)) | ssPv6(skf2(U_2)) | ssPv7(skf2(U_2)) | ~ssPv5(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv3(U_2)))). % 12.51/5.00 tff(c_3754, plain, (![U_448]: (ssPv1(skf2(U_448)) | ~ssPv4(skf2(U_448)) | ssPv6(skf2(U_448)) | ~ssPv8(skf2(U_448)) | ssPv7(skf2(U_448)) | ~ssPv5(skf2(U_448)) | ssPv2(skf2(U_448)) | ~ssPv3(skf2(U_448)) | ~ssPv3(U_448)))). % 12.51/5.00 tff(c_2535, plain, (![U_382]: (ssPv2(skf3(skf2(U_382))) | ~ssPv4(skf2(U_382)) | ssPv6(skf2(U_382)) | ~ssPv8(skf2(U_382)) | ssPv7(skf2(U_382)) | ~ssPv5(skf2(U_382)) | ssPv2(skf2(U_382)) | ~ssPv3(skf2(U_382)) | ~ssPv3(U_382)))). % 12.51/5.00 tff(c_2285, plain, (![U_243]: (ssPv2(skf3(U_243)) | ssPv4(skf3(U_243)) | ssPv2(U_243) | ~ssPv3(skf3(U_243)) | ~ssPv6(skf3(U_243)) | ~ssPv4(U_243) | ~ssPv5(U_243) | ssPv7(skf3(U_243)) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.51/5.00 tff(c_3703, plain, (![U_445]: (ssPv1(skf2(U_445)) | ~ssPv4(skf2(U_445)) | ssPv7(skf2(U_445)) | ~ssPv5(skf2(U_445)) | ssPv2(skf2(U_445)) | ~ssPv3(skf2(U_445)) | ssPv6(skf2(U_445)) | ~ssPv8(skf2(U_445)) | ~ssPv8(U_445)))). % 12.51/5.00 tff(c_1163, plain, (![U_2]: (ssPv2(skf3(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv7(skf2(U_2)) | ~ssPv5(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ssPv6(skf2(U_2)) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_2)))). % 12.51/5.00 tff(c_1447, plain, (![U_311]: (ssPv2(skf3(skf3(U_311))) | ~ssPv4(skf3(U_311)) | ssPv8(skf3(U_311)) | ~ssPv3(skf3(skf3(U_311))) | ssPv6(U_311) | ssPv7(skf3(U_311)) | ~ssPv1(skf2(skf3(U_311))) | ~ssPv6(skf3(U_311))))). % 12.51/5.00 tff(c_3641, plain, (![U_440]: (ssPv2(skf3(skf3(U_440))) | ssPv6(skf3(U_440)) | ~ssPv8(skf3(U_440)) | ~ssPv4(skf3(U_440)) | ~ssPv1(skf3(U_440)) | ssPv6(U_440) | ssPv7(skf3(U_440)) | ~ssPv5(skf3(U_440)) | ~ssPv4(U_440)))). % 12.51/5.00 tff(c_3564, plain, (![U_437]: (ssPv2(skf3(skf3(U_437))) | ssPv6(skf3(U_437)) | ~ssPv8(skf3(U_437)) | ~ssPv4(skf3(U_437)) | ~ssPv5(skf3(U_437)) | ~ssPv1(skf3(U_437)) | ssPv7(skf3(U_437)) | ssPv6(U_437) | ~ssPv3(U_437)))). % 12.51/5.00 tff(c_2138, plain, (![U_357]: (ssPv2(skf3(skf3(U_357))) | ~ssPv3(skf3(skf3(U_357))) | ~ssPv4(skf3(U_357)) | ssPv1(skf3(U_357)) | ~ssPv7(skf3(U_357)) | ~ssPv6(skf3(U_357)) | ~ssPv4(U_357) | ~ssPv5(skf2(skf3(U_357)))))). % 12.51/5.00 tff(c_1589, plain, (![U_283]: (ssPv6(skf3(U_283)) | ssPv3(skf3(skf3(U_283))) | ~ssPv8(skf3(U_283)) | ~ssPv4(skf3(U_283)) | ~ssPv1(skf3(U_283)) | ssPv6(U_283) | ssPv7(skf3(U_283)) | ~ssPv5(skf3(U_283)) | ~ssPv4(U_283)))). % 12.51/5.00 tff(c_2124, plain, (![U_354]: (ssPv2(skf3(skf3(U_354))) | ~ssPv3(skf3(skf3(U_354))) | ~ssPv4(skf3(U_354)) | ssPv1(skf3(U_354)) | ~ssPv7(skf3(U_354)) | ~ssPv6(skf3(U_354)) | ~ssPv4(skf2(skf3(U_354))) | ~ssPv5(U_354)))). % 12.51/5.00 tff(c_1350, plain, (![U_303]: (ssPv1(skf2(U_303)) | ssPv8(U_303) | ~ssPv7(skf2(U_303)) | ~ssPv6(skf2(U_303)) | ~ssPv4(skf2(skf2(U_303))) | ssPv2(skf2(skf2(U_303))) | ~ssPv3(skf2(skf2(U_303))) | ~ssPv3(skf2(U_303))))). % 12.51/5.00 tff(c_1590, plain, (![U_239]: (ssPv6(skf3(U_239)) | ssPv3(skf3(skf3(U_239))) | ~ssPv8(skf3(U_239)) | ~ssPv4(skf3(U_239)) | ~ssPv5(skf3(U_239)) | ~ssPv1(skf3(U_239)) | ssPv7(skf3(U_239)) | ssPv6(U_239) | ~ssPv3(U_239)))). % 12.51/5.00 tff(c_2755, plain, (![U_2]: (ssPv2(U_2) | ssPv5(U_2) | ~ssPv4(U_2) | ~ssPv3(U_2) | ~ssPv4(skf2(U_2)) | ssPv7(U_2) | ssPv4(skf3(U_2)) | ~ssPv3(skf2(U_2)) | ssPv8(U_2) | ~ssPv6(U_2) | ~ssPv1(skf2(U_2))))). % 12.51/5.00 tff(c_2263, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ~ssPv5(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.51/5.00 tff(c_1543, plain, (![U_175]: (~ssPv3(skf2(U_175)) | ~ssPv3(U_175) | ssPv2(skf3(skf2(U_175))) | ~ssPv3(skf3(skf2(U_175))) | ~ssPv4(skf2(U_175)) | ssPv5(skf2(U_175)) | ~ssPv4(skf3(skf2(U_175))) | ~ssPv1(skf2(U_175))))). % 12.51/5.00 tff(c_1141, plain, (![U_285]: (~ssPv6(skf3(U_285)) | ssPv3(skf3(U_285)) | ~ssPv4(skf3(U_285)) | ssPv8(skf3(U_285)) | ~ssPv3(skf3(skf3(U_285))) | ssPv6(U_285) | ssPv7(skf3(U_285)) | ~ssPv5(skf3(U_285)) | ~ssPv4(U_285)))). % 12.51/5.01 tff(c_2192, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(skf2(skf3(U_1))) | ssPv3(skf3(U_1)) | ~ssPv8(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.51/5.01 tff(c_1152, plain, (![U_201]: (ssPv6(skf2(U_201)) | ssPv3(U_201) | ~ssPv8(skf2(U_201)) | ssPv7(skf2(U_201)) | ~ssPv3(skf3(skf2(U_201))) | ssPv7(skf3(skf2(U_201))) | ~ssPv5(skf3(skf2(U_201))) | ~ssPv4(skf2(U_201))))). % 12.51/5.01 tff(c_1183, plain, (![U_170]: (ssPv6(skf2(U_170)) | ssPv3(U_170) | ~ssPv8(skf2(U_170)) | ssPv7(skf2(U_170)) | ~ssPv5(skf2(U_170)) | ssPv3(skf2(U_170)) | ssPv7(U_170) | ~ssPv4(skf3(skf2(U_170))) | ~ssPv1(skf2(U_170))))). % 12.51/5.01 tff(c_1676, plain, (![U_324]: (ssPv2(skf3(U_324)) | ~ssPv6(skf2(skf3(U_324))) | ssPv4(skf3(U_324)) | ssPv2(U_324) | ~ssPv3(skf3(U_324)) | ~ssPv6(skf3(U_324)) | ~ssPv4(skf2(skf3(U_324))) | ~ssPv5(skf2(skf3(U_324)))))). % 12.51/5.01 tff(c_2064, plain, (![U_2]: (ssPv2(skf3(U_2)) | ~ssPv3(skf3(U_2)) | ~ssPv4(U_2) | ssPv1(U_2) | ~ssPv7(U_2) | ~ssPv6(U_2) | ~ssPv4(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.51/5.01 tff(c_1009, plain, (![U_248]: (ssPv2(skf3(U_248)) | ~ssPv6(skf2(skf3(U_248))) | ssPv4(skf3(U_248)) | ssPv2(skf2(skf3(U_248))) | ~ssPv3(skf3(U_248)) | ~ssPv6(skf3(U_248)) | ~ssPv4(U_248) | ~ssPv5(skf2(skf3(U_248)))))). % 12.51/5.01 tff(c_1351, plain, (![U_303]: (ssPv1(skf2(U_303)) | ssPv8(U_303) | ~ssPv7(skf2(U_303)) | ~ssPv6(skf2(U_303)) | ~ssPv4(skf2(skf2(U_303))) | ~ssPv3(skf2(skf2(U_303))) | ~ssPv3(skf2(U_303)) | ~ssPv5(skf2(U_303))))). % 12.51/5.01 tff(c_3307, plain, (![U_424]: (~ssPv8(U_424) | ~ssPv6(skf3(U_424)) | ssPv3(skf3(U_424)) | ~ssPv4(skf3(U_424)) | ~ssPv1(skf3(U_424)) | ssPv6(U_424) | ssPv7(skf3(U_424)) | ~ssPv5(skf3(U_424)) | ~ssPv4(U_424)))). % 12.51/5.01 tff(c_1376, plain, (![U_283]: (ssPv8(skf3(U_283)) | ~ssPv6(skf3(U_283)) | ssPv3(skf3(U_283)) | ~ssPv4(skf3(U_283)) | ~ssPv1(skf3(U_283)) | ssPv6(U_283) | ssPv7(skf3(U_283)) | ~ssPv5(skf3(U_283)) | ~ssPv4(U_283)))). % 12.51/5.01 tff(c_3273, plain, (![U_422]: (~ssPv8(U_422) | ~ssPv6(skf3(U_422)) | ssPv3(skf3(U_422)) | ~ssPv4(skf3(U_422)) | ~ssPv5(skf3(U_422)) | ~ssPv1(skf3(U_422)) | ssPv7(skf3(U_422)) | ssPv6(U_422) | ~ssPv3(U_422)))). % 12.51/5.01 tff(c_1377, plain, (![U_239]: (ssPv8(skf3(U_239)) | ~ssPv6(skf3(U_239)) | ssPv3(skf3(U_239)) | ~ssPv4(skf3(U_239)) | ~ssPv5(skf3(U_239)) | ~ssPv1(skf3(U_239)) | ssPv7(skf3(U_239)) | ssPv6(U_239) | ~ssPv3(U_239)))). % 12.51/5.01 tff(c_2143, plain, (![U_358]: (ssPv6(skf2(U_358)) | ssPv3(U_358) | ~ssPv8(skf2(U_358)) | ssPv7(skf2(U_358)) | ~ssPv4(skf2(U_358)) | ssPv5(skf3(skf2(U_358))) | ~ssPv4(skf3(skf2(U_358))) | ~ssPv1(skf2(U_358))))). % 12.51/5.01 tff(c_3041, plain, (![U_410]: (ssPv2(skf2(U_410)) | ssPv2(skf2(skf2(U_410))) | ssPv8(skf2(U_410)) | ssPv4(skf2(U_410)) | ssPv8(U_410) | ~ssPv3(skf2(skf2(U_410))) | ~ssPv3(skf2(U_410)) | ~ssPv5(skf2(U_410))))). % 12.51/5.01 tff(c_3178, plain, (![U_417]: (ssPv5(skf3(U_417)) | ~ssPv3(skf3(U_417)) | ~ssPv5(skf3(skf3(U_417))) | ssPv6(skf3(U_417)) | ~ssPv8(skf3(U_417)) | ssPv1(skf3(U_417)) | ~ssPv7(skf3(U_417)) | ~ssPv7(U_417)))). % 12.51/5.01 tff(c_1509, plain, (![U_314, U_114]: (ssPv5(skf3(U_314)) | ~ssPv3(skf3(U_314)) | ~ssPv5(U_114) | ~ssRr(U_114, skf3(U_314)) | ssPv6(skf3(U_314)) | ~ssPv8(skf3(U_314)) | ssPv1(skf3(U_314)) | ~ssPv7(skf3(U_314)) | ~ssPv7(U_314)))). % 12.51/5.01 tff(c_1451, plain, (![U_311]: (ssPv3(skf3(U_311)) | ~ssPv4(skf3(U_311)) | ssPv8(skf3(U_311)) | ~ssPv3(skf3(skf3(U_311))) | ssPv6(U_311) | ssPv7(skf3(U_311)) | ~ssPv1(skf2(skf3(U_311))) | ~ssPv6(skf3(U_311))))). % 12.51/5.01 tff(c_1273, plain, (![U_175]: (~ssPv3(skf2(U_175)) | ~ssPv3(U_175) | ssPv6(skf2(U_175)) | ssPv3(skf3(skf2(U_175))) | ~ssPv8(skf2(U_175)) | ssPv5(skf2(U_175)) | ~ssPv4(skf3(skf2(U_175))) | ~ssPv1(skf2(U_175))))). % 12.51/5.01 tff(c_1938, plain, (![U_343]: (ssPv2(skf3(skf3(U_343))) | ~ssPv3(skf3(skf3(U_343))) | ~ssPv4(skf3(U_343)) | ssPv1(skf3(U_343)) | ~ssPv7(skf3(U_343)) | ssPv8(skf3(U_343)) | ~ssPv5(skf3(U_343)) | ~ssPv5(U_343)))). % 12.51/5.01 tff(c_3056, plain, (![U_2]: (ssPv2(U_2) | ssPv4(U_2) | ~ssPv6(U_2) | ~ssPv4(skf2(U_2)) | ssPv7(U_2) | ssPv4(skf3(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.51/5.01 tff(c_1837, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv5(skf2(U_2)) | ~ssPv5(skf2(skf2(U_2))) | ssPv8(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv8(U_2)))). % 12.51/5.01 tff(c_2369, plain, (![U_376]: (ssPv7(skf2(U_376)) | ~ssPv5(skf2(U_376)) | ssPv6(skf2(U_376)) | ssPv3(U_376) | ~ssPv8(skf2(U_376)) | ssPv2(skf2(U_376)) | ssPv3(skf2(U_376)) | ~ssPv1(skf2(U_376)) | ~ssPv6(U_376)))). % 12.51/5.01 tff(c_1011, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ~ssPv5(U_1)))). % 12.51/5.01 tff(c_2738, plain, (![U_390]: (ssPv6(skf2(U_390)) | ssPv3(U_390) | ~ssPv8(skf2(U_390)) | ssPv2(skf2(U_390)) | ssPv3(skf2(U_390)) | ssPv5(skf3(skf2(U_390))) | ~ssPv4(skf3(skf2(U_390))) | ~ssPv1(skf2(U_390))))). % 12.51/5.01 tff(c_720, plain, (![U_226]: (ssPv2(skf3(U_226)) | ~ssPv6(skf2(skf3(U_226))) | ssPv5(skf3(U_226)) | ~ssPv4(skf3(U_226)) | ~ssPv3(skf3(U_226)) | ~ssPv6(skf3(U_226)) | ~ssPv4(skf2(skf3(U_226))) | ~ssPv5(U_226)))). % 12.51/5.01 tff(c_1013, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ssPv8(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv5(U_1)))). % 12.51/5.01 tff(c_897, plain, (![U_258]: (ssPv2(skf3(U_258)) | ~ssPv6(skf2(skf3(U_258))) | ssPv5(skf3(U_258)) | ~ssPv4(skf3(U_258)) | ~ssPv3(skf3(U_258)) | ~ssPv6(skf3(U_258)) | ~ssPv4(U_258) | ~ssPv5(skf2(skf3(U_258)))))). % 12.51/5.02 tff(c_1678, plain, (![U_324]: (ssPv2(skf3(U_324)) | ~ssPv6(skf2(skf3(U_324))) | ssPv4(skf3(U_324)) | ssPv2(U_324) | ~ssPv3(skf3(U_324)) | ssPv8(skf3(U_324)) | ~ssPv5(skf3(U_324)) | ~ssPv5(skf2(skf3(U_324)))))). % 12.51/5.02 tff(c_1424, plain, (![U_239]: (~ssPv6(skf3(U_239)) | ssPv2(skf3(skf3(U_239))) | ~ssPv4(skf3(U_239)) | ssPv8(skf3(U_239)) | ~ssPv3(skf3(skf3(U_239))) | ssPv7(skf3(U_239)) | ssPv6(U_239) | ~ssPv3(U_239)))). % 12.51/5.02 tff(c_2065, plain, (![U_2]: (ssPv2(skf3(U_2)) | ~ssPv3(skf3(U_2)) | ~ssPv4(U_2) | ssPv1(U_2) | ~ssPv7(U_2) | ~ssPv6(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv5(U_2)))). % 12.51/5.02 tff(c_1074, plain, (![U_201]: (ssPv6(skf2(U_201)) | ssPv3(U_201) | ~ssPv8(skf2(U_201)) | ssPv1(skf2(U_201)) | ~ssPv7(skf2(U_201)) | ssPv6(skf2(skf2(U_201))) | ssPv1(skf2(skf2(U_201))) | ~ssPv2(skf2(U_201))))). % 12.51/5.02 tff(c_1808, plain, (![U_333]: (ssPv2(skf3(skf3(U_333))) | ~ssPv3(skf3(skf3(U_333))) | ~ssPv4(skf3(U_333)) | ssPv1(skf3(U_333)) | ~ssPv7(skf3(U_333)) | ~ssPv6(skf3(U_333)) | ~ssPv4(U_333) | ~ssPv5(U_333)))). % 12.51/5.02 tff(c_2216, plain, (![U_364]: (ssPv2(skf2(U_364)) | ~ssPv7(skf2(U_364)) | ssPv8(skf2(U_364)) | ssPv4(skf2(U_364)) | ssPv8(U_364) | ~ssPv3(skf2(skf2(U_364))) | ~ssPv3(skf2(U_364)) | ~ssPv5(skf2(U_364))))). % 12.51/5.02 tff(c_2217, plain, (![U_364]: (ssPv2(skf2(U_364)) | ~ssPv7(skf2(U_364)) | ~ssPv5(skf2(U_364)) | ssPv4(skf2(U_364)) | ssPv8(U_364) | ssPv8(skf2(U_364)) | ~ssPv6(skf2(U_364)) | ~ssPv1(skf2(skf2(U_364)))))). % 12.51/5.02 tff(c_1363, plain, (![U_283]: (ssPv2(skf3(skf3(U_283))) | ~ssPv3(skf3(skf3(U_283))) | ~ssPv4(skf3(U_283)) | ~ssPv1(skf3(U_283)) | ssPv6(U_283) | ssPv7(skf3(U_283)) | ~ssPv5(skf3(U_283)) | ~ssPv4(U_283)))). % 12.78/5.02 tff(c_1364, plain, (![U_239]: (ssPv2(skf3(skf3(U_239))) | ~ssPv3(skf3(skf3(U_239))) | ~ssPv4(skf3(U_239)) | ~ssPv5(skf3(U_239)) | ~ssPv1(skf3(U_239)) | ssPv7(skf3(U_239)) | ssPv6(U_239) | ~ssPv3(U_239)))). % 12.78/5.02 tff(c_1923, plain, (![U_340]: (~ssPv6(skf3(U_340)) | ~ssPv4(skf3(U_340)) | ~ssPv3(skf3(skf3(U_340))) | ssPv7(skf3(U_340)) | ssPv6(U_340) | ssPv8(skf3(U_340)) | ssPv5(skf3(U_340)) | ssPv3(skf3(U_340))))). % 12.78/5.02 tff(c_1184, plain, (![U_288]: (ssPv6(skf2(U_288)) | ssPv3(U_288) | ~ssPv8(skf2(U_288)) | ssPv7(skf2(U_288)) | ~ssPv4(skf2(U_288)) | ~ssPv5(skf2(U_288)) | ~ssPv4(skf3(skf2(U_288))) | ~ssPv1(skf2(U_288))))). % 12.78/5.02 tff(c_1290, plain, (![U_239]: (ssPv2(skf3(skf3(U_239))) | ~ssPv4(skf3(U_239)) | ~ssPv5(skf3(U_239)) | ssPv8(skf3(U_239)) | ~ssPv3(skf3(skf3(U_239))) | ssPv7(skf3(U_239)) | ssPv6(U_239) | ~ssPv3(U_239)))). % 12.78/5.02 tff(c_1703, plain, (![U_1]: (ssPv2(U_1) | ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv6(U_1) | ~ssPv4(skf2(U_1)) | ~ssPv5(skf2(U_1)) | ssPv7(U_1) | ssPv4(skf3(U_1)) | ~ssPv3(skf2(U_1))))). % 12.78/5.02 tff(c_1650, plain, (![U_323]: (ssPv6(skf2(U_323)) | ssPv3(U_323) | ~ssPv8(skf2(U_323)) | ssPv5(skf3(skf2(U_323))) | ssPv2(skf2(U_323)) | ssPv3(skf2(U_323)) | ~ssPv1(skf2(U_323)) | ~ssPv6(skf3(skf2(U_323)))))). % 12.78/5.02 tff(c_1289, plain, (![U_283]: (ssPv2(skf3(skf3(U_283))) | ~ssPv4(skf3(U_283)) | ssPv8(skf3(U_283)) | ~ssPv3(skf3(skf3(U_283))) | ssPv6(U_283) | ssPv7(skf3(U_283)) | ~ssPv5(skf3(U_283)) | ~ssPv4(U_283)))). % 12.78/5.02 tff(c_2684, plain, (![U_2]: (ssPv2(U_2) | ssPv4(U_2) | ssPv8(U_2) | ~ssPv5(U_2) | ssPv7(U_2) | ssPv4(skf3(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.78/5.02 tff(c_2048, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.78/5.02 tff(c_1187, plain, (![U_288]: (ssPv6(skf2(U_288)) | ssPv3(U_288) | ~ssPv8(skf2(U_288)) | ssPv7(skf2(U_288)) | ~ssPv5(skf2(U_288)) | ssPv2(skf2(U_288)) | ~ssPv3(skf2(U_288)) | ~ssPv3(skf3(skf2(U_288)))))). % 12.78/5.02 tff(c_1673, plain, (![U_248]: (ssPv2(skf3(U_248)) | ~ssPv6(skf2(skf3(U_248))) | ssPv4(skf3(U_248)) | ssPv2(U_248) | ~ssPv3(skf3(U_248)) | ~ssPv6(skf3(U_248)) | ~ssPv4(U_248) | ~ssPv5(skf2(skf3(U_248)))))). % 12.78/5.02 tff(c_1675, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ~ssPv5(U_1)))). % 12.78/5.02 tff(c_757, plain, (![U_2]: (ssPv6(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv8(skf2(U_2)) | ssPv7(skf2(U_2)) | ~ssPv5(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.78/5.02 tff(c_1010, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ~ssPv3(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1)))). % 12.78/5.02 tff(c_1753, plain, (![U_1]: (ssPv5(skf2(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv6(skf2(skf3(U_1))) | ~ssPv8(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.78/5.02 tff(c_817, plain, (![U_239]: (~ssPv6(skf3(U_239)) | ssPv3(skf3(U_239)) | ~ssPv4(skf3(U_239)) | ssPv8(skf3(U_239)) | ~ssPv3(skf3(skf3(U_239))) | ssPv7(skf3(U_239)) | ssPv6(U_239) | ~ssPv3(U_239)))). % 12.78/5.02 tff(c_845, plain, (![U_250]: (ssPv2(skf3(U_250)) | ~ssPv6(skf2(skf3(U_250))) | ssPv5(skf3(U_250)) | ~ssPv4(skf3(U_250)) | ~ssPv3(skf3(U_250)) | ~ssPv6(skf3(U_250)) | ~ssPv4(U_250) | ~ssPv5(U_250)))). % 12.78/5.02 tff(c_1677, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ssPv8(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv5(U_1)))). % 12.78/5.02 tff(c_1649, plain, (![U_2]: (ssPv6(skf2(U_2)) | ssPv3(U_2) | ~ssPv8(skf2(U_2)) | ssPv5(skf3(skf2(U_2))) | ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.78/5.02 tff(c_2067, plain, (![U_2]: (ssPv2(skf3(U_2)) | ~ssPv3(skf3(U_2)) | ~ssPv4(U_2) | ssPv1(U_2) | ~ssPv7(U_2) | ~ssPv4(skf2(U_2)) | ssPv8(U_2) | ~ssPv6(U_2) | ~ssPv1(skf2(U_2))))). % 12.78/5.02 tff(c_1352, plain, (![U_303]: (ssPv1(skf2(U_303)) | ssPv8(U_303) | ~ssPv7(skf2(U_303)) | ~ssPv4(skf2(skf2(U_303))) | ssPv8(skf2(U_303)) | ~ssPv6(skf2(U_303)) | ~ssPv1(skf2(skf2(U_303)))))). % 12.78/5.02 tff(c_597, plain, (![U_204]: (ssPv6(skf2(U_204)) | ssPv3(U_204) | ~ssPv8(skf2(U_204)) | ssPv7(skf2(U_204)) | ~ssPv5(skf3(skf2(U_204))) | ~ssPv6(skf3(skf2(U_204))) | ~ssPv1(skf2(U_204))))). % 12.78/5.02 tff(c_2291, plain, (![U_370]: (~ssPv6(skf2(U_370)) | ssPv3(skf2(U_370)) | ~ssPv1(skf2(U_370)) | ~ssPv6(U_370) | ssPv2(skf2(U_370)) | ssPv8(skf2(U_370)) | ~ssPv3(skf3(skf2(U_370)))))). % 12.78/5.02 tff(c_1514, plain, (![U_315]: (ssPv6(skf2(U_315)) | ssPv3(U_315) | ~ssPv8(skf2(U_315)) | ssPv5(skf2(U_315)) | ssPv5(skf3(skf2(U_315))) | ~ssPv4(skf3(skf2(U_315))) | ~ssPv1(skf2(U_315))))). % 12.78/5.02 tff(c_1489, plain, (![U_313]: (~ssPv6(skf2(U_313)) | ssPv3(skf2(U_313)) | ~ssPv1(skf2(U_313)) | ~ssPv6(U_313) | ssPv8(skf2(U_313)) | ~ssPv4(skf3(skf2(U_313))) | ~ssPv3(skf3(skf2(U_313)))))). % 12.78/5.02 tff(c_1674, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1)))). % 12.78/5.02 tff(c_721, plain, (![U_226]: (ssPv2(skf3(U_226)) | ~ssPv7(skf3(U_226)) | ~ssPv5(skf3(U_226)) | ~ssPv6(skf2(skf3(U_226))) | ~ssPv6(skf3(U_226)) | ~ssPv4(skf2(skf3(U_226))) | ~ssPv5(U_226)))). % 12.78/5.02 tff(c_1854, plain, (![U_2]: (ssPv2(skf3(U_2)) | ~ssPv3(skf3(U_2)) | ~ssPv4(U_2) | ssPv1(U_2) | ~ssPv7(U_2) | ~ssPv5(U_2) | ssPv8(U_2) | ~ssPv6(U_2) | ~ssPv1(skf2(U_2))))). % 12.78/5.02 tff(c_1852, plain, (![U_2]: (ssPv2(skf3(U_2)) | ~ssPv3(skf3(U_2)) | ~ssPv4(U_2) | ssPv1(U_2) | ~ssPv7(U_2) | ssPv8(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv5(U_2)))). % 12.78/5.02 tff(c_1109, plain, (![U_281]: (ssPv1(skf2(U_281)) | ssPv8(U_281) | ~ssPv7(skf2(U_281)) | ~ssPv5(skf2(U_281)) | ssPv8(skf2(U_281)) | ~ssPv6(skf2(U_281)) | ~ssPv1(skf2(skf2(U_281)))))). % 12.78/5.02 tff(c_795, plain, (![U_2]: (ssPv2(skf2(U_2)) | ~ssPv7(skf2(U_2)) | ~ssPv5(skf2(U_2)) | ~ssPv5(skf2(skf2(U_2))) | ssPv8(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv8(U_2)))). % 12.78/5.02 tff(c_1108, plain, (![U_281]: (ssPv1(skf2(U_281)) | ssPv8(U_281) | ~ssPv7(skf2(U_281)) | ssPv8(skf2(U_281)) | ~ssPv3(skf2(skf2(U_281))) | ~ssPv3(skf2(U_281)) | ~ssPv5(skf2(U_281))))). % 12.78/5.02 tff(c_1554, plain, (![U_317]: (ssPv7(U_317) | ~ssPv4(U_317) | ssPv2(skf2(skf3(U_317))) | ~ssPv3(skf3(U_317)) | ssPv7(skf3(U_317)) | ~ssPv1(skf2(skf3(U_317))) | ~ssPv6(skf3(U_317))))). % 12.78/5.02 tff(c_898, plain, (![U_258]: (ssPv2(skf3(U_258)) | ~ssPv7(skf3(U_258)) | ~ssPv5(skf3(U_258)) | ~ssPv6(skf2(skf3(U_258))) | ~ssPv6(skf3(U_258)) | ~ssPv4(U_258) | ~ssPv5(skf2(skf3(U_258)))))). % 12.78/5.02 tff(c_2152, plain, (![U_2]: (ssPv5(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ssPv6(skf2(U_2)) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_2)))). % 12.78/5.02 tff(c_910, plain, (![U_201]: (ssPv6(skf2(U_201)) | ssPv3(U_201) | ~ssPv8(skf2(U_201)) | ssPv7(skf2(U_201)) | ~ssPv4(skf2(U_201)) | ~ssPv6(skf3(skf2(U_201))) | ~ssPv1(skf2(U_201))))). % 12.78/5.02 tff(c_2129, plain, (![U_355]: (ssPv1(skf3(U_355)) | ssPv8(skf3(skf3(U_355))) | ~ssPv7(skf3(U_355)) | ~ssPv6(skf3(U_355)) | ~ssPv4(U_355) | ~ssPv5(skf2(skf3(U_355)))))). % 12.78/5.02 tff(c_899, plain, (![U_258, U_120]: (ssPv1(skf3(U_258)) | ssPv8(U_120) | ~ssPv7(skf3(U_258)) | ~ssRr(U_120, skf3(U_258)) | ~ssPv6(skf3(U_258)) | ~ssPv4(U_258) | ~ssPv5(skf2(skf3(U_258)))))). % 12.78/5.02 tff(c_2115, plain, (![U_352]: (ssPv1(skf3(U_352)) | ssPv8(skf3(skf3(U_352))) | ~ssPv7(skf3(U_352)) | ~ssPv6(skf3(U_352)) | ~ssPv4(skf2(skf3(U_352))) | ~ssPv5(U_352)))). % 12.78/5.03 tff(c_722, plain, (![U_226, U_120]: (ssPv1(skf3(U_226)) | ssPv8(U_120) | ~ssPv7(skf3(U_226)) | ~ssRr(U_120, skf3(U_226)) | ~ssPv6(skf3(U_226)) | ~ssPv4(skf2(skf3(U_226))) | ~ssPv5(U_226)))). % 12.78/5.03 tff(c_1055, plain, (![U_274]: (ssPv8(skf2(U_274)) | ~ssPv6(skf2(U_274)) | ~ssPv4(skf2(U_274)) | ssPv3(skf2(U_274)) | ssPv7(U_274) | ~ssPv4(skf3(skf2(U_274))) | ~ssPv1(skf2(U_274))))). % 12.78/5.03 tff(c_1628, plain, (![U_191]: (ssPv2(skf3(skf3(U_191))) | ~ssPv4(skf3(U_191)) | ssPv6(skf3(U_191)) | ~ssPv8(skf3(U_191)) | ssPv1(skf3(U_191)) | ~ssPv7(skf3(U_191)) | ~ssPv7(U_191)))). % 12.78/5.03 tff(c_951, plain, (![U_2]: (ssPv2(skf3(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv5(skf3(skf2(U_2))) | ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.78/5.03 tff(c_1252, plain, (![U_295]: (ssPv2(skf3(U_295)) | ~ssPv3(skf3(U_295)) | ~ssPv4(U_295) | ssPv1(U_295) | ~ssPv7(U_295) | ~ssPv6(U_295) | ~ssPv4(skf2(U_295)) | ~ssPv5(skf2(U_295))))). % 12.78/5.03 tff(c_846, plain, (![U_250]: (ssPv2(skf3(U_250)) | ~ssPv7(skf3(U_250)) | ~ssPv5(skf3(U_250)) | ~ssPv6(skf2(skf3(U_250))) | ~ssPv6(skf3(U_250)) | ~ssPv4(U_250) | ~ssPv5(U_250)))). % 12.78/5.03 tff(c_1076, plain, (![U_277]: (ssPv2(skf3(U_277)) | ~ssPv3(skf3(U_277)) | ~ssPv4(U_277) | ssPv1(U_277) | ~ssPv7(U_277) | ssPv6(skf2(U_277)) | ssPv1(skf2(U_277)) | ~ssPv2(U_277)))). % 12.78/5.03 tff(c_1898, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv2(U_1) | ssPv3(U_1) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.03 tff(c_1012, plain, (![U_2]: (ssPv2(U_2) | ~ssPv6(skf2(U_2)) | ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv6(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv5(skf2(U_2))))). % 12.78/5.03 tff(c_1929, plain, (![U_341]: (ssPv1(skf3(U_341)) | ssPv8(skf3(skf3(U_341))) | ~ssPv7(skf3(U_341)) | ssPv8(skf3(U_341)) | ~ssPv5(skf3(U_341)) | ~ssPv5(U_341)))). % 12.78/5.03 tff(c_232, plain, (![U_1, U_123]: (ssPv1(skf3(U_1)) | ssPv8(U_123) | ~ssPv7(skf3(U_1)) | ~ssRr(U_123, skf3(U_1)) | ssPv8(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv5(U_1)))). % 12.78/5.03 tff(c_1893, plain, (![U_337]: (ssPv7(skf3(U_337)) | ssPv6(U_337) | ssPv4(skf3(skf3(U_337))) | ssPv8(skf3(U_337)) | ssPv5(skf3(U_337)) | ssPv3(skf3(U_337))))). % 12.78/5.03 tff(c_952, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv5(skf3(U_1)) | ssPv2(U_1) | ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv6(skf3(U_1))))). % 12.78/5.03 tff(c_939, plain, (![U_264, U_265]: (ssPv7(skf3(U_264)) | ssPv6(U_264) | ssPv4(U_265) | ~ssRr(U_265, skf3(U_264)) | ssPv8(skf3(U_264)) | ssPv5(skf3(U_264)) | ssPv3(skf3(U_264))))). % 12.78/5.03 tff(c_1206, plain, (![U_1]: (ssPv6(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(U_1) | ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.03 tff(c_1096, plain, (![U_280]: (ssPv2(skf3(U_280)) | ~ssPv3(skf3(U_280)) | ~ssPv4(U_280) | ssPv1(U_280) | ~ssPv7(U_280) | ssPv8(U_280) | ~ssPv5(U_280) | ~ssPv5(skf2(U_280))))). % 12.78/5.03 tff(c_1014, plain, (![U_2]: (ssPv2(U_2) | ~ssPv6(skf2(U_2)) | ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv3(U_2) | ssPv8(U_2) | ~ssPv5(U_2) | ~ssPv5(skf2(U_2))))). % 12.78/5.03 tff(c_1799, plain, (![U_331]: (ssPv1(skf3(U_331)) | ssPv8(skf3(skf3(U_331))) | ~ssPv7(skf3(U_331)) | ~ssPv6(skf3(U_331)) | ~ssPv4(U_331) | ~ssPv5(U_331)))). % 12.78/5.03 tff(c_847, plain, (![U_250, U_120]: (ssPv1(skf3(U_250)) | ssPv8(U_120) | ~ssPv7(skf3(U_250)) | ~ssRr(U_120, skf3(U_250)) | ~ssPv6(skf3(U_250)) | ~ssPv4(U_250) | ~ssPv5(U_250)))). % 12.78/5.03 tff(c_1734, plain, (![U_327]: (ssPv5(skf2(U_327)) | ~ssPv3(skf2(U_327)) | ~ssPv5(skf3(skf2(U_327))) | ssPv6(skf2(U_327)) | ~ssPv8(skf2(U_327)) | ~ssPv8(U_327)))). % 12.78/5.03 tff(c_1735, plain, (![U_2]: (ssPv5(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv5(U_2) | ssPv6(skf2(U_2)) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_2)))). % 12.78/5.03 tff(c_307, plain, (![U_146, U_114]: (ssPv5(skf2(U_146)) | ~ssPv3(skf2(U_146)) | ~ssPv5(U_114) | ~ssRr(U_114, skf2(U_146)) | ssPv6(skf2(U_146)) | ~ssPv8(skf2(U_146)) | ~ssPv8(U_146)))). % 12.78/5.03 tff(c_1075, plain, (![U_277]: (ssPv6(U_277) | ssPv3(skf3(U_277)) | ~ssPv8(U_277) | ssPv1(U_277) | ~ssPv7(U_277) | ssPv6(skf2(U_277)) | ssPv1(skf2(U_277)) | ~ssPv2(U_277)))). % 12.78/5.03 tff(c_708, plain, (![U_225]: (ssPv2(U_225) | ~ssPv6(skf2(U_225)) | ssPv5(U_225) | ~ssPv4(U_225) | ~ssPv3(U_225) | ~ssPv6(U_225) | ~ssPv4(skf2(U_225)) | ~ssPv5(skf2(U_225))))). % 12.78/5.03 tff(c_660, plain, (![U_215]: (ssPv2(skf3(U_215)) | ~ssPv7(skf2(skf3(U_215))) | ~ssPv6(skf2(skf3(U_215))) | ssPv4(skf3(U_215)) | ssPv2(U_215) | ~ssPv3(skf3(U_215))))). % 12.78/5.03 tff(c_600, plain, (![U_204]: (ssPv6(skf2(U_204)) | ssPv3(U_204) | ~ssPv8(skf2(U_204)) | ssPv5(skf3(skf2(U_204))) | ssPv2(skf2(U_204)) | ~ssPv7(skf3(skf2(U_204)))))). % 12.78/5.03 tff(c_484, plain, (![U_191]: (ssPv2(skf3(skf3(U_191))) | ~ssPv3(skf3(skf3(U_191))) | ~ssPv4(skf3(U_191)) | ssPv1(skf3(U_191)) | ~ssPv7(skf3(U_191)) | ~ssPv7(U_191)))). % 12.78/5.03 tff(c_1039, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.03 tff(c_924, plain, (![U_261]: (ssPv6(U_261) | ssPv3(skf3(U_261)) | ~ssPv8(U_261) | ssPv7(U_261) | ~ssPv4(U_261) | ~ssPv5(U_261) | ~ssPv4(skf3(U_261)) | ~ssPv1(U_261)))). % 12.78/5.03 tff(c_411, plain, (![U_178]: (ssPv5(skf2(U_178)) | ~ssPv3(skf2(U_178)) | ~ssPv3(U_178) | ssPv8(skf2(U_178)) | ~ssPv4(skf3(skf2(U_178))) | ~ssPv3(skf3(skf2(U_178)))))). % 12.78/5.03 tff(c_350, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv6(skf2(skf3(U_1))) | ssPv8(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv5(U_1)))). % 12.78/5.03 tff(c_884, plain, (![U_257]: (ssPv7(U_257) | ~ssPv6(skf3(U_257)) | ~ssPv4(U_257) | ssPv2(skf2(skf3(U_257))) | ~ssPv3(skf2(skf3(U_257))) | ~ssPv3(skf3(U_257))))). % 12.78/5.03 tff(c_1021, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ssPv5(U_1) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.03 tff(c_622, plain, (![U_201]: (ssPv6(skf2(U_201)) | ssPv3(U_201) | ~ssPv8(skf2(U_201)) | ssPv5(skf2(U_201)) | ~ssPv6(skf3(skf2(U_201))) | ~ssPv1(skf2(U_201))))). % 12.78/5.03 tff(c_483, plain, (![U_191]: (ssPv6(skf3(U_191)) | ssPv3(skf3(skf3(U_191))) | ~ssPv8(skf3(U_191)) | ssPv1(skf3(U_191)) | ~ssPv7(skf3(U_191)) | ~ssPv7(U_191)))). % 12.78/5.03 tff(c_506, plain, (![U_2]: (ssPv8(skf2(U_2)) | ~ssPv5(skf3(skf2(U_2))) | ~ssPv6(skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.78/5.03 tff(c_1425, plain, (![U_1]: (~ssPv6(U_1) | ssPv2(skf3(U_1)) | ssPv7(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ssPv8(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.03 tff(c_1430, plain, (![U_309]: (ssPv6(U_309) | ssPv4(skf3(skf3(U_309))) | ssPv7(skf3(U_309)) | ~ssPv1(skf2(skf3(U_309))) | ~ssPv6(skf3(U_309))))). % 12.78/5.03 tff(c_937, plain, (![U_264, U_265]: (ssPv6(U_264) | ssPv4(U_265) | ~ssRr(U_265, skf3(U_264)) | ssPv7(skf3(U_264)) | ~ssPv1(skf2(skf3(U_264))) | ~ssPv6(skf3(U_264))))). % 12.78/5.03 tff(c_1412, plain, (![U_1]: (~ssPv6(U_1) | ssPv2(skf3(U_1)) | ssPv7(U_1) | ~ssPv4(U_1) | ssPv8(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1))))). % 12.78/5.03 tff(c_1201, plain, (![U_289]: (ssPv8(U_289) | ~ssPv6(U_289) | ssPv2(skf3(U_289)) | ssPv7(U_289) | ~ssPv3(skf3(U_289)) | ~ssPv5(skf3(U_289)) | ~ssPv4(U_289)))). % 12.78/5.03 tff(c_1339, plain, (![U_302]: (ssPv8(U_302) | ~ssPv6(U_302) | ssPv7(U_302) | ~ssPv6(skf3(U_302)) | ~ssPv3(skf3(U_302)) | ~ssPv5(skf3(U_302)) | ~ssPv4(U_302)))). % 12.78/5.03 tff(c_925, plain, (![U_261]: (ssPv8(U_261) | ~ssPv6(U_261) | ssPv3(U_261) | ssPv7(U_261) | ~ssPv4(U_261) | ~ssPv5(U_261) | ~ssPv4(skf3(U_261)) | ~ssPv1(U_261)))). % 12.78/5.03 tff(c_982, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.03 tff(c_1239, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv8(U_2) | ~ssPv7(skf2(U_2)) | ~ssPv6(skf2(U_2)) | ~ssPv4(skf2(skf2(U_2))) | ~ssPv5(skf2(skf2(U_2)))))). % 12.78/5.03 tff(c_1325, plain, (![U_1]: (ssPv7(U_1) | ~ssPv6(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.03 tff(c_885, plain, (![U_257]: (ssPv7(U_257) | ~ssPv6(skf3(U_257)) | ~ssPv4(U_257) | ~ssPv3(skf2(skf3(U_257))) | ~ssPv3(skf3(U_257)) | ~ssPv5(skf3(U_257))))). % 12.78/5.03 tff(c_1291, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(U_1) | ~ssPv5(U_1) | ssPv2(U_1) | ssPv8(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.03 tff(c_577, plain, (![U_1]: (ssPv6(skf2(skf3(U_1))) | ssPv3(skf3(U_1)) | ~ssPv8(skf3(U_1)) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.78/5.03 tff(c_986, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(U_1) | ~ssPv5(U_1) | ssPv8(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1))))). % 12.78/5.03 tff(c_468, plain, (![U_188]: (ssPv6(U_188) | ssPv3(skf3(U_188)) | ~ssPv8(U_188) | ssPv7(U_188) | ~ssPv5(skf3(U_188)) | ~ssPv6(skf3(U_188)) | ~ssPv1(U_188)))). % 12.78/5.03 tff(c_679, plain, (![U_1]: (ssPv6(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(U_1) | ssPv5(U_1) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.03 tff(c_1238, plain, (![U_1]: (ssPv1(U_1) | ssPv8(skf3(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv4(skf2(U_1)) | ~ssPv5(skf2(U_1))))). % 12.78/5.03 tff(c_710, plain, (![U_225, U_120]: (ssPv1(U_225) | ssPv8(U_120) | ~ssPv7(U_225) | ~ssRr(U_120, U_225) | ~ssPv6(U_225) | ~ssPv4(skf2(U_225)) | ~ssPv5(skf2(U_225))))). % 12.78/5.03 tff(c_1063, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv8(U_2) | ~ssPv7(skf2(U_2)) | ssPv6(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2))))). % 12.78/5.03 tff(c_709, plain, (![U_225]: (ssPv2(U_225) | ~ssPv7(U_225) | ~ssPv5(U_225) | ~ssPv6(skf2(U_225)) | ~ssPv6(U_225) | ~ssPv4(skf2(U_225)) | ~ssPv5(skf2(U_225))))). % 12.78/5.03 tff(c_911, plain, (![U_259]: (ssPv6(U_259) | ssPv3(skf3(U_259)) | ~ssPv8(U_259) | ssPv7(U_259) | ~ssPv4(U_259) | ~ssPv6(skf3(U_259)) | ~ssPv1(U_259)))). % 12.78/5.03 tff(c_1154, plain, (![U_286]: (ssPv2(skf3(U_286)) | ssPv7(U_286) | ~ssPv3(skf3(U_286)) | ssPv7(skf3(U_286)) | ~ssPv5(skf3(U_286)) | ~ssPv4(U_286)))). % 12.78/5.04 tff(c_598, plain, (![U_204]: (ssPv6(skf2(U_204)) | ssPv3(U_204) | ~ssPv8(skf2(U_204)) | ssPv7(skf2(U_204)) | ~ssPv5(skf3(skf2(U_204))) | ~ssPv5(skf2(U_204))))). % 12.78/5.04 tff(c_985, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv4(U_1) | ssPv7(U_1) | ~ssPv5(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.04 tff(c_1033, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv7(U_1) | ~ssPv3(skf3(U_1)) | ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.04 tff(c_1136, plain, (![U_283]: (ssPv6(U_283) | ssPv4(skf3(skf3(U_283))) | ssPv7(skf3(U_283)) | ~ssPv5(skf3(U_283)) | ~ssPv4(U_283)))). % 12.78/5.04 tff(c_938, plain, (![U_1, U_265]: (ssPv6(U_1) | ssPv4(U_265) | ~ssRr(U_265, skf3(U_1)) | ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.04 tff(c_553, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv5(U_2) | ~ssPv3(skf2(U_2)) | ssPv6(skf2(U_2)) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_2)))). % 12.78/5.04 tff(c_1083, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv8(U_2) | ~ssPv7(skf2(U_2)) | ssPv8(skf2(U_2)) | ~ssPv5(skf2(U_2)) | ~ssPv5(skf2(skf2(U_2)))))). % 12.78/5.04 tff(c_1082, plain, (![U_1]: (ssPv1(U_1) | ssPv8(skf3(U_1)) | ~ssPv7(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv5(skf2(U_1))))). % 12.78/5.04 tff(c_233, plain, (![U_2, U_123]: (ssPv1(U_2) | ssPv8(U_123) | ~ssPv7(U_2) | ~ssRr(U_123, U_2) | ssPv8(U_2) | ~ssPv5(U_2) | ~ssPv5(skf2(U_2))))). % 12.78/5.04 tff(c_1062, plain, (![U_1]: (ssPv1(U_1) | ssPv8(skf3(U_1)) | ~ssPv7(U_1) | ssPv6(skf2(U_1)) | ssPv1(skf2(U_1)) | ~ssPv2(U_1)))). % 12.78/5.04 tff(c_234, plain, (![U_2, U_123]: (ssPv1(U_2) | ssPv8(U_123) | ~ssPv7(U_2) | ~ssRr(U_123, U_2) | ssPv6(skf2(U_2)) | ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.78/5.04 tff(c_376, plain, (![U_170]: (ssPv3(skf2(U_170)) | ssPv7(U_170) | ssPv5(skf3(skf2(U_170))) | ~ssPv4(skf3(skf2(U_170))) | ~ssPv1(skf2(U_170))))). % 12.78/5.04 tff(c_912, plain, (![U_259]: (ssPv2(skf3(U_259)) | ~ssPv3(skf3(U_259)) | ssPv7(U_259) | ~ssPv4(U_259) | ~ssPv6(skf3(U_259)) | ~ssPv1(U_259)))). % 12.78/5.04 tff(c_457, plain, (![U_186]: (ssPv8(skf3(U_186)) | ssPv7(U_186) | ~ssPv3(skf2(skf3(U_186))) | ~ssPv3(skf3(U_186)) | ~ssPv5(skf3(U_186))))). % 12.78/5.04 tff(c_624, plain, (![U_207]: (ssPv2(skf3(U_207)) | ~ssPv3(skf3(U_207)) | ~ssPv4(U_207) | ssPv5(U_207) | ~ssPv6(skf3(U_207)) | ~ssPv1(U_207)))). % 12.78/5.04 tff(c_459, plain, (![U_186]: (ssPv7(U_186) | ~ssPv5(skf3(U_186)) | ssPv8(skf3(U_186)) | ~ssPv6(skf3(U_186)) | ~ssPv1(skf2(skf3(U_186)))))). % 12.78/5.04 tff(c_199, plain, (![U_108]: (ssPv2(U_108) | ~ssPv7(skf2(U_108)) | ~ssPv6(skf2(U_108)) | ssPv4(U_108) | ssPv2(skf2(U_108)) | ~ssPv3(U_108)))). % 12.78/5.04 tff(c_441, plain, (![U_184]: (ssPv2(skf3(U_184)) | ~ssPv3(skf3(U_184)) | ~ssPv4(U_184) | ssPv7(U_184) | ~ssPv5(skf3(U_184)) | ~ssPv5(U_184)))). % 12.78/5.04 tff(c_296, plain, (![U_1]: (ssPv6(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(U_1) | ssPv5(skf3(U_1)) | ssPv2(U_1) | ~ssPv7(skf3(U_1))))). % 12.78/5.04 tff(c_152, plain, (![U_92]: (ssPv2(skf3(U_92)) | ~ssPv3(skf3(U_92)) | ~ssPv4(U_92) | ssPv5(skf3(U_92)) | ssPv2(U_92) | ~ssPv7(skf3(U_92))))). % 12.78/5.04 tff(c_775, plain, (![U_236, U_237]: (ssPv7(skf3(U_236)) | ssPv6(U_236) | ssPv4(U_237) | ~ssPv3(skf2(skf3(U_236))) | ~ssRr(U_237, skf3(U_236))))). % 12.78/5.04 tff(c_855, plain, (![U_251, V_253]: (ssPv7(U_251) | ~ssPv6(skf3(U_251)) | ~ssPv4(skf2(skf3(U_251))) | ~ssPv5(V_253) | ~ssRr(skf3(U_251), V_253)))). % 12.78/5.04 tff(c_870, plain, (![U_1]: (ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv5(U_1) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.04 tff(c_887, plain, (![U_257]: (ssPv7(U_257) | ~ssPv4(U_257) | ssPv8(skf3(U_257)) | ~ssPv6(skf3(U_257)) | ~ssPv1(skf2(skf3(U_257)))))). % 12.78/5.04 tff(c_886, plain, (![U_1]: (ssPv7(U_1) | ~ssPv4(U_1) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.04 tff(c_835, plain, (![U_248]: (ssPv7(skf2(skf3(U_248))) | ~ssPv6(skf3(U_248)) | ~ssPv4(U_248) | ~ssPv5(skf2(skf3(U_248)))))). % 12.78/5.04 tff(c_865, plain, (![U_254]: (ssPv7(U_254) | ~ssPv6(skf3(U_254)) | ~ssPv4(U_254) | ~ssPv5(skf2(skf3(U_254)))))). % 12.78/5.04 tff(c_864, plain, (![U_1]: (ssPv7(U_1) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1)))). % 12.78/5.04 tff(c_854, plain, (![U_1, V_253]: (ssPv7(U_1) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(V_253) | ~ssRr(skf3(U_1), V_253)))). % 12.78/5.04 tff(c_359, plain, (![U_1, W_165, V_166]: (ssPv7(U_1) | ~ssPv6(skf3(U_1)) | ~ssPv4(W_165) | ~ssRr(skf3(U_1), W_165) | ~ssPv5(V_166) | ~ssRr(skf3(U_1), V_166)))). % 12.78/5.04 tff(c_834, plain, (![U_1]: (ssPv7(skf2(skf3(U_1))) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(U_1)))). % 12.78/5.04 tff(c_690, plain, (![U_1, V_222]: (ssPv7(skf2(skf3(U_1))) | ~ssPv6(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv5(V_222) | ~ssRr(skf3(U_1), V_222)))). % 12.78/5.04 tff(c_818, plain, (![U_1]: (~ssPv6(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ssPv8(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.04 tff(c_547, plain, (![U_1]: (~ssPv6(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ssPv8(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1))))). % 12.78/5.04 tff(c_800, plain, (![U_243]: (ssPv7(skf3(U_243)) | ssPv6(skf2(skf3(U_243))) | ssPv4(skf3(skf3(U_243))) | ~ssPv3(U_243)))). % 12.78/5.04 tff(c_728, plain, (![U_1, U_228]: (ssPv7(skf3(U_1)) | ssPv6(skf2(skf3(U_1))) | ssPv4(U_228) | ~ssPv3(U_1) | ~ssRr(U_228, skf3(U_1))))). % 12.78/5.04 tff(c_351, plain, (![U_2]: (ssPv2(U_2) | ~ssPv7(U_2) | ~ssPv6(skf2(U_2)) | ssPv8(U_2) | ~ssPv5(U_2) | ~ssPv5(skf2(U_2))))). % 12.78/5.04 tff(c_781, plain, (![U_239]: (ssPv7(skf3(U_239)) | ssPv6(U_239) | ssPv4(skf3(skf3(U_239))) | ~ssPv3(U_239)))). % 12.78/5.04 tff(c_774, plain, (![U_1, U_237]: (ssPv7(skf3(U_1)) | ssPv6(U_1) | ssPv4(U_237) | ~ssPv3(U_1) | ~ssRr(U_237, skf3(U_1))))). % 12.78/5.04 tff(c_382, plain, (![U_1, U_173, W_174]: (ssPv7(skf3(U_1)) | ssPv6(U_1) | ssPv4(U_173) | ~ssPv3(W_174) | ~ssRr(skf3(U_1), W_174) | ~ssRr(U_173, skf3(U_1))))). % 12.78/5.04 tff(c_756, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ssPv3(skf3(U_1)) | ssPv3(U_1)))). % 12.78/5.04 tff(c_440, plain, (![U_184]: (ssPv6(U_184) | ssPv3(skf3(U_184)) | ~ssPv8(U_184) | ssPv7(U_184) | ~ssPv5(skf3(U_184)) | ~ssPv5(U_184)))). % 12.78/5.04 tff(c_736, plain, (![U_2]: (ssPv7(skf2(U_2)) | ssPv6(skf2(skf2(U_2))) | ssPv4(U_2) | ~ssPv3(skf2(skf2(U_2)))))). % 12.78/5.04 tff(c_735, plain, (![U_1]: (ssPv7(U_1) | ssPv6(skf2(U_1)) | ssPv4(skf3(U_1)) | ~ssPv3(skf2(U_1))))). % 12.78/5.04 tff(c_729, plain, (![U_2, U_228]: (ssPv7(U_2) | ssPv6(skf2(U_2)) | ssPv4(U_228) | ~ssPv3(skf2(U_2)) | ~ssRr(U_228, U_2)))). % 12.78/5.04 tff(c_383, plain, (![U_2, U_173, W_174]: (ssPv7(U_2) | ssPv6(skf2(U_2)) | ssPv4(U_173) | ~ssPv3(W_174) | ~ssRr(U_2, W_174) | ~ssRr(U_173, U_2)))). % 12.78/5.04 tff(c_697, plain, (![U_1]: (ssPv7(skf2(skf3(U_1))) | ~ssPv6(skf3(U_1)) | ~ssPv4(skf2(skf3(U_1))) | ~ssPv5(U_1)))). % 12.78/5.04 tff(c_698, plain, (![U_2]: (ssPv7(skf2(U_2)) | ~ssPv6(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv5(skf2(U_2))))). % 12.78/5.04 tff(c_691, plain, (![U_2, V_222]: (ssPv7(skf2(U_2)) | ~ssPv6(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv5(V_222) | ~ssRr(U_2, V_222)))). % 12.78/5.04 tff(c_360, plain, (![U_2, W_165, V_166]: (ssPv7(skf2(U_2)) | ~ssPv6(U_2) | ~ssPv4(W_165) | ~ssRr(U_2, W_165) | ~ssPv5(V_166) | ~ssRr(U_2, V_166)))). % 12.78/5.04 tff(c_507, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv6(skf3(U_1))))). % 12.78/5.04 tff(c_623, plain, (![U_207]: (ssPv6(U_207) | ssPv3(skf3(U_207)) | ~ssPv8(U_207) | ssPv5(U_207) | ~ssPv6(skf3(U_207)) | ~ssPv1(U_207)))). % 12.78/5.04 tff(c_528, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv5(U_2) | ~ssPv3(U_2) | ssPv7(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.78/5.04 tff(c_142, plain, (![U_2]: (ssPv2(U_2) | ~ssPv7(skf2(U_2)) | ~ssPv6(skf2(U_2)) | ssPv5(U_2) | ~ssPv4(U_2) | ~ssPv3(U_2)))). % 12.78/5.04 tff(c_650, plain, (![U_212]: (ssPv4(skf3(U_212)) | ssPv2(U_212) | ssPv8(skf2(skf3(U_212))) | ~ssPv3(skf3(U_212))))). % 12.78/5.04 tff(c_649, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ssPv8(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.04 tff(c_135, plain, (![U_1, V_88]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ssPv8(V_88) | ~ssPv3(skf3(U_1)) | ~ssRr(skf3(U_1), V_88)))). % 12.78/5.04 tff(c_630, plain, (![U_208]: (ssPv8(skf3(U_208)) | ssPv4(skf3(U_208)) | ssPv6(U_208) | ssPv8(skf3(skf3(U_208)))))). % 12.78/5.04 tff(c_611, plain, (![U_205]: (ssPv8(skf3(U_205)) | ssPv5(U_205) | ~ssPv6(skf3(U_205)) | ~ssPv1(skf2(skf3(U_205)))))). % 12.78/5.04 tff(c_121, plain, (![U_1, U_82]: (ssPv8(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv6(U_1) | ssPv8(U_82) | ~ssRr(U_82, skf3(U_1))))). % 12.78/5.04 tff(c_610, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv5(U_1) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.04 tff(c_242, plain, (![U_1, V_128]: (ssPv8(skf3(U_1)) | ssPv5(U_1) | ~ssPv6(skf3(U_1)) | ~ssPv1(V_128) | ~ssRr(skf3(U_1), V_128)))). % 12.78/5.04 tff(c_562, plain, (![U_201]: (ssPv6(skf2(U_201)) | ssPv3(U_201) | ~ssPv8(skf2(U_201)) | ~ssPv8(skf3(skf2(U_201)))))). % 12.78/5.04 tff(c_563, plain, (![U_2]: (ssPv6(skf2(U_2)) | ssPv3(U_2) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_2)))). % 12.78/5.04 tff(c_277, plain, (![U_2, U_140]: (ssPv6(skf2(U_2)) | ssPv3(U_2) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_140) | ~ssRr(U_140, skf2(U_2))))). % 12.78/5.04 tff(c_516, plain, (![U_195]: (ssPv2(skf2(U_195)) | ssPv5(U_195) | ~ssPv3(skf2(U_195)) | ~ssPv3(skf3(skf2(U_195)))))). % 12.78/5.04 tff(c_494, plain, (![U_192]: (ssPv8(U_192) | ~ssPv7(skf3(U_192)) | ~ssPv5(skf3(U_192)) | ~ssPv6(skf2(skf3(U_192)))))). % 12.78/5.04 tff(c_505, plain, (![U_1]: (ssPv8(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.04 tff(c_517, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv5(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.78/5.05 tff(c_330, plain, (![U_2, U_156]: (ssPv2(skf2(U_2)) | ssPv5(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_156) | ~ssRr(U_156, skf2(U_2))))). % 12.78/5.05 tff(c_493, plain, (![U_1]: (ssPv8(U_1) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.78/5.05 tff(c_256, plain, (![U_1, V_133]: (ssPv8(U_1) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(V_133) | ~ssRr(skf3(U_1), V_133)))). % 12.78/5.05 tff(c_475, plain, (![U_189]: (ssPv1(skf3(U_189)) | ssPv8(skf3(skf3(U_189))) | ~ssPv7(skf3(U_189)) | ~ssPv7(U_189)))). % 12.78/5.05 tff(c_223, plain, (![U_1, U_120]: (ssPv1(skf3(U_1)) | ssPv8(U_120) | ~ssPv7(skf3(U_1)) | ~ssPv7(U_1) | ~ssRr(U_120, skf3(U_1))))). % 12.78/5.05 tff(c_458, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(skf3(U_1)) | ssPv8(skf3(U_1)) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.05 tff(c_432, plain, (![U_182]: (ssPv7(skf3(U_182)) | ssPv3(U_182) | ~ssPv5(skf3(U_182)) | ~ssPv4(skf2(skf3(U_182)))))). % 12.78/5.05 tff(c_422, plain, (![U_180]: (ssPv8(skf3(U_180)) | ssPv7(U_180) | ~ssPv5(skf3(U_180)) | ~ssPv5(skf2(skf3(U_180)))))). % 12.78/5.05 tff(c_431, plain, (![U_1]: (ssPv7(skf3(U_1)) | ssPv3(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.05 tff(c_421, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv7(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv5(U_1)))). % 12.78/5.05 tff(c_313, plain, (![U_1, V_149]: (ssPv7(skf3(U_1)) | ssPv3(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv4(V_149) | ~ssRr(skf3(U_1), V_149)))). % 12.78/5.05 tff(c_185, plain, (![U_1, V_104]: (ssPv8(skf3(U_1)) | ssPv7(U_1) | ~ssPv5(skf3(U_1)) | ~ssPv5(V_104) | ~ssRr(skf3(U_1), V_104)))). % 12.78/5.05 tff(c_409, plain, (![U_2]: (ssPv5(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.78/5.05 tff(c_392, plain, (![U_175]: (ssPv5(skf2(U_175)) | ~ssPv3(skf2(U_175)) | ~ssPv3(U_175) | ~ssPv5(skf3(skf2(U_175)))))). % 12.78/5.05 tff(c_393, plain, (![U_2]: (ssPv5(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv5(U_2)))). % 12.78/5.05 tff(c_214, plain, (![U_2, U_114]: (ssPv5(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv5(U_114) | ~ssRr(U_114, skf2(U_2))))). % 12.78/5.05 tff(c_42, plain, (![V_51, X_53, U_50, W_52]: (ssPv7(V_51) | ssPv6(X_53) | ssPv4(U_50) | ~ssRr(V_51, X_53) | ~ssPv3(W_52) | ~ssRr(V_51, W_52) | ~ssRr(U_50, V_51)))). % 12.78/5.05 tff(c_369, plain, (![U_167]: (ssPv3(skf2(U_167)) | ssPv7(U_167) | ~ssPv1(skf2(U_167)) | ~ssPv6(skf3(skf2(U_167)))))). % 12.78/5.05 tff(c_370, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv7(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.78/5.05 tff(c_160, plain, (![U_2, U_96]: (ssPv3(skf2(U_2)) | ssPv7(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_96) | ~ssRr(U_96, skf2(U_2))))). % 12.78/5.05 tff(c_44, plain, (![X_57, U_54, W_56, V_55]: (ssPv7(X_57) | ~ssPv6(U_54) | ~ssRr(U_54, X_57) | ~ssPv4(W_56) | ~ssRr(U_54, W_56) | ~ssPv5(V_55) | ~ssRr(U_54, V_55)))). % 12.78/5.05 tff(c_297, plain, (![U_1]: (ssPv6(U_1) | ~ssPv8(U_1) | ssPv5(skf3(U_1)) | ssPv3(skf3(U_1)) | ssPv3(U_1)))). % 12.78/5.05 tff(c_270, plain, (![U_137]: (ssPv2(U_137) | ~ssPv7(skf2(U_137)) | ~ssPv7(U_137) | ~ssPv5(U_137) | ~ssPv6(skf2(U_137))))). % 12.78/5.05 tff(c_337, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv5(skf3(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv3(U_2)))). % 12.78/5.05 tff(c_336, plain, (![U_1]: (ssPv2(U_1) | ssPv5(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.05 tff(c_329, plain, (![U_1, U_156]: (ssPv2(U_1) | ssPv5(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv3(U_156) | ~ssRr(U_156, U_1)))). % 12.78/5.05 tff(c_34, plain, (![V_39, W_40, U_38]: (ssPv2(V_39) | ssPv5(W_40) | ~ssPv3(V_39) | ~ssRr(W_40, V_39) | ~ssPv3(U_38) | ~ssRr(U_38, V_39)))). % 12.78/5.05 tff(c_320, plain, (![U_1]: (ssPv7(skf3(U_1)) | ssPv3(skf2(skf3(U_1))) | ~ssPv5(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.05 tff(c_321, plain, (![U_2]: (ssPv7(U_2) | ssPv3(skf2(U_2)) | ~ssPv5(U_2) | ~ssPv4(skf2(U_2))))). % 12.78/5.05 tff(c_314, plain, (![U_2, V_149]: (ssPv7(U_2) | ssPv3(skf2(U_2)) | ~ssPv5(U_2) | ~ssPv4(V_149) | ~ssRr(U_2, V_149)))). % 12.78/5.05 tff(c_28, plain, (![U_29, W_31, V_30]: (ssPv7(U_29) | ssPv3(W_31) | ~ssPv5(U_29) | ~ssRr(U_29, W_31) | ~ssPv4(V_30) | ~ssRr(U_29, V_30)))). % 12.78/5.05 tff(c_284, plain, (![U_2]: (ssPv6(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv8(skf2(U_2)) | ~ssPv8(U_2)))). % 12.78/5.05 tff(c_264, plain, (![U_1]: (ssPv8(skf2(skf3(U_1))) | ~ssPv7(skf3(U_1)) | ~ssPv5(skf3(U_1)) | ~ssPv6(U_1)))). % 12.78/5.05 tff(c_249, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv5(skf2(skf3(U_1))) | ~ssPv6(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.05 tff(c_283, plain, (![U_1]: (ssPv6(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(U_1) | ~ssPv8(skf3(U_1))))). % 12.78/5.05 tff(c_276, plain, (![U_1, U_140]: (ssPv6(U_1) | ssPv3(skf3(U_1)) | ~ssPv8(U_1) | ~ssPv8(U_140) | ~ssRr(U_140, U_1)))). % 12.78/5.05 tff(c_30, plain, (![V_33, W_34, U_32]: (ssPv6(V_33) | ssPv3(W_34) | ~ssPv8(V_33) | ~ssRr(W_34, V_33) | ~ssPv8(U_32) | ~ssRr(U_32, V_33)))). % 12.78/5.05 tff(c_265, plain, (![U_2]: (ssPv8(skf2(U_2)) | ~ssPv7(U_2) | ~ssPv5(U_2) | ~ssPv6(skf2(U_2))))). % 12.78/5.05 tff(c_257, plain, (![U_2, V_133]: (ssPv8(skf2(U_2)) | ~ssPv7(U_2) | ~ssPv5(U_2) | ~ssPv6(V_133) | ~ssRr(U_2, V_133)))). % 12.78/5.05 tff(c_250, plain, (![U_2]: (ssPv8(U_2) | ssPv5(skf2(U_2)) | ~ssPv6(U_2) | ~ssPv1(skf2(U_2))))). % 12.78/5.05 tff(c_38, plain, (![W_46, U_44, V_45]: (ssPv8(W_46) | ~ssPv7(U_44) | ~ssPv5(U_44) | ~ssRr(U_44, W_46) | ~ssPv6(V_45) | ~ssRr(U_44, V_45)))). % 12.78/5.05 tff(c_243, plain, (![U_2, V_128]: (ssPv8(U_2) | ssPv5(skf2(U_2)) | ~ssPv6(U_2) | ~ssPv1(V_128) | ~ssRr(U_2, V_128)))). % 12.78/5.05 tff(c_24, plain, (![U_23, W_25, V_24]: (ssPv8(U_23) | ssPv5(W_25) | ~ssPv6(U_23) | ~ssRr(U_23, W_25) | ~ssPv1(V_24) | ~ssRr(U_23, V_24)))). % 12.78/5.05 tff(c_179, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv7(skf3(skf2(U_2))) | ~ssPv1(skf2(U_2)) | ~ssPv6(U_2)))). % 12.78/5.05 tff(c_167, plain, (![U_2]: (ssPv8(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv6(skf2(skf2(U_2))) | ssPv8(U_2)))). % 12.78/5.05 tff(c_224, plain, (![U_2, U_120]: (ssPv1(U_2) | ssPv8(U_120) | ~ssPv7(U_2) | ~ssPv7(skf2(U_2)) | ~ssRr(U_120, U_2)))). % 12.78/5.05 tff(c_36, plain, (![V_42, U_41, W_43]: (ssPv1(V_42) | ssPv8(U_41) | ~ssPv7(V_42) | ~ssPv7(W_43) | ~ssRr(V_42, W_43) | ~ssRr(U_41, V_42)))). % 12.78/5.05 tff(c_193, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ssPv8(U_1) | ~ssPv3(skf3(U_1))))). % 12.78/5.05 tff(c_205, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv7(skf2(skf3(U_1))) | ~ssPv5(skf3(U_1)) | ~ssPv5(U_1)))). % 12.78/5.05 tff(c_213, plain, (![U_1, U_114]: (ssPv5(U_1) | ~ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv5(U_114) | ~ssRr(U_114, U_1)))). % 12.78/5.05 tff(c_40, plain, (![V_48, W_49, U_47]: (ssPv5(V_48) | ~ssPv3(V_48) | ~ssPv3(W_49) | ~ssRr(W_49, V_48) | ~ssPv5(U_47) | ~ssRr(U_47, V_48)))). % 12.78/5.05 tff(c_206, plain, (![U_2]: (ssPv8(U_2) | ssPv7(skf2(U_2)) | ~ssPv5(U_2) | ~ssPv5(skf2(U_2))))). % 12.78/5.05 tff(c_186, plain, (![U_2, V_104]: (ssPv8(U_2) | ssPv7(skf2(U_2)) | ~ssPv5(U_2) | ~ssPv5(V_104) | ~ssRr(U_2, V_104)))). % 12.78/5.05 tff(c_194, plain, (![U_2]: (ssPv4(U_2) | ssPv2(skf2(U_2)) | ssPv8(skf2(U_2)) | ~ssPv3(U_2)))). % 12.78/5.05 tff(c_136, plain, (![U_2, V_88]: (ssPv4(U_2) | ssPv2(skf2(U_2)) | ssPv8(V_88) | ~ssPv3(U_2) | ~ssRr(U_2, V_88)))). % 12.78/5.05 tff(c_178, plain, (![U_1]: (ssPv3(U_1) | ssPv7(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv6(skf3(U_1))))). % 12.78/5.05 tff(c_26, plain, (![U_26, W_28, V_27]: (ssPv8(U_26) | ssPv7(W_28) | ~ssPv5(U_26) | ~ssRr(U_26, W_28) | ~ssPv5(V_27) | ~ssRr(U_26, V_27)))). % 12.78/5.05 tff(c_159, plain, (![U_1, U_96]: (ssPv3(U_1) | ssPv7(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv6(U_96) | ~ssRr(U_96, U_1)))). % 12.78/5.05 tff(c_166, plain, (![U_1]: (ssPv8(U_1) | ssPv4(U_1) | ssPv6(skf2(U_1)) | ssPv8(skf3(U_1))))). % 12.78/5.05 tff(c_122, plain, (![U_2, U_82]: (ssPv8(U_2) | ssPv4(U_2) | ssPv6(skf2(U_2)) | ssPv8(U_82) | ~ssRr(U_82, U_2)))). % 12.78/5.05 tff(c_32, plain, (![V_36, W_37, U_35]: (ssPv3(V_36) | ssPv7(W_37) | ~ssPv1(V_36) | ~ssRr(W_37, V_36) | ~ssPv6(U_35) | ~ssRr(U_35, V_36)))). % 12.78/5.05 tff(c_54, plain, (![U_1]: (ssPv5(skf3(U_1)) | ssPv8(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1))))). % 12.78/5.05 tff(c_104, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv5(skf3(U_1)) | ssPv2(U_1) | ~ssPv7(skf3(U_1))))). % 12.78/5.05 tff(c_93, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv8(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv4(U_1)))). % 12.78/5.05 tff(c_115, plain, (![U_2]: (ssPv2(U_2) | ~ssPv8(skf2(U_2)) | ~ssPv7(skf2(U_2)) | ~ssPv6(skf2(U_2))))). % 12.78/5.05 tff(c_64, plain, (![U_1]: (ssPv8(skf3(U_1)) | ssPv5(skf3(U_1)) | ssPv3(skf3(U_1)) | ssPv3(U_1)))). % 12.78/5.05 tff(c_22, plain, (![U_20, W_22, V_21]: (ssPv4(U_20) | ssPv2(W_22) | ssPv8(V_21) | ~ssPv3(U_20) | ~ssRr(U_20, W_22) | ~ssRr(U_20, V_21)))). % 12.78/5.05 tff(c_84, plain, (![U_1]: (ssPv6(skf3(U_1)) | ssPv5(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 12.78/5.05 tff(c_74, plain, (![U_2]: (ssPv7(skf2(U_2)) | ssPv6(skf2(U_2)) | ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.78/5.05 tff(c_114, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 12.78/5.05 tff(c_20, plain, (![V_18, W_19, U_17]: (ssPv8(V_18) | ssPv4(V_18) | ssPv6(W_19) | ssPv8(U_17) | ~ssRr(V_18, W_19) | ~ssRr(U_17, V_18)))). % 12.78/5.05 tff(c_16, plain, (![U_13, V_14]: (ssPv2(U_13) | ~ssPv8(V_14) | ~ssPv7(V_14) | ~ssPv6(V_14) | ~ssRr(U_13, V_14)))). % 12.78/5.05 tff(c_105, plain, (![U_2]: (ssPv8(U_2) | ssPv5(U_2) | ssPv2(skf2(U_2)) | ~ssPv7(U_2)))). % 12.78/5.05 tff(c_8, plain, (![U_5, V_6]: (ssPv8(U_5) | ssPv5(U_5) | ssPv2(V_6) | ~ssPv7(U_5) | ~ssRr(U_5, V_6)))). % 12.78/5.05 tff(c_94, plain, (![U_2]: (ssPv2(U_2) | ~ssPv8(U_2) | ~ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 12.78/5.05 tff(c_85, plain, (![U_2]: (ssPv6(U_2) | ssPv5(U_2) | ~ssPv4(U_2) | ~ssPv1(skf2(U_2))))). % 12.78/5.05 tff(c_18, plain, (![U_15, V_16]: (ssPv2(U_15) | ~ssPv8(U_15) | ~ssPv3(U_15) | ~ssPv4(V_16) | ~ssRr(U_15, V_16)))). % 12.78/5.05 tff(c_14, plain, (![U_11, V_12]: (ssPv6(U_11) | ssPv5(U_11) | ~ssPv4(U_11) | ~ssPv1(V_12) | ~ssRr(U_11, V_12)))). % 12.78/5.05 tff(c_73, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ssPv1(U_1) | ~ssPv2(skf3(U_1))))). % 12.78/5.05 tff(c_65, plain, (![U_2]: (ssPv8(U_2) | ssPv5(U_2) | ssPv3(U_2) | ssPv3(skf2(U_2))))). % 12.78/5.06 tff(c_10, plain, (![V_8, U_7]: (ssPv7(V_8) | ssPv6(V_8) | ssPv1(V_8) | ~ssPv2(U_7) | ~ssRr(U_7, V_8)))). % 12.78/5.06 tff(c_6, plain, (![U_3, V_4]: (ssPv8(U_3) | ssPv5(U_3) | ssPv3(U_3) | ssPv3(V_4) | ~ssRr(U_3, V_4)))). % 12.78/5.06 tff(c_55, plain, (![U_2]: (ssPv5(U_2) | ssPv8(skf2(U_2)) | ~ssPv4(U_2) | ~ssPv3(U_2)))). % 12.78/5.06 tff(c_12, plain, (![U_9, V_10]: (ssPv5(U_9) | ssPv8(V_10) | ~ssPv4(U_9) | ~ssPv3(U_9) | ~ssRr(U_9, V_10)))). % 12.78/5.06 tff(c_2, plain, (![U_1]: (ssRr(skf3(U_1), U_1)))). % 12.78/5.06 tff(c_4, plain, (![U_2]: (ssRr(U_2, skf2(U_2))))). % 12.78/5.06 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.78/5.06 %------------------------------------------------------------------------------