%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN775-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n025.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:54 PM UTC 2025 % Result : Satisfiable 16.19s 8.11s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN775-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 08:18:50 EDT 2025 % 0.13/0.34 % CPUTime : % 16.19/8.10 % 16.19/8.11 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.19/8.11 % 16.19/8.11 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.19/8.11 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf3 > skf2 % 16.19/8.11 % 16.19/8.11 %Foreground sorts: % 16.19/8.11 % 16.19/8.11 % 16.19/8.11 %Background operators: % 16.19/8.11 % 16.19/8.11 % 16.19/8.11 %Foreground operators: % 16.19/8.11 tff(skf3, type, skf3: $i > $i). % 16.19/8.11 tff(ssPv1, type, ssPv1: $i > $o). % 16.19/8.11 tff(ssPv3, type, ssPv3: $i > $o). % 16.19/8.11 tff(skf2, type, skf2: $i > $i). % 16.19/8.11 tff(ssRr, type, ssRr: ($i * $i) > $o). % 16.19/8.11 tff(ssPv4, type, ssPv4: $i > $o). % 16.19/8.11 tff(ssPv2, type, ssPv2: $i > $o). % 16.19/8.11 % 16.19/8.11 %Saturated clause set: % 16.19/8.12 tff(c_31740, plain, (![U_1164]: (ssPv1(U_1164) | ssPv2(skf3(skf3(U_1164))) | ~ssPv2(skf3(U_1164)) | ssPv4(skf3(U_1164)) | ~ssPv2(skf2(skf3(U_1164))) | ~ssPv1(skf2(skf3(U_1164))) | ssPv3(skf3(U_1164)) | ~ssPv1(skf3(U_1164))))). % 16.19/8.12 tff(c_32612, plain, (![U_707]: (~ssPv2(skf2(U_707)) | ~ssPv1(skf2(skf2(U_707))) | ssPv3(skf2(U_707)) | ~ssPv1(skf2(U_707)) | ssPv4(skf2(U_707)) | ssPv3(U_707) | ~ssPv1(skf3(skf2(U_707)))))). % 16.19/8.12 tff(c_32667, plain, (![U_815]: (ssPv3(U_815) | ~ssPv2(skf2(U_815)) | ssPv4(skf2(U_815)) | ssPv2(U_815) | ssPv3(skf2(U_815)) | ~ssPv1(skf2(U_815))))). % 16.19/8.12 tff(c_28896, plain, (![U_1124]: (~ssPv1(skf3(skf2(U_1124))) | ~ssPv1(skf2(U_1124)) | ~ssPv3(skf2(U_1124)) | ssPv4(skf2(U_1124)) | ~ssPv1(U_1124) | ~ssPv1(skf2(skf2(U_1124))) | ~ssPv2(skf2(U_1124)) | ~ssPv3(skf2(skf2(U_1124))) | ~ssPv2(skf2(skf2(U_1124)))))). % 16.19/8.12 tff(c_32371, plain, (![U_1188]: (~ssPv2(skf2(U_1188)) | ssPv3(skf2(U_1188)) | ~ssPv1(skf2(U_1188)) | ssPv3(U_1188) | ~ssPv1(U_1188)))). % 16.19/8.12 tff(c_32031, plain, (![U_1183]: (ssPv4(U_1183) | ~ssPv2(skf3(U_1183)) | ssPv3(skf3(U_1183)) | ~ssPv1(skf3(U_1183))))). % 16.19/8.12 tff(c_31745, plain, (![U_1179]: (ssPv2(skf3(U_1179)) | ~ssPv1(skf3(U_1179)) | ~ssPv2(U_1179) | ssPv4(U_1179) | ~ssPv2(skf2(U_1179)) | ~ssPv1(skf2(U_1179)) | ssPv3(U_1179) | ~ssPv1(U_1179)))). % 16.19/8.12 tff(c_26445, plain, (![U_1064]: (ssPv4(U_1064) | ~ssPv1(skf3(skf2(U_1064))) | ssPv2(skf2(U_1064)) | ~ssPv2(skf3(skf2(U_1064))) | ssPv1(skf2(skf2(U_1064))) | ~ssPv2(skf2(skf2(U_1064))) | ssPv3(skf2(U_1064)) | ssPv1(skf2(U_1064))))). % 16.19/8.12 tff(c_27243, plain, (![U_258]: (~ssPv2(U_258) | ssPv1(skf2(skf3(U_258))) | ~ssPv2(skf2(skf3(U_258))) | ssPv3(skf3(U_258)) | ~ssPv2(skf3(skf3(U_258))) | ~ssPv1(skf3(skf3(U_258))) | ssPv2(skf3(U_258)) | ~ssPv1(skf3(U_258))))). % 16.19/8.12 tff(c_28752, plain, (![U_2]: (ssPv2(skf3(skf2(U_2))) | ssPv4(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 16.19/8.12 tff(c_23360, plain, (![U_452]: (ssPv4(skf3(U_452)) | ~ssPv3(skf3(U_452)) | ~ssPv1(skf2(skf3(U_452))) | ~ssPv2(skf2(skf3(U_452))) | ssPv1(skf3(U_452)) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.12 tff(c_23519, plain, (![U_452]: (~ssPv3(skf3(U_452)) | ssPv4(skf3(U_452)) | ssPv1(skf2(skf3(U_452))) | ~ssPv2(skf2(skf3(U_452))) | ssPv1(skf3(U_452)) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.12 tff(c_31010, plain, (![U_1164]: (ssPv4(skf3(U_1164)) | ssPv1(U_1164) | ssPv2(skf3(skf3(U_1164))) | ~ssPv1(skf2(skf3(U_1164))) | ~ssPv2(skf3(U_1164)) | ~ssPv3(skf2(skf3(U_1164))) | ~ssPv2(skf2(skf3(U_1164)))))). % 16.19/8.12 tff(c_10171, plain, (![U_392, U_393]: (ssPv4(skf3(U_392)) | ssPv1(U_392) | ssPv2(U_393) | ~ssRr(U_393, skf3(U_392)) | ~ssPv1(skf2(skf3(U_392))) | ~ssPv2(skf3(U_392)) | ~ssPv3(skf2(skf3(U_392))) | ~ssPv2(skf2(skf3(U_392)))))). % 16.19/8.12 tff(c_30955, plain, (![U_1161]: (~ssPv3(skf2(U_1161)) | ~ssPv4(skf3(skf2(U_1161))) | ssPv4(skf2(U_1161)) | ssPv3(U_1161) | ~ssPv1(U_1161) | ~ssPv2(skf2(skf2(U_1161))) | ssPv1(skf2(U_1161)) | ~ssPv2(skf2(U_1161))))). % 16.19/8.12 tff(c_26600, plain, (![U_1067, U_215]: (~ssPv3(skf2(U_1067)) | ~ssPv4(U_215) | ~ssRr(U_215, skf2(U_1067)) | ssPv4(skf2(U_1067)) | ssPv3(U_1067) | ~ssPv1(U_1067) | ~ssPv2(skf2(skf2(U_1067))) | ssPv1(skf2(U_1067)) | ~ssPv2(skf2(U_1067))))). % 16.19/8.12 tff(c_30218, plain, (![U_1151]: (ssPv3(skf3(skf2(U_1151))) | ssPv4(skf3(skf2(U_1151))) | ~ssPv2(skf2(U_1151)) | ssPv4(skf2(U_1151)) | ssPv2(U_1151) | ssPv3(skf2(U_1151)) | ~ssPv1(skf2(U_1151))))). % 16.19/8.12 tff(c_30103, plain, (![U_1147, U_1146]: (ssPv3(skf3(skf2(U_1147))) | ssPv4(U_1146) | ~ssRr(U_1146, skf2(U_1147)) | ~ssPv2(skf2(U_1147)) | ssPv4(skf2(U_1147)) | ssPv2(U_1147) | ssPv3(skf2(U_1147)) | ~ssPv1(skf2(U_1147))))). % 16.19/8.12 tff(c_16219, plain, (![W_272, U_273, U_880]: (ssPv3(W_272) | ssPv4(U_273) | ~ssRr(W_272, skf2(U_880)) | ~ssRr(U_273, skf2(U_880)) | ~ssPv2(skf2(U_880)) | ssPv4(skf2(U_880)) | ssPv2(U_880) | ssPv3(skf2(U_880)) | ~ssPv1(skf2(U_880))))). % 16.19/8.12 tff(c_30032, plain, (![U_2]: (~ssPv1(skf2(skf2(U_2))) | ssPv1(skf3(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2)))). % 16.19/8.12 tff(c_29961, plain, (![U_707]: (~ssPv1(skf2(skf2(U_707))) | ssPv1(U_707) | ~ssPv2(skf2(U_707)) | ~ssPv1(skf2(U_707)) | ssPv4(skf2(U_707)) | ssPv3(U_707) | ~ssPv1(skf3(skf2(U_707)))))). % 16.19/8.12 tff(c_17795, plain, (![U_428]: (~ssPv3(skf2(skf3(U_428))) | ~ssPv1(skf3(U_428)) | ssPv1(skf2(skf3(U_428))) | ~ssPv2(skf2(skf3(U_428))) | ssPv4(skf3(U_428)) | ssPv2(U_428) | ~ssPv1(skf3(skf3(U_428)))))). % 16.19/8.12 tff(c_29823, plain, (![U_1137]: (~ssPv3(skf3(U_1137)) | ~ssPv4(skf3(skf3(U_1137))) | ssPv4(skf3(U_1137)) | ssPv1(U_1137) | ~ssPv2(skf2(skf3(U_1137))) | ssPv1(skf3(U_1137)) | ~ssPv2(skf3(U_1137))))). % 16.19/8.12 tff(c_21457, plain, (![U_985, U_215]: (~ssPv3(skf3(U_985)) | ~ssPv4(U_215) | ~ssRr(U_215, skf3(U_985)) | ssPv4(skf3(U_985)) | ssPv1(U_985) | ~ssPv2(skf2(skf3(U_985))) | ssPv1(skf3(U_985)) | ~ssPv2(skf3(U_985))))). % 16.19/8.12 tff(c_29710, plain, (![U_1135]: (ssPv1(U_1135) | ssPv3(U_1135) | ssPv2(U_1135) | ssPv1(skf2(U_1135)) | ~ssPv2(skf2(U_1135))))). % 16.19/8.12 tff(c_29597, plain, (![U_1134]: (ssPv3(U_1134) | ssPv2(U_1134) | ssPv3(skf2(U_1134)) | ssPv1(skf2(U_1134)) | ~ssPv2(skf2(U_1134))))). % 16.19/8.12 tff(c_29165, plain, (![U_1127]: (ssPv4(skf2(U_1127)) | ssPv3(U_1127) | ~ssPv1(skf3(skf2(U_1127))) | ~ssPv1(skf2(skf2(U_1127))) | ~ssPv2(skf2(U_1127)) | ~ssPv3(skf2(skf2(U_1127))) | ~ssPv2(skf2(skf2(U_1127)))))). % 16.19/8.12 tff(c_29166, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.12 tff(c_28597, plain, (![U_2, U_1118]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_1118) | ~ssRr(U_1118, skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.13 tff(c_24402, plain, (![U_1034]: (~ssPv1(skf2(skf3(U_1034))) | ssPv3(skf3(U_1034)) | ~ssPv2(skf3(skf3(U_1034))) | ~ssPv1(skf3(skf3(U_1034))) | ssPv2(skf3(U_1034)) | ssPv4(U_1034) | ~ssPv1(skf3(U_1034))))). % 16.19/8.13 tff(c_24671, plain, (![U_1039]: (~ssPv1(skf2(skf2(U_1039))) | ssPv3(skf2(U_1039)) | ~ssPv2(skf3(skf2(U_1039))) | ~ssPv1(skf3(skf2(U_1039))) | ssPv2(skf2(U_1039)) | ssPv2(U_1039) | ~ssPv1(skf2(U_1039))))). % 16.19/8.13 tff(c_28604, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv1(U_2) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.13 tff(c_28679, plain, (![U_1121]: (~ssPv1(U_1121) | ~ssPv3(U_1121) | ssPv4(U_1121) | ~ssPv1(skf3(U_1121)) | ~ssPv1(skf2(U_1121)) | ~ssPv2(U_1121) | ~ssPv3(skf2(U_1121)) | ~ssPv2(skf2(U_1121))))). % 16.19/8.13 tff(c_28674, plain, (![U_1121]: (ssPv2(skf3(U_1121)) | ssPv4(U_1121) | ~ssPv1(skf3(U_1121)) | ~ssPv1(skf2(U_1121)) | ~ssPv2(U_1121) | ~ssPv3(skf2(U_1121)) | ~ssPv2(skf2(U_1121))))). % 16.19/8.13 tff(c_28603, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssPv1(skf2(U_1)) | ~ssPv2(U_1) | ~ssPv3(skf2(U_1)) | ~ssPv2(skf2(U_1))))). % 16.19/8.13 tff(c_28596, plain, (![U_1, U_1118]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(U_1118) | ~ssRr(U_1118, U_1) | ~ssPv1(skf2(U_1)) | ~ssPv2(U_1) | ~ssPv3(skf2(U_1)) | ~ssPv2(skf2(U_1))))). % 16.19/8.13 tff(c_10172, plain, (![U_712, W_234, U_236]: (ssPv4(U_712) | ssPv3(W_234) | ~ssRr(W_234, U_712) | ~ssPv1(U_236) | ~ssRr(U_236, U_712) | ~ssPv1(skf2(U_712)) | ~ssPv2(U_712) | ~ssPv3(skf2(U_712)) | ~ssPv2(skf2(U_712))))). % 16.19/8.13 tff(c_9886, plain, (![U_452]: (~ssPv3(skf3(U_452)) | ssPv4(skf3(U_452)) | ssPv1(skf2(skf3(U_452))) | ssPv2(skf2(skf3(U_452))) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.13 tff(c_28390, plain, (![U_1112]: (ssPv3(skf2(skf2(U_1112))) | ssPv3(skf3(skf2(U_1112))) | ~ssPv2(skf2(U_1112)) | ssPv2(U_1112) | ssPv4(skf2(U_1112)) | ssPv3(skf2(U_1112)) | ssPv1(skf2(U_1112))))). % 16.19/8.13 tff(c_28293, plain, (![U_1110]: (ssPv3(skf3(skf2(U_1110))) | ssPv4(skf3(skf2(U_1110))) | ~ssPv2(skf2(U_1110)) | ssPv2(U_1110) | ssPv4(skf2(U_1110)) | ssPv3(skf2(U_1110)) | ssPv1(skf2(U_1110))))). % 16.19/8.13 tff(c_28102, plain, (![U_1105, U_1104]: (ssPv3(skf3(skf2(U_1105))) | ssPv4(U_1104) | ~ssPv2(skf2(U_1105)) | ~ssRr(U_1104, skf2(U_1105)) | ssPv2(U_1105) | ssPv4(skf2(U_1105)) | ssPv3(skf2(U_1105)) | ssPv1(skf2(U_1105))))). % 16.19/8.13 tff(c_2113, plain, (![W_272, U_273, U_415]: (ssPv3(W_272) | ssPv4(U_273) | ~ssPv2(skf2(U_415)) | ~ssRr(W_272, skf2(U_415)) | ~ssRr(U_273, skf2(U_415)) | ssPv2(U_415) | ssPv4(skf2(U_415)) | ssPv3(skf2(U_415)) | ssPv1(skf2(U_415))))). % 16.19/8.13 tff(c_27926, plain, (![U_241]: (ssPv3(U_241) | ~ssPv2(skf3(U_241)) | ssPv1(skf3(U_241)) | ~ssPv4(skf3(U_241)) | ~ssPv2(U_241)))). % 16.19/8.13 tff(c_27887, plain, (![U_302]: (~ssPv1(skf3(skf3(U_302))) | ~ssPv4(skf3(U_302)) | ssPv1(skf3(U_302)) | ssPv3(U_302) | ~ssPv2(skf3(U_302))))). % 16.19/8.13 tff(c_17794, plain, (![U_1]: (~ssPv3(skf2(skf3(U_1))) | ~ssPv1(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ~ssPv2(skf2(skf3(U_1))) | ssPv3(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_1)))). % 16.19/8.13 tff(c_11712, plain, (![U_452]: (~ssPv3(skf3(U_452)) | ssPv4(skf3(U_452)) | ~ssPv1(skf3(skf3(U_452))) | ssPv1(skf3(U_452)) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.13 tff(c_10530, plain, (![U_2]: (ssPv2(skf3(skf2(U_2))) | ssPv4(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 16.19/8.13 tff(c_27423, plain, (![U_1088]: (~ssPv2(skf2(U_1088)) | ssPv4(skf2(U_1088)) | ssPv3(U_1088) | ~ssPv1(skf3(skf2(U_1088))) | ssPv3(skf2(U_1088)) | ~ssPv1(skf2(U_1088)) | ssPv1(skf2(skf2(U_1088)))))). % 16.19/8.13 tff(c_27280, plain, (![U_1085]: (ssPv4(skf2(U_1085)) | ssPv3(U_1085) | ~ssPv1(skf3(skf2(U_1085))) | ssPv3(skf2(U_1085)) | ~ssPv1(skf2(U_1085)) | ssPv3(skf2(skf2(U_1085))) | ssPv1(skf2(skf2(U_1085)))))). % 16.19/8.13 tff(c_27281, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2)))))). % 16.19/8.13 tff(c_26776, plain, (![U_2, U_1076]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_1076) | ~ssRr(U_1076, skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2)))))). % 16.19/8.13 tff(c_25478, plain, (![U_914]: (~ssPv1(skf3(skf3(U_914))) | ~ssPv1(skf3(U_914)) | ~ssPv1(U_914) | ~ssPv1(skf2(skf3(U_914))) | ~ssPv4(skf3(U_914)) | ssPv4(U_914) | ~ssPv2(skf3(U_914))))). % 16.19/8.13 tff(c_19575, plain, (![U_1]: (ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv3(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv2(U_1) | ~ssPv1(U_1)))). % 16.19/8.13 tff(c_23833, plain, (![U_914]: (~ssPv1(skf3(U_914)) | ssPv1(skf3(skf3(U_914))) | ~ssPv1(U_914) | ~ssPv1(skf2(skf3(U_914))) | ~ssPv4(skf3(U_914)) | ssPv4(U_914) | ~ssPv2(skf3(U_914))))). % 16.19/8.13 tff(c_17792, plain, (![U_1]: (~ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv1(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ssPv2(U_1) | ~ssPv1(U_1)))). % 16.19/8.13 tff(c_26783, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2)))))). % 16.19/8.13 tff(c_26782, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv3(U_1) | ~ssPv1(U_1) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1))))). % 16.19/8.13 tff(c_26775, plain, (![U_1, U_1076]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(U_1076) | ~ssRr(U_1076, U_1) | ssPv3(U_1) | ~ssPv1(U_1) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1))))). % 16.19/8.13 tff(c_5274, plain, (![U_554, W_234, U_236]: (ssPv4(U_554) | ssPv3(W_234) | ~ssRr(W_234, U_554) | ~ssPv1(U_236) | ~ssRr(U_236, U_554) | ssPv3(U_554) | ~ssPv1(U_554) | ssPv3(skf2(U_554)) | ssPv1(skf2(U_554))))). % 16.19/8.13 tff(c_26763, plain, (![U_115, U_1071]: (ssPv2(U_115) | ~ssRr(U_115, skf3(U_1071)) | ~ssPv4(skf3(U_1071)) | ~ssPv3(skf3(U_1071)) | ssPv4(U_1071) | ~ssPv2(skf3(U_1071))))). % 16.19/8.13 tff(c_26676, plain, (![U_1070]: (~ssPv4(skf3(U_1070)) | ~ssPv3(skf3(U_1070)) | ssPv4(U_1070) | ~ssPv2(skf3(U_1070)) | ssPv2(skf2(skf3(U_1070)))))). % 16.19/8.13 tff(c_9643, plain, (![U_675]: (ssPv4(skf2(U_675)) | ssPv3(U_675) | ~ssPv1(U_675) | ~ssPv2(skf2(skf2(U_675))) | ssPv1(skf2(U_675)) | ~ssPv2(skf2(U_675)) | ssPv2(skf3(skf2(U_675)))))). % 16.19/8.13 tff(c_26553, plain, (![U_384]: (~ssPv1(skf3(skf2(U_384))) | ~ssPv4(skf2(U_384)) | ssPv2(skf2(U_384)) | ssPv1(skf2(skf2(U_384))) | ssPv4(U_384)))). % 16.19/8.13 tff(c_20651, plain, (![U_384]: (ssPv1(skf2(skf2(U_384))) | ssPv4(U_384) | ~ssPv1(skf3(skf2(U_384))) | ssPv2(skf2(U_384)) | ~ssPv3(skf3(skf2(U_384))) | ~ssPv2(skf3(skf2(U_384)))))). % 16.19/8.13 tff(c_13751, plain, (![U_452]: (~ssPv3(skf3(U_452)) | ssPv4(skf3(U_452)) | ssPv1(skf2(skf3(U_452))) | ~ssPv4(U_452) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.13 tff(c_26186, plain, (![U_1061]: (ssPv3(skf2(U_1061)) | ~ssPv1(skf2(U_1061)) | ssPv3(U_1061) | ~ssPv2(skf3(U_1061)) | ~ssPv1(skf3(U_1061)) | ssPv2(U_1061) | ~ssPv1(U_1061)))). % 16.19/8.13 tff(c_26101, plain, (![U_707]: (ssPv1(skf2(U_707)) | ~ssPv2(skf2(U_707)) | ~ssPv4(U_707) | ssPv4(skf2(U_707)) | ssPv3(U_707) | ~ssPv1(skf3(skf2(U_707)))))). % 16.19/8.13 tff(c_24410, plain, (![U_1034]: (~ssPv2(U_1034) | ssPv3(skf3(U_1034)) | ~ssPv2(skf3(skf3(U_1034))) | ~ssPv1(skf3(skf3(U_1034))) | ssPv2(skf3(U_1034)) | ssPv4(U_1034) | ~ssPv1(skf3(U_1034))))). % 16.19/8.13 tff(c_25849, plain, (![U_251]: (~ssPv1(U_251) | ~ssPv4(skf3(U_251)) | ssPv4(U_251) | ssPv3(U_251) | ~ssPv2(skf3(U_251)) | ~ssPv1(skf3(U_251))))). % 16.19/8.13 tff(c_25488, plain, (![U_767]: (~ssPv1(skf3(skf3(U_767))) | ~ssPv1(skf3(U_767)) | ~ssPv1(U_767) | ~ssPv4(skf3(U_767)) | ssPv3(U_767) | ssPv4(U_767) | ~ssPv2(skf3(U_767))))). % 16.19/8.13 tff(c_25795, plain, (![U_1023]: (~ssPv1(U_1023) | ~ssPv2(skf3(U_1023)) | ~ssPv4(skf3(U_1023)) | ~ssPv1(skf2(skf3(U_1023))) | ~ssPv1(skf3(U_1023))))). % 16.19/8.13 tff(c_25582, plain, (![U_537]: (~ssPv1(U_537) | ~ssPv2(U_537) | ~ssPv1(skf3(U_537)) | ~ssPv4(U_537) | ~ssPv3(skf3(U_537)) | ~ssPv2(skf3(U_537))))). % 16.19/8.13 tff(c_25536, plain, (![U_278]: (~ssPv1(skf3(U_278)) | ~ssPv1(U_278) | ~ssPv4(skf3(U_278)) | ~ssPv2(skf3(U_278)) | ~ssPv2(U_278)))). % 16.19/8.13 tff(c_25195, plain, (![U_1048]: (~ssPv4(skf3(U_1048)) | ~ssPv1(skf3(skf3(U_1048))) | ~ssPv1(skf3(U_1048)) | ~ssPv2(skf3(skf3(U_1048))) | ~ssPv2(skf3(U_1048)) | ~ssPv1(U_1048)))). % 16.19/8.13 tff(c_25193, plain, (![U_1048]: (~ssPv3(skf3(U_1048)) | ~ssPv1(skf3(skf3(U_1048))) | ~ssPv1(skf3(U_1048)) | ~ssPv2(skf3(skf3(U_1048))) | ~ssPv2(skf3(U_1048)) | ~ssPv1(U_1048)))). % 16.19/8.14 tff(c_23955, plain, (![U_452]: (~ssPv1(skf3(skf3(U_452))) | ~ssPv1(skf3(U_452)) | ~ssPv2(skf3(skf3(U_452))) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.14 tff(c_25067, plain, (![U_1046]: (ssPv3(skf3(U_1046)) | ssPv1(skf2(skf3(U_1046))) | ~ssPv2(skf2(skf3(U_1046))) | ~ssPv2(skf3(U_1046)) | ~ssPv4(U_1046)))). % 16.19/8.14 tff(c_17808, plain, (![U_2]: (~ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv2(skf2(U_2)) | ssPv4(U_2) | ~ssPv1(skf2(U_2))))). % 16.19/8.14 tff(c_16642, plain, (![U_892]: (~ssPv3(skf3(U_892)) | ssPv1(U_892) | ssPv2(skf2(skf3(U_892))) | ssPv3(skf3(skf3(U_892))) | ssPv1(skf3(skf3(U_892))) | ssPv4(skf3(U_892))))). % 16.19/8.14 tff(c_24840, plain, (![U_1042]: (~ssPv4(skf3(U_1042)) | ssPv1(skf2(skf3(U_1042))) | ~ssPv2(skf2(skf3(U_1042))) | ~ssPv2(skf3(U_1042)) | ~ssPv4(U_1042)))). % 16.19/8.14 tff(c_1746, plain, (![U_380]: (ssPv3(skf3(skf2(U_380))) | ssPv3(skf2(U_380)) | ~ssPv2(skf3(skf2(U_380))) | ~ssPv1(skf3(skf2(U_380))) | ssPv2(skf2(U_380)) | ssPv1(skf2(skf2(U_380))) | ~ssPv4(U_380)))). % 16.19/8.14 tff(c_1292, plain, (![U_288]: (ssPv3(skf3(skf2(U_288))) | ssPv3(skf2(U_288)) | ~ssPv2(skf3(skf2(U_288))) | ~ssPv1(skf3(skf2(U_288))) | ssPv2(skf2(U_288)) | ssPv2(U_288) | ~ssPv1(skf2(U_288))))). % 16.19/8.14 tff(c_4337, plain, (![U_2]: (ssPv1(skf3(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv3(skf3(skf2(U_2))) | ssPv2(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv4(U_2)))). % 16.19/8.14 tff(c_13756, plain, (![U_823]: (~ssPv3(skf3(U_823)) | ssPv1(skf2(skf3(U_823))) | ~ssPv4(U_823) | ssPv3(skf3(skf3(U_823))) | ssPv1(skf3(skf3(U_823))) | ssPv4(skf3(U_823))))). % 16.19/8.14 tff(c_11661, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(skf3(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 16.19/8.14 tff(c_1290, plain, (![U_327]: (ssPv3(skf3(skf3(U_327))) | ssPv3(skf3(U_327)) | ~ssPv2(skf3(skf3(U_327))) | ~ssPv1(skf3(skf3(U_327))) | ssPv2(skf3(U_327)) | ssPv4(U_327) | ~ssPv1(skf3(U_327))))). % 16.19/8.14 tff(c_4966, plain, (![U_428]: (ssPv3(skf3(U_428)) | ssPv1(skf2(skf3(U_428))) | ~ssPv2(skf2(skf3(U_428))) | ssPv4(skf3(U_428)) | ssPv2(U_428) | ~ssPv1(skf3(skf3(U_428)))))). % 16.19/8.14 tff(c_19901, plain, (![U_258]: (ssPv2(skf3(U_258)) | ~ssPv2(U_258) | ssPv1(skf2(skf3(U_258))) | ~ssPv2(skf2(skf3(U_258))) | ssPv3(skf3(U_258)) | ssPv1(skf3(U_258))))). % 16.19/8.14 tff(c_19595, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv2(skf2(U_2)) | ssPv4(U_2) | ~ssPv1(skf2(U_2))))). % 16.19/8.14 tff(c_17875, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 16.19/8.14 tff(c_1291, plain, (![U_307]: (ssPv3(skf3(skf3(U_307))) | ssPv3(skf3(U_307)) | ~ssPv2(skf3(skf3(U_307))) | ~ssPv1(skf3(skf3(U_307))) | ssPv1(skf3(U_307)) | ssPv4(U_307) | ~ssPv4(skf3(U_307))))). % 16.19/8.14 tff(c_17661, plain, (![U_912]: (~ssPv4(skf3(U_912)) | ~ssPv1(skf3(U_912)) | ssPv1(skf3(skf3(U_912))) | ~ssPv2(skf3(skf3(U_912))) | ~ssPv2(skf3(U_912)) | ~ssPv1(U_912)))). % 16.19/8.14 tff(c_21690, plain, (![U_248]: (~ssPv1(skf3(U_248)) | ~ssPv1(U_248) | ssPv1(skf2(skf3(U_248))) | ~ssPv2(skf2(skf3(U_248))) | ~ssPv4(skf3(U_248)) | ~ssPv3(skf3(U_248))))). % 16.19/8.14 tff(c_10169, plain, (![U_438]: (ssPv3(U_438) | ssPv4(U_438) | ~ssPv1(skf2(skf3(U_438))) | ~ssPv2(skf3(U_438)) | ~ssPv3(skf2(skf3(U_438))) | ~ssPv2(skf2(skf3(U_438)))))). % 16.19/8.14 tff(c_10124, plain, (![U_710]: (ssPv1(skf2(skf2(U_710))) | ssPv3(skf2(U_710)) | ssPv1(skf2(U_710)) | ssPv4(skf2(U_710)) | ssPv3(U_710) | ~ssPv1(skf3(skf2(U_710)))))). % 16.19/8.14 tff(c_10071, plain, (![U_705]: (~ssPv1(skf3(skf2(U_705))) | ~ssPv1(skf2(U_705)) | ~ssPv3(skf2(U_705)) | ssPv4(skf2(U_705)) | ~ssPv1(U_705) | ssPv2(skf2(skf2(U_705)))))). % 16.19/8.14 tff(c_23476, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv4(skf3(U_1)) | ssPv4(U_1) | ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv1(U_1) | ~ssPv2(U_1)))). % 16.19/8.14 tff(c_10235, plain, (![U_714, U_215]: (~ssPv3(U_714) | ~ssPv4(U_215) | ~ssRr(U_215, U_714) | ssPv4(U_714) | ssPv1(skf2(U_714)) | ~ssPv2(skf2(U_714)) | ssPv1(U_714) | ~ssPv2(U_714)))). % 16.19/8.14 tff(c_15326, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 16.19/8.14 tff(c_9927, plain, (![U_692]: (~ssPv1(skf3(skf3(U_692))) | ~ssPv1(skf3(U_692)) | ~ssPv3(skf3(U_692)) | ssPv4(skf3(U_692)) | ssPv1(U_692) | ssPv2(skf2(skf3(U_692)))))). % 16.19/8.14 tff(c_23317, plain, (![U_1]: (ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv1(U_1) | ~ssPv2(U_1)))). % 16.19/8.14 tff(c_15743, plain, (![U_873, U_215]: (ssPv4(U_873) | ~ssPv3(U_873) | ~ssPv4(U_215) | ~ssRr(U_215, U_873) | ~ssPv1(skf2(U_873)) | ~ssPv2(skf2(U_873)) | ssPv1(U_873) | ~ssPv2(U_873)))). % 16.19/8.14 tff(c_12531, plain, (![U_280]: (~ssPv1(skf3(skf3(U_280))) | ~ssPv1(skf3(U_280)) | ssPv2(skf3(skf3(U_280))) | ssPv2(skf3(U_280)) | ssPv1(U_280) | ~ssPv4(skf3(U_280))))). % 16.19/8.14 tff(c_23258, plain, (![U_315]: (ssPv2(skf3(U_315)) | ssPv1(skf2(skf3(U_315))) | ~ssPv4(skf3(U_315)) | ~ssPv3(skf3(U_315)) | ~ssPv3(U_315)))). % 16.19/8.14 tff(c_23168, plain, (![U_1007]: (~ssPv2(skf2(U_1007)) | ~ssPv4(U_1007) | ssPv2(U_1007) | ssPv1(skf2(U_1007))))). % 16.19/8.14 tff(c_23015, plain, (![U_1004]: (~ssPv1(skf2(skf2(U_1004))) | ssPv3(skf2(U_1004)) | ssPv1(skf2(U_1004)) | ~ssPv2(skf2(U_1004)) | ~ssPv4(U_1004)))). % 16.19/8.14 tff(c_22569, plain, (![U_989]: (~ssPv1(skf3(U_989)) | ssPv1(skf2(U_989)) | ~ssPv2(skf2(U_989)) | ~ssPv4(U_989) | ~ssPv3(U_989)))). % 16.19/8.14 tff(c_21626, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv1(skf2(U_2)) | ssPv4(U_2) | ~ssPv4(skf2(U_2))))). % 16.19/8.14 tff(c_21622, plain, (![U_223]: (ssPv1(skf2(U_223)) | ~ssPv2(skf2(U_223)) | ssPv1(skf3(U_223)) | ~ssPv2(skf3(U_223)) | ssPv1(U_223) | ~ssPv4(U_223)))). % 16.19/8.14 tff(c_21630, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv3(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2))))). % 16.19/8.14 tff(c_22089, plain, (![U_994]: (ssPv1(skf2(U_994)) | ~ssPv2(skf2(U_994)) | ~ssPv2(U_994) | ssPv1(U_994) | ~ssPv4(U_994)))). % 16.19/8.14 tff(c_21827, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 16.19/8.14 tff(c_21620, plain, (![U_1]: (ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv3(U_1) | ssPv1(U_1) | ~ssPv4(U_1)))). % 16.19/8.14 tff(c_21682, plain, (![U_989]: (ssPv2(skf3(U_989)) | ssPv1(skf2(U_989)) | ~ssPv2(skf2(U_989)) | ~ssPv4(U_989) | ~ssPv3(U_989)))). % 16.19/8.14 tff(c_21631, plain, (![U_1]: (ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 16.19/8.14 tff(c_21532, plain, (![U_987]: (~ssPv4(U_987) | ssPv1(skf2(U_987)) | ~ssPv4(skf2(U_987)) | ~ssPv2(skf2(U_987))))). % 16.19/8.14 tff(c_21498, plain, (![U_986]: (~ssPv1(skf2(skf2(U_986))) | ~ssPv4(skf2(U_986)) | ssPv1(skf2(U_986)) | ~ssPv2(skf2(U_986)) | ~ssPv4(U_986)))). % 16.19/8.14 tff(c_13039, plain, (![U_804]: (ssPv4(skf3(U_804)) | ssPv1(U_804) | ~ssPv2(skf2(skf3(U_804))) | ssPv1(skf3(U_804)) | ~ssPv2(skf3(U_804)) | ssPv2(skf3(skf3(U_804)))))). % 16.19/8.14 tff(c_13937, plain, (![U_828]: (ssPv2(skf3(skf3(U_828))) | ssPv4(skf3(U_828)) | ~ssPv1(skf3(skf3(U_828))) | ssPv3(skf3(U_828)) | ~ssPv2(skf3(U_828)) | ~ssPv3(U_828)))). % 16.19/8.14 tff(c_18577, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv1(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2)))). % 16.19/8.14 tff(c_21321, plain, (![U_241]: (~ssPv3(skf3(U_241)) | ~ssPv2(skf3(U_241)) | ssPv1(skf3(U_241)) | ~ssPv4(skf3(U_241)) | ~ssPv2(U_241)))). % 16.19/8.14 tff(c_21259, plain, (![U_624]: (~ssPv4(U_624) | ~ssPv1(skf3(U_624)) | ~ssPv3(U_624) | ssPv1(U_624) | ~ssPv2(U_624)))). % 16.19/8.14 tff(c_20932, plain, (![U_2]: (~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2)) | ssPv3(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2))))). % 16.19/8.14 tff(c_20813, plain, (![U_971]: (~ssPv3(skf3(U_971)) | ~ssPv4(skf3(skf3(U_971))) | ssPv4(skf3(U_971)) | ssPv2(U_971) | ~ssPv1(skf3(skf3(U_971)))))). % 16.19/8.14 tff(c_20540, plain, (![U_965, U_215]: (~ssPv3(skf3(U_965)) | ~ssPv4(U_215) | ~ssRr(U_215, skf3(U_965)) | ssPv4(skf3(U_965)) | ssPv2(U_965) | ~ssPv1(skf3(skf3(U_965)))))). % 16.19/8.14 tff(c_20645, plain, (![U_967]: (~ssPv3(U_967) | ~ssPv1(skf3(U_967)) | ssPv2(U_967) | ~ssPv3(skf3(U_967)) | ~ssPv2(skf3(U_967))))). % 16.19/8.14 tff(c_20565, plain, (![U_966]: (~ssPv1(skf3(U_966)) | ssPv2(U_966) | ssPv4(skf3(U_966)) | ~ssPv3(skf3(U_966)) | ~ssPv2(skf3(U_966))))). % 16.19/8.14 tff(c_20518, plain, (![U_964]: (~ssPv1(skf3(U_964)) | ~ssPv3(skf3(U_964)) | ssPv4(skf3(U_964)) | ssPv2(U_964) | ~ssPv1(skf3(skf3(U_964)))))). % 16.19/8.14 tff(c_20514, plain, (![U_964]: (ssPv2(skf3(skf3(U_964))) | ssPv4(skf3(U_964)) | ssPv2(U_964) | ~ssPv1(skf3(skf3(U_964)))))). % 16.19/8.14 tff(c_20467, plain, (![U_962]: (ssPv3(skf3(skf3(U_962))) | ssPv4(skf3(U_962)) | ssPv2(U_962) | ~ssPv1(skf3(skf3(U_962)))))). % 16.19/8.14 tff(c_2305, plain, (![W_234, U_430, U_236]: (ssPv3(W_234) | ~ssRr(W_234, skf3(U_430)) | ~ssPv1(U_236) | ~ssRr(U_236, skf3(U_430)) | ssPv4(skf3(U_430)) | ssPv2(U_430) | ~ssPv1(skf3(skf3(U_430)))))). % 16.19/8.14 tff(c_19589, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv3(U_2)))). % 16.19/8.14 tff(c_19593, plain, (![U_1]: (ssPv1(skf2(skf3(U_1))) | ~ssPv2(skf2(skf3(U_1))) | ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.19/8.14 tff(c_19927, plain, (![U_951]: (ssPv4(U_951) | ssPv1(skf3(U_951)) | ~ssPv4(skf3(U_951)) | ~ssPv2(skf3(U_951))))). % 16.19/8.14 tff(c_19590, plain, (![U_1]: (ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv3(U_1) | ssPv1(U_1) | ssPv3(skf3(U_1))))). % 16.19/8.14 tff(c_19748, plain, (![U_948]: (~ssPv2(U_948) | ~ssPv2(skf2(U_948)) | ssPv3(U_948) | ~ssPv1(U_948) | ssPv1(skf2(U_948))))). % 16.19/8.14 tff(c_19580, plain, (![U_2]: (~ssPv2(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2))))). % 16.19/8.14 tff(c_19574, plain, (![U_2]: (ssPv1(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2) | ssPv3(U_2) | ~ssPv1(U_2)))). % 16.19/8.14 tff(c_19494, plain, (![U_945]: (ssPv3(U_945) | ssPv1(skf2(U_945)) | ~ssPv4(skf2(U_945)) | ~ssPv2(skf2(U_945))))). % 16.19/8.14 tff(c_19340, plain, (![U_624]: (ssPv1(skf3(U_624)) | ssPv1(U_624) | ~ssPv2(U_624) | ssPv2(skf3(U_624))))). % 16.19/8.14 tff(c_19122, plain, (![U_280]: (~ssPv1(skf3(skf3(U_280))) | ~ssPv3(skf3(U_280)) | ssPv2(skf3(U_280)) | ssPv1(U_280) | ~ssPv4(skf3(U_280))))). % 16.19/8.14 tff(c_2308, plain, (![U_430]: (ssPv3(skf2(skf3(U_430))) | ~ssPv1(skf2(skf3(U_430))) | ~ssPv1(skf3(U_430)) | ssPv4(skf3(U_430)) | ssPv2(U_430) | ~ssPv1(skf3(skf3(U_430)))))). % 16.19/8.15 tff(c_2821, plain, (![U_454]: (ssPv3(skf3(U_454)) | ~ssPv2(skf3(skf3(U_454))) | ~ssPv1(skf3(skf3(U_454))) | ssPv3(skf3(skf3(U_454))) | ~ssPv2(skf3(U_454)) | ~ssPv1(U_454)))). % 16.19/8.15 tff(c_18730, plain, (![U_2]: (ssPv1(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ssPv3(U_2) | ~ssPv2(U_2) | ~ssPv3(skf2(U_2))))). % 16.19/8.15 tff(c_18570, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv2(skf3(U_1))))). % 16.19/8.15 tff(c_18511, plain, (![U_2]: (ssPv3(U_2) | ssPv1(skf2(U_2)) | ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2))))). % 16.19/8.15 tff(c_1756, plain, (![U_380]: (ssPv1(skf3(skf2(U_380))) | ssPv1(skf2(U_380)) | ~ssPv2(skf3(skf2(U_380))) | ssPv2(skf2(U_380)) | ssPv1(skf2(skf2(U_380))) | ~ssPv4(U_380)))). % 16.19/8.15 tff(c_17876, plain, (![U_1]: (ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv3(U_1) | ssPv1(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 16.19/8.15 tff(c_17711, plain, (![U_916]: (~ssPv3(skf2(U_916)) | ~ssPv1(U_916) | ssPv1(skf2(U_916)) | ~ssPv4(skf2(U_916)) | ~ssPv2(skf2(U_916))))). % 16.19/8.15 tff(c_17666, plain, (![U_914]: (ssPv2(skf3(skf3(U_914))) | ~ssPv1(skf2(skf3(U_914))) | ~ssPv4(skf3(U_914)) | ssPv4(U_914) | ~ssPv2(skf3(U_914))))). % 16.19/8.15 tff(c_17302, plain, (![U_115, U_906]: (ssPv2(U_115) | ~ssRr(U_115, skf3(U_906)) | ~ssPv1(skf2(skf3(U_906))) | ~ssPv4(skf3(U_906)) | ssPv4(U_906) | ~ssPv2(skf3(U_906))))). % 16.19/8.15 tff(c_17601, plain, (![U_452]: (ssPv1(skf3(skf3(U_452))) | ~ssPv2(skf3(skf3(U_452))) | ssPv3(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.19/8.15 tff(c_17555, plain, (![U_910]: (~ssPv2(U_910) | ssPv1(skf3(U_910)) | ~ssPv4(skf3(U_910)) | ~ssPv2(skf3(U_910))))). % 16.19/8.15 tff(c_17532, plain, (![U_241]: (~ssPv1(skf2(skf3(U_241))) | ~ssPv2(skf3(U_241)) | ssPv1(skf3(U_241)) | ~ssPv4(skf3(U_241)) | ~ssPv2(U_241)))). % 16.19/8.15 tff(c_17489, plain, (![U_908]: (~ssPv1(skf3(U_908)) | ~ssPv1(skf2(U_908)) | ~ssPv4(U_908) | ssPv1(U_908) | ~ssPv2(U_908)))). % 16.19/8.15 tff(c_17151, plain, (![U_406]: (~ssPv1(skf2(skf3(U_406))) | ~ssPv4(skf3(U_406)) | ssPv4(U_406) | ~ssPv2(skf3(U_406)) | ssPv2(skf2(skf3(U_406)))))). % 16.19/8.15 tff(c_17207, plain, (![U_2]: (ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 16.19/8.15 tff(c_17155, plain, (![U_1]: (~ssPv1(skf2(U_1)) | ~ssPv4(U_1) | ssPv2(skf2(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv2(skf3(U_1))))). % 16.19/8.15 tff(c_17206, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv1(U_1)))). % 16.19/8.15 tff(c_17200, plain, (![U_115, U_900]: (ssPv2(U_115) | ~ssPv2(U_900) | ~ssRr(U_115, U_900) | ~ssPv4(U_900) | ~ssPv1(skf2(U_900)) | ~ssPv1(U_900)))). % 16.19/8.15 tff(c_17154, plain, (![U_2]: (~ssPv4(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2) | ssPv2(skf2(U_2))))). % 16.19/8.15 tff(c_17076, plain, (![U_898]: (~ssPv1(skf2(U_898)) | ~ssPv3(skf2(U_898)) | ~ssPv4(U_898) | ssPv2(skf2(U_898))))). % 16.19/8.15 tff(c_16970, plain, (![U_896]: (~ssPv3(skf2(U_896)) | ~ssPv4(U_896) | ssPv2(skf2(U_896)) | ssPv1(skf2(skf2(U_896))) | ~ssPv4(skf2(U_896))))). % 16.19/8.15 tff(c_12836, plain, (![U_280]: (ssPv3(skf3(U_280)) | ~ssPv1(skf2(skf3(U_280))) | ~ssPv1(skf3(U_280)) | ssPv2(skf3(U_280)) | ssPv1(U_280) | ~ssPv4(skf3(U_280))))). % 16.19/8.15 tff(c_16601, plain, (![U_890]: (~ssPv3(skf3(U_890)) | ~ssPv4(skf3(skf3(U_890))) | ssPv4(skf3(U_890)) | ssPv1(U_890) | ssPv2(skf2(skf3(U_890)))))). % 16.19/8.15 tff(c_9928, plain, (![U_692, U_215]: (~ssPv3(skf3(U_692)) | ~ssPv4(U_215) | ~ssRr(U_215, skf3(U_692)) | ssPv4(skf3(U_692)) | ssPv1(U_692) | ssPv2(skf2(skf3(U_692)))))). % 16.19/8.15 tff(c_1808, plain, (![U_389]: (~ssPv1(skf3(skf3(U_389))) | ~ssPv1(skf3(U_389)) | ~ssPv3(skf3(U_389)) | ssPv4(skf3(U_389)) | ssPv1(skf2(skf3(U_389))) | ~ssPv4(U_389)))). % 16.19/8.15 tff(c_16500, plain, (![U_885]: (~ssPv3(skf3(U_885)) | ~ssPv4(skf3(skf3(U_885))) | ssPv4(skf3(U_885)) | ~ssPv4(U_885) | ~ssPv1(skf3(skf3(U_885)))))). % 16.19/8.15 tff(c_9738, plain, (![U_681, U_215]: (~ssPv3(skf3(U_681)) | ~ssPv4(U_215) | ~ssRr(U_215, skf3(U_681)) | ssPv4(skf3(U_681)) | ~ssPv4(U_681) | ~ssPv1(skf3(skf3(U_681)))))). % 16.19/8.15 tff(c_7238, plain, (![U_241]: (~ssPv3(skf3(U_241)) | ssPv2(skf3(U_241)) | ssPv1(skf2(skf3(U_241))) | ssPv1(skf3(U_241)) | ~ssPv4(skf3(U_241)) | ~ssPv2(U_241)))). % 16.19/8.15 tff(c_7239, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv1(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv1(U_2)))). % 16.19/8.15 tff(c_13414, plain, (![U_815]: (~ssPv2(skf2(U_815)) | ssPv4(skf2(U_815)) | ssPv2(U_815) | ssPv3(skf2(U_815)) | ~ssPv1(skf2(U_815)) | ssPv1(skf2(skf2(U_815)))))). % 16.19/8.15 tff(c_6913, plain, (![U_599]: (ssPv3(skf2(U_599)) | ~ssPv1(skf2(U_599)) | ssPv1(skf3(U_599)) | ~ssPv3(U_599) | ~ssPv3(skf3(U_599)) | ssPv2(U_599) | ~ssPv1(U_599)))). % 16.19/8.15 tff(c_10423, plain, (![U_725]: (~ssPv3(skf3(U_725)) | ssPv1(U_725) | ~ssPv4(U_725) | ssPv3(skf3(skf3(U_725))) | ssPv1(skf3(skf3(U_725))) | ssPv4(skf3(U_725))))). % 16.19/8.15 tff(c_15913, plain, (![U_491]: (~ssPv1(skf3(U_491)) | ~ssPv2(skf3(U_491)) | ssPv3(skf2(U_491)) | ssPv1(U_491) | ~ssPv4(U_491) | ~ssPv2(U_491)))). % 16.19/8.15 tff(c_15726, plain, (![U_2]: (~ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2))) | ssPv1(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2)))). % 16.19/8.15 tff(c_15719, plain, (![U_1]: (~ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv2(skf3(U_1))))). % 16.19/8.15 tff(c_2306, plain, (![U_430, U_341]: (ssPv1(skf2(skf3(U_430))) | ssPv2(U_341) | ~ssRr(U_341, skf3(U_430)) | ssPv4(skf3(U_430)) | ssPv2(U_430) | ~ssPv1(skf3(skf3(U_430)))))). % 16.19/8.15 tff(c_15660, plain, (![U_2]: (~ssPv1(skf2(U_2)) | ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2))))). % 16.19/8.15 tff(c_15327, plain, (![U_1]: (~ssPv4(U_1) | ssPv1(skf2(U_1)) | ~ssPv2(skf2(U_1)) | ssPv1(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 16.19/8.15 tff(c_15152, plain, (![U_861]: (~ssPv1(U_861) | ~ssPv1(skf2(skf3(U_861))) | ~ssPv1(skf3(U_861)) | ~ssPv4(skf3(U_861)) | ~ssPv3(skf3(U_861))))). % 16.19/8.15 tff(c_15236, plain, (![U_769]: (~ssPv4(U_769) | ssPv1(skf2(U_769)) | ~ssPv3(skf2(U_769)) | ~ssPv2(skf2(U_769))))). % 16.19/8.15 tff(c_1295, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv2(U_1) | ssPv4(skf2(U_1)) | ~ssPv1(U_1)))). % 16.19/8.15 tff(c_14897, plain, (![U_163]: (ssPv2(skf2(skf2(U_163))) | ~ssPv1(skf2(skf2(U_163))) | ssPv2(skf2(U_163)) | ssPv4(U_163) | ~ssPv1(skf2(U_163))))). % 16.19/8.15 tff(c_14893, plain, (![U_2]: (ssPv2(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2) | ssPv2(skf2(U_2))))). % 16.19/8.15 tff(c_14815, plain, (![U_854]: (~ssPv3(skf2(U_854)) | ssPv2(U_854) | ~ssPv1(skf2(U_854)) | ssPv2(skf2(U_854))))). % 16.19/8.15 tff(c_14677, plain, (![U_624]: (~ssPv1(skf3(U_624)) | ~ssPv3(U_624) | ssPv1(U_624) | ~ssPv2(U_624) | ssPv2(skf3(U_624))))). % 16.19/8.15 tff(c_14561, plain, (![U_850]: (~ssPv1(skf3(U_850)) | ~ssPv3(U_850) | ~ssPv3(skf3(U_850)) | ssPv2(skf3(U_850))))). % 16.19/8.15 tff(c_1293, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv1(U_1) | ssPv4(skf2(U_1)) | ~ssPv4(U_1)))). % 16.19/8.15 tff(c_10106, plain, (![U_709]: (ssPv1(skf2(skf2(U_709))) | ssPv3(skf2(U_709)) | ssPv1(skf2(U_709)) | ssPv4(skf2(U_709)) | ssPv3(U_709) | ~ssPv1(U_709)))). % 16.19/8.15 tff(c_2645, plain, (![U_440]: (ssPv3(U_440) | ssPv4(U_440) | ~ssPv2(skf3(U_440)) | ssPv1(skf3(U_440)) | ~ssPv3(skf2(skf3(U_440))) | ~ssPv2(skf2(skf3(U_440)))))). % 16.19/8.15 tff(c_14283, plain, (![U_843]: (ssPv2(skf3(U_843)) | ~ssPv1(skf2(U_843)) | ~ssPv1(U_843) | ~ssPv4(U_843) | ~ssPv3(U_843)))). % 16.19/8.15 tff(c_14123, plain, (![U_838]: (ssPv2(skf3(skf3(U_838))) | ~ssPv4(skf3(U_838)) | ssPv3(skf3(U_838)) | ssPv4(U_838) | ~ssPv2(skf3(U_838))))). % 16.19/8.15 tff(c_9788, plain, (![U_115, U_683]: (ssPv2(U_115) | ~ssPv4(skf3(U_683)) | ~ssRr(U_115, skf3(U_683)) | ssPv3(skf3(U_683)) | ssPv4(U_683) | ~ssPv2(skf3(U_683))))). % 16.19/8.15 tff(c_9597, plain, (![U_115, U_673]: (ssPv2(U_115) | ~ssPv2(skf3(U_673)) | ~ssRr(U_115, skf3(U_673)) | ~ssPv4(skf3(U_673)) | ~ssPv3(skf3(U_673)) | ~ssPv3(U_673)))). % 16.19/8.15 tff(c_9768, plain, (![U_682]: (~ssPv3(skf3(U_682)) | ~ssPv1(skf3(U_682)) | ~ssPv1(U_682) | ssPv4(U_682) | ~ssPv2(skf3(U_682)) | ssPv2(skf2(skf3(U_682)))))). % 16.19/8.15 tff(c_13761, plain, (![U_824]: (ssPv4(skf3(U_824)) | ssPv3(skf3(skf3(U_824))) | ~ssPv1(skf3(skf3(U_824))) | ssPv3(skf3(U_824)) | ~ssPv2(skf3(U_824)) | ~ssPv3(U_824)))). % 16.19/8.15 tff(c_12721, plain, (![U_788, U_790]: (ssPv4(skf3(U_788)) | ssPv3(skf3(skf3(U_788))) | ~ssPv1(U_790) | ~ssRr(U_790, skf3(U_788)) | ssPv3(skf3(U_788)) | ~ssPv2(skf3(U_788)) | ~ssPv3(U_788)))). % 16.19/8.15 tff(c_13594, plain, (![U_820]: (~ssPv3(skf3(U_820)) | ~ssPv4(skf3(skf3(U_820))) | ssPv4(skf3(U_820)) | ssPv1(skf2(skf3(U_820))) | ~ssPv4(U_820)))). % 16.19/8.15 tff(c_1809, plain, (![U_389, U_215]: (~ssPv3(skf3(U_389)) | ~ssPv4(U_215) | ~ssRr(U_215, skf3(U_389)) | ssPv4(skf3(U_389)) | ssPv1(skf2(skf3(U_389))) | ~ssPv4(U_389)))). % 16.19/8.15 tff(c_13353, plain, (![U_814]: (~ssPv2(U_814) | ssPv4(U_814) | ssPv2(skf3(U_814)) | ssPv3(U_814) | ~ssPv1(U_814) | ssPv1(skf2(U_814))))). % 16.19/8.15 tff(c_13274, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(U_2) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2)))))). % 16.19/8.15 tff(c_13273, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf3(U_1)) | ssPv3(U_1) | ~ssPv1(U_1) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1))))). % 16.19/8.15 tff(c_5275, plain, (![U_554, U_341]: (ssPv4(U_554) | ssPv2(U_341) | ~ssRr(U_341, U_554) | ssPv3(U_554) | ~ssPv1(U_554) | ssPv3(skf2(U_554)) | ssPv1(skf2(U_554))))). % 16.19/8.15 tff(c_13239, plain, (![U_1]: (~ssPv1(skf2(U_1)) | ~ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 16.19/8.15 tff(c_13207, plain, (![U_809]: (~ssPv1(skf3(U_809)) | ~ssPv1(skf2(U_809)) | ~ssPv1(U_809) | ~ssPv4(U_809) | ~ssPv3(U_809)))). % 16.19/8.15 tff(c_10378, plain, (![U_722]: (~ssPv3(skf3(U_722)) | ~ssPv1(U_722) | ~ssPv1(skf2(skf3(U_722))) | ~ssPv1(skf3(U_722)) | ~ssPv2(skf3(U_722)) | ~ssPv4(U_722)))). % 16.19/8.15 tff(c_11539, plain, (![U_758]: (ssPv4(skf3(U_758)) | ssPv1(U_758) | ssPv2(skf3(skf3(U_758))) | ssPv1(skf3(U_758)) | ~ssPv3(skf2(skf3(U_758))) | ~ssPv2(skf2(skf3(U_758)))))). % 16.19/8.15 tff(c_3640, plain, (![U_491]: (ssPv3(U_491) | ~ssPv2(skf3(U_491)) | ~ssPv1(skf3(U_491)) | ssPv3(skf3(U_491)) | ssPv1(U_491) | ~ssPv4(U_491) | ~ssPv2(U_491)))). % 16.19/8.15 tff(c_2304, plain, (![U_430, U_393]: (ssPv1(U_430) | ssPv2(U_393) | ~ssRr(U_393, skf3(U_430)) | ssPv4(skf3(U_430)) | ssPv2(U_430) | ~ssPv1(skf3(skf3(U_430)))))). % 16.19/8.15 tff(c_12683, plain, (![U_1]: (~ssPv1(skf2(U_1)) | ssPv3(U_1) | ssPv2(skf2(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ssPv2(skf3(U_1))))). % 16.19/8.15 tff(c_12533, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ssPv2(skf3(U_1)) | ssPv2(U_1) | ssPv1(skf2(U_1)) | ~ssPv4(U_1)))). % 16.19/8.15 tff(c_12716, plain, (![U_2]: (ssPv2(skf2(U_2)) | ~ssPv3(U_2) | ssPv3(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 16.19/8.15 tff(c_12715, plain, (![U_1]: (ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ssPv3(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv1(U_1)))). % 16.19/8.15 tff(c_1620, plain, (![U_1, W_360, U_361]: (ssPv4(skf3(U_1)) | ssPv3(W_360) | ~ssRr(W_360, skf3(U_1)) | ~ssPv1(U_361) | ~ssRr(U_361, skf3(U_1)) | ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.19/8.15 tff(c_12708, plain, (![U_785, U_205]: (ssPv2(U_785) | ~ssPv3(U_205) | ~ssRr(U_205, U_785) | ssPv3(U_785) | ~ssPv1(skf2(U_785)) | ~ssPv1(U_785)))). % 16.19/8.15 tff(c_12682, plain, (![U_2]: (ssPv3(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2) | ssPv2(skf2(U_2))))). % 16.19/8.15 tff(c_12609, plain, (![U_783]: (~ssPv1(skf2(U_783)) | ~ssPv3(skf2(U_783)) | ssPv3(U_783) | ssPv2(skf2(U_783))))). % 16.19/8.15 tff(c_12405, plain, (![U_781]: (~ssPv3(skf3(U_781)) | ~ssPv1(skf3(U_781)) | ~ssPv1(U_781) | ssPv2(skf3(U_781))))). % 16.19/8.15 tff(c_12336, plain, (![U_779]: (ssPv2(U_779) | ~ssPv1(skf2(U_779)) | ~ssPv1(U_779) | ~ssPv4(U_779) | ~ssPv3(U_779)))). % 16.19/8.15 tff(c_1855, plain, (![U_398]: (~ssPv1(skf3(skf3(U_398))) | ~ssPv1(skf3(U_398)) | ~ssPv3(skf3(U_398)) | ssPv4(skf3(U_398)) | ssPv1(U_398) | ~ssPv4(U_398)))). % 16.19/8.15 tff(c_11725, plain, (![U_767]: (ssPv2(skf3(skf3(U_767))) | ~ssPv4(skf3(U_767)) | ssPv3(U_767) | ssPv4(U_767) | ~ssPv2(skf3(U_767))))). % 16.19/8.15 tff(c_9519, plain, (![U_115, U_668]: (ssPv2(U_115) | ~ssPv4(skf3(U_668)) | ~ssRr(U_115, skf3(U_668)) | ssPv3(U_668) | ssPv4(U_668) | ~ssPv2(skf3(U_668))))). % 16.19/8.15 tff(c_11669, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv4(skf3(U_1)) | ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ssPv1(U_1) | ~ssPv2(U_1)))). % 16.19/8.15 tff(c_9579, plain, (![U_672, U_215]: (~ssPv3(U_672) | ~ssPv4(U_215) | ~ssRr(U_215, U_672) | ssPv4(U_672) | ~ssPv1(skf3(U_672)) | ssPv1(U_672) | ~ssPv2(U_672)))). % 16.19/8.15 tff(c_11447, plain, (![U_754]: (ssPv4(skf2(U_754)) | ssPv3(U_754) | ~ssPv1(skf3(skf2(U_754))) | ssPv3(skf2(U_754)) | ~ssPv2(skf2(U_754)) | ~ssPv3(skf2(skf2(U_754)))))). % 16.19/8.15 tff(c_9135, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ssPv1(U_1) | ~ssPv3(skf2(U_1)) | ~ssPv2(skf2(U_1))))). % 16.19/8.15 tff(c_6176, plain, (![U_330]: (~ssPv3(skf3(U_330)) | ~ssPv1(U_330) | ~ssPv1(skf3(U_330)) | ~ssPv1(skf2(skf3(U_330))) | ssPv2(skf2(skf3(U_330)))))). % 16.19/8.15 tff(c_1963, plain, (![U_401, U_402]: (ssPv4(skf3(U_401)) | ssPv1(U_401) | ssPv2(U_402) | ~ssRr(U_402, skf3(U_401)) | ssPv1(skf3(U_401)) | ~ssPv3(skf2(skf3(U_401))) | ~ssPv2(skf2(skf3(U_401)))))). % 16.19/8.15 tff(c_9893, plain, (![U_1]: (~ssPv3(U_1) | ssPv1(skf2(U_1)) | ssPv2(skf2(U_1)) | ssPv3(skf3(U_1)) | ssPv1(skf3(U_1)) | ssPv4(U_1)))). % 16.19/8.15 tff(c_11448, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2)))))). % 16.19/8.15 tff(c_10038, plain, (![U_2, U_704]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_704) | ~ssRr(U_704, skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_10430, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_11395, plain, (![U_750]: (ssPv4(skf3(U_750)) | ssPv1(skf2(skf3(U_750))) | ssPv2(skf3(skf3(U_750))) | ssPv3(skf3(U_750)) | ~ssPv2(skf3(U_750)) | ~ssPv3(U_750)))). % 16.19/8.16 tff(c_1468, plain, (![U_1, U_346]: (ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ssPv2(U_346) | ~ssRr(U_346, skf3(U_1)) | ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.19/8.16 tff(c_11235, plain, (![U_745]: (ssPv4(skf3(U_745)) | ssPv1(U_745) | ssPv2(skf3(skf3(U_745))) | ssPv3(skf3(U_745)) | ~ssPv2(skf3(U_745)) | ~ssPv3(skf2(skf3(U_745)))))). % 16.19/8.16 tff(c_11310, plain, (![U_320]: (~ssPv1(skf3(skf3(U_320))) | ssPv4(U_320) | ~ssPv4(skf3(U_320)) | ~ssPv3(skf3(U_320))))). % 16.19/8.16 tff(c_1960, plain, (![U_401, U_402]: (ssPv4(skf3(U_401)) | ssPv1(U_401) | ssPv2(U_402) | ~ssRr(U_402, skf3(U_401)) | ssPv3(skf3(U_401)) | ~ssPv2(skf3(U_401)) | ~ssPv3(skf2(skf3(U_401)))))). % 16.19/8.16 tff(c_10896, plain, (![U_319]: (~ssPv1(skf3(skf3(U_319))) | ~ssPv3(U_319) | ~ssPv4(skf3(U_319)) | ~ssPv3(skf3(U_319))))). % 16.19/8.16 tff(c_10463, plain, (![U_728]: (ssPv2(skf3(U_728)) | ssPv4(U_728) | ~ssPv1(skf3(U_728)) | ssPv3(U_728) | ~ssPv2(U_728) | ~ssPv3(skf2(U_728))))). % 16.19/8.16 tff(c_10429, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(skf2(U_1))))). % 16.19/8.16 tff(c_10037, plain, (![U_1, U_704]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(U_704) | ~ssRr(U_704, U_1) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(skf2(U_1))))). % 16.19/8.16 tff(c_10386, plain, (![U_723]: (~ssPv3(skf3(U_723)) | ~ssPv4(skf3(skf3(U_723))) | ssPv4(skf3(U_723)) | ssPv1(U_723) | ~ssPv4(U_723)))). % 16.19/8.16 tff(c_1856, plain, (![U_398, U_215]: (~ssPv3(skf3(U_398)) | ~ssPv4(U_215) | ~ssRr(U_215, skf3(U_398)) | ssPv4(skf3(U_398)) | ssPv1(U_398) | ~ssPv4(U_398)))). % 16.19/8.16 tff(c_1657, plain, (![U_367]: (~ssPv1(skf2(skf3(U_367))) | ~ssPv1(skf3(U_367)) | ssPv3(skf2(skf3(U_367))) | ~ssPv2(skf3(U_367)) | ~ssPv4(U_367)))). % 16.19/8.16 tff(c_2828, plain, (![U_454]: (ssPv1(skf3(U_454)) | ssPv3(skf2(skf3(U_454))) | ssPv3(skf3(skf3(U_454))) | ~ssPv2(skf3(U_454)) | ~ssPv1(U_454)))). % 16.19/8.16 tff(c_10242, plain, (![U_2]: (~ssPv3(skf2(U_2)) | ~ssPv4(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_10241, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv4(skf3(U_1)) | ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_10013, plain, (![U_700, U_215]: (~ssPv3(U_700) | ~ssPv4(U_215) | ~ssRr(U_215, U_700) | ssPv4(U_700) | ~ssPv1(skf3(U_700)) | ssPv2(skf2(U_700))))). % 16.19/8.16 tff(c_9450, plain, (![U_666]: (ssPv4(U_666) | ssPv1(skf2(U_666)) | ~ssPv2(skf2(U_666)) | ssPv1(U_666) | ~ssPv2(U_666) | ssPv2(skf3(U_666))))). % 16.19/8.16 tff(c_10144, plain, (![U_711]: (~ssPv1(skf2(U_711)) | ~ssPv2(U_711) | ssPv4(skf2(U_711)) | ~ssPv3(skf2(U_711)) | ~ssPv2(skf2(U_711))))). % 16.19/8.16 tff(c_9657, plain, (![U_676]: (~ssPv1(skf3(skf2(U_676))) | ~ssPv1(skf2(U_676)) | ssPv4(skf2(U_676)) | ~ssPv3(skf2(U_676)) | ~ssPv2(U_676)))). % 16.19/8.16 tff(c_10090, plain, (![U_707]: (ssPv4(skf2(U_707)) | ssPv3(U_707) | ~ssPv1(skf3(skf2(U_707))) | ssPv2(skf2(skf2(U_707)))))). % 16.19/8.16 tff(c_10091, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2) | ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_9953, plain, (![U_2, U_696]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_696) | ~ssRr(U_696, skf2(U_2)) | ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_9399, plain, (![U_280]: (~ssPv3(skf3(U_280)) | ssPv2(skf3(skf3(U_280))) | ssPv2(skf3(U_280)) | ssPv1(U_280) | ~ssPv4(skf3(U_280))))). % 16.19/8.16 tff(c_9960, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv1(U_2) | ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_1621, plain, (![U_2, W_360, U_361]: (ssPv4(U_2) | ssPv3(W_360) | ~ssRr(W_360, U_2) | ~ssPv1(U_361) | ~ssRr(U_361, U_2) | ssPv3(U_2) | ~ssPv2(U_2) | ~ssPv3(skf2(U_2))))). % 16.19/8.16 tff(c_9999, plain, (![U_699]: (~ssPv1(U_699) | ~ssPv3(U_699) | ssPv4(U_699) | ~ssPv1(skf3(U_699)) | ssPv2(skf2(U_699))))). % 16.19/8.16 tff(c_9993, plain, (![U_699]: (ssPv2(skf3(U_699)) | ssPv4(U_699) | ~ssPv1(skf3(U_699)) | ssPv2(skf2(U_699))))). % 16.19/8.16 tff(c_9959, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_9952, plain, (![U_1, U_696]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(U_696) | ~ssRr(U_696, U_1) | ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_9297, plain, (![U_2, W_234, U_236]: (ssPv4(U_2) | ssPv3(W_234) | ~ssRr(W_234, U_2) | ~ssPv1(U_236) | ~ssRr(U_236, U_2) | ssPv2(skf2(U_2))))). % 16.19/8.16 tff(c_9844, plain, (![U_2]: (~ssPv3(skf2(U_2)) | ~ssPv4(U_2) | ssPv4(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_9916, plain, (![U_690]: (ssPv4(skf3(U_690)) | ssPv1(U_690) | ssPv2(skf3(skf3(U_690))) | ssPv2(skf2(skf3(U_690)))))). % 16.19/8.16 tff(c_9294, plain, (![U_392, U_393]: (ssPv4(skf3(U_392)) | ssPv1(U_392) | ssPv2(U_393) | ~ssRr(U_393, skf3(U_392)) | ssPv2(skf2(skf3(U_392)))))). % 16.19/8.16 tff(c_8761, plain, (![U_650]: (~ssPv1(skf3(U_650)) | ~ssPv1(U_650) | ~ssPv3(U_650) | ssPv4(U_650) | ssPv1(skf2(U_650)) | ssPv2(skf2(U_650))))). % 16.19/8.16 tff(c_9843, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv4(skf3(U_1)) | ssPv4(U_1) | ssPv1(skf2(U_1)) | ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_8762, plain, (![U_650, U_215]: (~ssPv3(U_650) | ~ssPv4(U_215) | ~ssRr(U_215, U_650) | ssPv4(U_650) | ssPv1(skf2(U_650)) | ssPv2(skf2(U_650))))). % 16.19/8.16 tff(c_9296, plain, (![U_384]: (ssPv2(skf2(U_384)) | ssPv1(skf2(skf2(U_384))) | ssPv4(U_384) | ssPv2(skf3(skf2(U_384)))))). % 16.19/8.16 tff(c_8876, plain, (![U_654]: (ssPv4(skf2(U_654)) | ssPv3(U_654) | ~ssPv1(skf3(skf2(U_654))) | ssPv1(skf2(U_654)) | ~ssPv3(skf2(skf2(U_654))) | ~ssPv2(skf2(skf2(U_654)))))). % 16.19/8.16 tff(c_9769, plain, (![U_682]: (ssPv3(skf3(U_682)) | ssPv4(U_682) | ~ssPv2(skf3(U_682)) | ssPv2(skf2(skf3(U_682)))))). % 16.19/8.16 tff(c_9293, plain, (![U_406]: (ssPv3(skf2(skf3(U_406))) | ssPv4(U_406) | ~ssPv2(skf3(U_406)) | ssPv2(skf2(skf3(U_406)))))). % 16.19/8.16 tff(c_9144, plain, (![U_477]: (ssPv2(skf3(skf3(U_477))) | ssPv4(skf3(U_477)) | ~ssPv4(U_477) | ~ssPv1(skf3(skf3(U_477)))))). % 16.19/8.16 tff(c_401, plain, (![U_202]: (ssPv3(skf2(skf3(U_202))) | ~ssPv1(skf2(skf3(U_202))) | ~ssPv1(skf3(U_202)) | ssPv3(skf3(U_202)) | ~ssPv2(skf3(U_202)) | ~ssPv3(U_202)))). % 16.19/8.16 tff(c_9396, plain, (![U_319]: (ssPv2(skf3(skf3(U_319))) | ~ssPv3(U_319) | ~ssPv4(skf3(U_319)) | ~ssPv3(skf3(U_319))))). % 16.19/8.16 tff(c_9397, plain, (![U_320]: (ssPv2(skf3(skf3(U_320))) | ssPv4(U_320) | ~ssPv4(skf3(U_320)) | ~ssPv3(skf3(U_320))))). % 16.19/8.16 tff(c_9401, plain, (![U_1]: (~ssPv3(U_1) | ssPv2(skf3(U_1)) | ssPv2(U_1) | ssPv1(skf2(U_1)) | ~ssPv4(U_1)))). % 16.19/8.16 tff(c_9305, plain, (![U_300]: (ssPv4(skf2(U_300)) | ~ssPv3(skf2(U_300)) | ~ssPv2(U_300) | ssPv2(skf3(skf2(U_300)))))). % 16.19/8.16 tff(c_8877, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_2) | ssPv1(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_9304, plain, (![U_302]: (ssPv1(skf3(U_302)) | ssPv3(U_302) | ~ssPv2(skf3(U_302)) | ssPv2(skf3(skf3(U_302)))))). % 16.19/8.16 tff(c_9301, plain, (![U_315]: (~ssPv4(skf3(U_315)) | ~ssPv3(skf3(U_315)) | ~ssPv3(U_315) | ssPv2(skf2(skf3(U_315)))))). % 16.19/8.16 tff(c_9134, plain, (![U_624]: (ssPv4(U_624) | ~ssPv1(skf3(U_624)) | ssPv1(U_624) | ~ssPv2(U_624) | ssPv2(skf3(U_624))))). % 16.19/8.16 tff(c_9141, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 16.19/8.16 tff(c_9381, plain, (![U_624]: (~ssPv3(U_624) | ~ssPv4(U_624) | ssPv1(U_624) | ~ssPv2(U_624) | ssPv2(skf3(U_624))))). % 16.19/8.16 tff(c_9292, plain, (![U_438]: (ssPv3(U_438) | ssPv4(U_438) | ~ssPv2(skf3(U_438)) | ssPv2(skf2(skf3(U_438)))))). % 16.19/8.16 tff(c_9308, plain, (![U_2]: (ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2) | ssPv2(skf2(U_2))))). % 16.19/8.16 tff(c_9306, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf2(U_1)) | ~ssPv2(U_1) | ssPv2(skf3(U_1))))). % 16.19/8.16 tff(c_9215, plain, (![U_661]: (ssPv4(skf3(U_661)) | ssPv1(U_661) | ssPv2(skf3(skf3(U_661))) | ssPv3(skf3(U_661)) | ~ssPv2(skf3(U_661)) | ~ssPv3(U_661)))). % 16.19/8.16 tff(c_9302, plain, (![U_1]: (~ssPv3(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv4(U_1) | ssPv2(skf3(U_1))))). % 16.19/8.16 tff(c_9202, plain, (![U_1]: (ssPv2(U_1) | ssPv4(U_1)))). % 16.19/8.16 tff(c_1959, plain, (![U_1, U_402]: (ssPv4(skf3(U_1)) | ssPv1(U_1) | ssPv2(U_402) | ~ssRr(U_402, skf3(U_1)) | ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.19/8.16 tff(c_9035, plain, (![U_657]: (ssPv4(U_657) | ~ssPv3(skf3(U_657)) | ~ssPv1(skf3(U_657)) | ssPv2(skf3(U_657))))). % 16.19/8.16 tff(c_4124, plain, (![U_2, U_519]: (ssPv4(skf2(U_2)) | ssPv3(U_2) | ~ssPv1(U_519) | ~ssRr(U_519, skf2(U_2)) | ssPv1(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_8746, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(U_2) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_866, plain, (![U_306]: (ssPv1(skf3(U_306)) | ssPv3(U_306) | ~ssPv2(skf3(U_306)) | ssPv3(skf3(skf3(U_306))) | ssPv1(skf3(skf3(U_306))) | ssPv4(skf3(U_306))))). % 16.19/8.16 tff(c_8745, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf3(U_1)) | ssPv1(skf2(U_1)) | ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_8244, plain, (![U_2, U_341]: (ssPv4(U_2) | ssPv2(U_341) | ~ssRr(U_341, U_2) | ssPv1(skf2(U_2)) | ssPv2(skf2(U_2))))). % 16.19/8.16 tff(c_6702, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv1(U_2) | ssPv1(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_7058, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ssPv2(U_2) | ssPv1(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_7634, plain, (![U_624]: (ssPv1(U_624) | ssPv3(skf3(U_624)) | ~ssPv2(U_624) | ssPv2(skf3(U_624))))). % 16.19/8.16 tff(c_5870, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ssPv2(U_2) | ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2)))))). % 16.19/8.16 tff(c_7198, plain, (![U_610]: (~ssPv3(U_610) | ~ssPv1(skf3(U_610)) | ssPv2(U_610) | ssPv1(skf2(U_610)) | ~ssPv4(U_610)))). % 16.19/8.16 tff(c_7057, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ssPv1(U_1) | ~ssPv3(skf2(U_1)) | ~ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_1474, plain, (![U_2, U_346]: (ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_346) | ~ssRr(U_346, U_2) | ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2))))). % 16.19/8.16 tff(c_6701, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv1(U_1) | ~ssPv3(skf2(U_1)) | ~ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_4343, plain, (![U_1]: (ssPv1(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ssPv2(U_1) | ssPv4(skf2(U_1)) | ~ssPv1(U_1)))). % 16.19/8.16 tff(c_3650, plain, (![U_491]: (ssPv1(skf3(U_491)) | ~ssPv2(skf3(U_491)) | ssPv3(skf3(U_491)) | ssPv1(U_491) | ~ssPv4(U_491) | ~ssPv2(U_491)))). % 16.19/8.16 tff(c_4123, plain, (![U_1, U_519]: (ssPv4(U_1) | ssPv3(skf3(U_1)) | ~ssPv1(U_519) | ~ssRr(U_519, U_1) | ssPv1(U_1) | ~ssPv3(skf2(U_1)) | ~ssPv2(skf2(U_1))))). % 16.19/8.16 tff(c_6617, plain, (![U_590]: (~ssPv1(skf2(U_590)) | ~ssPv3(skf3(skf2(U_590))) | ssPv2(skf2(U_590)) | ssPv3(U_590) | ~ssPv4(skf2(U_590))))). % 16.19/8.16 tff(c_361, plain, (![U_2, U_189]: (~ssPv1(skf2(U_2)) | ~ssPv3(U_189) | ~ssRr(U_189, skf2(U_2)) | ssPv2(skf2(U_2)) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 16.19/8.16 tff(c_3644, plain, (![U_302]: (ssPv3(U_302) | ssPv3(skf3(skf3(U_302))) | ssPv1(skf3(U_302)) | ~ssPv4(skf3(U_302)) | ~ssPv2(skf3(U_302))))). % 16.19/8.16 tff(c_6348, plain, (![U_581]: (ssPv1(U_581) | ssPv2(skf3(skf3(U_581))) | ssPv4(skf3(U_581)) | ssPv3(skf3(U_581)) | ssPv1(skf3(U_581))))). % 16.19/8.16 tff(c_5581, plain, (![U_319]: (~ssPv3(U_319) | ~ssPv3(skf3(U_319)) | ~ssPv4(skf3(U_319)) | ~ssPv2(skf3(U_319)) | ~ssPv1(skf3(U_319))))). % 16.19/8.16 tff(c_1965, plain, (![U_401, U_402]: (ssPv1(U_401) | ssPv2(U_402) | ~ssRr(U_402, skf3(U_401)) | ssPv4(skf3(U_401)) | ssPv3(skf3(U_401)) | ssPv1(skf3(U_401))))). % 16.19/8.16 tff(c_5869, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(skf2(U_1))))). % 16.19/8.16 tff(c_1469, plain, (![U_2, U_346]: (ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_346) | ~ssRr(U_346, U_2) | ssPv3(U_2) | ~ssPv2(U_2) | ~ssPv3(skf2(U_2))))). % 16.19/8.16 tff(c_5583, plain, (![U_320]: (ssPv4(U_320) | ~ssPv3(skf3(U_320)) | ~ssPv4(skf3(U_320)) | ~ssPv2(skf3(U_320)) | ~ssPv1(skf3(U_320))))). % 16.19/8.16 tff(c_5550, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv4(U_1) | ssPv1(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 16.19/8.16 tff(c_5245, plain, (![U_552]: (ssPv3(U_552) | ~ssPv1(skf3(skf2(U_552))) | ssPv4(skf2(U_552)) | ssPv3(skf2(U_552)) | ssPv1(skf2(U_552))))). % 16.19/8.16 tff(c_5246, plain, (![U_2]: (ssPv3(U_2) | ~ssPv1(U_2) | ssPv4(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2))))). % 16.19/8.16 tff(c_3715, plain, (![U_2, U_496]: (ssPv3(U_2) | ~ssPv1(U_496) | ~ssRr(U_496, skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2))))). % 16.19/8.16 tff(c_897, plain, (![U_309]: (ssPv1(skf3(skf3(U_309))) | ~ssPv2(skf3(skf3(U_309))) | ssPv1(skf3(U_309)) | ssPv4(U_309) | ~ssPv4(skf3(U_309))))). % 16.19/8.16 tff(c_4989, plain, (![U_2]: (ssPv1(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ssPv4(U_2) | ssPv3(U_2) | ssPv1(U_2)))). % 16.19/8.16 tff(c_849, plain, (![U_305]: (~ssPv3(skf2(U_305)) | ~ssPv2(U_305) | ssPv3(skf3(skf2(U_305))) | ssPv1(skf3(skf2(U_305))) | ssPv4(skf2(U_305))))). % 16.19/8.16 tff(c_4683, plain, (![U_538]: (~ssPv3(U_538) | ~ssPv1(skf3(U_538)) | ~ssPv4(U_538) | ~ssPv3(skf3(U_538)) | ~ssPv2(skf3(U_538))))). % 16.19/8.16 tff(c_4622, plain, (![U_537]: (~ssPv1(skf3(U_537)) | ~ssPv4(U_537) | ssPv4(skf3(U_537)) | ~ssPv3(skf3(U_537)) | ~ssPv2(skf3(U_537))))). % 16.19/8.16 tff(c_3251, plain, (![U_479]: (~ssPv1(skf3(U_479)) | ~ssPv3(skf3(U_479)) | ssPv4(skf3(U_479)) | ~ssPv4(U_479) | ~ssPv1(skf3(skf3(U_479)))))). % 16.19/8.16 tff(c_4335, plain, (![U_529]: (~ssPv3(U_529) | ~ssPv3(skf3(U_529)) | ssPv2(skf3(U_529)) | ssPv1(skf3(U_529))))). % 16.19/8.16 tff(c_280, plain, (![U_163]: (ssPv3(skf2(skf2(U_163))) | ~ssPv1(skf2(skf2(U_163))) | ssPv2(skf2(U_163)) | ssPv4(U_163) | ~ssPv1(skf2(U_163))))). % 16.19/8.16 tff(c_4282, plain, (![U_319]: (ssPv1(skf3(U_319)) | ~ssPv3(U_319) | ~ssPv4(skf3(U_319)) | ~ssPv3(skf3(U_319))))). % 16.19/8.16 tff(c_3560, plain, (![U_2]: (ssPv3(skf3(skf2(U_2))) | ssPv4(U_2) | ssPv1(skf2(U_2)) | ~ssPv4(skf2(U_2)) | ~ssPv2(skf2(U_2))))). % 16.19/8.16 tff(c_1626, plain, (![U_2, W_360, U_361]: (ssPv4(U_2) | ssPv3(W_360) | ~ssRr(W_360, U_2) | ~ssPv1(U_361) | ~ssRr(U_361, U_2) | ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2))))). % 16.19/8.16 tff(c_3746, plain, (![U_2]: (ssPv3(skf3(skf2(U_2))) | ~ssPv1(U_2) | ssPv4(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2))))). % 16.19/8.16 tff(c_3745, plain, (![U_1]: (ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 16.19/8.16 tff(c_3714, plain, (![U_1, U_496]: (ssPv3(skf3(U_1)) | ~ssPv1(U_496) | ~ssRr(U_496, U_1) | ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 16.19/8.16 tff(c_3188, plain, (![U_399]: (ssPv2(skf3(skf2(U_399))) | ~ssPv1(U_399) | ssPv1(skf3(skf2(U_399))) | ssPv4(skf2(U_399))))). % 16.19/8.17 tff(c_1628, plain, (![W_360, U_2, U_361]: (ssPv3(W_360) | ~ssRr(W_360, U_2) | ~ssPv1(U_361) | ~ssRr(U_361, U_2) | ssPv4(U_2) | ssPv3(U_2) | ssPv1(U_2)))). % 16.19/8.17 tff(c_3649, plain, (![U_491]: (ssPv3(skf2(U_491)) | ssPv3(skf3(U_491)) | ssPv1(U_491) | ~ssPv4(U_491) | ~ssPv2(U_491)))). % 16.19/8.17 tff(c_3559, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv1(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 16.19/8.17 tff(c_3491, plain, (![U_1, U_485]: (ssPv3(skf3(U_1)) | ssPv4(U_485) | ~ssRr(U_485, U_1) | ssPv1(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 16.43/8.17 tff(c_1763, plain, (![W_381, U_382, U_2]: (ssPv3(W_381) | ssPv4(U_382) | ~ssRr(W_381, U_2) | ~ssRr(U_382, U_2) | ssPv1(U_2) | ~ssPv4(U_2) | ~ssPv2(U_2)))). % 16.43/8.17 tff(c_3224, plain, (![U_477]: (ssPv4(skf3(U_477)) | ssPv3(skf3(skf3(U_477))) | ~ssPv4(U_477) | ~ssPv1(skf3(skf3(U_477)))))). % 16.43/8.17 tff(c_3211, plain, (![U_473, U_475]: (ssPv4(skf3(U_473)) | ssPv3(skf3(skf3(U_473))) | ~ssPv4(U_473) | ~ssPv1(U_475) | ~ssRr(U_475, skf3(U_473))))). % 16.43/8.17 tff(c_498, plain, (![U_1, W_234, U_236]: (ssPv4(skf3(U_1)) | ssPv3(W_234) | ~ssPv4(U_1) | ~ssRr(W_234, skf3(U_1)) | ~ssPv1(U_236) | ~ssRr(U_236, skf3(U_1))))). % 16.43/8.17 tff(c_3193, plain, (![U_271]: (ssPv2(skf3(U_271)) | ~ssPv2(U_271) | ssPv1(skf3(U_271)) | ssPv4(U_271)))). % 16.43/8.17 tff(c_3120, plain, (![U_470]: (ssPv4(U_470) | ~ssPv3(skf3(U_470)) | ssPv2(skf3(U_470)) | ssPv1(skf3(U_470))))). % 16.43/8.17 tff(c_3077, plain, (![U_320]: (ssPv1(skf3(U_320)) | ssPv4(U_320) | ~ssPv4(skf3(U_320)) | ~ssPv3(skf3(U_320))))). % 16.43/8.17 tff(c_1031, plain, (![U_319]: (~ssPv3(skf3(U_319)) | ~ssPv3(U_319) | ~ssPv3(skf2(skf3(U_319))) | ~ssPv2(skf3(U_319)) | ~ssPv4(skf3(U_319))))). % 16.43/8.17 tff(c_1237, plain, (![U_333]: (~ssPv3(skf3(U_333)) | ~ssPv1(U_333) | ssPv1(skf3(skf3(U_333))) | ~ssPv2(skf3(U_333)) | ~ssPv1(skf3(U_333))))). % 16.43/8.17 tff(c_2954, plain, (![U_460, U_462]: (ssPv2(skf3(U_460)) | ssPv1(U_460) | ssPv4(skf3(skf3(U_460))) | ~ssPv4(U_462) | ~ssRr(U_462, skf3(U_460))))). % 16.43/8.17 tff(c_757, plain, (![U_1, W_293, U_294]: (ssPv2(skf3(U_1)) | ssPv1(U_1) | ssPv4(W_293) | ~ssRr(W_293, skf3(U_1)) | ~ssPv4(U_294) | ~ssRr(U_294, skf3(U_1))))). % 16.43/8.17 tff(c_168, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf2(U_1)) | ~ssPv2(U_1) | ssPv3(skf3(U_1)) | ssPv1(skf3(U_1)) | ssPv4(U_1)))). % 16.43/8.17 tff(c_2825, plain, (![U_454]: (ssPv1(skf3(U_454)) | ssPv3(U_454) | ssPv3(skf3(skf3(U_454))) | ~ssPv2(skf3(U_454)) | ~ssPv1(U_454)))). % 16.43/8.17 tff(c_2792, plain, (![U_452]: (ssPv3(skf3(skf3(U_452))) | ssPv4(skf3(skf3(U_452))) | ~ssPv2(skf3(U_452)) | ~ssPv1(U_452)))). % 16.43/8.17 tff(c_2721, plain, (![U_449, U_448]: (ssPv3(skf3(skf3(U_449))) | ssPv4(U_448) | ~ssPv2(skf3(U_449)) | ~ssPv1(U_449) | ~ssRr(U_448, skf3(U_449))))). % 16.43/8.17 tff(c_2762, plain, (![U_1]: (~ssPv2(skf3(U_1)) | ssPv3(skf3(U_1)) | ssPv1(skf3(U_1)) | ssPv4(U_1)))). % 16.43/8.17 tff(c_672, plain, (![W_272, U_273, U_1]: (ssPv3(W_272) | ssPv4(U_273) | ~ssPv2(skf3(U_1)) | ~ssPv1(U_1) | ~ssRr(W_272, skf3(U_1)) | ~ssRr(U_273, skf3(U_1))))). % 16.43/8.17 tff(c_569, plain, (![U_250]: (~ssPv1(skf3(U_250)) | ~ssPv1(U_250) | ssPv2(skf3(U_250)) | ssPv1(skf2(skf3(U_250))) | ~ssPv4(skf3(U_250))))). % 16.43/8.17 tff(c_2663, plain, (![U_1]: (ssPv3(U_1) | ssPv4(skf2(skf3(U_1))) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_1)))). % 16.43/8.17 tff(c_2556, plain, (![U_435, V_437]: (ssPv3(U_435) | ssPv4(skf2(skf3(U_435))) | ~ssPv2(skf3(U_435)) | ~ssPv4(V_437) | ~ssRr(skf3(U_435), V_437)))). % 16.43/8.17 tff(c_2635, plain, (![U_440]: (ssPv3(U_440) | ssPv4(U_440) | ~ssPv3(skf2(skf3(U_440))) | ~ssPv2(skf3(U_440)) | ~ssPv4(skf3(U_440))))). % 16.43/8.17 tff(c_2566, plain, (![U_438]: (ssPv3(U_438) | ssPv4(U_438) | ~ssPv2(skf3(U_438)) | ~ssPv4(skf2(skf3(U_438)))))). % 16.43/8.17 tff(c_2555, plain, (![U_1, V_437]: (ssPv3(U_1) | ssPv4(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(V_437) | ~ssRr(skf3(U_1), V_437)))). % 16.43/8.17 tff(c_583, plain, (![U_1, W_254, V_256]: (ssPv3(U_1) | ssPv4(W_254) | ~ssPv2(skf3(U_1)) | ~ssRr(skf3(U_1), W_254) | ~ssPv4(V_256) | ~ssRr(skf3(U_1), V_256)))). % 16.43/8.17 tff(c_2286, plain, (![U_428]: (ssPv4(skf3(U_428)) | ssPv2(U_428) | ssPv4(skf2(skf3(U_428))) | ~ssPv1(skf3(skf3(U_428)))))). % 16.43/8.17 tff(c_2201, plain, (![U_421, U_423]: (ssPv4(skf3(U_421)) | ssPv2(U_421) | ssPv4(skf2(skf3(U_421))) | ~ssPv1(U_423) | ~ssRr(U_423, skf3(U_421))))). % 16.43/8.17 tff(c_713, plain, (![U_1, W_285, U_286]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ssPv4(W_285) | ~ssRr(skf3(U_1), W_285) | ~ssPv1(U_286) | ~ssRr(U_286, skf3(U_1))))). % 16.43/8.17 tff(c_610, plain, (![U_260]: (ssPv3(skf3(U_260)) | ~ssPv2(U_260) | ssPv2(skf3(U_260)) | ssPv1(skf2(skf3(U_260))) | ~ssPv4(skf3(U_260))))). % 16.43/8.17 tff(c_224, plain, (![U_148]: (ssPv3(skf2(U_148)) | ~ssPv1(skf2(U_148)) | ~ssPv1(U_148) | ssPv3(skf3(U_148)) | ~ssPv4(U_148) | ~ssPv3(U_148)))). % 16.43/8.17 tff(c_863, plain, (![U_306]: (ssPv3(U_306) | ~ssPv2(skf3(U_306)) | ssPv1(skf3(U_306)) | ssPv4(skf2(skf3(U_306))) | ~ssPv4(skf3(U_306))))). % 16.43/8.17 tff(c_1495, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ssPv2(U_2) | ssPv4(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2))))). % 16.43/8.17 tff(c_1995, plain, (![U_408, U_410]: (ssPv4(skf2(U_408)) | ssPv1(U_408) | ~ssPv1(skf3(skf2(U_408))) | ~ssPv4(U_410) | ~ssRr(U_410, skf2(U_408))))). % 16.43/8.17 tff(c_1988, plain, (![U_406]: (ssPv3(skf2(skf3(U_406))) | ssPv4(U_406) | ~ssPv2(skf3(U_406)) | ~ssPv4(skf2(skf3(U_406)))))). % 16.43/8.17 tff(c_634, plain, (![U_2, W_266, U_267]: (ssPv4(skf2(U_2)) | ssPv1(U_2) | ~ssPv1(W_266) | ~ssRr(W_266, skf2(U_2)) | ~ssPv4(U_267) | ~ssRr(U_267, skf2(U_2))))). % 16.43/8.17 tff(c_1634, plain, (![U_1, V_364]: (ssPv3(skf2(skf3(U_1))) | ssPv4(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(V_364) | ~ssRr(skf3(U_1), V_364)))). % 16.43/8.17 tff(c_1970, plain, (![U_403]: (ssPv4(skf3(U_403)) | ssPv2(skf2(skf3(U_403))) | ssPv4(U_403) | ~ssPv1(skf3(skf3(U_403)))))). % 16.43/8.17 tff(c_1663, plain, (![U_1, U_370]: (ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ssPv4(U_1) | ~ssPv1(U_370) | ~ssRr(U_370, skf3(U_1))))). % 16.43/8.17 tff(c_1825, plain, (![U_392, U_393]: (ssPv4(skf3(U_392)) | ssPv1(U_392) | ssPv2(U_393) | ~ssPv4(skf2(skf3(U_392))) | ~ssRr(U_393, skf3(U_392))))). % 16.43/8.17 tff(c_1881, plain, (![U_399]: (~ssPv1(U_399) | ssPv3(skf3(skf2(U_399))) | ssPv1(skf3(skf2(U_399))) | ssPv4(skf2(U_399))))). % 16.43/8.17 tff(c_1816, plain, (![U_390]: (ssPv4(skf2(U_390)) | ssPv1(skf3(skf2(U_390))) | ~ssPv1(U_390) | ~ssPv4(skf3(skf2(U_390)))))). % 16.43/8.17 tff(c_1848, plain, (![U_396]: (ssPv4(skf3(U_396)) | ssPv1(U_396) | ssPv2(skf3(skf3(U_396))) | ~ssPv4(U_396)))). % 16.43/8.17 tff(c_1824, plain, (![U_1, U_393]: (ssPv4(skf3(U_1)) | ssPv1(U_1) | ssPv2(U_393) | ~ssPv4(U_1) | ~ssRr(U_393, skf3(U_1))))). % 16.43/8.17 tff(c_1817, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv1(skf3(skf2(U_2))) | ~ssPv1(U_2) | ~ssPv4(U_2)))). % 16.43/8.17 tff(c_547, plain, (![U_1, U_246, W_247]: (ssPv4(skf3(U_1)) | ssPv1(U_1) | ssPv2(U_246) | ~ssPv4(W_247) | ~ssRr(skf3(U_1), W_247) | ~ssRr(U_246, skf3(U_1))))). % 16.43/8.17 tff(c_1551, plain, (![U_2, U_356]: (ssPv4(skf2(U_2)) | ssPv1(skf3(skf2(U_2))) | ~ssPv1(U_2) | ~ssPv4(U_356) | ~ssRr(U_356, skf2(U_2))))). % 16.43/8.17 tff(c_1801, plain, (![U_387]: (ssPv4(skf3(U_387)) | ssPv1(skf2(skf3(U_387))) | ssPv2(skf3(skf3(U_387))) | ~ssPv4(U_387)))). % 16.43/8.17 tff(c_1358, plain, (![U_1, U_341]: (ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ssPv2(U_341) | ~ssPv4(U_1) | ~ssRr(U_341, skf3(U_1))))). % 16.43/8.17 tff(c_1770, plain, (![U_384]: (ssPv2(skf2(U_384)) | ssPv1(skf2(skf2(U_384))) | ssPv4(U_384) | ~ssPv4(skf3(skf2(U_384)))))). % 16.43/8.17 tff(c_1693, plain, (![U_2, U_376]: (ssPv2(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ssPv4(U_2) | ~ssPv4(U_376) | ~ssRr(U_376, skf2(U_2))))). % 16.43/8.17 tff(c_673, plain, (![W_272, U_273, U_2]: (ssPv3(W_272) | ssPv4(U_273) | ~ssPv2(U_2) | ~ssPv1(skf2(U_2)) | ~ssRr(W_272, U_2) | ~ssRr(U_273, U_2)))). % 16.43/8.17 tff(c_1700, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ssPv4(skf3(skf2(U_2))) | ~ssPv4(U_2)))). % 16.43/8.17 tff(c_1692, plain, (![U_1, U_376]: (ssPv2(U_1) | ssPv1(skf2(U_1)) | ssPv4(skf3(U_1)) | ~ssPv4(U_376) | ~ssRr(U_376, U_1)))). % 16.43/8.17 tff(c_758, plain, (![U_2, W_293, U_294]: (ssPv2(U_2) | ssPv1(skf2(U_2)) | ssPv4(W_293) | ~ssRr(W_293, U_2) | ~ssPv4(U_294) | ~ssRr(U_294, U_2)))). % 16.43/8.17 tff(c_714, plain, (![U_2, W_285, U_286]: (ssPv4(U_2) | ssPv2(skf2(U_2)) | ssPv4(W_285) | ~ssRr(U_2, W_285) | ~ssPv1(U_286) | ~ssRr(U_286, U_2)))). % 16.43/8.17 tff(c_1641, plain, (![U_1]: (ssPv3(skf2(skf3(U_1))) | ssPv4(skf2(skf3(U_1))) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_1)))). % 16.43/8.17 tff(c_1635, plain, (![U_2, V_364]: (ssPv3(skf2(U_2)) | ssPv4(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv4(V_364) | ~ssRr(U_2, V_364)))). % 16.43/8.17 tff(c_584, plain, (![U_2, W_254, V_256]: (ssPv3(skf2(U_2)) | ssPv4(W_254) | ~ssPv2(U_2) | ~ssRr(U_2, W_254) | ~ssPv4(V_256) | ~ssRr(U_2, V_256)))). % 16.43/8.17 tff(c_499, plain, (![U_2, W_234, U_236]: (ssPv4(U_2) | ssPv3(W_234) | ~ssPv4(skf2(U_2)) | ~ssRr(W_234, U_2) | ~ssPv1(U_236) | ~ssRr(U_236, U_2)))). % 16.43/8.17 tff(c_633, plain, (![U_1, W_266, U_267]: (ssPv4(U_1) | ssPv1(skf3(U_1)) | ~ssPv1(W_266) | ~ssRr(W_266, U_1) | ~ssPv4(U_267) | ~ssRr(U_267, U_1)))). % 16.43/8.17 tff(c_984, plain, (![U_1]: (~ssPv3(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv4(U_1) | ssPv2(U_1) | ssPv4(skf2(U_1)) | ~ssPv1(U_1)))). % 16.43/8.17 tff(c_1494, plain, (![U_1]: (ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 16.43/8.17 tff(c_1476, plain, (![U_2, U_346]: (ssPv1(skf2(U_2)) | ssPv2(U_346) | ~ssRr(U_346, U_2) | ssPv4(U_2) | ssPv3(U_2) | ssPv1(U_2)))). % 16.43/8.17 tff(c_1359, plain, (![U_2, U_341]: (ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_341) | ~ssPv4(skf2(U_2)) | ~ssRr(U_341, U_2)))). % 16.43/8.17 tff(c_548, plain, (![U_2, U_246, W_247]: (ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_246) | ~ssPv4(W_247) | ~ssRr(U_2, W_247) | ~ssRr(U_246, U_2)))). % 16.43/8.17 tff(c_589, plain, (![U_257]: (ssPv3(skf3(U_257)) | ~ssPv4(skf3(U_257)) | ssPv3(U_257) | ~ssPv2(skf3(U_257)) | ~ssPv1(skf3(U_257))))). % 16.43/8.17 tff(c_1223, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ssPv4(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.43/8.17 tff(c_1183, plain, (![U_330]: (~ssPv3(skf3(U_330)) | ~ssPv1(skf3(U_330)) | ~ssPv1(U_330) | ~ssPv3(skf2(skf3(U_330)))))). % 16.43/8.17 tff(c_1182, plain, (![U_1]: (~ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv3(U_1)))). % 16.43/8.17 tff(c_369, plain, (![U_1, V_193]: (~ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv3(V_193) | ~ssRr(skf3(U_1), V_193)))). % 16.43/8.17 tff(c_1132, plain, (![U_327]: (ssPv2(skf3(U_327)) | ssPv4(U_327) | ssPv4(skf3(skf3(U_327))) | ~ssPv1(skf3(U_327))))). % 16.43/8.17 tff(c_254, plain, (![U_1, U_159]: (ssPv2(skf3(U_1)) | ssPv4(U_1) | ssPv4(U_159) | ~ssPv1(skf3(U_1)) | ~ssRr(U_159, skf3(U_1))))). % 16.43/8.17 tff(c_1058, plain, (![U_322]: (~ssPv1(skf3(U_322)) | ~ssPv1(U_322) | ssPv4(U_322) | ~ssPv4(skf3(U_322)) | ~ssPv3(skf3(U_322))))). % 16.43/8.17 tff(c_1040, plain, (![U_319]: (~ssPv3(U_319) | ssPv3(skf3(skf3(U_319))) | ~ssPv4(skf3(U_319)) | ~ssPv3(skf3(U_319))))). % 16.43/8.17 tff(c_982, plain, (![U_1]: (~ssPv3(skf3(U_1)) | ~ssPv3(U_1) | ssPv1(U_1) | ssPv4(skf2(U_1)) | ~ssPv4(U_1)))). % 16.43/8.17 tff(c_1049, plain, (![U_320]: (ssPv4(U_320) | ssPv3(skf3(skf3(U_320))) | ~ssPv4(skf3(U_320)) | ~ssPv3(skf3(U_320))))). % 16.43/8.17 tff(c_205, plain, (![U_1, U_142]: (ssPv4(U_1) | ssPv3(U_142) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssRr(U_142, skf3(U_1))))). % 16.43/8.17 tff(c_960, plain, (![U_315]: (~ssPv4(skf3(U_315)) | ~ssPv3(skf3(U_315)) | ~ssPv3(U_315) | ~ssPv4(skf2(skf3(U_315)))))). % 16.43/8.17 tff(c_941, plain, (![U_312]: (ssPv3(skf3(U_312)) | ssPv4(U_312) | ~ssPv2(skf3(U_312)) | ~ssPv3(skf2(skf3(U_312)))))). % 16.43/8.17 tff(c_959, plain, (![U_1]: (~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv4(U_1)))). % 16.43/8.17 tff(c_231, plain, (![U_1, V_152]: (~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv4(V_152) | ~ssRr(skf3(U_1), V_152)))). % 16.43/8.17 tff(c_940, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv4(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.43/8.17 tff(c_376, plain, (![U_1, V_196]: (ssPv3(skf3(U_1)) | ssPv4(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv3(V_196) | ~ssRr(skf3(U_1), V_196)))). % 16.43/8.17 tff(c_872, plain, (![U_307]: (ssPv1(skf3(U_307)) | ssPv4(U_307) | ssPv4(skf3(skf3(U_307))) | ~ssPv4(skf3(U_307))))). % 16.43/8.17 tff(c_430, plain, (![U_1, U_218]: (ssPv1(skf3(U_1)) | ssPv4(U_1) | ssPv4(U_218) | ~ssPv4(skf3(U_1)) | ~ssRr(U_218, skf3(U_1))))). % 16.43/8.17 tff(c_823, plain, (![U_302]: (ssPv1(skf3(U_302)) | ssPv3(U_302) | ~ssPv2(skf3(U_302)) | ~ssPv4(skf3(skf3(U_302)))))). % 16.43/8.17 tff(c_816, plain, (![U_300]: (ssPv4(skf2(U_300)) | ~ssPv3(skf2(U_300)) | ~ssPv2(U_300) | ~ssPv4(skf3(skf2(U_300)))))). % 16.43/8.17 tff(c_817, plain, (![U_2]: (ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv4(U_2)))). % 16.43/8.17 tff(c_155, plain, (![U_1, U_124]: (ssPv1(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_124) | ~ssRr(U_124, skf3(U_1))))). % 16.43/8.17 tff(c_424, plain, (![U_2, U_215]: (ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv4(U_215) | ~ssRr(U_215, skf2(U_2))))). % 16.43/8.17 tff(c_797, plain, (![U_297]: (ssPv1(skf2(U_297)) | ssPv1(U_297) | ~ssPv3(skf2(U_297)) | ~ssPv1(skf3(skf2(U_297)))))). % 16.43/8.17 tff(c_299, plain, (![U_2, U_170]: (ssPv1(skf2(U_2)) | ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv1(U_170) | ~ssRr(U_170, skf2(U_2))))). % 16.43/8.17 tff(c_740, plain, (![U_288]: (ssPv2(skf2(U_288)) | ssPv2(U_288) | ssPv4(skf3(skf2(U_288))) | ~ssPv1(skf2(U_288))))). % 16.43/8.17 tff(c_56, plain, (![V_76, X_78, W_77, U_75]: (ssPv2(V_76) | ssPv1(X_78) | ssPv4(W_77) | ~ssRr(V_76, X_78) | ~ssRr(W_77, V_76) | ~ssPv4(U_75) | ~ssRr(U_75, V_76)))). % 16.43/8.17 tff(c_292, plain, (![U_2, U_167]: (ssPv2(skf2(U_2)) | ssPv2(U_2) | ssPv4(U_167) | ~ssPv1(skf2(U_2)) | ~ssRr(U_167, skf2(U_2))))). % 16.43/8.17 tff(c_52, plain, (![V_68, X_70, W_69, U_67]: (ssPv4(V_68) | ssPv2(X_70) | ssPv4(W_69) | ~ssRr(V_68, X_70) | ~ssRr(V_68, W_69) | ~ssPv1(U_67) | ~ssRr(U_67, V_68)))). % 16.43/8.17 tff(c_698, plain, (![U_280]: (ssPv2(skf3(U_280)) | ssPv1(U_280) | ssPv3(skf3(skf3(U_280))) | ~ssPv4(skf3(U_280))))). % 16.43/8.17 tff(c_332, plain, (![U_1, U_178]: (ssPv2(skf3(U_1)) | ssPv1(U_1) | ssPv3(U_178) | ~ssPv4(skf3(U_1)) | ~ssRr(U_178, skf3(U_1))))). % 16.43/8.17 tff(c_688, plain, (![U_278]: (ssPv2(skf3(skf3(U_278))) | ~ssPv4(skf3(U_278)) | ~ssPv2(skf3(U_278)) | ~ssPv2(U_278)))). % 16.43/8.17 tff(c_129, plain, (![U_115, U_1]: (ssPv2(U_115) | ~ssPv4(skf3(U_1)) | ~ssPv2(skf3(U_1)) | ~ssPv2(U_1) | ~ssRr(U_115, skf3(U_1))))). % 16.43/8.17 tff(c_60, plain, (![W_85, U_83, V_84, X_86]: (ssPv3(W_85) | ssPv4(U_83) | ~ssPv2(V_84) | ~ssPv1(X_86) | ~ssRr(V_84, X_86) | ~ssRr(W_85, V_84) | ~ssRr(U_83, V_84)))). % 16.43/8.17 tff(c_657, plain, (![U_269]: (ssPv3(skf3(U_269)) | ssPv1(skf3(U_269)) | ssPv4(U_269) | ssPv3(skf3(skf3(U_269)))))). % 16.43/8.17 tff(c_474, plain, (![U_1, U_228]: (ssPv3(skf3(U_1)) | ssPv1(skf3(U_1)) | ssPv4(U_1) | ssPv3(U_228) | ~ssRr(U_228, skf3(U_1))))). % 16.43/8.17 tff(c_64, plain, (![V_92, X_94, W_93, U_91]: (ssPv4(V_92) | ssPv1(X_94) | ~ssRr(X_94, V_92) | ~ssPv1(W_93) | ~ssRr(W_93, V_92) | ~ssPv4(U_91) | ~ssRr(U_91, V_92)))). % 16.43/8.17 tff(c_595, plain, (![U_258]: (ssPv3(skf3(U_258)) | ssPv2(skf3(U_258)) | ~ssPv2(U_258) | ~ssPv3(skf3(skf3(U_258)))))). % 16.43/8.17 tff(c_407, plain, (![U_1, U_205]: (ssPv3(skf3(U_1)) | ssPv2(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv3(U_205) | ~ssRr(U_205, skf3(U_1))))). % 16.43/8.17 tff(c_577, plain, (![U_251]: (ssPv3(U_251) | ssPv1(skf3(skf3(U_251))) | ~ssPv2(skf3(U_251)) | ~ssPv1(skf3(U_251))))). % 16.43/8.17 tff(c_62, plain, (![X_90, W_89, U_87, V_88]: (ssPv3(X_90) | ssPv4(W_89) | ~ssPv2(U_87) | ~ssRr(U_87, X_90) | ~ssRr(U_87, W_89) | ~ssPv4(V_88) | ~ssRr(U_87, V_88)))). % 16.43/8.17 tff(c_176, plain, (![U_1, U_131]: (ssPv3(U_1) | ssPv1(U_131) | ~ssPv2(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssRr(U_131, skf3(U_1))))). % 16.43/8.17 tff(c_554, plain, (![U_248]: (~ssPv4(skf3(U_248)) | ~ssPv1(skf3(U_248)) | ~ssPv1(U_248) | ~ssPv3(skf3(skf3(U_248)))))). % 16.43/8.17 tff(c_354, plain, (![U_1, U_187]: (~ssPv4(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv3(U_187) | ~ssRr(U_187, skf3(U_1))))). % 16.43/8.18 tff(c_54, plain, (![V_72, X_74, U_71, W_73]: (ssPv4(V_72) | ssPv1(X_74) | ssPv2(U_71) | ~ssRr(V_72, X_74) | ~ssPv4(W_73) | ~ssRr(V_72, W_73) | ~ssRr(U_71, V_72)))). % 16.43/8.18 tff(c_536, plain, (![U_241]: (ssPv1(skf3(U_241)) | ssPv1(skf3(skf3(U_241))) | ~ssPv4(skf3(U_241)) | ~ssPv2(U_241)))). % 16.43/8.18 tff(c_414, plain, (![U_1, U_207]: (ssPv1(skf3(U_1)) | ssPv1(U_207) | ~ssPv4(skf3(U_1)) | ~ssPv2(U_1) | ~ssRr(U_207, skf3(U_1))))). % 16.43/8.18 tff(c_458, plain, (![U_223]: (ssPv1(skf3(U_223)) | ~ssPv2(skf3(U_223)) | ssPv1(U_223) | ssPv4(skf2(U_223)) | ~ssPv4(U_223)))). % 16.43/8.18 tff(c_58, plain, (![V_80, W_81, X_82, U_79]: (ssPv4(V_80) | ssPv3(W_81) | ~ssPv4(X_82) | ~ssRr(V_80, X_82) | ~ssRr(W_81, V_80) | ~ssPv1(U_79) | ~ssRr(U_79, V_80)))). % 16.43/8.18 tff(c_482, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv4(skf2(skf2(U_2))) | ssPv3(U_2)))). % 16.43/8.18 tff(c_481, plain, (![U_1]: (ssPv3(U_1) | ssPv1(U_1) | ssPv4(skf2(U_1)) | ssPv3(skf3(U_1))))). % 16.43/8.18 tff(c_475, plain, (![U_2, U_228]: (ssPv3(U_2) | ssPv1(U_2) | ssPv4(skf2(U_2)) | ssPv3(U_228) | ~ssRr(U_228, U_2)))). % 16.43/8.18 tff(c_16, plain, (![V_14, W_15, U_13]: (ssPv3(V_14) | ssPv1(V_14) | ssPv4(W_15) | ssPv3(U_13) | ~ssRr(V_14, W_15) | ~ssRr(U_13, V_14)))). % 16.43/8.18 tff(c_457, plain, (![U_223]: (ssPv3(skf2(U_223)) | ~ssPv2(U_223) | ssPv1(U_223) | ssPv4(skf2(U_223)) | ~ssPv4(U_223)))). % 16.43/8.18 tff(c_445, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv4(skf2(skf2(U_2))) | ssPv4(U_2) | ~ssPv4(skf2(U_2))))). % 16.43/8.18 tff(c_444, plain, (![U_1]: (ssPv1(U_1) | ssPv4(skf2(U_1)) | ssPv4(skf3(U_1)) | ~ssPv4(U_1)))). % 16.43/8.18 tff(c_431, plain, (![U_2, U_218]: (ssPv1(U_2) | ssPv4(skf2(U_2)) | ssPv4(U_218) | ~ssPv4(U_2) | ~ssRr(U_218, U_2)))). % 16.43/8.18 tff(c_423, plain, (![U_1, U_215]: (ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_215) | ~ssRr(U_215, U_1)))). % 16.43/8.18 tff(c_26, plain, (![V_29, W_30, U_28]: (ssPv1(V_29) | ssPv4(W_30) | ssPv4(U_28) | ~ssPv4(V_29) | ~ssRr(V_29, W_30) | ~ssRr(U_28, V_29)))). % 16.43/8.18 tff(c_44, plain, (![V_56, W_57, U_55]: (ssPv4(V_56) | ~ssPv3(V_56) | ~ssPv2(W_57) | ~ssRr(W_57, V_56) | ~ssPv4(U_55) | ~ssRr(U_55, V_56)))). % 16.43/8.18 tff(c_415, plain, (![U_2, U_207]: (ssPv1(U_2) | ssPv1(U_207) | ~ssPv4(U_2) | ~ssPv2(skf2(U_2)) | ~ssRr(U_207, U_2)))). % 16.43/8.18 tff(c_408, plain, (![U_2, U_205]: (ssPv3(U_2) | ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv3(U_205) | ~ssRr(U_205, U_2)))). % 16.43/8.18 tff(c_36, plain, (![V_44, U_43, W_45]: (ssPv1(V_44) | ssPv1(U_43) | ~ssPv4(V_44) | ~ssPv2(W_45) | ~ssRr(V_44, W_45) | ~ssRr(U_43, V_44)))). % 16.43/8.18 tff(c_34, plain, (![V_41, W_42, U_40]: (ssPv3(V_41) | ssPv2(V_41) | ~ssPv2(W_42) | ~ssRr(V_41, W_42) | ~ssPv3(U_40) | ~ssRr(U_40, V_41)))). % 16.43/8.18 tff(c_390, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv4(skf2(skf3(U_1))) | ~ssPv2(skf3(U_1)) | ~ssPv3(U_1)))). % 16.43/8.18 tff(c_391, plain, (![U_2]: (ssPv3(U_2) | ssPv4(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv3(skf2(U_2))))). % 16.43/8.18 tff(c_377, plain, (![U_2, V_196]: (ssPv3(U_2) | ssPv4(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv3(V_196) | ~ssRr(U_2, V_196)))). % 16.43/8.18 tff(c_370, plain, (![U_2, V_193]: (~ssPv3(U_2) | ~ssPv1(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv3(V_193) | ~ssRr(U_2, V_193)))). % 16.43/8.18 tff(c_32, plain, (![U_37, W_39, V_38]: (ssPv3(U_37) | ssPv4(W_39) | ~ssPv2(U_37) | ~ssRr(U_37, W_39) | ~ssPv3(V_38) | ~ssRr(U_37, V_38)))). % 16.43/8.18 tff(c_50, plain, (![U_64, W_66, V_65]: (~ssPv3(U_64) | ~ssPv1(U_64) | ~ssPv1(W_66) | ~ssRr(U_64, W_66) | ~ssPv3(V_65) | ~ssRr(U_64, V_65)))). % 16.43/8.18 tff(c_355, plain, (![U_2, U_187]: (~ssPv4(U_2) | ~ssPv1(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv3(U_187) | ~ssRr(U_187, U_2)))). % 16.43/8.18 tff(c_48, plain, (![V_62, W_63, U_61]: (~ssPv4(V_62) | ~ssPv1(V_62) | ~ssPv1(W_63) | ~ssRr(V_62, W_63) | ~ssPv3(U_61) | ~ssRr(U_61, V_62)))). % 16.43/8.18 tff(c_340, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 16.43/8.18 tff(c_326, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv1(skf3(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv1(U_2)))). % 16.43/8.18 tff(c_306, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv2(skf3(skf2(U_2))) | ssPv4(U_2) | ~ssPv1(skf2(U_2))))). % 16.43/8.18 tff(c_339, plain, (![U_1]: (ssPv2(U_1) | ssPv1(skf2(U_1)) | ssPv3(skf3(U_1)) | ~ssPv4(U_1)))). % 16.43/8.18 tff(c_333, plain, (![U_2, U_178]: (ssPv2(U_2) | ssPv1(skf2(U_2)) | ssPv3(U_178) | ~ssPv4(U_2) | ~ssRr(U_178, U_2)))). % 16.43/8.18 tff(c_18, plain, (![V_17, W_18, U_16]: (ssPv2(V_17) | ssPv1(W_18) | ssPv3(U_16) | ~ssPv4(V_17) | ~ssRr(V_17, W_18) | ~ssRr(U_16, V_17)))). % 16.43/8.18 tff(c_298, plain, (![U_1, U_170]: (ssPv1(U_1) | ssPv1(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_170) | ~ssRr(U_170, U_1)))). % 16.43/8.18 tff(c_291, plain, (![U_1, U_167]: (ssPv2(U_1) | ssPv2(skf3(U_1)) | ssPv4(U_167) | ~ssPv1(U_1) | ~ssRr(U_167, U_1)))). % 16.43/8.18 tff(c_38, plain, (![V_47, W_48, U_46]: (ssPv1(V_47) | ssPv1(W_48) | ~ssPv3(V_47) | ~ssRr(W_48, V_47) | ~ssPv1(U_46) | ~ssRr(U_46, V_47)))). % 16.43/8.18 tff(c_20, plain, (![V_20, W_21, U_19]: (ssPv2(V_20) | ssPv2(W_21) | ssPv4(U_19) | ~ssPv1(V_20) | ~ssRr(W_21, V_20) | ~ssRr(U_19, V_20)))). % 16.43/8.18 tff(c_262, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv4(skf2(skf2(U_2))) | ssPv4(U_2) | ~ssPv1(skf2(U_2))))). % 16.43/8.18 tff(c_261, plain, (![U_1]: (ssPv2(U_1) | ssPv4(skf2(U_1)) | ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 16.43/8.18 tff(c_255, plain, (![U_2, U_159]: (ssPv2(U_2) | ssPv4(skf2(U_2)) | ssPv4(U_159) | ~ssPv1(U_2) | ~ssRr(U_159, U_2)))). % 16.43/8.18 tff(c_22, plain, (![V_23, W_24, U_22]: (ssPv2(V_23) | ssPv4(W_24) | ssPv4(U_22) | ~ssPv1(V_23) | ~ssRr(V_23, W_24) | ~ssRr(U_22, V_23)))). % 16.43/8.18 tff(c_219, plain, (![U_2]: (ssPv4(skf2(skf2(U_2))) | ssPv3(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv3(skf2(U_2))))). % 16.43/8.18 tff(c_191, plain, (![U_2]: (ssPv3(skf2(skf2(U_2))) | ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 16.43/8.18 tff(c_232, plain, (![U_2, V_152]: (~ssPv4(U_2) | ~ssPv3(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv4(V_152) | ~ssRr(U_2, V_152)))). % 16.43/8.18 tff(c_46, plain, (![U_58, W_60, V_59]: (~ssPv4(U_58) | ~ssPv3(U_58) | ~ssPv3(W_60) | ~ssRr(U_58, W_60) | ~ssPv4(V_59) | ~ssRr(U_58, V_59)))). % 16.43/8.18 tff(c_218, plain, (![U_1]: (ssPv4(skf2(U_1)) | ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 16.43/8.18 tff(c_206, plain, (![U_2, U_142]: (ssPv4(skf2(U_2)) | ssPv3(U_142) | ~ssPv4(U_2) | ~ssPv3(U_2) | ~ssRr(U_142, U_2)))). % 16.43/8.18 tff(c_28, plain, (![W_33, U_31, V_32]: (ssPv4(W_33) | ssPv3(U_31) | ~ssPv4(V_32) | ~ssPv3(V_32) | ~ssRr(V_32, W_33) | ~ssRr(U_31, V_32)))). % 16.43/8.18 tff(c_190, plain, (![U_1]: (ssPv3(skf2(U_1)) | ssPv1(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 16.43/8.18 tff(c_177, plain, (![U_2, U_131]: (ssPv3(skf2(U_2)) | ssPv1(U_131) | ~ssPv2(U_2) | ~ssPv1(U_2) | ~ssRr(U_131, U_2)))). % 16.43/8.18 tff(c_30, plain, (![W_36, U_34, V_35]: (ssPv3(W_36) | ssPv1(U_34) | ~ssPv2(V_35) | ~ssPv1(V_35) | ~ssRr(V_35, W_36) | ~ssRr(U_34, V_35)))). % 16.43/8.18 tff(c_163, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2)))). % 16.43/8.18 tff(c_162, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf2(U_1)) | ~ssPv2(U_1) | ~ssPv4(skf3(U_1))))). % 16.43/8.18 tff(c_156, plain, (![U_2, U_124]: (ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv4(U_124) | ~ssRr(U_124, U_2)))). % 16.43/8.18 tff(c_40, plain, (![V_50, W_51, U_49]: (ssPv1(V_50) | ssPv3(W_51) | ~ssPv2(V_50) | ~ssRr(V_50, W_51) | ~ssPv4(U_49) | ~ssRr(U_49, V_50)))). % 16.43/8.18 tff(c_130, plain, (![U_115, U_2]: (ssPv2(U_115) | ~ssPv4(U_2) | ~ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssRr(U_115, U_2)))). % 16.43/8.18 tff(c_117, plain, (![U_1]: (ssPv1(skf3(U_1)) | ssPv1(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 16.43/8.18 tff(c_94, plain, (![U_2]: (ssPv3(skf2(U_2)) | ~ssPv4(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2)))). % 16.43/8.18 tff(c_42, plain, (![U_52, V_53, W_54]: (ssPv2(U_52) | ~ssPv4(V_53) | ~ssPv2(V_53) | ~ssPv2(W_54) | ~ssRr(V_53, W_54) | ~ssRr(U_52, V_53)))). % 16.43/8.18 tff(c_74, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv3(skf3(U_1)) | ssPv1(skf3(U_1)) | ssPv4(U_1)))). % 16.51/8.18 tff(c_85, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv2(skf2(U_2))))). % 16.51/8.18 tff(c_118, plain, (![U_2]: (ssPv1(U_2) | ssPv1(skf2(U_2)) | ~ssPv4(U_2) | ~ssPv2(U_2)))). % 16.51/8.18 tff(c_12, plain, (![U_9, V_10]: (ssPv1(U_9) | ssPv1(V_10) | ~ssPv4(U_9) | ~ssPv2(U_9) | ~ssRr(U_9, V_10)))). % 16.51/8.18 tff(c_93, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssPv1(skf3(U_1))))). % 16.51/8.18 tff(c_84, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1)))). % 16.51/8.18 tff(c_14, plain, (![V_12, U_11]: (ssPv3(V_12) | ~ssPv4(V_12) | ~ssPv1(V_12) | ~ssPv1(U_11) | ~ssRr(U_11, V_12)))). % 16.51/8.18 tff(c_10, plain, (![V_8, U_7]: (ssPv4(V_8) | ssPv1(U_7) | ~ssPv3(V_8) | ~ssPv2(V_8) | ~ssRr(U_7, V_8)))). % 16.51/8.18 tff(c_75, plain, (![U_2]: (ssPv4(U_2) | ssPv3(U_2) | ssPv1(U_2) | ssPv4(skf2(U_2))))). % 16.51/8.18 tff(c_6, plain, (![U_3, V_4]: (ssPv4(U_3) | ssPv3(U_3) | ssPv1(U_3) | ssPv4(V_4) | ~ssRr(U_3, V_4)))). % 16.51/8.18 tff(c_2, plain, (![U_1]: (ssRr(skf3(U_1), U_1)))). % 16.51/8.18 tff(c_4, plain, (![U_2]: (ssRr(U_2, skf2(U_2))))). % 16.51/8.18 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.51/8.18 %------------------------------------------------------------------------------