%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN763-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 : n018.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 23.39s 13.92s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN763-1 : TPTP v9.0.0. Released v2.5.0. % 0.07/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.14/0.35 % Computer : n018.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 08:17:32 EDT 2025 % 0.14/0.35 % CPUTime : % 23.39/13.92 % 23.39/13.92 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.39/13.92 % 23.39/13.92 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.39/13.93 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 23.39/13.93 % 23.39/13.93 %Foreground sorts: % 23.39/13.93 % 23.39/13.93 % 23.39/13.93 %Background operators: % 23.39/13.93 % 23.39/13.93 % 23.39/13.93 %Foreground operators: % 23.39/13.93 tff(skf1, type, skf1: $i > $i). % 23.39/13.93 tff(ssPv1, type, ssPv1: $i > $o). % 23.39/13.93 tff(ssPv3, type, ssPv3: $i > $o). % 23.39/13.93 tff(ssPv7, type, ssPv7: $i > $o). % 23.39/13.93 tff(ssPv6, type, ssPv6: $i > $o). % 23.39/13.93 tff(ssPv5, type, ssPv5: $i > $o). % 23.39/13.93 tff(ssRr, type, ssRr: ($i * $i) > $o). % 23.39/13.93 tff(ssPv4, type, ssPv4: $i > $o). % 23.39/13.93 tff(ssPv2, type, ssPv2: $i > $o). % 23.39/13.93 tff(ssPv8, type, ssPv8: $i > $o). % 23.39/13.93 % 23.39/13.93 %Saturated clause set: % 23.39/13.93 tff(c_45148, plain, (![U_1]: (~ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv6(U_1) | ssPv3(U_1)))). % 23.39/13.93 tff(c_44875, plain, (![U_1416]: (~ssPv3(skf1(U_1416)) | ssPv5(skf1(U_1416)) | ssPv2(skf1(U_1416)) | ssPv4(skf1(U_1416)) | ssPv1(skf1(U_1416)) | ~ssPv6(skf1(U_1416)) | ssPv4(U_1416) | ~ssPv8(U_1416) | ~ssPv7(U_1416)))). % 23.39/13.93 tff(c_35350, plain, (![U_1]: (~ssPv8(U_1) | ssPv3(U_1) | ssPv4(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 23.39/13.93 tff(c_44723, plain, (![U_1]: (ssPv3(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.93 tff(c_44347, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.93 tff(c_44267, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv6(U_1) | ssPv3(U_1)))). % 23.39/13.93 tff(c_43496, plain, (![V_222, U_1396]: (~ssPv8(V_222) | ~ssRr(U_1396, V_222) | ~ssPv3(skf1(U_1396)) | ssPv1(skf1(U_1396)) | ssPv2(skf1(U_1396)) | ssPv4(skf1(U_1396)) | ~ssPv7(U_1396) | ~ssPv4(U_1396) | ssPv6(U_1396) | ssPv3(U_1396)))). % 23.39/13.93 tff(c_44115, plain, (![U_1401]: (~ssPv3(skf1(U_1401)) | ssPv5(skf1(U_1401)) | ssPv2(skf1(U_1401)) | ssPv4(skf1(U_1401)) | ssPv1(skf1(U_1401)) | ssPv4(U_1401) | ~ssPv6(U_1401) | ~ssPv6(skf1(U_1401))))). % 23.39/13.93 tff(c_35364, plain, (![U_1]: (ssPv7(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 23.39/13.93 tff(c_43777, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.93 tff(c_43159, plain, (![U_1]: (~ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv6(U_1) | ssPv3(U_1)))). % 23.39/13.94 tff(c_43160, plain, (![U_1]: (~ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(U_1) | ~ssPv6(U_1)))). % 23.39/13.94 tff(c_43174, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.94 tff(c_35362, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ~ssPv7(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 23.39/13.94 tff(c_43026, plain, (![U_1391]: (~ssPv3(skf1(U_1391)) | ssPv2(skf1(U_1391)) | ssPv4(skf1(U_1391)) | ssPv1(skf1(U_1391)) | ~ssPv6(skf1(U_1391)) | ssPv5(skf1(U_1391)) | ~ssPv7(U_1391) | ~ssPv4(U_1391)))). % 23.39/13.94 tff(c_42853, plain, (![U_1389]: (~ssPv3(U_1389) | ssPv5(U_1389) | ~ssPv8(U_1389) | ssPv2(U_1389) | ssPv4(U_1389) | ssPv7(U_1389) | ssPv1(U_1389) | ~ssPv6(U_1389)))). % 23.39/13.94 tff(c_42690, plain, (![U_1]: (ssPv5(U_1) | ~ssPv8(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.94 tff(c_35363, plain, (![U_1]: (ssPv2(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 23.39/13.94 tff(c_42245, plain, (![U_1]: (~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_42180, plain, (![U_1372]: (ssPv1(U_1372) | ~ssPv2(U_1372) | ssPv8(U_1372) | ~ssPv5(U_1372) | ~ssPv1(skf1(U_1372)) | ssPv3(skf1(U_1372)) | ~ssPv6(U_1372) | ~ssPv2(skf1(U_1372)) | ~ssPv7(U_1372) | ~ssPv4(U_1372)))). % 23.39/13.94 tff(c_42027, plain, (![U_1]: (ssPv5(U_1) | ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.94 tff(c_41756, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.94 tff(c_13626, plain, (![U_828, V_231]: (ssPv1(U_828) | ~ssPv2(U_828) | ~ssPv8(V_231) | ~ssRr(U_828, V_231) | ssPv8(U_828) | ~ssPv5(U_828) | ~ssPv1(skf1(U_828)) | ssPv3(skf1(U_828)) | ~ssPv7(U_828) | ~ssPv6(U_828) | ~ssPv2(skf1(U_828))))). % 23.39/13.94 tff(c_36710, plain, (![U_1269]: (ssPv2(U_1269) | ssPv4(skf1(U_1269)) | ~ssPv3(U_1269) | ~ssPv8(U_1269) | ssPv7(U_1269) | ssPv5(U_1269) | ~ssPv6(U_1269) | ssPv4(U_1269) | ssPv1(skf1(U_1269)) | ~ssPv1(U_1269) | ~ssPv3(skf1(U_1269))))). % 23.39/13.94 tff(c_41623, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ~ssPv8(U_1) | ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.94 tff(c_36597, plain, (![V_222, U_1267]: (~ssPv8(V_222) | ~ssRr(U_1267, V_222) | ~ssPv8(U_1267) | ssPv1(U_1267) | ~ssPv2(skf1(U_1267)) | ssPv1(skf1(U_1267)) | ssPv3(U_1267) | ssPv6(U_1267) | ~ssPv2(U_1267) | ~ssPv7(U_1267) | ~ssPv4(U_1267)))). % 23.39/13.94 tff(c_41513, plain, (![U_1, V_1353]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_1353) | ~ssRr(U_1, V_1353) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv5(U_1) | ~ssPv6(U_1)))). % 23.39/13.94 tff(c_34782, plain, (![W_478, U_1209, V_479]: (~ssPv6(W_478) | ~ssRr(U_1209, W_478) | ~ssPv8(V_479) | ~ssRr(U_1209, V_479) | ~ssPv2(U_1209) | ssPv7(U_1209) | ssPv4(U_1209) | ssPv1(skf1(U_1209)) | ~ssPv1(U_1209) | ssPv5(U_1209) | ~ssPv6(U_1209)))). % 23.39/13.94 tff(c_41420, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.94 tff(c_41270, plain, (![U_1, V_1344]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_1344) | ~ssRr(U_1, V_1344) | ~ssPv8(U_1) | ssPv7(U_1) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_34059, plain, (![W_478, U_1190, V_479]: (~ssPv6(W_478) | ~ssRr(U_1190, W_478) | ~ssPv8(V_479) | ~ssRr(U_1190, V_479) | ~ssPv8(U_1190) | ssPv7(U_1190) | ssPv5(U_1190) | ~ssPv6(U_1190) | ssPv4(U_1190) | ssPv1(skf1(U_1190)) | ~ssPv1(U_1190)))). % 23.39/13.94 tff(c_41160, plain, (![U_1, V_1339]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_1339) | ~ssRr(U_1, V_1339) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.94 tff(c_13000, plain, (![W_478, U_812, V_479]: (~ssPv6(W_478) | ~ssRr(U_812, W_478) | ~ssPv8(V_479) | ~ssRr(U_812, V_479) | ~ssPv2(U_812) | ssPv7(U_812) | ssPv6(U_812) | ~ssPv1(U_812) | ssPv8(U_812) | ssPv5(U_812) | ssPv1(skf1(U_812))))). % 23.39/13.94 tff(c_41093, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.94 tff(c_40955, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ~ssPv8(U_1) | ssPv1(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_40951, plain, (![V_242, U_1332]: (~ssPv6(V_242) | ~ssRr(U_1332, V_242) | ~ssPv8(U_1332) | ssPv1(skf1(U_1332)) | ssPv2(U_1332) | ~ssPv5(U_1332) | ~ssPv3(U_1332) | ssPv7(U_1332) | ssPv6(U_1332) | ~ssPv1(U_1332)))). % 23.39/13.94 tff(c_40891, plain, (![U_1]: (~ssPv8(U_1) | ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_40785, plain, (![U_1]: (~ssPv2(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.94 tff(c_40647, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ~ssPv2(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_40643, plain, (![V_242, U_1324]: (~ssPv6(V_242) | ~ssRr(U_1324, V_242) | ~ssPv2(U_1324) | ssPv8(U_1324) | ~ssPv5(U_1324) | ~ssPv4(U_1324) | ssPv1(skf1(U_1324)) | ~ssPv7(U_1324) | ~ssPv3(U_1324) | ~ssPv1(U_1324)))). % 23.39/13.94 tff(c_40585, plain, (![U_1]: (~ssPv2(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_40174, plain, (![U_1]: (~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_8774, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ~ssPv6(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.94 tff(c_39927, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.94 tff(c_39789, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_39785, plain, (![V_242, U_1311]: (~ssPv6(V_242) | ~ssRr(U_1311, V_242) | ssPv8(U_1311) | ~ssPv5(U_1311) | ssPv6(U_1311) | ~ssPv2(U_1311) | ssPv1(skf1(U_1311)) | ~ssPv7(U_1311) | ~ssPv3(U_1311) | ~ssPv1(U_1311)))). % 23.39/13.94 tff(c_39727, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(U_1) | ssPv2(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.94 tff(c_39112, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.95 tff(c_39116, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.95 tff(c_39109, plain, (![U_1]: (ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.95 tff(c_38983, plain, (![U_372]: (~ssPv8(U_372) | ~ssPv2(U_372) | ssPv4(U_372) | ~ssPv6(U_372) | ssPv3(U_372) | ~ssPv2(skf1(U_372)) | ~ssPv5(U_372) | ssPv1(U_372) | ssPv1(skf1(U_372))))). % 23.39/13.95 tff(c_38690, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.95 tff(c_38548, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.95 tff(c_38512, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.95 tff(c_38157, plain, (![U_1292, V_459]: (~ssPv8(U_1292) | ~ssPv8(V_459) | ~ssRr(U_1292, V_459) | ssPv1(U_1292) | ssPv1(skf1(U_1292)) | ~ssPv6(U_1292) | ssPv3(U_1292) | ~ssPv2(skf1(U_1292)) | ssPv4(U_1292) | ~ssPv2(U_1292)))). % 23.39/13.95 tff(c_38163, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.95 tff(c_38159, plain, (![V_383, U_1292]: (~ssPv4(V_383) | ~ssRr(U_1292, V_383) | ssPv1(U_1292) | ssPv1(skf1(U_1292)) | ~ssPv6(U_1292) | ssPv3(U_1292) | ~ssPv2(skf1(U_1292)) | ssPv4(U_1292) | ~ssPv2(U_1292)))). % 23.39/13.95 tff(c_38140, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.95 tff(c_37576, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.95 tff(c_37045, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.95 tff(c_37041, plain, (![V_383, U_1278]: (~ssPv4(V_383) | ~ssRr(U_1278, V_383) | ~ssPv2(U_1278) | ~ssPv2(skf1(U_1278)) | ssPv1(skf1(U_1278)) | ssPv4(U_1278) | ssPv7(U_1278) | ssPv1(U_1278) | ~ssPv6(U_1278)))). % 23.39/13.95 tff(c_37022, plain, (![U_1]: (~ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.95 tff(c_36795, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv5(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.95 tff(c_13586, plain, (![U_827, V_231]: (~ssPv2(U_827) | ~ssPv8(V_231) | ~ssRr(U_827, V_231) | ~ssPv5(U_827) | ssPv3(skf1(U_827)) | ~ssPv2(skf1(U_827)) | ssPv1(skf1(U_827)) | ssPv7(U_827) | ssPv1(U_827) | ~ssPv6(U_827)))). % 23.39/13.95 tff(c_33333, plain, (![U_1177]: (ssPv7(U_1177) | ssPv4(skf1(U_1177)) | ~ssPv8(U_1177) | ssPv2(U_1177) | ~ssPv5(U_1177) | ~ssPv3(U_1177) | ssPv4(U_1177) | ssPv1(skf1(U_1177)) | ~ssPv1(U_1177) | ~ssPv3(skf1(U_1177))))). % 23.39/13.95 tff(c_34256, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv8(U_1) | ssPv7(U_1) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.95 tff(c_28469, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.95 tff(c_29708, plain, (![U_1]: (ssPv6(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.95 tff(c_36228, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.95 tff(c_36398, plain, (![U_1]: (~ssPv2(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/13.95 tff(c_36222, plain, (![U_1]: (ssPv4(U_1) | ~ssPv7(U_1) | ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.95 tff(c_36078, plain, (![U_1, V_1256]: (ssPv5(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv8(V_1256) | ~ssRr(U_1, V_1256) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.95 tff(c_25690, plain, (![U_1028, W_478, V_479]: (ssPv5(U_1028) | ~ssPv6(W_478) | ~ssRr(U_1028, W_478) | ~ssPv8(V_479) | ~ssRr(U_1028, V_479) | ssPv1(skf1(U_1028)) | ssPv6(U_1028) | ssPv7(U_1028) | ssPv3(U_1028) | ~ssPv2(U_1028)))). % 23.39/13.95 tff(c_36033, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ~ssPv8(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.95 tff(c_26745, plain, (![V_222, U_1055]: (~ssPv8(V_222) | ~ssRr(U_1055, V_222) | ~ssPv8(U_1055) | ssPv6(U_1055) | ssPv3(U_1055) | ssPv2(skf1(U_1055)) | ssPv1(U_1055) | ssPv1(skf1(U_1055)) | ~ssPv7(U_1055) | ~ssPv4(U_1055)))). % 23.39/13.95 tff(c_35923, plain, (![U_1, V_1248]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_1248) | ~ssRr(U_1, V_1248) | ~ssPv8(U_1) | ssPv6(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.95 tff(c_21752, plain, (![W_478, U_962, V_479]: (~ssPv6(W_478) | ~ssRr(U_962, W_478) | ~ssPv8(V_479) | ~ssRr(U_962, V_479) | ~ssPv8(U_962) | ssPv6(U_962) | ssPv1(skf1(U_962)) | ssPv5(U_962) | ssPv3(U_962) | ssPv1(U_962)))). % 23.39/13.95 tff(c_35878, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.95 tff(c_7354, plain, (![U_706, V_222]: (ssPv6(U_706) | ssPv3(U_706) | ~ssPv8(V_222) | ~ssRr(U_706, V_222) | ~ssPv2(skf1(U_706)) | ssPv4(skf1(U_706)) | ~ssPv7(U_706) | ~ssPv4(U_706) | ssPv1(U_706) | ssPv1(skf1(U_706))))). % 23.39/13.95 tff(c_35768, plain, (![U_1, V_1240]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_1240) | ~ssRr(U_1, V_1240) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.95 tff(c_19770, plain, (![W_478, U_923, V_479]: (~ssPv6(W_478) | ~ssRr(U_923, W_478) | ~ssPv8(V_479) | ~ssRr(U_923, V_479) | ~ssPv2(U_923) | ssPv4(U_923) | ~ssPv1(U_923) | ssPv8(U_923) | ssPv5(U_923) | ssPv1(skf1(U_923))))). % 23.39/13.95 tff(c_35755, plain, (![U_1]: (~ssPv8(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv6(U_1) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.95 tff(c_35604, plain, (![U_1, V_1231]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_1231) | ~ssRr(U_1, V_1231) | ~ssPv8(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.95 tff(c_9524, plain, (![W_478, U_756, V_479]: (~ssPv6(W_478) | ~ssRr(U_756, W_478) | ~ssPv8(V_479) | ~ssRr(U_756, V_479) | ~ssPv8(U_756) | ssPv2(U_756) | ssPv1(skf1(U_756)) | ssPv5(U_756) | ssPv3(U_756) | ssPv1(U_756)))). % 23.39/13.95 tff(c_35549, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.95 tff(c_22599, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.95 tff(c_35223, plain, (![U_1222]: (~ssPv3(U_1222) | ~ssPv2(U_1222) | ssPv8(U_1222) | ssPv5(U_1222) | ssPv4(U_1222) | ssPv7(U_1222) | ssPv1(U_1222) | ~ssPv6(U_1222)))). % 23.39/13.95 tff(c_35206, plain, (![U_1221]: (~ssPv2(U_1221) | ssPv8(U_1221) | ssPv5(U_1221) | ssPv1(skf1(U_1221)) | ssPv4(U_1221) | ssPv7(U_1221) | ssPv1(U_1221) | ~ssPv6(U_1221)))). % 23.39/13.95 tff(c_34967, plain, (![U_1]: (ssPv3(U_1) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.95 tff(c_34791, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv5(U_1) | ~ssPv6(U_1)))). % 23.39/13.95 tff(c_34787, plain, (![U_1209, V_242]: (~ssPv3(U_1209) | ~ssPv6(V_242) | ~ssRr(U_1209, V_242) | ~ssPv2(U_1209) | ssPv7(U_1209) | ssPv4(U_1209) | ssPv1(skf1(U_1209)) | ~ssPv1(U_1209) | ssPv5(U_1209) | ~ssPv6(U_1209)))). % 23.39/13.95 tff(c_34697, plain, (![U_734]: (~ssPv2(U_734) | ssPv7(U_734) | ssPv2(skf1(U_734)) | ssPv4(U_734) | ssPv1(skf1(U_734)) | ~ssPv1(U_734) | ssPv5(U_734) | ~ssPv6(U_734)))). % 23.39/13.95 tff(c_34385, plain, (![U_1]: (ssPv3(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.95 tff(c_34118, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv8(U_1) | ssPv7(U_1) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.95 tff(c_34064, plain, (![U_1190, V_242]: (~ssPv3(U_1190) | ~ssPv6(V_242) | ~ssRr(U_1190, V_242) | ~ssPv8(U_1190) | ssPv7(U_1190) | ssPv5(U_1190) | ~ssPv6(U_1190) | ssPv4(U_1190) | ssPv1(skf1(U_1190)) | ~ssPv1(U_1190)))). % 23.39/13.95 tff(c_34099, plain, (![U_1]: (ssPv3(U_1) | ~ssPv8(U_1) | ssPv7(U_1) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_33867, plain, (![U_1]: (~ssPv8(U_1) | ssPv7(U_1) | ssPv2(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_22847, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.96 tff(c_33661, plain, (![U_574]: (ssPv6(U_574) | ~ssPv1(U_574) | ssPv7(U_574) | ssPv2(skf1(U_574)) | ssPv3(skf1(U_574)) | ssPv1(skf1(U_574)) | ssPv2(U_574) | ~ssPv5(U_574) | ~ssPv3(U_574)))). % 23.39/13.96 tff(c_33785, plain, (![U_1]: (~ssPv8(U_1) | ssPv3(U_1) | ~ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/13.96 tff(c_33275, plain, (![U_1]: (~ssPv8(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.96 tff(c_33137, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ~ssPv8(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_33133, plain, (![V_242, U_1173]: (~ssPv6(V_242) | ~ssRr(U_1173, V_242) | ~ssPv8(U_1173) | ssPv2(U_1173) | ~ssPv5(U_1173) | ~ssPv3(U_1173) | ssPv4(U_1173) | ssPv1(skf1(U_1173)) | ~ssPv1(U_1173)))). % 23.39/13.96 tff(c_33077, plain, (![U_1]: (~ssPv8(U_1) | ssPv2(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_32689, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.96 tff(c_32596, plain, (![U_1]: (~ssPv6(U_1) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.39/13.96 tff(c_32193, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_10482, plain, (![U_779, V_222]: (ssPv6(U_779) | ssPv3(U_779) | ~ssPv8(V_222) | ~ssRr(U_779, V_222) | ssPv2(skf1(U_779)) | ssPv3(skf1(U_779)) | ~ssPv7(U_779) | ~ssPv4(U_779) | ssPv8(U_779) | ssPv5(U_779) | ssPv1(skf1(U_779))))). % 23.39/13.96 tff(c_7640, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.96 tff(c_31970, plain, (![U_734]: (ssPv3(skf1(U_734)) | ssPv7(U_734) | ssPv2(skf1(U_734)) | ssPv4(U_734) | ssPv1(skf1(U_734)) | ~ssPv1(U_734) | ssPv5(U_734) | ~ssPv6(U_734)))). % 23.39/13.96 tff(c_7230, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.96 tff(c_22841, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.96 tff(c_31268, plain, (![U_1148]: (~ssPv2(U_1148) | ssPv3(skf1(U_1148)) | ~ssPv1(skf1(U_1148)) | ssPv5(skf1(U_1148)) | ssPv4(skf1(U_1148)) | ssPv3(U_1148) | ssPv1(U_1148) | ssPv5(U_1148) | ~ssPv6(U_1148)))). % 23.39/13.96 tff(c_30960, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.96 tff(c_14910, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv1(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.96 tff(c_22594, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_10442, plain, (![U_778, V_222]: (ssPv6(U_778) | ssPv3(U_778) | ~ssPv8(V_222) | ~ssRr(U_778, V_222) | ssPv2(skf1(U_778)) | ssPv4(skf1(U_778)) | ~ssPv7(U_778) | ~ssPv4(U_778) | ~ssPv5(U_778) | ~ssPv1(U_778) | ~ssPv3(skf1(U_778))))). % 23.39/13.96 tff(c_7308, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.96 tff(c_7306, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.96 tff(c_7313, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.96 tff(c_30636, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_9097, plain, (![U_743, V_222]: (ssPv6(U_743) | ssPv3(U_743) | ~ssPv8(V_222) | ~ssRr(U_743, V_222) | ssPv2(skf1(U_743)) | ssPv4(skf1(U_743)) | ~ssPv7(U_743) | ~ssPv4(U_743) | ssPv8(U_743) | ssPv5(U_743) | ssPv1(skf1(U_743))))). % 23.39/13.96 tff(c_14909, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.96 tff(c_30383, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_8768, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.96 tff(c_29715, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_13005, plain, (![U_812, V_242]: (~ssPv3(U_812) | ~ssPv6(V_242) | ~ssRr(U_812, V_242) | ~ssPv2(U_812) | ssPv7(U_812) | ssPv6(U_812) | ~ssPv1(U_812) | ssPv8(U_812) | ssPv5(U_812) | ssPv1(skf1(U_812))))). % 23.39/13.96 tff(c_29586, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_14424, plain, (![V_242, U_836]: (~ssPv6(V_242) | ~ssRr(U_836, V_242) | ssPv6(U_836) | ~ssPv2(U_836) | ssPv8(U_836) | ssPv5(U_836) | ssPv1(skf1(U_836)) | ~ssPv7(U_836) | ~ssPv3(U_836) | ~ssPv1(U_836)))). % 23.39/13.96 tff(c_29522, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.96 tff(c_29489, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_9918, plain, (![U_765, V_231]: (ssPv1(U_765) | ~ssPv2(U_765) | ~ssPv8(V_231) | ~ssRr(U_765, V_231) | ~ssPv7(U_765) | ssPv3(U_765) | ~ssPv2(skf1(U_765)) | ssPv3(skf1(U_765)) | ssPv1(skf1(U_765))))). % 23.39/13.96 tff(c_27408, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.96 tff(c_29392, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_18453, plain, (![U_906, V_231]: (~ssPv2(U_906) | ~ssPv8(V_231) | ~ssRr(U_906, V_231) | ssPv3(skf1(U_906)) | ssPv3(U_906) | ~ssPv2(skf1(U_906)) | ~ssPv5(U_906) | ssPv1(U_906) | ssPv1(skf1(U_906))))). % 23.39/13.96 tff(c_29034, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_28919, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv3(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_28556, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv3(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_28533, plain, (![V_383, U_1101]: (~ssPv4(V_383) | ~ssRr(U_1101, V_383) | ssPv1(U_1101) | ~ssPv2(U_1101) | ssPv3(U_1101) | ssPv5(U_1101) | ssPv1(skf1(U_1101)) | ~ssPv2(skf1(U_1101))))). % 23.39/13.96 tff(c_28514, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.96 tff(c_28436, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.96 tff(c_28060, plain, (![U_1090, V_459]: (~ssPv8(U_1090) | ~ssPv8(V_459) | ~ssRr(U_1090, V_459) | ssPv1(U_1090) | ~ssPv2(skf1(U_1090)) | ssPv1(skf1(U_1090)) | ssPv3(U_1090) | ssPv6(U_1090) | ~ssPv2(U_1090)))). % 23.39/13.96 tff(c_28043, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_28066, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.96 tff(c_28062, plain, (![V_383, U_1090]: (~ssPv4(V_383) | ~ssRr(U_1090, V_383) | ssPv1(U_1090) | ~ssPv2(skf1(U_1090)) | ssPv1(skf1(U_1090)) | ssPv3(U_1090) | ssPv6(U_1090) | ~ssPv2(U_1090)))). % 23.39/13.96 tff(c_28036, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.96 tff(c_6472, plain, (![U_685, V_222]: (ssPv6(U_685) | ssPv3(U_685) | ~ssPv8(V_222) | ~ssRr(U_685, V_222) | ssPv2(skf1(U_685)) | ~ssPv7(U_685) | ~ssPv4(U_685) | ~ssPv4(skf1(U_685)) | ssPv3(skf1(U_685)) | ssPv1(skf1(U_685))))). % 23.39/13.96 tff(c_27918, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv6(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_27555, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv6(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_27532, plain, (![V_383, U_1076]: (~ssPv4(V_383) | ~ssRr(U_1076, V_383) | ssPv1(U_1076) | ~ssPv2(U_1076) | ~ssPv6(U_1076) | ssPv5(U_1076) | ssPv1(skf1(U_1076)) | ~ssPv2(skf1(U_1076))))). % 23.39/13.96 tff(c_27506, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv6(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_8372, plain, (![U_730]: (ssPv3(U_730) | ssPv2(U_730) | ssPv1(U_730) | ~ssPv1(skf1(U_730)) | ssPv3(skf1(U_730)) | ssPv4(skf1(U_730)) | ~ssPv7(U_730) | ~ssPv6(U_730) | ~ssPv2(skf1(U_730))))). % 23.39/13.96 tff(c_27375, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_3479, plain, (![U_585, V_231]: (ssPv1(U_585) | ~ssPv2(U_585) | ~ssPv8(V_231) | ~ssRr(U_585, V_231) | ssPv1(skf1(U_585)) | ssPv3(skf1(U_585)) | ~ssPv7(U_585) | ~ssPv6(U_585) | ~ssPv2(skf1(U_585))))). % 23.39/13.96 tff(c_27346, plain, (![U_974]: (~ssPv2(U_974) | ssPv6(U_974) | ssPv1(skf1(U_974)) | ssPv5(U_974) | ssPv3(U_974) | ssPv1(U_974)))). % 23.39/13.96 tff(c_27177, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv4(skf1(U_1)) | ssPv1(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_11774, plain, (![U_1]: (ssPv5(U_1) | ssPv4(U_1) | ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.96 tff(c_7315, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.96 tff(c_7647, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.96 tff(c_4588, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.96 tff(c_25893, plain, (![U_1]: (~ssPv8(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.96 tff(c_26680, plain, (![U_1]: (~ssPv1(U_1) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/13.96 tff(c_26222, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_26216, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/13.96 tff(c_3917, plain, (![U_605, V_222]: (ssPv6(U_605) | ssPv3(U_605) | ~ssPv8(V_222) | ~ssRr(U_605, V_222) | ssPv2(skf1(U_605)) | ssPv4(skf1(U_605)) | ~ssPv7(U_605) | ~ssPv4(U_605) | ssPv1(U_605) | ssPv1(skf1(U_605))))). % 23.39/13.96 tff(c_25860, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.96 tff(c_25813, plain, (![U_1033, V_459]: (~ssPv8(U_1033) | ~ssPv8(V_459) | ~ssRr(U_1033, V_459) | ssPv6(U_1033) | ssPv3(U_1033) | ssPv2(skf1(U_1033)) | ssPv1(U_1033) | ssPv1(skf1(U_1033)) | ~ssPv7(U_1033)))). % 23.39/13.96 tff(c_25795, plain, (![U_1032]: (ssPv6(U_1032) | ssPv3(U_1032) | ssPv2(skf1(U_1032)) | ssPv1(U_1032) | ssPv1(skf1(U_1032)) | ssPv3(skf1(U_1032)) | ~ssPv7(U_1032)))). % 23.39/13.96 tff(c_25699, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_3065, plain, (![U_570, V_222]: (ssPv6(U_570) | ssPv3(U_570) | ~ssPv8(V_222) | ~ssRr(U_570, V_222) | ssPv4(skf1(U_570)) | ssPv2(skf1(U_570)) | ssPv3(skf1(U_570)) | ssPv1(U_570) | ssPv1(skf1(U_570))))). % 23.39/13.96 tff(c_25652, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.96 tff(c_24974, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.96 tff(c_24925, plain, (![U_1]: (~ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_24456, plain, (![U_1]: (~ssPv8(U_1) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.96 tff(c_24417, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.96 tff(c_2574, plain, (![U_543, V_222]: (ssPv6(U_543) | ssPv3(U_543) | ~ssPv8(V_222) | ~ssRr(U_543, V_222) | ssPv4(skf1(U_543)) | ssPv2(skf1(U_543)) | ssPv3(skf1(U_543)) | ssPv8(U_543) | ssPv5(U_543) | ssPv1(skf1(U_543))))). % 23.39/13.97 tff(c_24309, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.97 tff(c_4158, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.97 tff(c_24095, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_23761, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.97 tff(c_23233, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.97 tff(c_2958, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_22906, plain, (![U_981, V_459]: (~ssPv8(U_981) | ~ssPv8(V_459) | ~ssRr(U_981, V_459) | ssPv3(U_981) | ssPv2(skf1(U_981)) | ssPv1(U_981) | ssPv1(skf1(U_981)) | ssPv6(U_981) | ~ssPv2(U_981)))). % 23.39/13.97 tff(c_22912, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.97 tff(c_22908, plain, (![V_383, U_981]: (~ssPv4(V_383) | ~ssRr(U_981, V_383) | ssPv3(U_981) | ssPv2(skf1(U_981)) | ssPv1(U_981) | ssPv1(skf1(U_981)) | ssPv6(U_981) | ~ssPv2(U_981)))). % 23.39/13.97 tff(c_22886, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.97 tff(c_1611, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_22641, plain, (![U_1]: (ssPv6(U_1) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.97 tff(c_722, plain, (![U_325]: (ssPv3(skf1(U_325)) | ssPv1(skf1(U_325)) | ssPv2(skf1(U_325)) | ~ssPv7(skf1(U_325)) | ~ssPv4(skf1(U_325)) | ssPv4(U_325) | ~ssPv6(U_325) | ~ssPv6(skf1(U_325))))). % 23.39/13.97 tff(c_9758, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.97 tff(c_21237, plain, (![U_950]: (ssPv2(U_950) | ssPv7(U_950) | ~ssPv1(U_950) | ssPv4(skf1(U_950)) | ssPv2(skf1(U_950)) | ssPv3(skf1(U_950)) | ssPv1(skf1(U_950)) | ssPv5(U_950) | ~ssPv6(U_950)))). % 23.39/13.97 tff(c_21674, plain, (![U_958]: (~ssPv2(U_958) | ssPv2(skf1(U_958)) | ssPv3(skf1(U_958)) | ssPv1(skf1(U_958)) | ssPv5(skf1(U_958)) | ~ssPv7(U_958) | ~ssPv4(U_958) | ssPv5(U_958) | ~ssPv6(U_958)))). % 23.39/13.97 tff(c_13852, plain, (![U_830]: (ssPv8(U_830) | ~ssPv5(U_830) | ssPv2(skf1(U_830)) | ssPv7(U_830) | ssPv6(U_830) | ~ssPv1(U_830) | ~ssPv4(skf1(U_830)) | ssPv3(skf1(U_830)) | ssPv1(skf1(U_830))))). % 23.39/13.97 tff(c_21715, plain, (![U_1]: (~ssPv8(U_1) | ssPv6(U_1) | ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.97 tff(c_2775, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_21504, plain, (![U_1]: (ssPv6(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.97 tff(c_8658, plain, (![U_734]: (ssPv5(skf1(U_734)) | ~ssPv2(U_734) | ssPv2(skf1(U_734)) | ssPv4(skf1(U_734)) | ssPv4(U_734) | ssPv1(skf1(U_734)) | ~ssPv1(U_734) | ssPv5(U_734) | ~ssPv6(U_734)))). % 23.39/13.97 tff(c_9494, plain, (![U_1]: (~ssPv8(U_1) | ssPv3(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_4458, plain, (![U_623]: (ssPv7(U_623) | ~ssPv1(U_623) | ssPv4(skf1(U_623)) | ssPv2(skf1(U_623)) | ssPv5(skf1(U_623)) | ssPv3(skf1(U_623)) | ssPv1(skf1(U_623)) | ssPv5(U_623) | ~ssPv6(U_623)))). % 23.39/13.97 tff(c_21140, plain, (![U_1]: (~ssPv8(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_20533, plain, (![U_1]: (ssPv3(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/13.97 tff(c_20463, plain, (![U_1]: (ssPv3(U_1) | ~ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/13.97 tff(c_19946, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv3(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.97 tff(c_9458, plain, (![V_383, U_752]: (~ssPv4(V_383) | ~ssRr(U_752, V_383) | ~ssPv7(U_752) | ssPv3(U_752) | ssPv5(U_752) | ssPv1(skf1(U_752)) | ~ssPv2(skf1(U_752)) | ssPv4(U_752) | ~ssPv2(U_752)))). % 23.39/13.97 tff(c_19829, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_19775, plain, (![U_923, V_242]: (~ssPv3(U_923) | ~ssPv6(V_242) | ~ssRr(U_923, V_242) | ~ssPv2(U_923) | ssPv4(U_923) | ~ssPv1(U_923) | ssPv8(U_923) | ssPv5(U_923) | ssPv1(skf1(U_923))))). % 23.39/13.97 tff(c_19810, plain, (![U_1]: (ssPv3(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.97 tff(c_19717, plain, (![U_1]: (~ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv4(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_19331, plain, (![U_917]: (ssPv2(U_917) | ssPv4(skf1(U_917)) | ssPv5(U_917) | ssPv1(skf1(U_917)) | ~ssPv2(skf1(U_917)) | ssPv7(U_917) | ~ssPv1(U_917) | ~ssPv3(skf1(U_917))))). % 23.39/13.97 tff(c_19321, plain, (![U_917]: (ssPv3(U_917) | ssPv4(skf1(U_917)) | ssPv5(U_917) | ssPv1(skf1(U_917)) | ~ssPv2(skf1(U_917)) | ssPv7(U_917) | ~ssPv1(U_917) | ~ssPv3(skf1(U_917))))). % 23.39/13.97 tff(c_5881, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.97 tff(c_2266, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_19044, plain, (![U_913]: (ssPv2(U_913) | ~ssPv2(skf1(U_913)) | ssPv4(skf1(U_913)) | ssPv4(U_913) | ssPv1(skf1(U_913)) | ssPv7(U_913) | ~ssPv1(U_913) | ~ssPv3(skf1(U_913))))). % 23.39/13.97 tff(c_19033, plain, (![U_913]: (ssPv3(U_913) | ~ssPv2(skf1(U_913)) | ssPv4(skf1(U_913)) | ssPv4(U_913) | ssPv1(skf1(U_913)) | ssPv7(U_913) | ~ssPv1(U_913) | ~ssPv3(skf1(U_913))))). % 23.39/13.97 tff(c_5820, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.97 tff(c_18944, plain, (![U_911]: (ssPv2(U_911) | ~ssPv2(skf1(U_911)) | ssPv1(skf1(U_911)) | ssPv4(skf1(U_911)) | ssPv6(U_911) | ssPv7(U_911) | ~ssPv1(U_911) | ~ssPv3(skf1(U_911))))). % 23.39/13.97 tff(c_5708, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.97 tff(c_2774, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_18457, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv4(skf1(U_1)) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv7(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_5126, plain, (![U_641, V_383]: (~ssPv2(U_641) | ~ssPv4(V_383) | ~ssRr(U_641, V_383) | ssPv1(U_641) | ssPv2(skf1(U_641)) | ~ssPv7(U_641) | ssPv8(U_641) | ssPv5(U_641) | ssPv1(skf1(U_641))))). % 23.39/13.97 tff(c_18409, plain, (![U_372]: (ssPv3(skf1(U_372)) | ssPv4(skf1(U_372)) | ssPv3(U_372) | ~ssPv2(skf1(U_372)) | ~ssPv5(U_372) | ssPv1(U_372) | ssPv1(skf1(U_372))))). % 23.39/13.97 tff(c_11040, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv2(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.97 tff(c_17875, plain, (![U_1]: (~ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.97 tff(c_2265, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_17868, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.97 tff(c_17754, plain, (![U_1]: (~ssPv6(U_1) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.97 tff(c_17753, plain, (![U_895]: (ssPv4(U_895) | ~ssPv6(U_895) | ssPv3(U_895) | ssPv4(skf1(U_895)) | ~ssPv2(skf1(U_895)) | ssPv3(skf1(U_895)) | ssPv1(skf1(U_895))))). % 23.39/13.97 tff(c_17461, plain, (![U_1]: (~ssPv1(U_1) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.97 tff(c_17460, plain, (![U_892]: (ssPv4(U_892) | ~ssPv1(U_892) | ssPv3(U_892) | ssPv4(skf1(U_892)) | ~ssPv2(skf1(U_892)) | ssPv3(skf1(U_892)) | ssPv1(skf1(U_892))))). % 23.39/13.97 tff(c_14859, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_4153, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_11489, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(U_1) | ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.97 tff(c_16971, plain, (![U_887]: (~ssPv2(U_887) | ~ssPv1(skf1(U_887)) | ssPv5(skf1(U_887)) | ssPv3(skf1(U_887)) | ssPv4(skf1(U_887)) | ~ssPv7(U_887) | ssPv5(U_887) | ~ssPv6(U_887)))). % 23.39/13.97 tff(c_3344, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_16795, plain, (![U_885]: (ssPv2(U_885) | ~ssPv2(skf1(U_885)) | ssPv4(skf1(U_885)) | ssPv4(U_885) | ssPv1(skf1(U_885)) | ssPv7(U_885) | ssPv1(U_885) | ~ssPv6(U_885)))). % 23.39/13.97 tff(c_16740, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_7637, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.97 tff(c_3343, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_16434, plain, (![U_880]: (~ssPv2(skf1(U_880)) | ssPv1(skf1(U_880)) | ssPv4(skf1(U_880)) | ssPv3(skf1(U_880)) | ~ssPv2(U_880) | ssPv6(U_880) | ssPv3(U_880)))). % 23.39/13.97 tff(c_15050, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_7585, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_16040, plain, (![U_875]: (ssPv8(U_875) | ssPv2(skf1(U_875)) | ssPv3(skf1(U_875)) | ssPv1(skf1(U_875)) | ~ssPv7(U_875) | ~ssPv4(U_875) | ssPv2(U_875) | ~ssPv5(U_875) | ~ssPv3(U_875)))). % 23.39/13.97 tff(c_2783, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.97 tff(c_15950, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_455, plain, (![U_1, V_222]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(V_222) | ~ssRr(U_1, V_222) | ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_10922, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.97 tff(c_15096, plain, (![U_847]: (ssPv3(skf1(U_847)) | ssPv2(skf1(U_847)) | ssPv4(U_847) | ssPv8(U_847) | ssPv5(U_847) | ssPv1(skf1(U_847)) | ssPv7(U_847) | ssPv1(U_847) | ~ssPv6(U_847)))). % 23.39/13.97 tff(c_5178, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.97 tff(c_7439, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_7232, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_15484, plain, (![U_1]: (ssPv5(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_15362, plain, (![U_1]: (ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_15358, plain, (![U_1, V_859]: (ssPv5(U_1) | ~ssPv8(V_859) | ~ssRr(U_1, V_859) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_15294, plain, (![U_1, V_857]: (ssPv5(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv8(V_857) | ~ssRr(U_1, V_857) | ssPv1(U_1) | ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 23.39/13.97 tff(c_1862, plain, (![U_512, W_478, V_479]: (ssPv5(U_512) | ~ssPv6(W_478) | ~ssRr(U_512, W_478) | ~ssPv8(V_479) | ~ssRr(U_512, V_479) | ssPv1(U_512) | ssPv7(U_512) | ~ssPv3(U_512) | ~ssPv1(skf1(U_512))))). % 23.39/13.97 tff(c_15220, plain, (![U_852]: (~ssPv2(U_852) | ssPv8(U_852) | ssPv1(skf1(U_852)) | ssPv5(U_852) | ssPv3(U_852) | ssPv1(U_852)))). % 23.39/13.97 tff(c_667, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.97 tff(c_7709, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_1614, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.97 tff(c_4159, plain, (![U_613]: (ssPv2(skf1(U_613)) | ssPv4(U_613) | ~ssPv6(U_613) | ~ssPv6(skf1(U_613)) | ~ssPv4(skf1(U_613)) | ssPv5(skf1(U_613)) | ssPv3(skf1(U_613)) | ssPv1(skf1(U_613))))). % 23.39/13.97 tff(c_1616, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.97 tff(c_666, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.97 tff(c_14772, plain, (![U_841]: (ssPv2(U_841) | ssPv2(skf1(U_841)) | ssPv4(skf1(U_841)) | ssPv4(U_841) | ssPv1(skf1(U_841)) | ssPv7(U_841) | ~ssPv1(U_841) | ~ssPv3(skf1(U_841))))). % 23.39/13.97 tff(c_9761, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_14505, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.97 tff(c_2431, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.97 tff(c_4148, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.97 tff(c_12967, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.39/13.98 tff(c_2268, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.98 tff(c_7766, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_5819, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_3459, plain, (![U_584]: (ssPv2(skf1(U_584)) | ssPv7(U_584) | ssPv6(U_584) | ~ssPv1(U_584) | ~ssPv4(skf1(U_584)) | ssPv5(skf1(U_584)) | ssPv3(skf1(U_584)) | ssPv1(skf1(U_584))))). % 23.39/13.98 tff(c_5880, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_8369, plain, (![U_730]: (ssPv8(U_730) | ~ssPv5(U_730) | ~ssPv1(skf1(U_730)) | ssPv3(skf1(U_730)) | ssPv4(skf1(U_730)) | ~ssPv7(U_730) | ~ssPv6(U_730) | ~ssPv2(skf1(U_730))))). % 23.39/13.98 tff(c_8840, plain, (![U_1]: (~ssPv5(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.98 tff(c_9059, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.98 tff(c_13465, plain, (![U_824]: (ssPv2(U_824) | ssPv2(skf1(U_824)) | ssPv4(skf1(U_824)) | ssPv4(U_824) | ssPv1(skf1(U_824)) | ssPv7(U_824) | ssPv1(U_824) | ~ssPv6(U_824)))). % 23.39/13.98 tff(c_13422, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.98 tff(c_1962, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_12046, plain, (![U_799]: (ssPv3(skf1(U_799)) | ~ssPv2(skf1(U_799)) | ssPv4(skf1(U_799)) | ssPv4(U_799) | ssPv1(skf1(U_799)) | ~ssPv1(U_799) | ssPv6(U_799) | ssPv3(U_799)))). % 23.39/13.98 tff(c_4587, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_5176, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_4258, plain, (![U_617]: (ssPv5(skf1(U_617)) | ~ssPv2(U_617) | ssPv2(skf1(U_617)) | ssPv3(skf1(U_617)) | ssPv4(skf1(U_617)) | ~ssPv7(U_617) | ssPv5(U_617) | ~ssPv6(U_617)))). % 23.39/13.98 tff(c_4468, plain, (![U_623]: (~ssPv2(U_623) | ssPv4(skf1(U_623)) | ssPv2(skf1(U_623)) | ssPv5(skf1(U_623)) | ssPv3(skf1(U_623)) | ssPv1(skf1(U_623)) | ssPv5(U_623) | ~ssPv6(U_623)))). % 23.39/13.98 tff(c_12932, plain, (![U_1]: (~ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_12746, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_12742, plain, (![V_383, U_808]: (~ssPv4(V_383) | ~ssRr(U_808, V_383) | ssPv2(skf1(U_808)) | ssPv6(U_808) | ~ssPv2(U_808) | ssPv8(U_808) | ssPv5(U_808) | ssPv1(skf1(U_808))))). % 23.39/13.98 tff(c_12685, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_2968, plain, (![U_565]: (ssPv2(skf1(U_565)) | ssPv4(U_565) | ~ssPv8(U_565) | ~ssPv7(U_565) | ~ssPv4(skf1(U_565)) | ssPv5(skf1(U_565)) | ssPv3(skf1(U_565)) | ssPv1(skf1(U_565))))). % 23.39/13.98 tff(c_12415, plain, (![U_804]: (ssPv8(U_804) | ~ssPv1(skf1(U_804)) | ssPv3(skf1(U_804)) | ssPv4(skf1(U_804)) | ~ssPv7(U_804) | ssPv2(U_804) | ~ssPv5(U_804) | ~ssPv3(U_804)))). % 23.39/13.98 tff(c_3352, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.98 tff(c_2548, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_12303, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_3405, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.98 tff(c_2546, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.98 tff(c_5918, plain, (![U_1]: (ssPv4(U_1) | ~ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.98 tff(c_3452, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.98 tff(c_11805, plain, (![U_1]: (ssPv5(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_6438, plain, (![U_1]: (ssPv5(U_1) | ssPv4(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.98 tff(c_11595, plain, (![U_793]: (~ssPv2(skf1(U_793)) | ssPv1(skf1(U_793)) | ssPv4(skf1(U_793)) | ssPv7(U_793) | ~ssPv1(U_793) | ssPv6(U_793) | ssPv3(U_793)))). % 23.39/13.98 tff(c_11070, plain, (![U_789]: (ssPv3(skf1(U_789)) | ssPv2(skf1(U_789)) | ssPv4(U_789) | ssPv2(U_789) | ~ssPv5(U_789) | ~ssPv3(U_789) | ssPv7(U_789) | ssPv1(U_789) | ~ssPv6(U_789)))). % 23.39/13.98 tff(c_6845, plain, (![U_690]: (ssPv8(U_690) | ~ssPv5(U_690) | ssPv2(skf1(U_690)) | ssPv4(U_690) | ~ssPv1(U_690) | ~ssPv4(skf1(U_690)) | ssPv3(skf1(U_690)) | ssPv1(skf1(U_690))))). % 23.39/13.98 tff(c_6244, plain, (![U_674]: (ssPv8(U_674) | ~ssPv5(U_674) | ssPv2(skf1(U_674)) | ssPv6(U_674) | ~ssPv2(U_674) | ~ssPv4(skf1(U_674)) | ssPv3(skf1(U_674)) | ssPv1(skf1(U_674))))). % 23.39/13.98 tff(c_5611, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.98 tff(c_10966, plain, (![U_1]: (~ssPv1(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_2465, plain, (![U_538, V_242]: (~ssPv1(U_538) | ~ssPv6(V_242) | ~ssRr(U_538, V_242) | ~ssPv3(U_538) | ~ssPv1(skf1(U_538)) | ssPv8(U_538) | ~ssPv5(U_538) | ssPv4(U_538) | ~ssPv2(U_538)))). % 23.39/13.98 tff(c_10650, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv5(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_6471, plain, (![U_685]: (ssPv8(U_685) | ~ssPv5(U_685) | ssPv2(skf1(U_685)) | ~ssPv7(U_685) | ~ssPv4(U_685) | ~ssPv4(skf1(U_685)) | ssPv3(skf1(U_685)) | ssPv1(skf1(U_685))))). % 23.39/13.98 tff(c_10692, plain, (![U_782]: (ssPv2(U_782) | ssPv2(skf1(U_782)) | ssPv4(skf1(U_782)) | ssPv4(U_782) | ~ssPv6(U_782) | ssPv7(U_782) | ~ssPv1(U_782) | ~ssPv3(skf1(U_782))))). % 23.39/13.98 tff(c_3233, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_1970, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_2130, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.98 tff(c_2778, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_2137, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_3146, plain, (![U_574]: (ssPv7(U_574) | ssPv4(skf1(U_574)) | ssPv2(skf1(U_574)) | ssPv3(skf1(U_574)) | ssPv1(skf1(U_574)) | ssPv2(U_574) | ~ssPv5(U_574) | ~ssPv3(U_574)))). % 23.39/13.98 tff(c_2575, plain, (![U_543]: (ssPv7(U_543) | ssPv2(U_543) | ssPv4(skf1(U_543)) | ssPv2(skf1(U_543)) | ssPv3(skf1(U_543)) | ssPv8(U_543) | ssPv5(U_543) | ssPv1(skf1(U_543))))). % 23.39/13.98 tff(c_3144, plain, (![U_574]: (ssPv8(U_574) | ssPv4(skf1(U_574)) | ssPv2(skf1(U_574)) | ssPv3(skf1(U_574)) | ssPv1(skf1(U_574)) | ssPv2(U_574) | ~ssPv5(U_574) | ~ssPv3(U_574)))). % 23.39/13.98 tff(c_10212, plain, (![U_771]: (~ssPv2(U_771) | ssPv2(skf1(U_771)) | ssPv4(skf1(U_771)) | ssPv5(skf1(U_771)) | ~ssPv7(U_771) | ~ssPv4(U_771) | ssPv5(U_771) | ~ssPv6(U_771)))). % 23.39/13.98 tff(c_2131, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.98 tff(c_10086, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_9893, plain, (![U_764]: (~ssPv7(U_764) | ssPv3(U_764) | ssPv4(skf1(U_764)) | ~ssPv2(skf1(U_764)) | ssPv3(skf1(U_764)) | ssPv1(skf1(U_764))))). % 23.39/13.98 tff(c_1965, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_2642, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.98 tff(c_9563, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.98 tff(c_9499, plain, (![U_1]: (~ssPv8(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.98 tff(c_9462, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_4168, plain, (![U_614, V_459]: (~ssPv8(U_614) | ~ssPv8(V_459) | ~ssRr(U_614, V_459) | ssPv3(U_614) | ssPv2(U_614) | ssPv2(skf1(U_614)) | ssPv1(U_614) | ssPv1(skf1(U_614))))). % 23.39/13.98 tff(c_6789, plain, (![U_1]: (~ssPv7(U_1) | ssPv3(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_2024, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.98 tff(c_9326, plain, (![U_749]: (ssPv5(U_749) | ssPv3(U_749) | ssPv4(skf1(U_749)) | ~ssPv2(skf1(U_749)) | ssPv3(skf1(U_749)) | ssPv1(skf1(U_749))))). % 23.39/13.98 tff(c_7356, plain, (![U_706]: (ssPv3(U_706) | ssPv2(U_706) | ~ssPv2(skf1(U_706)) | ssPv4(skf1(U_706)) | ~ssPv7(U_706) | ~ssPv4(U_706) | ssPv1(U_706) | ssPv1(skf1(U_706))))). % 23.39/13.98 tff(c_9103, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_4728, plain, (![U_629, V_459]: (~ssPv8(U_629) | ~ssPv8(V_459) | ~ssRr(U_629, V_459) | ssPv7(U_629) | ssPv2(U_629) | ssPv2(skf1(U_629)) | ssPv1(U_629) | ssPv1(skf1(U_629))))). % 23.39/13.98 tff(c_2134, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_7636, plain, (![U_712]: (ssPv4(U_712) | ~ssPv6(U_712) | ssPv3(skf1(U_712)) | ~ssPv2(skf1(U_712)) | ssPv4(skf1(U_712)) | ssPv1(skf1(U_712)) | ~ssPv6(skf1(U_712))))). % 23.39/13.98 tff(c_2544, plain, (![U_542]: (ssPv4(U_542) | ~ssPv1(U_542) | ssPv3(skf1(U_542)) | ~ssPv2(skf1(U_542)) | ssPv4(skf1(U_542)) | ssPv1(skf1(U_542)) | ~ssPv6(skf1(U_542))))). % 23.39/13.98 tff(c_7530, plain, (![U_710]: (ssPv6(U_710) | ~ssPv2(U_710) | ssPv3(skf1(U_710)) | ~ssPv2(skf1(U_710)) | ssPv4(skf1(U_710)) | ssPv1(skf1(U_710)) | ~ssPv6(skf1(U_710))))). % 23.39/13.98 tff(c_8647, plain, (![U_734]: (ssPv7(U_734) | ssPv2(skf1(U_734)) | ssPv4(skf1(U_734)) | ssPv4(U_734) | ssPv1(skf1(U_734)) | ~ssPv1(U_734) | ssPv5(U_734) | ~ssPv6(U_734)))). % 23.39/13.98 tff(c_1833, plain, (![U_1]: (ssPv1(U_1) | ~ssPv5(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 23.39/13.98 tff(c_8722, plain, (![U_1]: (~ssPv1(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(U_1) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/13.98 tff(c_8586, plain, (![U_1]: (ssPv5(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_2025, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.98 tff(c_8453, plain, (![U_1]: (ssPv5(U_1) | ~ssPv7(U_1) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_2555, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.98 tff(c_3348, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.98 tff(c_8162, plain, (![U_1]: (ssPv5(U_1) | ~ssPv7(U_1) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_6871, plain, (![U_691]: (ssPv3(skf1(U_691)) | ssPv3(U_691) | ssPv2(U_691) | ssPv2(skf1(U_691)) | ~ssPv7(U_691) | ~ssPv4(U_691) | ssPv1(U_691) | ssPv1(skf1(U_691))))). % 23.39/13.98 tff(c_2132, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_8014, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_7839, plain, (![U_718]: (~ssPv5(U_718) | ~ssPv6(U_718) | ssPv1(skf1(U_718)) | ssPv1(U_718) | ssPv4(U_718) | ~ssPv8(U_718) | ~ssPv7(U_718)))). % 23.39/13.98 tff(c_7810, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.98 tff(c_7643, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.98 tff(c_1967, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.98 tff(c_724, plain, (![U_325]: (~ssPv2(skf1(U_325)) | ssPv1(skf1(U_325)) | ssPv4(skf1(U_325)) | ~ssPv7(skf1(U_325)) | ssPv4(U_325) | ~ssPv6(U_325) | ~ssPv6(skf1(U_325))))). % 23.39/13.98 tff(c_665, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_547, plain, (![U_282]: (~ssPv2(skf1(U_282)) | ssPv1(skf1(U_282)) | ssPv4(skf1(U_282)) | ~ssPv7(skf1(U_282)) | ssPv6(U_282) | ssPv3(skf1(U_282)) | ~ssPv2(U_282)))). % 23.39/13.98 tff(c_3175, plain, (![U_575]: (ssPv5(skf1(U_575)) | ~ssPv2(U_575) | ssPv2(skf1(U_575)) | ssPv4(skf1(U_575)) | ssPv3(U_575) | ssPv1(U_575) | ssPv5(U_575) | ~ssPv6(U_575)))). % 23.39/13.98 tff(c_1613, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_7311, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.98 tff(c_7305, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.98 tff(c_616, plain, (![U_305]: (~ssPv2(skf1(U_305)) | ssPv1(skf1(U_305)) | ssPv4(skf1(U_305)) | ~ssPv7(skf1(U_305)) | ssPv5(skf1(U_305)) | ~ssPv7(U_305) | ~ssPv4(U_305)))). % 23.39/13.98 tff(c_2026, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.98 tff(c_874, plain, (![U_355]: (ssPv3(skf1(U_355)) | ssPv2(skf1(U_355)) | ~ssPv7(skf1(U_355)) | ~ssPv4(skf1(U_355)) | ssPv4(U_355) | ssPv1(skf1(U_355)) | ~ssPv1(U_355)))). % 23.39/13.98 tff(c_7119, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv8(skf1(U_1)) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/13.98 tff(c_1408, plain, (![U_482, V_459]: (ssPv1(skf1(U_482)) | ~ssPv8(V_459) | ~ssRr(U_482, V_459) | ssPv1(U_482) | ssPv2(skf1(U_482)) | ssPv6(U_482) | ~ssPv8(U_482) | ~ssPv5(U_482)))). % 23.39/13.98 tff(c_7089, plain, (![U_696]: (~ssPv5(U_696) | ~ssPv6(U_696) | ssPv1(skf1(U_696)) | ~ssPv2(U_696) | ssPv4(U_696) | ssPv1(U_696) | ~ssPv7(U_696)))). % 23.39/13.98 tff(c_7058, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.39/13.98 tff(c_3919, plain, (![U_605]: (ssPv3(U_605) | ssPv2(U_605) | ssPv2(skf1(U_605)) | ssPv4(skf1(U_605)) | ~ssPv7(U_605) | ~ssPv4(U_605) | ssPv1(U_605) | ssPv1(skf1(U_605))))). % 23.39/13.98 tff(c_2275, plain, (![U_527]: (ssPv2(skf1(U_527)) | ssPv4(U_527) | ~ssPv1(U_527) | ~ssPv4(skf1(U_527)) | ssPv5(skf1(U_527)) | ssPv3(skf1(U_527)) | ssPv1(skf1(U_527))))). % 23.39/13.98 tff(c_6579, plain, (![U_1]: (ssPv5(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.98 tff(c_6439, plain, (![U_1]: (ssPv4(U_1) | ~ssPv7(U_1) | ssPv3(U_1) | ~ssPv5(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.98 tff(c_6446, plain, (![U_1]: (ssPv4(U_1) | ~ssPv7(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/13.98 tff(c_6445, plain, (![U_1]: (ssPv5(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.98 tff(c_2784, plain, (![U_554]: (ssPv2(skf1(U_554)) | ~ssPv7(U_554) | ~ssPv4(U_554) | ~ssPv4(skf1(U_554)) | ssPv5(skf1(U_554)) | ssPv3(skf1(U_554)) | ssPv1(skf1(U_554))))). % 23.39/13.98 tff(c_6409, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_1731, plain, (![V_507, U_1]: (~ssPv8(V_507) | ~ssRr(U_1, V_507) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_1663, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_1709, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_1707, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_2139, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.99 tff(c_2033, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.99 tff(c_2836, plain, (![U_1]: (ssPv3(U_1) | ssPv4(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_2441, plain, (![U_535]: (ssPv2(skf1(U_535)) | ssPv6(U_535) | ~ssPv2(U_535) | ~ssPv4(skf1(U_535)) | ssPv5(skf1(U_535)) | ssPv3(skf1(U_535)) | ssPv1(skf1(U_535))))). % 23.39/13.99 tff(c_5745, plain, (![U_1]: (~ssPv8(U_1) | ssPv3(U_1) | ssPv4(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.39/13.99 tff(c_6053, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv3(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2979, plain, (![V_383, U_566]: (~ssPv4(V_383) | ~ssRr(U_566, V_383) | ssPv3(U_566) | ~ssPv5(U_566) | ssPv1(U_566) | ssPv1(skf1(U_566)) | ssPv6(U_566) | ~ssPv2(U_566)))). % 23.39/13.99 tff(c_5879, plain, (![U_1]: (ssPv7(U_1) | ~ssPv1(U_1) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1)))). % 23.39/13.99 tff(c_2895, plain, (![U_563]: (ssPv5(skf1(U_563)) | ~ssPv2(U_563) | ssPv4(skf1(U_563)) | ssPv1(skf1(U_563)) | ~ssPv2(skf1(U_563)) | ssPv5(U_563) | ~ssPv6(U_563)))). % 23.39/13.99 tff(c_5919, plain, (![U_1]: (ssPv5(U_1) | ~ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/13.99 tff(c_5924, plain, (![U_1]: (ssPv5(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_5888, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_1732, plain, (![V_507, U_1]: (~ssPv8(V_507) | ~ssRr(U_1, V_507) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_1083, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_2549, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_5751, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_5715, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv4(U_1) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2284, plain, (![U_528, V_459]: (ssPv1(skf1(U_528)) | ~ssPv8(U_528) | ~ssPv8(V_459) | ~ssRr(U_528, V_459) | ssPv3(U_528) | ssPv4(U_528) | ssPv6(U_528) | ~ssPv2(U_528)))). % 23.39/13.99 tff(c_5172, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_4973, plain, (![U_1]: (ssPv1(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_1082, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_1972, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.99 tff(c_457, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv1(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_1080, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_2553, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_5250, plain, (![U_644]: (~ssPv2(skf1(U_644)) | ssPv3(U_644) | ssPv5(U_644) | ~ssPv7(U_644) | ssPv4(U_644) | ~ssPv6(U_644) | ~ssPv1(U_644) | ~ssPv3(skf1(U_644))))). % 23.39/13.99 tff(c_5312, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/13.99 tff(c_1656, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_381, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.99 tff(c_5110, plain, (![U_640]: (ssPv1(U_640) | ssPv2(skf1(U_640)) | ssPv3(skf1(U_640)) | ~ssPv7(U_640) | ssPv8(U_640) | ssPv5(U_640) | ssPv1(skf1(U_640))))). % 23.39/13.99 tff(c_1301, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_5089, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv1(U_1) | ssPv6(U_1) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_1158, plain, (![U_426]: (~ssPv2(U_426) | ssPv1(U_426) | ~ssPv7(U_426) | ssPv4(U_426) | ~ssPv6(U_426) | ssPv3(U_426) | ~ssPv2(skf1(U_426)) | ~ssPv5(skf1(U_426))))). % 23.39/13.99 tff(c_4844, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv6(U_1) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_841, plain, (![U_352]: (ssPv4(skf1(U_352)) | ssPv2(skf1(U_352)) | ssPv5(skf1(U_352)) | ssPv3(skf1(U_352)) | ssPv1(skf1(U_352)) | ssPv6(U_352) | ssPv3(U_352) | ssPv6(skf1(U_352))))). % 23.39/13.99 tff(c_4714, plain, (![U_628]: (ssPv7(U_628) | ssPv2(U_628) | ssPv2(skf1(U_628)) | ssPv3(skf1(U_628)) | ssPv1(U_628) | ssPv1(skf1(U_628))))). % 23.39/13.99 tff(c_4593, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.99 tff(c_382, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_2325, plain, (![U_419]: (ssPv3(U_419) | ~ssPv2(skf1(U_419)) | ssPv2(U_419) | ~ssPv7(U_419) | ssPv4(U_419) | ~ssPv6(U_419) | ~ssPv1(U_419) | ~ssPv3(skf1(U_419))))). % 23.39/13.99 tff(c_811, plain, (![U_342]: (ssPv4(skf1(U_342)) | ssPv2(skf1(U_342)) | ssPv5(skf1(U_342)) | ssPv3(skf1(U_342)) | ssPv1(skf1(U_342)) | ssPv5(U_342) | ssPv6(skf1(U_342)) | ~ssPv6(U_342)))). % 23.39/13.99 tff(c_1297, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_4369, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/13.99 tff(c_1298, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.99 tff(c_4189, plain, (![U_615]: (ssPv2(U_615) | ssPv2(skf1(U_615)) | ssPv4(skf1(U_615)) | ssPv6(U_615) | ssPv7(U_615) | ~ssPv1(U_615) | ~ssPv3(skf1(U_615))))). % 23.39/13.99 tff(c_1917, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_4105, plain, (![U_612]: (ssPv3(U_612) | ssPv2(U_612) | ssPv2(skf1(U_612)) | ssPv3(skf1(U_612)) | ssPv1(U_612) | ssPv1(skf1(U_612))))). % 23.39/13.99 tff(c_726, plain, (![U_325]: (ssPv2(skf1(U_325)) | ~ssPv7(skf1(U_325)) | ssPv5(skf1(U_325)) | ssPv3(skf1(U_325)) | ssPv1(skf1(U_325)) | ssPv4(U_325) | ~ssPv6(U_325) | ~ssPv6(skf1(U_325))))). % 23.39/13.99 tff(c_2027, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_4047, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ssPv6(U_1) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2773, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_2129, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_3659, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_681, plain, (![U_316]: (ssPv4(skf1(U_316)) | ssPv2(skf1(U_316)) | ssPv5(skf1(U_316)) | ssPv3(skf1(U_316)) | ssPv1(skf1(U_316)) | ssPv7(U_316) | ~ssPv1(U_316) | ~ssPv6(skf1(U_316))))). % 23.39/13.99 tff(c_2031, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_2430, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_2077, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_3750, plain, (![U_598]: (ssPv3(skf1(U_598)) | ssPv2(U_598) | ssPv2(skf1(U_598)) | ssPv5(U_598) | ssPv3(U_598) | ssPv1(U_598) | ssPv1(skf1(U_598))))). % 23.39/13.99 tff(c_3731, plain, (![U_597]: (ssPv2(U_597) | ssPv2(skf1(U_597)) | ssPv4(skf1(U_597)) | ssPv5(U_597) | ssPv3(U_597) | ssPv1(U_597) | ssPv1(skf1(U_597))))). % 23.39/13.99 tff(c_1773, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_1714, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.99 tff(c_2914, plain, (![U_564]: (ssPv7(U_564) | ssPv2(U_564) | ssPv4(skf1(U_564)) | ssPv5(U_564) | ~ssPv2(skf1(U_564)) | ssPv1(U_564) | ssPv1(skf1(U_564))))). % 23.39/13.99 tff(c_2649, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_2915, plain, (![U_564]: (ssPv3(U_564) | ssPv2(U_564) | ssPv4(skf1(U_564)) | ssPv5(U_564) | ~ssPv2(skf1(U_564)) | ssPv1(U_564) | ssPv1(skf1(U_564))))). % 23.39/13.99 tff(c_3560, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1)))). % 23.39/13.99 tff(c_1832, plain, (![U_395]: (ssPv5(U_395) | ssPv3(skf1(U_395)) | ~ssPv2(skf1(U_395)) | ssPv4(skf1(U_395)) | ssPv1(skf1(U_395)) | ~ssPv6(skf1(U_395))))). % 23.39/13.99 tff(c_2551, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.99 tff(c_3394, plain, (![U_583]: (~ssPv7(U_583) | ssPv3(skf1(U_583)) | ~ssPv2(skf1(U_583)) | ssPv4(skf1(U_583)) | ssPv1(skf1(U_583)) | ~ssPv6(skf1(U_583))))). % 23.39/13.99 tff(c_3401, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/13.99 tff(c_262, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1)))). % 23.39/13.99 tff(c_1240, plain, (![U_449]: (~ssPv2(skf1(U_449)) | ssPv1(skf1(U_449)) | ~ssPv7(skf1(U_449)) | ssPv3(skf1(U_449)) | ssPv4(skf1(U_449)) | ~ssPv7(U_449)))). % 23.39/13.99 tff(c_1608, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_3277, plain, (![U_580]: (~ssPv1(skf1(U_580)) | ssPv1(U_580) | ssPv2(skf1(U_580)) | ~ssPv7(U_580) | ssPv2(U_580) | ~ssPv5(U_580) | ~ssPv3(U_580)))). % 23.39/13.99 tff(c_3266, plain, (![U_579]: (ssPv1(U_579) | ssPv2(skf1(U_579)) | ssPv3(skf1(U_579)) | ~ssPv7(U_579) | ssPv2(U_579) | ~ssPv5(U_579) | ~ssPv3(U_579)))). % 23.39/13.99 tff(c_1306, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.99 tff(c_3106, plain, (![U_572]: (ssPv3(skf1(U_572)) | ssPv2(skf1(U_572)) | ssPv3(U_572) | ssPv1(U_572) | ssPv8(U_572) | ssPv5(U_572) | ssPv1(skf1(U_572))))). % 23.39/13.99 tff(c_1966, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_1774, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(U_1) | ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1))))). % 23.39/13.99 tff(c_1775, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv1(U_1) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.99 tff(c_250, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.39/13.99 tff(c_2028, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv4(U_1) | ~ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_1778, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv1(U_1) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_1501, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.39/13.99 tff(c_926, plain, (![U_372]: (ssPv4(skf1(U_372)) | ssPv2(skf1(U_372)) | ssPv3(skf1(U_372)) | ssPv1(U_372) | ssPv1(skf1(U_372)) | ssPv5(skf1(U_372))))). % 23.39/13.99 tff(c_1712, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_3001, plain, (![U_567]: (ssPv2(skf1(U_567)) | ssPv4(skf1(U_567)) | ssPv7(U_567) | ~ssPv1(U_567) | ssPv6(U_567) | ssPv3(U_567)))). % 23.39/13.99 tff(c_2647, plain, (![U_1]: (ssPv3(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_263, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_1079, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1))))). % 23.39/13.99 tff(c_1081, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.39/13.99 tff(c_1457, plain, (![U_488]: (~ssPv3(U_488) | ~ssPv1(skf1(U_488)) | ssPv1(U_488) | ssPv2(skf1(U_488)) | ssPv2(U_488) | ~ssPv8(U_488) | ~ssPv7(U_488)))). % 23.39/13.99 tff(c_2840, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv4(U_1) | ~ssPv2(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/13.99 tff(c_2841, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv6(U_1) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2789, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv4(U_1) | ssPv6(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2286, plain, (![U_528, V_383]: (ssPv1(skf1(U_528)) | ~ssPv4(V_383) | ~ssRr(U_528, V_383) | ssPv3(U_528) | ssPv4(U_528) | ssPv6(U_528) | ~ssPv2(U_528)))). % 23.39/13.99 tff(c_2730, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_618, plain, (![U_305]: (ssPv2(skf1(U_305)) | ~ssPv7(skf1(U_305)) | ssPv3(skf1(U_305)) | ssPv1(skf1(U_305)) | ssPv5(skf1(U_305)) | ~ssPv7(U_305) | ~ssPv4(U_305)))). % 23.39/13.99 tff(c_2678, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv4(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_968, plain, (![U_373, V_385]: (~ssPv2(U_373) | ~ssPv4(V_385) | ~ssRr(U_373, V_385) | ssPv8(U_373) | ~ssPv5(U_373) | ssPv1(U_373) | ssPv1(skf1(U_373))))). % 23.39/13.99 tff(c_502, plain, (![U_270]: (ssPv8(U_270) | ~ssPv5(U_270) | ssPv4(skf1(U_270)) | ~ssPv2(skf1(U_270)) | ssPv3(skf1(U_270)) | ssPv1(skf1(U_270))))). % 23.39/13.99 tff(c_456, plain, (![U_1]: (ssPv7(U_1) | ssPv2(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_2613, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 23.39/13.99 tff(c_940, plain, (![U_373, V_222]: (ssPv6(U_373) | ssPv3(U_373) | ~ssPv8(V_222) | ~ssRr(U_373, V_222) | ~ssPv5(U_373) | ssPv1(U_373) | ssPv1(skf1(U_373))))). % 23.39/13.99 tff(c_1409, plain, (![U_482]: (~ssPv3(U_482) | ~ssPv1(skf1(U_482)) | ssPv1(U_482) | ssPv2(skf1(U_482)) | ssPv6(U_482) | ~ssPv8(U_482) | ~ssPv5(U_482)))). % 23.39/13.99 tff(c_2178, plain, (![U_1]: (ssPv1(U_1) | ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_647, plain, (![U_309]: (ssPv4(skf1(U_309)) | ssPv2(skf1(U_309)) | ssPv5(skf1(U_309)) | ssPv3(skf1(U_309)) | ssPv8(U_309) | ssPv5(U_309) | ssPv1(skf1(U_309))))). % 23.39/13.99 tff(c_876, plain, (![U_355]: (~ssPv2(skf1(U_355)) | ssPv4(skf1(U_355)) | ~ssPv7(skf1(U_355)) | ssPv4(U_355) | ssPv1(skf1(U_355)) | ~ssPv1(U_355)))). % 23.39/13.99 tff(c_2502, plain, (![U_1]: (~ssPv2(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_1523, plain, (![U_1]: (~ssPv3(U_1) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1) | ssPv5(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.39/13.99 tff(c_1193, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2387, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_2385, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_549, plain, (![U_282]: (ssPv2(skf1(U_282)) | ~ssPv7(skf1(U_282)) | ssPv5(skf1(U_282)) | ssPv1(skf1(U_282)) | ssPv6(U_282) | ssPv3(skf1(U_282)) | ~ssPv2(U_282)))). % 23.39/13.99 tff(c_2343, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_972, plain, (![U_1, V_385]: (ssPv1(skf1(U_1)) | ~ssPv4(V_385) | ~ssRr(U_1, V_385) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ~ssPv2(U_1)))). % 23.39/13.99 tff(c_1571, plain, (![U_1]: (ssPv3(U_1) | ~ssPv1(U_1) | ssPv5(U_1) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/13.99 tff(c_1159, plain, (![U_426]: (ssPv2(U_426) | ~ssPv7(U_426) | ssPv4(U_426) | ~ssPv6(U_426) | ssPv3(U_426) | ~ssPv2(skf1(U_426)) | ~ssPv5(skf1(U_426))))). % 23.39/14.00 tff(c_1122, plain, (![U_419]: (ssPv2(U_419) | ~ssPv7(U_419) | ssPv4(U_419) | ~ssPv6(U_419) | ssPv5(skf1(U_419)) | ~ssPv1(U_419) | ~ssPv3(skf1(U_419))))). % 23.39/14.00 tff(c_2219, plain, (![U_1]: (ssPv3(U_1) | ssPv4(U_1) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/14.00 tff(c_878, plain, (![U_355]: (ssPv2(skf1(U_355)) | ~ssPv7(skf1(U_355)) | ssPv5(skf1(U_355)) | ssPv3(skf1(U_355)) | ssPv4(U_355) | ssPv1(skf1(U_355)) | ~ssPv1(U_355)))). % 23.39/14.00 tff(c_2144, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 23.39/14.00 tff(c_344, plain, (![U_1, V_236]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(V_236) | ~ssRr(U_1, V_236) | ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 23.39/14.00 tff(c_619, plain, (![U_305]: (ssPv2(skf1(U_305)) | ssPv4(skf1(U_305)) | ~ssPv7(skf1(U_305)) | ssPv5(skf1(U_305)) | ~ssPv7(U_305) | ~ssPv4(U_305)))). % 23.39/14.00 tff(c_550, plain, (![U_282]: (ssPv2(skf1(U_282)) | ssPv4(skf1(U_282)) | ~ssPv7(skf1(U_282)) | ssPv6(U_282) | ssPv3(skf1(U_282)) | ~ssPv2(U_282)))). % 23.39/14.00 tff(c_879, plain, (![U_355]: (ssPv2(skf1(U_355)) | ssPv4(skf1(U_355)) | ~ssPv7(skf1(U_355)) | ssPv4(U_355) | ssPv1(skf1(U_355)) | ~ssPv1(U_355)))). % 23.39/14.00 tff(c_1085, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.39/14.00 tff(c_727, plain, (![U_325]: (ssPv2(skf1(U_325)) | ssPv4(skf1(U_325)) | ~ssPv7(skf1(U_325)) | ssPv4(U_325) | ~ssPv6(U_325) | ~ssPv6(skf1(U_325))))). % 23.39/14.00 tff(c_1708, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/14.00 tff(c_1574, plain, (![U_1]: (ssPv3(U_1) | ~ssPv1(U_1) | ssPv5(U_1) | ~ssPv7(U_1) | ssPv4(U_1) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1))))). % 23.39/14.00 tff(c_501, plain, (![U_1]: (ssPv8(U_1) | ssPv3(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/14.00 tff(c_1844, plain, (![U_511]: (ssPv1(U_511) | ssPv2(skf1(U_511)) | ssPv7(U_511) | ~ssPv3(U_511) | ~ssPv1(skf1(U_511))))). % 23.39/14.00 tff(c_1805, plain, (![U_1]: (ssPv3(U_1) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.39/14.00 tff(c_185, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.39/14.00 tff(c_1719, plain, (![U_1, V_505]: (~ssPv6(skf1(U_1)) | ~ssPv8(V_505) | ~ssRr(U_1, V_505) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1414, plain, (![W_484, U_1, V_485]: (~ssPv6(W_484) | ~ssRr(U_1, W_484) | ~ssPv8(V_485) | ~ssRr(U_1, V_485) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_234, plain, (![U_194]: (ssPv2(skf1(U_194)) | ssPv4(skf1(U_194)) | ~ssPv7(skf1(U_194)) | ssPv7(U_194) | ssPv6(U_194) | ~ssPv1(U_194)))). % 23.39/14.00 tff(c_184, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(skf1(U_1)) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1573, plain, (![U_1]: (ssPv3(U_1) | ssPv5(U_1) | ~ssPv7(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1)))). % 23.39/14.00 tff(c_1578, plain, (![U_1]: (ssPv3(U_1) | ~ssPv1(U_1) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1542, plain, (![U_1]: (ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv8(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_516, plain, (![U_1, V_279]: (ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv8(V_279) | ~ssRr(U_1, V_279) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1502, plain, (![U_1]: (ssPv1(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.39/14.00 tff(c_1468, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1463, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/14.00 tff(c_387, plain, (![U_1, V_245]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv6(V_245) | ~ssRr(U_1, V_245) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_346, plain, (![U_1, V_236]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv8(V_236) | ~ssRr(U_1, V_236) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/14.00 tff(c_1380, plain, (![U_449]: (ssPv1(U_449) | ssPv2(skf1(U_449)) | ssPv2(U_449) | ~ssPv8(U_449) | ssPv3(skf1(U_449)) | ~ssPv7(U_449)))). % 23.39/14.00 tff(c_1398, plain, (![U_481]: (~ssPv3(U_481) | ~ssPv1(skf1(U_481)) | ssPv2(skf1(U_481)) | ssPv4(U_481) | ssPv1(U_481) | ~ssPv7(U_481)))). % 23.39/14.00 tff(c_1387, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.39/14.00 tff(c_1351, plain, (![U_1, W_478, V_479]: (ssPv5(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv6(W_478) | ~ssRr(U_1, W_478) | ~ssPv8(V_479) | ~ssRr(U_1, V_479)))). % 23.39/14.00 tff(c_1386, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.39/14.00 tff(c_1385, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1347, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 23.39/14.00 tff(c_94, plain, (![U_130, X_133, W_132, V_131]: (ssPv5(U_130) | ~ssPv2(X_133) | ~ssRr(U_130, X_133) | ~ssPv6(W_132) | ~ssRr(U_130, W_132) | ~ssPv8(V_131) | ~ssRr(U_130, V_131)))). % 23.39/14.00 tff(c_1343, plain, (![U_1, V_473]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(V_473) | ~ssRr(U_1, V_473)))). % 23.39/14.00 tff(c_1315, plain, (![U_1, W_462, V_463]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(W_462) | ~ssRr(U_1, W_462) | ~ssPv4(V_463) | ~ssRr(U_1, V_463)))). % 23.39/14.00 tff(c_1335, plain, (![U_1, V_468]: (ssPv4(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv7(V_468) | ~ssRr(U_1, V_468)))). % 23.39/14.00 tff(c_1197, plain, (![U_1, W_438, V_440]: (ssPv4(skf1(U_1)) | ssPv7(W_438) | ~ssPv7(U_1) | ~ssRr(U_1, W_438) | ~ssPv7(V_440) | ~ssRr(U_1, V_440)))). % 23.39/14.00 tff(c_1311, plain, (![U_1, V_459]: (ssPv1(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv8(V_459) | ~ssRr(U_1, V_459)))). % 23.39/14.00 tff(c_84, plain, (![U_110, X_113, W_112, V_111]: (ssPv1(U_110) | ssPv2(X_113) | ssPv3(W_112) | ~ssRr(U_110, X_113) | ~ssRr(U_110, W_112) | ~ssPv4(V_111) | ~ssRr(U_110, V_111)))). % 23.39/14.00 tff(c_1254, plain, (![U_1, W_453, V_454]: (ssPv1(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv3(W_453) | ~ssRr(U_1, W_453) | ~ssPv8(V_454) | ~ssRr(U_1, V_454)))). % 23.39/14.00 tff(c_1243, plain, (![U_449]: (ssPv2(skf1(U_449)) | ~ssPv7(skf1(U_449)) | ssPv3(skf1(U_449)) | ssPv4(skf1(U_449)) | ~ssPv7(U_449)))). % 23.39/14.00 tff(c_1245, plain, (![U_449]: (ssPv2(U_449) | ~ssPv8(U_449) | ssPv3(skf1(U_449)) | ssPv4(skf1(U_449)) | ~ssPv7(U_449)))). % 23.39/14.00 tff(c_100, plain, (![X_145, U_142, W_144, V_143]: (ssPv1(X_145) | ~ssPv8(U_142) | ~ssRr(U_142, X_145) | ~ssPv3(W_144) | ~ssRr(U_142, W_144) | ~ssPv8(V_143) | ~ssRr(U_142, V_143)))). % 23.39/14.00 tff(c_1244, plain, (![U_449]: (ssPv4(U_449) | ssPv2(U_449) | ssPv3(skf1(U_449)) | ssPv4(skf1(U_449)) | ~ssPv7(U_449)))). % 23.39/14.00 tff(c_1209, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv7(U_1)))). % 23.39/14.00 tff(c_1205, plain, (![U_1, V_446]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv8(V_446) | ~ssPv7(U_1) | ~ssRr(U_1, V_446)))). % 23.39/14.00 tff(c_1094, plain, (![U_1, W_406, V_407]: (ssPv3(skf1(U_1)) | ssPv4(W_406) | ssPv8(V_407) | ~ssPv7(U_1) | ~ssRr(U_1, W_406) | ~ssRr(U_1, V_407)))). % 23.39/14.00 tff(c_1164, plain, (![U_1, W_429, V_430]: (ssPv1(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(W_429) | ~ssRr(U_1, W_429) | ~ssPv4(V_430) | ~ssRr(U_1, V_430)))). % 23.39/14.00 tff(c_90, plain, (![X_125, W_124, U_122, V_123]: (ssPv4(X_125) | ssPv7(W_124) | ~ssPv7(U_122) | ~ssRr(U_122, X_125) | ~ssRr(U_122, W_124) | ~ssPv7(V_123) | ~ssRr(U_122, V_123)))). % 23.39/14.00 tff(c_1172, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 23.39/14.00 tff(c_1168, plain, (![U_1, V_433]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_433) | ~ssRr(U_1, V_433)))). % 23.39/14.00 tff(c_1110, plain, (![U_1, W_417, V_418]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(W_417) | ~ssRr(U_1, W_417) | ~ssPv3(V_418) | ~ssRr(U_1, V_418)))). % 23.39/14.00 tff(c_102, plain, (![X_149, U_146, W_148, V_147]: (ssPv1(X_149) | ~ssPv5(U_146) | ~ssRr(U_146, X_149) | ~ssPv1(W_148) | ~ssRr(U_146, W_148) | ~ssPv4(V_147) | ~ssRr(U_146, V_147)))). % 23.39/14.00 tff(c_1147, plain, (![U_1]: (ssPv3(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.39/14.00 tff(c_1143, plain, (![U_1, V_423]: (ssPv3(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(V_423) | ~ssRr(U_1, V_423)))). % 23.77/14.00 tff(c_1025, plain, (![U_1, W_398, V_399]: (ssPv3(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(W_398) | ~ssRr(U_1, W_398) | ~ssPv5(V_399) | ~ssRr(U_1, V_399)))). % 23.77/14.00 tff(c_1123, plain, (![U_419]: (~ssPv6(U_419) | ~ssPv2(U_419) | ssPv5(skf1(U_419)) | ~ssPv1(U_419) | ~ssPv3(skf1(U_419))))). % 23.77/14.00 tff(c_1106, plain, (![U_1]: (ssPv5(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.77/14.00 tff(c_96, plain, (![X_137, U_134, W_136, V_135]: (ssPv2(X_137) | ~ssPv3(U_134) | ~ssRr(U_134, X_137) | ~ssPv1(W_136) | ~ssRr(U_134, W_136) | ~ssPv3(V_135) | ~ssRr(U_134, V_135)))). % 23.77/14.00 tff(c_1102, plain, (![U_1, V_412]: (ssPv5(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(V_412) | ~ssRr(U_1, V_412)))). % 23.77/14.00 tff(c_976, plain, (![U_1, W_387, V_389]: (ssPv5(skf1(U_1)) | ssPv6(W_387) | ~ssPv1(U_1) | ~ssRr(U_1, W_387) | ~ssPv3(V_389) | ~ssRr(U_1, V_389)))). % 23.77/14.00 tff(c_1084, plain, (![U_1]: (ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1))))). % 23.77/14.00 tff(c_86, plain, (![X_117, W_116, V_115, U_114]: (ssPv3(X_117) | ssPv4(W_116) | ssPv8(V_115) | ~ssPv7(U_114) | ~ssRr(U_114, X_117) | ~ssRr(U_114, W_116) | ~ssRr(U_114, V_115)))). % 23.77/14.00 tff(c_1015, plain, (![U_395]: (ssPv4(skf1(U_395)) | ~ssPv7(skf1(U_395)) | ssPv5(U_395) | ssPv1(skf1(U_395)) | ~ssPv2(skf1(U_395))))). % 23.77/14.00 tff(c_1020, plain, (![U_395]: (ssPv2(U_395) | ~ssPv8(U_395) | ~ssPv7(U_395) | ssPv5(U_395) | ssPv1(skf1(U_395)) | ~ssPv2(skf1(U_395))))). % 23.77/14.00 tff(c_1021, plain, (![U_395]: (ssPv7(U_395) | ssPv3(U_395) | ~ssPv4(U_395) | ssPv5(U_395) | ssPv1(skf1(U_395)) | ~ssPv2(skf1(U_395))))). % 23.77/14.00 tff(c_1030, plain, (![U_1]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv5(U_1) | ssPv4(U_1) | ~ssPv7(U_1)))). % 23.77/14.00 tff(c_88, plain, (![U_118, X_121, W_120, V_119]: (ssPv3(U_118) | ssPv6(X_121) | ~ssRr(U_118, X_121) | ~ssPv2(W_120) | ~ssRr(U_118, W_120) | ~ssPv5(V_119) | ~ssRr(U_118, V_119)))). % 23.77/14.00 tff(c_984, plain, (![U_1]: (ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 23.77/14.00 tff(c_980, plain, (![U_1, V_392]: (ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv2(V_392) | ~ssRr(U_1, V_392)))). % 23.77/14.00 tff(c_946, plain, (![U_1, W_376, V_377]: (ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv8(W_376) | ~ssRr(U_1, W_376) | ~ssPv2(V_377) | ~ssRr(U_1, V_377)))). % 23.77/14.00 tff(c_92, plain, (![X_129, W_128, U_126, V_127]: (ssPv5(X_129) | ssPv6(W_128) | ~ssPv1(U_126) | ~ssRr(U_126, X_129) | ~ssRr(U_126, W_128) | ~ssPv3(V_127) | ~ssRr(U_126, V_127)))). % 23.77/14.00 tff(c_956, plain, (![U_1, V_383]: (ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_383) | ~ssRr(U_1, V_383)))). % 23.77/14.00 tff(c_913, plain, (![U_1, W_368, V_369]: (ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(W_368) | ~ssRr(U_1, W_368) | ~ssPv4(V_369) | ~ssRr(U_1, V_369)))). % 23.77/14.00 tff(c_941, plain, (![U_373]: (ssPv7(U_373) | ssPv2(U_373) | ssPv4(skf1(U_373)) | ~ssPv5(U_373) | ssPv1(U_373) | ssPv1(skf1(U_373))))). % 23.77/14.00 tff(c_939, plain, (![U_373]: (ssPv8(U_373) | ssPv3(skf1(U_373)) | ~ssPv5(U_373) | ssPv1(U_373) | ssPv1(skf1(U_373))))). % 23.77/14.00 tff(c_942, plain, (![U_373]: (ssPv3(U_373) | ssPv2(U_373) | ~ssPv5(U_373) | ssPv1(U_373) | ssPv1(skf1(U_373))))). % 23.77/14.00 tff(c_82, plain, (![U_106, X_109, W_108, V_107]: (ssPv5(U_106) | ssPv1(X_109) | ssPv8(W_108) | ~ssRr(U_106, X_109) | ~ssRr(U_106, W_108) | ~ssPv2(V_107) | ~ssRr(U_106, V_107)))). % 23.77/14.00 tff(c_925, plain, (![U_372]: (~ssPv5(U_372) | ssPv1(U_372) | ssPv1(skf1(U_372)) | ssPv5(skf1(U_372))))). % 23.77/14.00 tff(c_917, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv7(skf1(U_1))))). % 23.77/14.00 tff(c_909, plain, (![U_1, V_365]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(skf1(U_1)) | ssPv7(V_365) | ~ssRr(U_1, V_365)))). % 23.77/14.00 tff(c_98, plain, (![X_141, U_138, W_140, V_139]: (ssPv1(X_141) | ~ssPv2(U_138) | ~ssRr(U_138, X_141) | ~ssPv3(W_140) | ~ssRr(U_138, W_140) | ~ssPv4(V_139) | ~ssRr(U_138, V_139)))). % 23.77/14.00 tff(c_886, plain, (![U_1, W_358, V_359]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv5(W_358) | ssPv7(V_359) | ~ssRr(U_1, W_358) | ~ssRr(U_1, V_359)))). % 23.77/14.00 tff(c_788, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.77/14.00 tff(c_840, plain, (![U_352]: (ssPv1(U_352) | ssPv1(skf1(U_352)) | ~ssPv5(U_352) | ssPv6(U_352) | ssPv3(U_352) | ssPv6(skf1(U_352))))). % 23.77/14.00 tff(c_880, plain, (![U_355]: (ssPv2(U_355) | ~ssPv7(U_355) | ssPv4(U_355) | ssPv1(skf1(U_355)) | ~ssPv1(U_355)))). % 23.77/14.00 tff(c_80, plain, (![U_102, X_105, W_104, V_103]: (ssPv1(U_102) | ssPv1(X_105) | ssPv5(W_104) | ssPv7(V_103) | ~ssRr(U_102, X_105) | ~ssRr(U_102, W_104) | ~ssRr(U_102, V_103)))). % 23.77/14.00 tff(c_845, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv1(U_1)))). % 23.77/14.00 tff(c_832, plain, (![U_1, V_351]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv8(V_351) | ~ssPv1(U_1) | ~ssRr(U_1, V_351)))). % 23.77/14.00 tff(c_828, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1)) | ssPv7(skf1(U_1))))). % 23.77/14.00 tff(c_42, plain, (![U_45, W_47, V_46]: (ssPv4(U_45) | ssPv1(W_47) | ssPv8(V_46) | ~ssPv1(U_45) | ~ssRr(U_45, W_47) | ~ssRr(U_45, V_46)))). % 23.77/14.00 tff(c_824, plain, (![U_1, V_346]: (ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1)) | ssPv7(V_346) | ~ssRr(U_1, V_346)))). % 23.77/14.00 tff(c_34, plain, (![U_33, W_35, V_34]: (ssPv6(U_33) | ssPv3(U_33) | ssPv6(W_35) | ssPv7(V_34) | ~ssRr(U_33, W_35) | ~ssRr(U_33, V_34)))). % 23.77/14.00 tff(c_725, plain, (![U_325]: (~ssPv2(U_325) | ssPv1(U_325) | ~ssPv7(U_325) | ssPv4(U_325) | ~ssPv6(U_325) | ~ssPv6(skf1(U_325))))). % 23.77/14.00 tff(c_802, plain, (![U_1]: (ssPv5(U_1) | ssPv6(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv6(U_1)))). % 23.77/14.00 tff(c_798, plain, (![U_1, V_339]: (ssPv5(U_1) | ssPv6(skf1(U_1)) | ssPv7(V_339) | ~ssPv6(U_1) | ~ssRr(U_1, V_339)))). % 23.77/14.00 tff(c_38, plain, (![U_39, W_41, V_40]: (ssPv5(U_39) | ssPv6(W_41) | ssPv7(V_40) | ~ssPv6(U_39) | ~ssRr(U_39, W_41) | ~ssRr(U_39, V_40)))). % 23.77/14.00 tff(c_792, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.77/14.00 tff(c_756, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv7(skf1(U_1))))). % 23.77/14.00 tff(c_752, plain, (![U_1, V_332]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv7(V_332) | ~ssRr(U_1, V_332)))). % 23.77/14.00 tff(c_64, plain, (![U_78, W_80, V_79]: (ssPv1(U_78) | ssPv1(W_80) | ~ssPv5(U_78) | ~ssRr(U_78, W_80) | ~ssPv7(V_79) | ~ssRr(U_78, V_79)))). % 23.77/14.00 tff(c_743, plain, (![U_1]: (ssPv2(U_1) | ssPv7(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 23.77/14.00 tff(c_689, plain, (![U_1, V_322]: (ssPv2(U_1) | ssPv7(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv3(V_322) | ~ssRr(U_1, V_322)))). % 23.77/14.00 tff(c_728, plain, (![U_325]: (ssPv2(U_325) | ~ssPv7(U_325) | ssPv4(U_325) | ~ssPv6(U_325) | ~ssPv6(skf1(U_325))))). % 23.77/14.00 tff(c_693, plain, (![U_1]: (ssPv4(U_1) | ssPv8(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv6(skf1(U_1))))). % 23.77/14.00 tff(c_685, plain, (![U_1, V_319]: (ssPv4(U_1) | ssPv8(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv6(V_319) | ~ssRr(U_1, V_319)))). % 23.77/14.00 tff(c_62, plain, (![U_75, W_77, V_76]: (ssPv2(U_75) | ssPv7(W_77) | ~ssPv3(U_75) | ~ssRr(U_75, W_77) | ~ssPv3(V_76) | ~ssRr(U_75, V_76)))). % 23.77/14.00 tff(c_58, plain, (![U_69, W_71, V_70]: (ssPv4(U_69) | ssPv8(W_71) | ~ssPv6(U_69) | ~ssRr(U_69, W_71) | ~ssPv6(V_70) | ~ssRr(U_69, V_70)))). % 23.77/14.00 tff(c_676, plain, (![U_1]: (ssPv7(U_1) | ssPv7(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 23.77/14.00 tff(c_672, plain, (![U_1, V_313]: (ssPv7(U_1) | ssPv7(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv6(V_313) | ~ssRr(U_1, V_313)))). % 23.77/14.00 tff(c_56, plain, (![U_66, W_68, V_67]: (ssPv7(U_66) | ssPv7(W_68) | ~ssPv1(U_66) | ~ssRr(U_66, W_68) | ~ssPv6(V_67) | ~ssRr(U_66, V_67)))). % 23.77/14.00 tff(c_638, plain, (![U_306]: (ssPv3(U_306) | ssPv1(U_306) | ssPv2(U_306) | ~ssPv8(U_306) | ~ssPv7(U_306) | ~ssPv4(U_306)))). % 23.77/14.00 tff(c_642, plain, (![U_1]: (ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv7(skf1(U_1))))). % 23.77/14.00 tff(c_589, plain, (![U_1, V_304]: (ssPv8(U_1) | ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv7(V_304) | ~ssRr(U_1, V_304)))). % 23.77/14.00 tff(c_621, plain, (![U_305]: (ssPv2(U_305) | ~ssPv8(U_305) | ssPv5(skf1(U_305)) | ~ssPv7(U_305) | ~ssPv4(U_305)))). % 23.77/14.00 tff(c_585, plain, (![U_1]: (ssPv5(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 23.77/14.00 tff(c_32, plain, (![U_30, W_32, V_31]: (ssPv8(U_30) | ssPv5(U_30) | ssPv1(W_32) | ssPv7(V_31) | ~ssRr(U_30, W_32) | ~ssRr(U_30, V_31)))). % 23.77/14.00 tff(c_581, plain, (![U_1, V_298]: (ssPv5(skf1(U_1)) | ssPv8(V_298) | ~ssPv7(U_1) | ~ssPv4(U_1) | ~ssRr(U_1, V_298)))). % 23.77/14.00 tff(c_50, plain, (![W_59, V_58, U_57]: (ssPv5(W_59) | ssPv8(V_58) | ~ssPv7(U_57) | ~ssPv4(U_57) | ~ssRr(U_57, W_59) | ~ssRr(U_57, V_58)))). % 23.77/14.00 tff(c_573, plain, (![U_1, V_294]: (ssPv8(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv2(U_1) | ~ssPv8(V_294) | ~ssRr(U_1, V_294)))). % 23.77/14.00 tff(c_70, plain, (![W_89, U_87, V_88]: (ssPv8(W_89) | ~ssPv5(U_87) | ~ssPv2(U_87) | ~ssRr(U_87, W_89) | ~ssPv8(V_88) | ~ssRr(U_87, V_88)))). % 23.77/14.00 tff(c_548, plain, (![U_282]: (ssPv4(U_282) | ssPv1(U_282) | ~ssPv7(U_282) | ssPv6(U_282) | ssPv3(skf1(U_282)) | ~ssPv2(U_282)))). % 23.77/14.00 tff(c_546, plain, (![U_282]: (ssPv1(U_282) | ssPv7(U_282) | ssPv3(U_282) | ssPv6(U_282) | ssPv3(skf1(U_282)) | ~ssPv2(U_282)))). % 23.77/14.01 tff(c_553, plain, (![U_282]: (ssPv7(U_282) | ssPv3(U_282) | ~ssPv4(U_282) | ssPv6(U_282) | ssPv3(skf1(U_282)) | ~ssPv2(U_282)))). % 23.77/14.01 tff(c_561, plain, (![U_1]: (ssPv7(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(skf1(U_1))))). % 23.77/14.01 tff(c_557, plain, (![U_1, V_285]: (ssPv7(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv2(V_285) | ~ssRr(U_1, V_285)))). % 23.77/14.01 tff(c_66, plain, (![W_83, U_81, V_82]: (ssPv7(W_83) | ~ssPv7(U_81) | ~ssPv6(U_81) | ~ssRr(U_81, W_83) | ~ssPv2(V_82) | ~ssRr(U_81, V_82)))). % 23.77/14.01 tff(c_520, plain, (![U_1]: (ssPv6(U_1) | ssPv3(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv2(U_1)))). % 23.77/14.01 tff(c_512, plain, (![U_1, V_277]: (ssPv6(U_1) | ssPv3(skf1(U_1)) | ssPv8(V_277) | ~ssPv2(U_1) | ~ssRr(U_1, V_277)))). % 23.77/14.01 tff(c_508, plain, (![U_1, V_274]: (ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv8(V_274) | ~ssRr(U_1, V_274)))). % 23.77/14.01 tff(c_36, plain, (![U_36, W_38, V_37]: (ssPv6(U_36) | ssPv3(W_38) | ssPv8(V_37) | ~ssPv2(U_36) | ~ssRr(U_36, W_38) | ~ssRr(U_36, V_37)))). % 23.77/14.01 tff(c_74, plain, (![U_93, W_95, V_94]: (ssPv3(U_93) | ~ssPv1(U_93) | ~ssPv2(W_95) | ~ssRr(U_93, W_95) | ~ssPv8(V_94) | ~ssRr(U_93, V_94)))). % 23.77/14.01 tff(c_503, plain, (![U_1]: (ssPv8(U_1) | ~ssPv5(U_1) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 23.77/14.01 tff(c_490, plain, (![U_1]: (ssPv8(U_1) | ssPv3(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv5(skf1(U_1))))). % 23.77/14.01 tff(c_474, plain, (![U_1, V_266]: (ssPv8(U_1) | ssPv3(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv5(V_266) | ~ssRr(U_1, V_266)))). % 23.77/14.01 tff(c_470, plain, (![U_1]: (ssPv5(skf1(U_1)) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv1(U_1) | ~ssPv6(U_1)))). % 23.77/14.01 tff(c_52, plain, (![U_60, W_62, V_61]: (ssPv8(U_60) | ssPv3(W_62) | ~ssPv5(U_60) | ~ssRr(U_60, W_62) | ~ssPv5(V_61) | ~ssRr(U_60, V_61)))). % 23.77/14.01 tff(c_461, plain, (![U_1]: (ssPv5(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv6(skf1(U_1))))). % 23.77/14.01 tff(c_444, plain, (![U_1, V_259]: (ssPv5(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv6(V_259) | ~ssRr(U_1, V_259)))). % 23.77/14.01 tff(c_439, plain, (![U_256]: (ssPv4(U_256) | ~ssPv2(U_256) | ssPv5(U_256) | ssPv3(U_256) | ssPv1(U_256)))). % 23.77/14.01 tff(c_68, plain, (![W_86, U_84, V_85]: (ssPv5(W_86) | ~ssPv6(U_84) | ~ssPv2(U_84) | ~ssRr(U_84, W_86) | ~ssPv6(V_85) | ~ssRr(U_84, V_85)))). % 23.77/14.01 tff(c_431, plain, (![U_1]: (ssPv7(U_1) | ~ssPv2(U_1) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.77/14.01 tff(c_418, plain, (![U_1]: (ssPv1(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.77/14.01 tff(c_347, plain, (![U_1, V_236]: (ssPv1(U_1) | ~ssPv8(V_236) | ~ssRr(U_1, V_236) | ssPv7(U_1) | ssPv3(U_1) | ~ssPv2(U_1)))). % 23.77/14.01 tff(c_412, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.77/14.01 tff(c_408, plain, (![U_1, V_249]: (ssPv6(U_1) | ssPv3(U_1) | ssPv6(skf1(U_1)) | ~ssPv5(V_249) | ~ssRr(U_1, V_249)))). % 23.77/14.01 tff(c_44, plain, (![U_48, W_50, V_49]: (ssPv6(U_48) | ssPv3(U_48) | ssPv6(W_50) | ~ssRr(U_48, W_50) | ~ssPv5(V_49) | ~ssRr(U_48, V_49)))). % 23.77/14.01 tff(c_370, plain, (![U_1, V_242]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv6(V_242) | ~ssRr(U_1, V_242)))). % 23.77/14.01 tff(c_365, plain, (![U_1]: (~ssPv2(U_1) | ssPv1(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.77/14.01 tff(c_78, plain, (![U_99, W_101, V_100]: (~ssPv3(U_99) | ~ssPv1(U_99) | ~ssPv2(W_101) | ~ssRr(U_99, W_101) | ~ssPv6(V_100) | ~ssRr(U_99, V_100)))). % 23.77/14.01 tff(c_353, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv8(skf1(U_1)) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.77/14.01 tff(c_345, plain, (![U_1, V_236]: (~ssPv2(U_1) | ~ssPv8(V_236) | ~ssRr(U_1, V_236) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv7(U_1)))). % 23.77/14.01 tff(c_327, plain, (![U_1, V_231]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv8(V_231) | ~ssRr(U_1, V_231)))). % 23.77/14.01 tff(c_331, plain, (![U_1]: (ssPv7(U_1) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 23.77/14.01 tff(c_323, plain, (![U_1, V_228]: (ssPv7(U_1) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(V_228) | ~ssRr(U_1, V_228)))). % 23.77/14.01 tff(c_76, plain, (![U_96, W_98, V_97]: (ssPv1(U_96) | ~ssPv2(U_96) | ~ssPv4(W_98) | ~ssRr(U_96, W_98) | ~ssPv8(V_97) | ~ssRr(U_96, V_97)))). % 23.77/14.01 tff(c_54, plain, (![U_63, W_65, V_64]: (ssPv7(U_63) | ssPv4(W_65) | ~ssPv3(U_63) | ~ssRr(U_63, W_65) | ~ssPv1(V_64) | ~ssRr(U_63, V_64)))). % 23.77/14.01 tff(c_306, plain, (![U_1, V_222]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv5(skf1(U_1)) | ~ssPv8(V_222) | ~ssRr(U_1, V_222)))). % 23.77/14.01 tff(c_302, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv2(U_1)))). % 23.77/14.01 tff(c_60, plain, (![U_72, W_74, V_73]: (ssPv6(U_72) | ssPv3(U_72) | ~ssPv5(W_74) | ~ssRr(U_72, W_74) | ~ssPv8(V_73) | ~ssRr(U_72, V_73)))). % 23.77/14.01 tff(c_298, plain, (![U_1, V_217]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv5(V_217) | ~ssPv2(U_1) | ~ssRr(U_1, V_217)))). % 23.77/14.01 tff(c_40, plain, (![U_42, W_44, V_43]: (ssPv4(U_42) | ssPv3(W_44) | ssPv5(V_43) | ~ssPv2(U_42) | ~ssRr(U_42, W_44) | ~ssRr(U_42, V_43)))). % 23.77/14.01 tff(c_293, plain, (![U_1]: (ssPv7(U_1) | ssPv2(U_1) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 23.77/14.01 tff(c_285, plain, (![U_1, V_209]: (ssPv7(U_1) | ssPv2(U_1) | ssPv4(skf1(U_1)) | ~ssPv5(V_209) | ~ssRr(U_1, V_209)))). % 23.77/14.01 tff(c_281, plain, (![U_1, V_206]: (ssPv6(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(V_206) | ~ssRr(U_1, V_206)))). % 23.77/14.01 tff(c_46, plain, (![U_51, W_53, V_52]: (ssPv7(U_51) | ssPv2(U_51) | ssPv4(W_53) | ~ssRr(U_51, W_53) | ~ssPv5(V_52) | ~ssRr(U_51, V_52)))). % 23.77/14.01 tff(c_48, plain, (![U_54, W_56, V_55]: (ssPv6(U_54) | ssPv2(U_54) | ssPv2(W_56) | ~ssRr(U_54, W_56) | ~ssPv2(V_55) | ~ssRr(U_54, V_55)))). % 23.77/14.01 tff(c_272, plain, (![U_1]: (ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 23.77/14.01 tff(c_268, plain, (![U_1, V_200]: (ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv3(V_200) | ~ssRr(U_1, V_200)))). % 23.77/14.01 tff(c_72, plain, (![W_92, U_90, V_91]: (ssPv7(W_92) | ~ssPv5(U_90) | ~ssPv1(U_90) | ~ssRr(U_90, W_92) | ~ssPv3(V_91) | ~ssRr(U_90, V_91)))). % 23.77/14.01 tff(c_141, plain, (![U_1]: (ssPv2(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.77/14.01 tff(c_163, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ~ssPv7(U_1) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.77/14.01 tff(c_237, plain, (![U_194]: (ssPv3(U_194) | ~ssPv4(U_194) | ssPv7(U_194) | ssPv6(U_194) | ~ssPv1(U_194)))). % 23.77/14.01 tff(c_219, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ssPv8(skf1(U_1)) | ~ssPv1(U_1)))). % 23.77/14.01 tff(c_214, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv5(skf1(U_1))))). % 23.77/14.01 tff(c_6, plain, (![U_4, V_5]: (ssPv7(U_4) | ssPv6(U_4) | ssPv8(V_5) | ~ssPv1(U_4) | ~ssRr(U_4, V_5)))). % 23.77/14.01 tff(c_16, plain, (![U_14, V_15]: (ssPv3(U_14) | ssPv2(U_14) | ssPv1(U_14) | ~ssPv5(V_15) | ~ssRr(U_14, V_15)))). % 23.77/14.01 tff(c_207, plain, (![U_1]: (ssPv4(U_1) | ssPv1(U_1) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 23.77/14.01 tff(c_202, plain, (![U_1]: (ssPv6(U_1) | ssPv4(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 23.77/14.01 tff(c_14, plain, (![U_12, V_13]: (ssPv4(U_12) | ssPv1(U_12) | ssPv4(V_13) | ~ssPv7(U_12) | ~ssRr(U_12, V_13)))). % 23.77/14.01 tff(c_18, plain, (![U_16, V_17]: (ssPv6(U_16) | ssPv4(V_17) | ~ssPv8(U_16) | ~ssPv5(U_16) | ~ssRr(U_16, V_17)))). % 23.77/14.01 tff(c_196, plain, (![U_1]: (ssPv7(U_1) | ssPv1(U_1) | ssPv6(skf1(U_1)) | ~ssPv6(U_1)))). % 23.77/14.01 tff(c_12, plain, (![U_10, V_11]: (ssPv7(U_10) | ssPv1(U_10) | ssPv6(V_11) | ~ssPv6(U_10) | ~ssRr(U_10, V_11)))). % 23.77/14.01 tff(c_190, plain, (![U_1]: (ssPv2(U_1) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 23.77/14.01 tff(c_24, plain, (![U_22, V_23]: (ssPv2(U_22) | ssPv7(V_23) | ~ssPv5(U_22) | ~ssPv3(U_22) | ~ssRr(U_22, V_23)))). % 23.77/14.01 tff(c_174, plain, (![U_175]: (ssPv2(U_175) | ssPv4(U_175) | ~ssPv8(U_175) | ~ssPv7(U_175)))). % 23.77/14.01 tff(c_158, plain, (![U_1]: (ssPv4(U_1) | ssPv8(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv7(U_1)))). % 23.77/14.01 tff(c_153, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ~ssPv7(U_1) | ~ssPv8(skf1(U_1))))). % 23.77/14.01 tff(c_20, plain, (![U_18, V_19]: (ssPv4(U_18) | ssPv8(V_19) | ~ssPv8(U_18) | ~ssPv7(U_18) | ~ssRr(U_18, V_19)))). % 23.77/14.01 tff(c_26, plain, (![U_24, V_25]: (ssPv4(U_24) | ssPv2(U_24) | ~ssPv7(U_24) | ~ssPv8(V_25) | ~ssRr(U_24, V_25)))). % 23.77/14.01 tff(c_147, plain, (![U_1]: (ssPv5(U_1) | ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv7(U_1)))). % 23.77/14.01 tff(c_8, plain, (![U_6, V_7]: (ssPv5(U_6) | ssPv4(U_6) | ssPv2(V_7) | ~ssPv7(U_6) | ~ssRr(U_6, V_7)))). % 23.77/14.01 tff(c_136, plain, (![U_1]: (ssPv7(U_1) | ssPv3(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 23.77/14.01 tff(c_131, plain, (![U_1]: (ssPv2(U_1) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv8(skf1(U_1))))). % 23.77/14.01 tff(c_10, plain, (![U_8, V_9]: (ssPv7(U_8) | ssPv3(U_8) | ssPv4(V_9) | ~ssPv2(U_8) | ~ssRr(U_8, V_9)))). % 23.77/14.01 tff(c_30, plain, (![U_28, V_29]: (ssPv2(U_28) | ~ssPv8(U_28) | ~ssPv7(U_28) | ~ssPv8(V_29) | ~ssRr(U_28, V_29)))). % 23.77/14.01 tff(c_125, plain, (![U_1]: (ssPv7(U_1) | ~ssPv4(U_1) | ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 23.77/14.01 tff(c_120, plain, (![U_1]: (ssPv7(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv8(skf1(U_1))))). % 23.77/14.01 tff(c_22, plain, (![U_20, V_21]: (ssPv7(U_20) | ssPv3(U_20) | ~ssPv4(U_20) | ~ssPv8(V_21) | ~ssRr(U_20, V_21)))). % 23.77/14.01 tff(c_114, plain, (![U_1]: (ssPv5(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv8(skf1(U_1))))). % 23.77/14.01 tff(c_4, plain, (![U_2, V_3]: (ssPv5(U_2) | ssPv3(U_2) | ssPv1(U_2) | ssPv8(V_3) | ~ssRr(U_2, V_3)))). % 23.77/14.01 tff(c_108, plain, (![U_1]: (ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 23.77/14.01 tff(c_28, plain, (![V_27, U_26]: (ssPv4(V_27) | ~ssPv7(U_26) | ~ssPv3(U_26) | ~ssPv1(U_26) | ~ssRr(U_26, V_27)))). % 23.77/14.01 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 23.77/14.01 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.77/14.01 %------------------------------------------------------------------------------