%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN768-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 : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:04:53 PM UTC 2025 % Result : Satisfiable 12.15s 4.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN768-1 : TPTP v9.0.0. Released v2.5.0. % 0.06/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.12/0.34 % Computer : n026.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 08:16:38 EDT 2025 % 0.12/0.35 % CPUTime : % 12.15/4.40 % 12.15/4.40 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.15/4.40 % 12.15/4.40 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.15/4.41 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf3 > skf2 % 12.15/4.41 % 12.15/4.41 %Foreground sorts: % 12.15/4.41 % 12.15/4.41 % 12.15/4.41 %Background operators: % 12.15/4.41 % 12.15/4.41 % 12.15/4.41 %Foreground operators: % 12.15/4.41 tff(skf3, type, skf3: $i > $i). % 12.15/4.41 tff(ssPv1, type, ssPv1: $i > $o). % 12.15/4.41 tff(ssPv3, type, ssPv3: $i > $o). % 12.15/4.41 tff(skf2, type, skf2: $i > $i). % 12.15/4.41 tff(ssRr, type, ssRr: ($i * $i) > $o). % 12.15/4.41 tff(ssPv4, type, ssPv4: $i > $o). % 12.15/4.41 tff(ssPv2, type, ssPv2: $i > $o). % 12.15/4.41 % 12.15/4.41 %Saturated clause set: % 12.15/4.41 tff(c_8620, plain, (![U_728]: (~ssPv1(skf3(U_728)) | ~ssPv1(U_728) | ~ssPv4(skf3(skf3(U_728))) | ssPv2(skf2(skf3(U_728))) | ssPv2(skf3(U_728)) | ~ssPv1(skf2(skf3(U_728))) | ~ssPv1(skf3(skf3(U_728))) | ssPv2(skf3(skf3(U_728))) | ~ssPv4(skf3(U_728))))). % 12.15/4.41 tff(c_4285, plain, (![U_267, U_269]: (~ssPv1(skf3(U_267)) | ~ssPv1(U_267) | ~ssPv4(U_269) | ~ssRr(U_269, skf3(U_267)) | ssPv2(skf2(skf3(U_267))) | ssPv2(skf3(U_267)) | ~ssPv1(skf2(skf3(U_267))) | ~ssPv1(skf3(skf3(U_267))) | ssPv2(skf3(skf3(U_267))) | ~ssPv4(skf3(U_267))))). % 12.15/4.41 tff(c_4976, plain, (![U_544]: (ssPv2(skf2(skf3(U_544))) | ssPv3(skf2(skf3(U_544))) | ssPv2(skf3(U_544)) | ~ssPv1(skf2(skf3(U_544))) | ~ssPv1(skf3(U_544)) | ~ssPv1(U_544) | ~ssPv3(U_544) | ssPv3(skf3(U_544)) | ssPv2(skf3(skf3(U_544))) | ssPv1(skf3(skf3(U_544)))))). % 12.15/4.41 tff(c_8334, plain, (![U_715]: (~ssPv1(U_715) | ~ssPv2(skf2(skf2(U_715))) | ssPv3(skf2(skf2(U_715))) | ssPv1(skf2(skf2(U_715))) | ssPv2(skf2(U_715)) | ~ssPv2(skf3(skf2(U_715))) | ssPv3(skf2(U_715)) | ssPv1(skf3(skf2(U_715))) | ~ssPv4(skf2(U_715))))). % 12.15/4.41 tff(c_7640, plain, (![U_689]: (~ssPv1(U_689) | ~ssPv2(skf2(skf2(U_689))) | ssPv3(skf2(skf2(U_689))) | ssPv1(skf2(skf2(U_689))) | ssPv2(skf2(U_689)) | ssPv1(skf2(U_689)) | ~ssPv3(skf3(skf2(U_689))) | ssPv2(skf3(skf2(U_689))) | ~ssPv4(skf2(U_689))))). % 12.15/4.41 tff(c_7379, plain, (![U_681]: (~ssPv1(U_681) | ~ssPv1(skf2(skf2(U_681))) | ~ssPv3(skf2(skf2(U_681))) | ssPv2(skf2(skf2(U_681))) | ~ssPv2(skf2(U_681)) | ssPv1(skf2(U_681)) | ~ssPv3(skf3(skf2(U_681))) | ssPv2(skf3(skf2(U_681))) | ~ssPv4(skf2(U_681))))). % 12.15/4.41 tff(c_4974, plain, (![U_544]: (~ssPv2(skf2(skf3(U_544))) | ssPv3(skf2(skf3(U_544))) | ssPv2(skf3(U_544)) | ~ssPv1(skf3(U_544)) | ~ssPv1(U_544) | ~ssPv3(U_544) | ssPv3(skf3(U_544)) | ssPv2(skf3(skf3(U_544))) | ssPv1(skf3(skf3(U_544)))))). % 12.15/4.41 tff(c_8452, plain, (![U_718]: (~ssPv4(skf3(skf3(U_718))) | ~ssPv1(skf3(U_718)) | ssPv1(skf2(skf3(U_718))) | ssPv2(skf3(U_718)) | ~ssPv1(U_718) | ~ssPv1(skf3(skf3(U_718))) | ssPv2(skf3(skf3(U_718))) | ~ssPv4(skf3(U_718))))). % 12.15/4.41 tff(c_8420, plain, (![U_594]: (~ssPv2(skf2(skf3(U_594))) | ~ssPv1(skf3(U_594)) | ssPv1(skf2(skf3(U_594))) | ssPv2(skf3(U_594)) | ~ssPv1(U_594) | ~ssPv1(skf3(skf3(U_594))) | ssPv2(skf3(skf3(U_594))) | ~ssPv4(skf3(U_594))))). % 12.15/4.41 tff(c_8468, plain, (![U_719]: (~ssPv3(skf3(U_719)) | ~ssPv1(U_719) | ~ssPv1(skf3(skf3(U_719))) | ~ssPv1(skf3(U_719)) | ~ssPv2(skf2(skf3(U_719))) | ~ssPv4(skf3(U_719)) | ssPv1(skf2(skf3(U_719))) | ssPv2(skf3(U_719))))). % 12.15/4.42 tff(c_8271, plain, (![U_269, U_712]: (~ssPv4(U_269) | ~ssRr(U_269, skf3(U_712)) | ~ssPv1(skf3(U_712)) | ssPv1(skf2(skf3(U_712))) | ssPv2(skf3(U_712)) | ~ssPv1(U_712) | ~ssPv1(skf3(skf3(U_712))) | ssPv2(skf3(skf3(U_712))) | ~ssPv4(skf3(U_712))))). % 12.15/4.42 tff(c_5571, plain, (![U_597]: (ssPv1(skf2(skf3(U_597))) | ~ssPv3(skf2(skf3(U_597))) | ~ssPv2(skf2(skf3(U_597))) | ssPv2(skf3(U_597)) | ~ssPv1(U_597) | ~ssPv1(skf3(skf3(U_597))) | ssPv2(skf3(skf3(U_597))) | ~ssPv4(skf3(U_597))))). % 12.15/4.42 tff(c_7642, plain, (![U_689]: (~ssPv1(U_689) | ~ssPv2(skf2(skf2(U_689))) | ~ssPv4(skf2(U_689)) | ssPv3(skf2(skf2(U_689))) | ssPv1(skf2(skf2(U_689))) | ssPv2(skf2(U_689)) | ~ssPv3(skf3(skf2(U_689))) | ~ssPv2(skf3(skf2(U_689)))))). % 12.15/4.42 tff(c_7056, plain, (![U_671]: (~ssPv1(U_671) | ssPv2(skf2(skf2(U_671))) | ssPv3(skf2(skf2(U_671))) | ssPv1(skf2(skf2(U_671))) | ssPv2(skf2(U_671)) | ssPv1(skf2(U_671)) | ~ssPv3(skf3(skf2(U_671))) | ssPv2(skf3(skf2(U_671))) | ~ssPv4(skf2(U_671))))). % 12.15/4.42 tff(c_7058, plain, (![U_671]: (~ssPv4(skf2(U_671)) | ~ssPv1(U_671) | ssPv2(skf2(skf2(U_671))) | ssPv3(skf2(skf2(U_671))) | ssPv1(skf2(skf2(U_671))) | ssPv2(skf2(U_671)) | ~ssPv3(skf3(skf2(U_671))) | ~ssPv2(skf3(skf2(U_671)))))). % 12.15/4.42 tff(c_5542, plain, (![U_594]: (~ssPv1(skf3(U_594)) | ssPv3(skf2(skf3(U_594))) | ssPv1(skf2(skf3(U_594))) | ssPv2(skf3(U_594)) | ~ssPv1(U_594) | ~ssPv1(skf3(skf3(U_594))) | ssPv2(skf3(skf3(U_594))) | ~ssPv4(skf3(U_594))))). % 12.15/4.42 tff(c_7641, plain, (![U_689]: (~ssPv1(U_689) | ~ssPv2(skf2(skf2(U_689))) | ssPv3(skf2(skf2(U_689))) | ssPv1(skf2(skf2(U_689))) | ssPv2(skf2(U_689)) | ssPv3(skf2(U_689)) | ssPv2(skf3(skf2(U_689))) | ~ssPv4(skf2(U_689))))). % 12.15/4.42 tff(c_7777, plain, (![U_699]: (~ssPv1(U_699) | ~ssPv1(skf3(U_699)) | ~ssPv2(skf2(skf3(U_699))) | ~ssPv4(skf3(U_699)) | ssPv1(skf2(skf3(U_699))) | ssPv2(skf3(U_699)) | ~ssPv3(skf3(skf3(U_699))) | ~ssPv2(skf3(skf3(U_699)))))). % 12.15/4.42 tff(c_8088, plain, (![U_707]: (~ssPv1(U_707) | ssPv3(skf2(U_707)) | ~ssPv4(skf2(U_707)) | ssPv2(skf2(skf2(U_707))) | ~ssPv1(skf2(skf2(U_707))) | ~ssPv2(skf2(U_707))))). % 12.15/4.42 tff(c_2459, plain, (![U_402]: (~ssPv1(skf3(U_402)) | ~ssPv1(U_402) | ssPv2(skf2(skf3(U_402))) | ~ssPv1(skf2(skf3(U_402))) | ~ssPv2(skf3(U_402)) | ssPv3(skf3(U_402)) | ssPv2(skf3(skf3(U_402))) | ssPv3(skf3(skf3(U_402))) | ssPv1(skf3(skf3(U_402)))))). % 12.15/4.42 tff(c_7755, plain, (![U_696]: (~ssPv1(U_696) | ~ssPv1(skf3(U_696)) | ~ssPv4(skf3(U_696)) | ssPv2(skf2(skf3(U_696))) | ssPv1(skf2(skf3(U_696))) | ssPv2(skf3(U_696)) | ~ssPv3(skf3(skf3(U_696))) | ~ssPv2(skf3(skf3(U_696)))))). % 12.15/4.42 tff(c_7887, plain, (![U_607]: (~ssPv2(skf2(skf3(U_607))) | ssPv1(skf2(skf3(U_607))) | ssPv2(skf3(U_607)) | ~ssPv1(U_607) | ssPv3(skf3(U_607)) | ssPv1(skf3(skf3(U_607))) | ~ssPv4(skf3(U_607))))). % 12.15/4.42 tff(c_7785, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2) | ssPv2(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 12.15/4.42 tff(c_7760, plain, (![U_697]: (~ssPv1(U_697) | ~ssPv4(skf3(skf3(U_697))) | ~ssPv1(skf3(U_697)) | ~ssPv2(skf2(skf3(U_697))) | ~ssPv4(skf3(U_697)) | ssPv1(skf2(skf3(U_697))) | ssPv2(skf3(U_697))))). % 12.15/4.42 tff(c_5104, plain, (![U_267, U_269]: (~ssPv1(U_267) | ~ssPv4(U_269) | ~ssRr(U_269, skf3(U_267)) | ~ssPv1(skf3(U_267)) | ~ssPv2(skf2(skf3(U_267))) | ~ssPv4(skf3(U_267)) | ssPv1(skf2(skf3(U_267))) | ssPv2(skf3(U_267))))). % 12.15/4.42 tff(c_7738, plain, (![U_694]: (~ssPv1(U_694) | ~ssPv4(skf3(skf3(U_694))) | ~ssPv1(skf3(U_694)) | ~ssPv4(skf3(U_694)) | ssPv2(skf2(skf3(U_694))) | ssPv1(skf2(skf3(U_694))) | ssPv2(skf3(U_694))))). % 12.15/4.42 tff(c_2761, plain, (![U_267, U_269]: (~ssPv1(U_267) | ~ssPv4(U_269) | ~ssRr(U_269, skf3(U_267)) | ~ssPv1(skf3(U_267)) | ~ssPv4(skf3(U_267)) | ssPv2(skf2(skf3(U_267))) | ssPv1(skf2(skf3(U_267))) | ssPv2(skf3(U_267))))). % 12.15/4.42 tff(c_4588, plain, (![U_522]: (~ssPv4(U_522) | ssPv2(skf2(U_522)) | ~ssPv2(U_522) | ~ssPv3(skf2(U_522)) | ~ssPv1(skf2(U_522)) | ~ssPv1(skf3(skf2(U_522))) | ssPv2(skf3(skf2(U_522))) | ~ssPv4(skf2(U_522))))). % 12.15/4.42 tff(c_7687, plain, (![U_153]: (~ssPv2(skf2(U_153)) | ssPv3(skf2(U_153)) | ssPv1(skf2(U_153)) | ssPv2(U_153) | ssPv1(U_153) | ~ssPv1(skf3(U_153)) | ssPv2(skf3(U_153)) | ~ssPv4(U_153)))). % 12.15/4.42 tff(c_5275, plain, (![U_2]: (~ssPv1(skf3(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 12.15/4.42 tff(c_7574, plain, (![U_684]: (~ssPv1(U_684) | ~ssPv4(skf3(skf2(U_684))) | ~ssPv2(skf2(skf2(U_684))) | ~ssPv4(skf2(U_684)) | ssPv3(skf2(skf2(U_684))) | ssPv1(skf2(skf2(U_684))) | ssPv2(skf2(U_684))))). % 12.15/4.42 tff(c_7592, plain, (![U_201]: (~ssPv1(U_201) | ssPv1(skf2(U_201)) | ~ssPv1(skf3(skf2(U_201))) | ~ssPv4(skf2(U_201)) | ssPv2(skf2(skf2(U_201))) | ~ssPv1(skf2(skf2(U_201))) | ~ssPv2(skf2(U_201))))). % 12.15/4.42 tff(c_7575, plain, (![U_2]: (~ssPv1(U_2) | ~ssPv4(U_2) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.15/4.42 tff(c_7567, plain, (![U_2]: (ssPv1(U_2) | ~ssPv1(skf3(U_2)) | ssPv2(skf3(U_2)) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.15/4.42 tff(c_6226, plain, (![U_2, U_628]: (~ssPv1(U_2) | ~ssPv4(U_628) | ~ssRr(U_628, skf2(U_2)) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.15/4.42 tff(c_7202, plain, (![U_676]: (~ssPv1(U_676) | ~ssPv4(skf3(skf2(U_676))) | ~ssPv1(skf2(skf2(U_676))) | ~ssPv4(skf2(U_676)) | ~ssPv3(skf2(skf2(U_676))) | ssPv2(skf2(skf2(U_676))) | ~ssPv2(skf2(U_676))))). % 12.15/4.42 tff(c_7348, plain, (![U_679]: (~ssPv1(U_679) | ~ssPv4(U_679) | ~ssPv4(skf2(U_679)) | ssPv2(skf2(skf2(U_679))) | ~ssPv1(skf2(skf2(U_679))) | ~ssPv2(skf2(U_679))))). % 12.15/4.42 tff(c_7190, plain, (![U_153]: (ssPv2(skf2(U_153)) | ssPv3(skf2(U_153)) | ssPv1(skf2(U_153)) | ssPv2(U_153) | ssPv1(U_153) | ~ssPv1(skf3(U_153)) | ssPv2(skf3(U_153)) | ~ssPv4(U_153)))). % 12.15/4.42 tff(c_6032, plain, (![U_2, U_619]: (~ssPv1(U_2) | ~ssPv4(U_619) | ~ssRr(U_619, skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ~ssPv3(skf2(skf2(U_2))) | ssPv2(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2))))). % 12.15/4.42 tff(c_2827, plain, (![U_240]: (~ssPv2(skf2(skf3(U_240))) | ~ssPv1(skf3(U_240)) | ssPv1(skf2(skf3(U_240))) | ssPv3(skf2(skf3(U_240))) | ssPv2(skf3(U_240)) | ~ssPv1(U_240) | ~ssPv3(skf3(skf3(U_240)))))). % 12.15/4.42 tff(c_7112, plain, (![U_449]: (ssPv2(U_449) | ssPv2(skf2(U_449)) | ssPv1(skf3(skf2(U_449))) | ~ssPv1(U_449) | ssPv1(skf2(U_449)) | ssPv3(skf2(U_449)) | ~ssPv4(skf2(U_449))))). % 12.15/4.42 tff(c_6951, plain, (![U_663]: (~ssPv4(skf2(U_663)) | ~ssPv1(U_663) | ~ssPv4(skf3(skf2(U_663))) | ssPv2(skf2(skf2(U_663))) | ssPv3(skf2(skf2(U_663))) | ssPv1(skf2(skf2(U_663))) | ssPv2(skf2(U_663))))). % 12.15/4.42 tff(c_7006, plain, (![U_669]: (ssPv4(skf3(U_669)) | ssPv2(skf3(U_669)) | ~ssPv1(skf3(U_669)) | ~ssPv1(U_669) | ~ssPv3(U_669) | ssPv3(skf3(U_669)) | ssPv1(skf3(skf3(U_669)))))). % 12.15/4.42 tff(c_6973, plain, (![U_2]: (~ssPv1(skf2(U_2)) | ssPv2(U_2) | ~ssPv4(U_2) | ssPv2(skf2(skf2(U_2))) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2))))). % 12.15/4.42 tff(c_6952, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_2) | ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.15/4.42 tff(c_5461, plain, (![U_2, U_588]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_588) | ~ssRr(U_588, skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.15/4.42 tff(c_2782, plain, (![U_428]: (~ssPv4(skf2(U_428)) | ~ssPv1(U_428) | ssPv3(skf2(U_428)) | ssPv1(skf2(U_428)) | ssPv2(U_428) | ssPv2(skf2(U_428)) | ~ssPv3(skf3(skf2(U_428))) | ~ssPv2(skf3(skf2(U_428)))))). % 12.15/4.42 tff(c_6883, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2)) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.15/4.43 tff(c_6764, plain, (![U_658]: (~ssPv4(skf3(skf3(U_658))) | ~ssPv3(skf3(U_658)) | ssPv2(skf3(U_658)) | ~ssPv4(U_658) | ssPv4(skf3(U_658)) | ~ssPv1(skf3(U_658)) | ~ssPv1(skf3(skf3(U_658)))))). % 12.15/4.43 tff(c_5413, plain, (![U_580, U_579]: (~ssPv4(U_580) | ~ssRr(U_580, skf3(U_579)) | ~ssPv3(skf3(U_579)) | ssPv2(skf3(U_579)) | ~ssPv4(U_579) | ssPv4(skf3(U_579)) | ~ssPv1(skf3(U_579)) | ~ssPv1(skf3(skf3(U_579)))))). % 12.15/4.43 tff(c_6738, plain, (![U_655]: (~ssPv1(skf3(U_655)) | ~ssPv3(skf3(U_655)) | ~ssPv4(U_655) | ssPv4(skf3(U_655)) | ssPv2(skf3(U_655)) | ~ssPv3(skf3(skf3(U_655))) | ~ssPv2(skf3(skf3(U_655)))))). % 12.15/4.43 tff(c_6721, plain, (![U_653]: (~ssPv1(skf3(U_653)) | ~ssPv4(skf3(skf3(U_653))) | ~ssPv3(skf3(U_653)) | ~ssPv4(U_653) | ssPv4(skf3(U_653)) | ssPv2(skf3(U_653)) | ~ssPv2(skf3(skf3(U_653)))))). % 12.15/4.43 tff(c_5412, plain, (![U_579, U_580]: (~ssPv1(skf3(U_579)) | ~ssPv4(U_580) | ~ssRr(U_580, skf3(U_579)) | ~ssPv3(skf3(U_579)) | ~ssPv4(U_579) | ssPv4(skf3(U_579)) | ssPv2(skf3(U_579)) | ~ssPv2(skf3(skf3(U_579)))))). % 12.15/4.43 tff(c_6233, plain, (![U_2]: (~ssPv1(skf3(skf2(U_2))) | ~ssPv4(U_2) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.15/4.43 tff(c_6686, plain, (![U_650]: (~ssPv4(skf3(skf3(U_650))) | ssPv4(skf3(U_650)) | ssPv2(skf3(U_650)) | ~ssPv4(U_650) | ssPv2(skf2(skf3(U_650))) | ~ssPv3(skf3(U_650)) | ~ssPv1(skf3(U_650))))). % 12.15/4.43 tff(c_5411, plain, (![U_580, U_579]: (~ssPv4(U_580) | ~ssRr(U_580, skf3(U_579)) | ssPv4(skf3(U_579)) | ssPv2(skf3(U_579)) | ~ssPv4(U_579) | ssPv2(skf2(skf3(U_579))) | ~ssPv3(skf3(U_579)) | ~ssPv1(skf3(U_579))))). % 12.15/4.43 tff(c_4085, plain, (![U_165]: (~ssPv2(skf2(skf2(U_165))) | ssPv3(skf2(skf2(U_165))) | ssPv2(skf2(U_165)) | ~ssPv1(skf2(skf2(U_165))) | ssPv3(skf2(U_165)) | ssPv1(U_165) | ~ssPv4(skf2(U_165))))). % 12.15/4.43 tff(c_3921, plain, (![U_165]: (ssPv2(skf2(skf2(U_165))) | ssPv3(skf2(skf2(U_165))) | ssPv2(skf2(U_165)) | ~ssPv1(skf2(skf2(U_165))) | ssPv3(skf2(U_165)) | ssPv1(U_165) | ~ssPv4(skf2(U_165))))). % 12.15/4.43 tff(c_4390, plain, (![U_511]: (~ssPv2(skf2(skf3(U_511))) | ssPv3(skf2(skf3(U_511))) | ssPv2(skf3(U_511)) | ~ssPv1(U_511) | ssPv3(skf3(U_511)) | ssPv1(skf3(skf3(U_511))) | ~ssPv4(skf3(U_511))))). % 12.15/4.43 tff(c_6629, plain, (![U_644]: (~ssPv1(skf3(skf2(U_644))) | ~ssPv4(U_644) | ~ssPv4(skf2(U_644)) | ssPv2(skf2(skf2(U_644))) | ~ssPv1(skf2(skf2(U_644))) | ~ssPv2(skf2(U_644))))). % 12.15/4.43 tff(c_6432, plain, (![U_638, U_640]: (~ssPv1(skf2(U_638)) | ~ssPv3(skf2(skf2(U_638))) | ~ssPv4(U_640) | ~ssRr(U_640, skf2(U_638)) | ~ssPv4(skf2(U_638)) | ~ssPv1(U_638) | ~ssPv2(skf2(U_638)) | ~ssPv4(U_638)))). % 12.15/4.43 tff(c_657, plain, (![U_229, W_235, U_236]: (~ssPv1(skf2(U_229)) | ~ssPv3(W_235) | ~ssRr(skf2(U_229), W_235) | ~ssPv4(U_236) | ~ssRr(U_236, skf2(U_229)) | ~ssPv4(skf2(U_229)) | ~ssPv1(U_229) | ~ssPv2(skf2(U_229)) | ~ssPv4(U_229)))). % 12.15/4.43 tff(c_5725, plain, (![U_607]: (ssPv1(skf2(skf3(U_607))) | ssPv3(skf2(skf3(U_607))) | ssPv2(skf3(U_607)) | ~ssPv1(U_607) | ssPv3(skf3(U_607)) | ssPv1(skf3(skf3(U_607))) | ~ssPv4(skf3(U_607))))). % 12.15/4.43 tff(c_6354, plain, (![U_449]: (~ssPv1(skf2(skf2(U_449))) | ssPv2(skf2(U_449)) | ssPv1(skf3(skf2(U_449))) | ~ssPv1(U_449) | ssPv1(skf2(U_449)) | ssPv3(skf2(U_449)) | ~ssPv4(skf2(U_449))))). % 12.15/4.43 tff(c_6346, plain, (![U_606]: (~ssPv1(U_606) | ssPv2(skf2(U_606)) | ~ssPv1(skf2(skf2(U_606))) | ssPv3(skf2(U_606)) | ssPv1(skf3(skf2(U_606))) | ~ssPv4(skf2(U_606))))). % 12.15/4.43 tff(c_5732, plain, (![U_608]: (~ssPv1(U_608) | ~ssPv4(skf3(skf2(U_608))) | ssPv2(skf2(U_608)) | ~ssPv2(skf2(skf2(U_608))) | ~ssPv4(skf2(U_608)) | ~ssPv1(skf2(skf2(U_608))) | ~ssPv1(skf2(U_608))))). % 12.15/4.43 tff(c_6250, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.15/4.43 tff(c_6232, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1)))). % 12.15/4.43 tff(c_6225, plain, (![U_1, U_628]: (~ssPv1(skf3(U_1)) | ~ssPv4(U_628) | ~ssRr(U_628, U_1) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1)))). % 12.15/4.43 tff(c_5055, plain, (![W_151, U_547, U_152]: (~ssPv1(W_151) | ~ssRr(W_151, U_547) | ~ssPv4(U_152) | ~ssRr(U_152, U_547) | ~ssPv2(skf2(U_547)) | ~ssPv4(U_547) | ssPv3(skf2(U_547)) | ssPv1(skf2(U_547)) | ssPv2(U_547)))). % 12.15/4.43 tff(c_6185, plain, (![U_2]: (~ssPv1(skf3(U_2)) | ssPv3(U_2) | ssPv2(skf3(U_2)) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.15/4.43 tff(c_6038, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv1(skf2(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf2(U_1)) | ssPv2(skf2(U_1)) | ~ssPv2(U_1)))). % 12.15/4.43 tff(c_6031, plain, (![U_1, U_619]: (~ssPv1(skf3(U_1)) | ~ssPv4(U_619) | ~ssRr(U_619, U_1) | ~ssPv1(skf2(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf2(U_1)) | ssPv2(skf2(U_1)) | ~ssPv2(U_1)))). % 12.15/4.43 tff(c_3349, plain, (![W_151, U_454, U_152]: (~ssPv1(W_151) | ~ssRr(W_151, U_454) | ~ssPv4(U_152) | ~ssRr(U_152, U_454) | ~ssPv1(skf2(U_454)) | ~ssPv4(U_454) | ~ssPv3(skf2(U_454)) | ssPv2(skf2(U_454)) | ~ssPv2(U_454)))). % 12.15/4.43 tff(c_5990, plain, (![U_615]: (ssPv2(skf3(U_615)) | ssPv4(U_615) | ~ssPv1(skf3(U_615)) | ~ssPv1(U_615) | ~ssPv3(U_615) | ssPv3(skf3(U_615)) | ssPv1(skf3(skf3(U_615)))))). % 12.15/4.43 tff(c_5953, plain, (![U_2]: (~ssPv1(U_2) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.15/4.43 tff(c_5733, plain, (![U_2]: (~ssPv1(U_2) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 12.15/4.43 tff(c_5206, plain, (![U_2, U_564]: (~ssPv1(U_2) | ~ssPv4(U_564) | ~ssRr(U_564, skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 12.15/4.43 tff(c_3427, plain, (![U_240]: (~ssPv4(skf3(U_240)) | ssPv1(skf2(skf3(U_240))) | ssPv3(skf2(skf3(U_240))) | ssPv3(skf3(U_240)) | ssPv2(skf3(U_240)) | ~ssPv1(U_240) | ~ssPv3(skf3(skf3(U_240)))))). % 12.15/4.43 tff(c_4259, plain, (![U_498]: (~ssPv1(U_498) | ssPv2(skf2(U_498)) | ~ssPv1(skf2(skf2(U_498))) | ~ssPv3(skf3(skf2(U_498))) | ssPv3(skf2(U_498)) | ssPv2(skf3(skf2(U_498))) | ~ssPv4(skf2(U_498))))). % 12.15/4.43 tff(c_5663, plain, (![U_604]: (ssPv2(skf3(U_604)) | ~ssPv1(U_604) | ssPv1(skf3(U_604)) | ~ssPv1(skf3(skf3(U_604))) | ssPv2(skf3(skf3(U_604))) | ~ssPv4(skf3(U_604))))). % 12.15/4.43 tff(c_4440, plain, (![U_517]: (~ssPv2(U_517) | ssPv2(skf2(skf2(U_517))) | ~ssPv3(skf2(U_517)) | ~ssPv1(skf2(U_517)) | ssPv2(skf2(U_517)) | ~ssPv3(skf3(skf2(U_517))) | ~ssPv2(skf3(skf2(U_517)))))). % 12.15/4.43 tff(c_4258, plain, (![U_498]: (~ssPv1(U_498) | ssPv2(skf2(U_498)) | ~ssPv1(skf2(skf2(U_498))) | ssPv1(skf2(U_498)) | ~ssPv3(skf3(skf2(U_498))) | ssPv2(skf3(skf2(U_498))) | ~ssPv4(skf2(U_498))))). % 12.15/4.43 tff(c_5590, plain, (![U_2]: (ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2)))))). % 12.15/4.43 tff(c_5553, plain, (![U_2]: (ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2) | ssPv2(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 12.15/4.43 tff(c_1384, plain, (![U_240]: (ssPv1(skf2(skf3(U_240))) | ~ssPv3(skf2(skf3(U_240))) | ~ssPv2(skf2(skf3(U_240))) | ~ssPv4(skf3(U_240)) | ssPv2(skf3(U_240)) | ~ssPv1(U_240) | ~ssPv3(skf3(skf3(U_240)))))). % 12.15/4.43 tff(c_2744, plain, (![U_240]: (~ssPv1(skf3(U_240)) | ~ssPv4(skf3(U_240)) | ssPv3(skf2(skf3(U_240))) | ssPv1(skf2(skf3(U_240))) | ssPv2(skf3(U_240)) | ~ssPv1(U_240) | ~ssPv3(skf3(skf3(U_240)))))). % 12.15/4.43 tff(c_5468, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ~ssPv4(U_2) | ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.15/4.43 tff(c_5485, plain, (![U_1]: (~ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.15/4.43 tff(c_5467, plain, (![U_1]: (~ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1)))). % 12.15/4.43 tff(c_5460, plain, (![U_1, U_588]: (~ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv4(U_588) | ~ssRr(U_588, U_1) | ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1)))). % 12.15/4.43 tff(c_1959, plain, (![U_366, W_151, U_152]: (~ssPv4(U_366) | ~ssPv1(W_151) | ~ssRr(W_151, U_366) | ~ssPv4(U_152) | ~ssRr(U_152, U_366) | ssPv2(skf2(U_366)) | ssPv3(skf2(U_366)) | ssPv1(skf2(U_366)) | ssPv2(U_366)))). % 12.15/4.43 tff(c_5448, plain, (![U_584]: (~ssPv2(skf3(U_584)) | ssPv1(skf2(skf3(U_584))) | ~ssPv1(U_584) | ssPv4(skf3(U_584)) | ~ssPv1(skf3(U_584)) | ~ssPv1(skf3(skf3(U_584)))))). % 12.15/4.43 tff(c_5420, plain, (![U_582]: (~ssPv4(skf3(skf3(U_582))) | ssPv4(skf3(U_582)) | ssPv2(skf3(U_582)) | ~ssPv4(U_582) | ssPv2(U_582) | ~ssPv3(skf3(U_582)) | ~ssPv1(skf3(U_582))))). % 12.15/4.43 tff(c_5409, plain, (![U_580, U_190]: (~ssPv4(U_580) | ~ssRr(U_580, skf3(U_190)) | ssPv4(skf3(U_190)) | ssPv2(skf3(U_190)) | ~ssPv4(U_190) | ssPv2(U_190) | ~ssPv3(skf3(U_190)) | ~ssPv1(skf3(U_190))))). % 12.31/4.44 tff(c_5285, plain, (![U_572, U_574]: (~ssPv1(skf3(U_572)) | ~ssPv3(skf2(skf3(U_572))) | ~ssPv4(U_574) | ~ssRr(U_574, skf3(U_572)) | ~ssPv3(skf3(U_572)) | ssPv4(skf3(U_572)) | ssPv2(skf3(U_572)) | ~ssPv4(U_572)))). % 12.31/4.44 tff(c_1807, plain, (![U_352]: (~ssPv1(U_352) | ssPv2(skf2(skf3(U_352))) | ~ssPv3(skf3(U_352)) | ~ssPv1(skf3(U_352)) | ssPv2(skf3(U_352)) | ~ssPv3(skf3(skf3(U_352))) | ~ssPv2(skf3(skf3(U_352)))))). % 12.31/4.44 tff(c_5291, plain, (![U_575]: (~ssPv1(skf3(U_575)) | ~ssPv3(U_575) | ~ssPv4(skf3(skf3(U_575))) | ~ssPv3(skf3(U_575)) | ssPv4(skf3(U_575)) | ssPv2(skf3(U_575)) | ~ssPv4(U_575)))). % 12.31/4.44 tff(c_5284, plain, (![U_1, U_574]: (~ssPv1(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv4(U_574) | ~ssRr(U_574, skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv2(skf3(U_1)) | ~ssPv4(U_1)))). % 12.31/4.44 tff(c_809, plain, (![U_265, W_188, U_189]: (~ssPv1(skf3(U_265)) | ~ssPv3(W_188) | ~ssRr(skf3(U_265), W_188) | ~ssPv4(U_189) | ~ssRr(U_189, skf3(U_265)) | ~ssPv3(skf3(U_265)) | ssPv4(skf3(U_265)) | ssPv2(skf3(U_265)) | ~ssPv4(U_265)))). % 12.31/4.44 tff(c_5213, plain, (![U_2]: (~ssPv1(skf3(skf2(U_2))) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv2(skf2(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 12.31/4.44 tff(c_5235, plain, (![U_569]: (~ssPv4(skf3(skf3(U_569))) | ~ssPv2(skf2(skf3(U_569))) | ~ssPv1(skf3(U_569)) | ssPv4(skf3(U_569)) | ssPv1(skf2(skf3(U_569))) | ~ssPv1(U_569)))). % 12.31/4.44 tff(c_4349, plain, (![U_269, U_508]: (~ssPv4(U_269) | ~ssRr(U_269, skf3(U_508)) | ~ssPv2(skf2(skf3(U_508))) | ~ssPv1(skf3(U_508)) | ssPv4(skf3(U_508)) | ssPv1(skf2(skf3(U_508))) | ~ssPv1(U_508)))). % 12.31/4.44 tff(c_5212, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv1(U_1)))). % 12.31/4.44 tff(c_5205, plain, (![U_1, U_564]: (~ssPv1(skf3(U_1)) | ~ssPv4(U_564) | ~ssRr(U_564, U_1) | ssPv2(U_1) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv1(U_1)))). % 12.31/4.44 tff(c_4670, plain, (![W_151, U_526, U_152]: (~ssPv1(W_151) | ~ssRr(W_151, U_526) | ~ssPv4(U_152) | ~ssRr(U_152, U_526) | ssPv2(U_526) | ~ssPv2(skf2(U_526)) | ~ssPv4(U_526) | ~ssPv1(skf2(U_526)) | ~ssPv1(U_526)))). % 12.31/4.44 tff(c_5167, plain, (![U_558]: (ssPv1(skf2(skf3(U_558))) | ssPv2(skf3(U_558)) | ssPv3(U_558) | ~ssPv1(skf3(U_558)) | ~ssPv3(skf3(U_558)) | ~ssPv1(skf3(skf3(U_558))) | ~ssPv4(skf3(U_558))))). % 12.31/4.44 tff(c_3385, plain, (![U_457]: (~ssPv1(skf2(U_457)) | ~ssPv3(skf2(U_457)) | ssPv4(skf2(U_457)) | ~ssPv2(U_457) | ssPv2(skf2(U_457)) | ~ssPv3(skf3(skf2(U_457))) | ~ssPv2(skf3(skf2(U_457)))))). % 12.31/4.44 tff(c_5165, plain, (![U_558]: (ssPv1(U_558) | ssPv2(skf3(U_558)) | ssPv3(U_558) | ~ssPv1(skf3(U_558)) | ~ssPv3(skf3(U_558)) | ~ssPv1(skf3(skf3(U_558))) | ~ssPv4(skf3(U_558))))). % 12.31/4.44 tff(c_1751, plain, (![U_337]: (ssPv2(skf3(U_337)) | ssPv3(U_337) | ~ssPv1(skf3(U_337)) | ~ssPv3(skf3(U_337)) | ~ssPv1(skf3(skf3(U_337))) | ssPv2(skf3(skf3(U_337))) | ~ssPv4(skf3(U_337))))). % 12.31/4.44 tff(c_5126, plain, (![U_555]: (~ssPv4(skf3(U_555)) | ~ssPv1(skf3(skf3(U_555))) | ~ssPv1(U_555) | ssPv2(skf3(U_555)) | ~ssPv3(skf3(skf3(U_555))) | ~ssPv2(skf3(skf3(U_555)))))). % 12.31/4.44 tff(c_5109, plain, (![U_553]: (~ssPv4(skf3(U_553)) | ~ssPv1(skf3(skf3(U_553))) | ~ssPv4(skf3(skf3(U_553))) | ssPv2(skf3(U_553)) | ~ssPv1(U_553) | ~ssPv3(skf3(skf3(U_553)))))). % 12.31/4.44 tff(c_5084, plain, (![U_549, U_551]: (~ssPv4(skf3(U_549)) | ~ssPv1(skf3(skf3(U_549))) | ~ssPv4(U_551) | ~ssRr(U_551, skf3(U_549)) | ssPv2(skf3(U_549)) | ~ssPv1(U_549) | ~ssPv3(skf3(skf3(U_549)))))). % 12.31/4.44 tff(c_5050, plain, (![U_547]: (~ssPv1(U_547) | ~ssPv2(skf2(U_547)) | ~ssPv4(U_547) | ssPv3(skf2(U_547)) | ssPv1(skf2(U_547)) | ssPv2(U_547)))). % 12.31/4.44 tff(c_695, plain, (![U_242, W_151, U_152]: (~ssPv4(skf3(U_242)) | ~ssPv1(W_151) | ~ssRr(W_151, skf3(U_242)) | ~ssPv4(U_152) | ~ssRr(U_152, skf3(U_242)) | ssPv2(skf3(U_242)) | ~ssPv1(U_242) | ~ssPv3(skf3(skf3(U_242)))))). % 12.31/4.44 tff(c_5049, plain, (![U_547]: (ssPv3(U_547) | ~ssPv2(skf2(U_547)) | ~ssPv4(U_547) | ssPv3(skf2(U_547)) | ssPv1(skf2(U_547)) | ssPv2(U_547)))). % 12.31/4.44 tff(c_5000, plain, (![U_2]: (ssPv4(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.44 tff(c_1356, plain, (![U_270]: (~ssPv1(skf3(U_270)) | ~ssPv1(U_270) | ~ssPv3(U_270) | ssPv3(skf3(U_270)) | ssPv2(skf3(skf3(U_270))) | ssPv3(skf3(skf3(U_270))) | ssPv1(skf3(skf3(U_270)))))). % 12.31/4.44 tff(c_4823, plain, (![U_534, U_536]: (~ssPv4(skf2(U_534)) | ~ssPv1(skf3(skf2(U_534))) | ~ssPv4(U_536) | ~ssRr(U_536, skf2(U_534)) | ssPv2(skf2(U_534)) | ~ssPv1(skf2(skf2(U_534))) | ~ssPv3(U_534)))). % 12.31/4.44 tff(c_4831, plain, (![U_537]: (~ssPv4(skf2(U_537)) | ~ssPv1(U_537) | ~ssPv4(skf3(skf2(U_537))) | ssPv2(skf2(U_537)) | ~ssPv1(skf2(skf2(U_537))) | ~ssPv3(U_537)))). % 12.31/4.44 tff(c_4848, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_2) | ~ssPv3(U_2) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2)))). % 12.31/4.44 tff(c_4832, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.44 tff(c_4824, plain, (![U_2, U_536]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_536) | ~ssRr(U_536, skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.44 tff(c_672, plain, (![U_2, W_238, U_239]: (~ssPv4(skf2(U_2)) | ~ssPv1(W_238) | ~ssRr(W_238, skf2(U_2)) | ~ssPv4(U_239) | ~ssRr(U_239, skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.44 tff(c_2963, plain, (![U_222]: (ssPv2(skf2(skf3(U_222))) | ~ssPv2(skf3(U_222)) | ssPv1(skf3(U_222)) | ssPv3(skf3(U_222)) | ssPv4(skf3(U_222)) | ssPv1(skf2(skf3(U_222))) | ~ssPv1(U_222)))). % 12.31/4.44 tff(c_2681, plain, (![U_419]: (ssPv3(skf2(skf3(U_419))) | ssPv1(skf3(U_419)) | ssPv2(skf3(U_419)) | ~ssPv1(U_419) | ssPv3(skf3(U_419)) | ssPv1(skf3(skf3(U_419))) | ~ssPv4(skf3(U_419))))). % 12.31/4.44 tff(c_822, plain, (![U_165]: (ssPv3(skf2(skf2(U_165))) | ssPv1(skf2(U_165)) | ssPv2(skf2(U_165)) | ~ssPv1(skf2(skf2(U_165))) | ssPv3(skf2(U_165)) | ssPv1(U_165) | ~ssPv4(skf2(U_165))))). % 12.31/4.44 tff(c_4180, plain, (![U_493]: (ssPv1(skf2(skf3(U_493))) | ~ssPv3(skf3(U_493)) | ssPv2(skf3(U_493)) | ssPv4(U_493) | ~ssPv1(U_493) | ~ssPv1(skf3(skf3(U_493))) | ~ssPv4(skf3(U_493))))). % 12.31/4.44 tff(c_4767, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.44 tff(c_4619, plain, (![U_2]: (ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2)))). % 12.31/4.44 tff(c_1239, plain, (![U_314]: (~ssPv1(U_314) | ssPv2(U_314) | ~ssPv3(skf3(U_314)) | ~ssPv1(skf3(U_314)) | ssPv2(skf3(U_314)) | ~ssPv3(skf3(skf3(U_314))) | ~ssPv2(skf3(skf3(U_314)))))). % 12.31/4.44 tff(c_4449, plain, (![U_519]: (~ssPv3(skf3(skf2(U_519))) | ~ssPv4(U_519) | ssPv2(skf2(U_519)) | ~ssPv2(U_519) | ~ssPv3(skf2(U_519)) | ~ssPv1(skf2(U_519))))). % 12.31/4.44 tff(c_4559, plain, (![U_2]: (~ssPv3(U_2) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.31/4.44 tff(c_4423, plain, (![U_143, U_516]: (~ssPv3(U_143) | ~ssRr(U_143, skf2(U_516)) | ~ssPv4(U_516) | ssPv2(skf2(U_516)) | ~ssPv2(U_516) | ~ssPv3(skf2(U_516)) | ~ssPv1(skf2(U_516))))). % 12.31/4.44 tff(c_4418, plain, (![U_515]: (~ssPv4(skf3(skf2(U_515))) | ssPv2(skf2(U_515)) | ~ssPv2(U_515) | ssPv2(skf2(skf2(U_515))) | ~ssPv3(skf2(U_515)) | ~ssPv1(skf2(U_515))))). % 12.31/4.44 tff(c_4419, plain, (![U_2]: (~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv2(U_2) | ssPv2(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv1(skf2(U_2))))). % 12.31/4.44 tff(c_2614, plain, (![U_415, U_414]: (~ssPv4(U_415) | ~ssRr(U_415, skf2(U_414)) | ssPv2(skf2(U_414)) | ~ssPv2(U_414) | ssPv2(skf2(skf2(U_414))) | ~ssPv3(skf2(U_414)) | ~ssPv1(skf2(U_414))))). % 12.31/4.44 tff(c_4054, plain, (![U_2]: (~ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.44 tff(c_4051, plain, (![U_307]: (~ssPv2(skf2(skf3(U_307))) | ssPv3(skf2(skf3(U_307))) | ssPv3(skf3(U_307)) | ssPv4(skf3(U_307)) | ssPv1(U_307) | ~ssPv1(skf2(skf3(U_307)))))). % 12.31/4.44 tff(c_4052, plain, (![U_240]: (~ssPv2(skf2(skf3(U_240))) | ssPv3(skf2(skf3(U_240))) | ssPv3(skf3(U_240)) | ssPv2(skf3(U_240)) | ~ssPv1(U_240) | ~ssPv3(skf3(skf3(U_240)))))). % 12.31/4.44 tff(c_3784, plain, (![U_2]: (~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf3(skf2(U_2))) | ssPv2(skf3(skf2(U_2))) | ~ssPv4(skf2(U_2))))). % 12.31/4.44 tff(c_2421, plain, (![U_1]: (~ssPv2(skf2(skf3(U_1))) | ssPv3(skf2(skf3(U_1))) | ssPv3(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ~ssPv1(U_1)))). % 12.31/4.44 tff(c_3284, plain, (![U_1]: (~ssPv2(skf2(skf3(U_1))) | ~ssPv1(skf3(U_1)) | ssPv3(skf2(skf3(U_1))) | ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ~ssPv1(U_1)))). % 12.31/4.44 tff(c_4311, plain, (![U_502, U_503]: (ssPv4(skf2(U_502)) | ssPv2(U_503) | ~ssPv4(skf2(skf2(U_502))) | ~ssRr(U_503, skf2(U_502)) | ssPv2(U_502) | ~ssPv2(skf2(U_502)) | ~ssPv4(U_502)))). % 12.31/4.44 tff(c_736, plain, (![U_248, U_179, W_181]: (ssPv4(skf2(U_248)) | ssPv2(U_179) | ~ssPv4(W_181) | ~ssRr(skf2(U_248), W_181) | ~ssRr(U_179, skf2(U_248)) | ssPv2(U_248) | ~ssPv2(skf2(U_248)) | ~ssPv4(U_248)))). % 12.31/4.44 tff(c_4260, plain, (![U_498]: (~ssPv4(skf2(U_498)) | ~ssPv1(U_498) | ~ssPv1(skf2(skf2(U_498))) | ssPv2(skf2(U_498)) | ~ssPv3(skf3(skf2(U_498))) | ~ssPv2(skf3(skf2(U_498)))))). % 12.31/4.44 tff(c_3918, plain, (![U_153]: (ssPv2(skf2(U_153)) | ssPv3(skf2(U_153)) | ssPv2(U_153) | ~ssPv1(skf2(U_153)) | ~ssPv1(skf3(U_153)) | ssPv2(skf3(U_153)) | ~ssPv4(U_153)))). % 12.31/4.44 tff(c_4237, plain, (![U_496]: (ssPv1(skf2(skf3(U_496))) | ssPv2(skf3(U_496)) | ~ssPv3(skf3(U_496)) | ~ssPv2(U_496) | ~ssPv1(skf3(skf3(U_496))) | ~ssPv4(skf3(U_496))))). % 12.31/4.44 tff(c_3700, plain, (![U_471]: (~ssPv4(skf2(U_471)) | ~ssPv1(U_471) | ~ssPv4(skf3(skf2(U_471))) | ssPv2(skf2(U_471)) | ~ssPv1(skf2(skf2(U_471))) | ~ssPv3(skf3(skf2(U_471)))))). % 12.31/4.44 tff(c_4235, plain, (![U_496]: (ssPv1(U_496) | ssPv2(skf3(U_496)) | ~ssPv3(skf3(U_496)) | ~ssPv2(U_496) | ~ssPv1(skf3(skf3(U_496))) | ~ssPv4(skf3(U_496))))). % 12.31/4.44 tff(c_3802, plain, (![U_158]: (ssPv2(skf3(U_158)) | ~ssPv3(skf3(U_158)) | ~ssPv2(U_158) | ~ssPv1(skf3(skf3(U_158))) | ssPv2(skf3(skf3(U_158))) | ~ssPv4(skf3(U_158))))). % 12.31/4.44 tff(c_3923, plain, (![U_1]: (ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ssPv3(U_1) | ssPv1(skf3(U_1)) | ~ssPv4(U_1)))). % 12.31/4.44 tff(c_4087, plain, (![U_1]: (~ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ssPv3(U_1) | ssPv1(skf3(U_1)) | ~ssPv4(U_1)))). % 12.31/4.44 tff(c_3799, plain, (![U_253]: (ssPv2(skf3(U_253)) | ssPv4(U_253) | ~ssPv1(U_253) | ~ssPv1(skf3(skf3(U_253))) | ssPv2(skf3(skf3(U_253))) | ~ssPv4(skf3(U_253))))). % 12.31/4.44 tff(c_3892, plain, (![U_2]: (ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(skf2(U_2))) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.44 tff(c_3889, plain, (![U_307]: (ssPv2(skf2(skf3(U_307))) | ssPv3(skf2(skf3(U_307))) | ssPv4(skf3(U_307)) | ssPv1(U_307) | ~ssPv1(skf2(skf3(U_307)))))). % 12.31/4.44 tff(c_4062, plain, (![U_485, U_487]: (~ssPv1(skf2(U_485)) | ~ssPv3(skf2(skf2(U_485))) | ~ssPv4(U_487) | ~ssRr(U_487, skf2(U_485)) | ssPv2(U_485) | ~ssPv2(skf2(U_485)) | ~ssPv4(U_485)))). % 12.31/4.44 tff(c_4055, plain, (![U_1]: (~ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.44 tff(c_735, plain, (![U_248, W_188, U_189]: (~ssPv1(skf2(U_248)) | ~ssPv3(W_188) | ~ssRr(skf2(U_248), W_188) | ~ssPv4(U_189) | ~ssRr(U_189, skf2(U_248)) | ssPv2(U_248) | ~ssPv2(skf2(U_248)) | ~ssPv4(U_248)))). % 12.31/4.44 tff(c_4020, plain, (![U_2]: (~ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 12.31/4.44 tff(c_3800, plain, (![U_205]: (ssPv3(skf2(U_205)) | ssPv3(U_205) | ~ssPv1(skf3(skf2(U_205))) | ssPv2(skf3(skf2(U_205))) | ~ssPv4(skf2(U_205))))). % 12.31/4.45 tff(c_3785, plain, (![U_474]: (ssPv2(U_474) | ~ssPv1(skf2(U_474)) | ssPv1(U_474) | ~ssPv1(skf3(U_474)) | ssPv2(skf3(U_474)) | ~ssPv4(U_474)))). % 12.31/4.45 tff(c_3797, plain, (![U_474]: (ssPv1(skf2(U_474)) | ~ssPv2(U_474) | ssPv1(U_474) | ~ssPv1(skf3(U_474)) | ssPv2(skf3(U_474)) | ~ssPv4(U_474)))). % 12.31/4.45 tff(c_3701, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2)))))). % 12.31/4.45 tff(c_3893, plain, (![U_1]: (ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.45 tff(c_3844, plain, (![U_282]: (ssPv2(U_282) | ~ssPv1(U_282) | ssPv3(U_282) | ~ssPv4(U_282)))). % 12.31/4.45 tff(c_3801, plain, (![U_474]: (ssPv2(U_474) | ssPv3(U_474) | ~ssPv1(skf3(U_474)) | ssPv2(skf3(U_474)) | ~ssPv4(U_474)))). % 12.31/4.45 tff(c_3719, plain, (![U_153]: (ssPv3(skf3(U_153)) | ~ssPv1(skf3(U_153)) | ssPv2(skf3(U_153)) | ~ssPv4(U_153)))). % 12.31/4.45 tff(c_2979, plain, (![U_2, U_437]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_437) | ~ssRr(U_437, skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2)))))). % 12.31/4.45 tff(c_2986, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2)))))). % 12.31/4.45 tff(c_1355, plain, (![U_278]: (ssPv1(U_278) | ~ssPv2(skf3(U_278)) | ssPv3(skf3(U_278)) | ssPv2(skf3(skf3(U_278))) | ssPv3(skf3(skf3(U_278))) | ssPv1(skf3(skf3(U_278)))))). % 12.31/4.45 tff(c_3452, plain, (![U_461]: (ssPv1(skf2(U_461)) | ssPv2(U_461) | ssPv3(U_461) | ssPv3(skf2(U_461)) | ssPv2(skf3(skf2(U_461))) | ~ssPv4(skf2(U_461))))). % 12.31/4.45 tff(c_3425, plain, (![U_2]: (~ssPv4(U_2) | ssPv3(U_2) | ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.45 tff(c_3394, plain, (![U_459]: (~ssPv4(skf3(skf2(U_459))) | ssPv1(skf2(U_459)) | ssPv2(U_459) | ssPv3(skf2(U_459)) | ssPv3(U_459) | ~ssPv4(skf2(U_459))))). % 12.31/4.45 tff(c_3395, plain, (![U_2]: (~ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_2) | ssPv3(skf2(U_2)) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 12.31/4.45 tff(c_3364, plain, (![U_456, U_2]: (~ssPv4(U_456) | ~ssRr(U_456, skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2) | ssPv3(skf2(U_2)) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 12.31/4.45 tff(c_3297, plain, (![U_452]: (~ssPv1(skf2(U_452)) | ~ssPv4(skf3(skf2(U_452))) | ~ssPv3(skf2(U_452)) | ssPv4(skf2(U_452)) | ssPv2(skf2(U_452)) | ~ssPv2(U_452)))). % 12.31/4.45 tff(c_2705, plain, (![U_421, U_423]: (~ssPv4(skf2(U_421)) | ~ssPv1(skf3(skf2(U_421))) | ~ssPv4(U_423) | ~ssRr(U_423, skf2(U_421)) | ssPv3(skf2(U_421)) | ssPv1(skf2(U_421)) | ssPv2(U_421)))). % 12.31/4.45 tff(c_3298, plain, (![U_2]: (~ssPv1(skf2(U_2)) | ~ssPv4(U_2) | ~ssPv3(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv2(U_2)))). % 12.31/4.45 tff(c_2615, plain, (![U_2, U_415]: (~ssPv1(skf2(U_2)) | ~ssPv4(U_415) | ~ssRr(U_415, skf2(U_2)) | ~ssPv3(skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv2(U_2)))). % 12.31/4.45 tff(c_3253, plain, (![U_450]: (~ssPv2(skf2(U_450)) | ~ssPv1(U_450) | ssPv1(skf2(U_450)) | ssPv3(skf2(U_450)) | ~ssPv4(skf2(U_450))))). % 12.31/4.45 tff(c_3237, plain, (![U_449]: (~ssPv1(U_449) | ssPv1(skf2(U_449)) | ssPv3(skf2(U_449)) | ssPv2(skf3(skf2(U_449))) | ~ssPv4(skf2(U_449))))). % 12.31/4.45 tff(c_3128, plain, (![U_1]: (ssPv1(skf2(U_1)) | ssPv2(U_1) | ~ssPv2(skf2(U_1)) | ~ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf3(U_1))))). % 12.31/4.45 tff(c_3007, plain, (![U_1]: (~ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv1(skf2(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.31/4.45 tff(c_2985, plain, (![U_1]: (~ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.45 tff(c_2978, plain, (![U_1, U_437]: (~ssPv4(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv4(U_437) | ~ssRr(U_437, U_1) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.45 tff(c_673, plain, (![U_1, W_238, U_239]: (~ssPv4(U_1) | ~ssPv1(W_238) | ~ssRr(W_238, U_1) | ~ssPv4(U_239) | ~ssRr(U_239, U_1) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.45 tff(c_587, plain, (![U_222]: (ssPv2(skf2(skf3(U_222))) | ~ssPv3(skf2(skf3(U_222))) | ~ssPv2(skf3(U_222)) | ssPv4(skf3(U_222)) | ssPv1(skf2(skf3(U_222))) | ~ssPv1(U_222)))). % 12.31/4.45 tff(c_2894, plain, (![U_432]: (ssPv1(skf3(U_432)) | ssPv1(U_432) | ~ssPv2(skf3(U_432)) | ~ssPv1(skf3(skf3(U_432))) | ssPv2(skf3(skf3(U_432))) | ~ssPv4(skf3(U_432))))). % 12.31/4.45 tff(c_1439, plain, (![U_201]: (~ssPv1(U_201) | ssPv1(skf2(U_201)) | ssPv1(skf2(skf2(U_201))) | ~ssPv2(skf2(U_201)) | ~ssPv1(skf3(skf2(U_201))) | ~ssPv4(skf2(U_201))))). % 12.31/4.45 tff(c_2715, plain, (![U_424]: (~ssPv4(skf2(U_424)) | ~ssPv1(U_424) | ~ssPv4(skf3(skf2(U_424))) | ssPv3(skf2(U_424)) | ssPv1(skf2(U_424)) | ssPv2(U_424)))). % 12.31/4.45 tff(c_2742, plain, (![U_2]: (~ssPv1(U_2) | ~ssPv4(U_2) | ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.45 tff(c_2716, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_2) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.45 tff(c_2706, plain, (![U_2, U_423]: (~ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_423) | ~ssRr(U_423, skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.45 tff(c_674, plain, (![U_2, W_238, U_239]: (~ssPv4(skf2(U_2)) | ~ssPv1(W_238) | ~ssRr(W_238, skf2(U_2)) | ~ssPv4(U_239) | ~ssRr(U_239, skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.45 tff(c_2148, plain, (![U_378]: (~ssPv1(skf3(U_378)) | ~ssPv1(U_378) | ssPv4(skf3(U_378)) | ssPv2(skf3(U_378)) | ~ssPv3(skf3(skf3(U_378))) | ~ssPv2(skf3(skf3(U_378)))))). % 12.31/4.45 tff(c_698, plain, (![U_242]: (ssPv3(skf2(skf3(U_242))) | ssPv1(skf3(U_242)) | ssPv3(skf3(U_242)) | ssPv2(skf3(U_242)) | ~ssPv1(U_242) | ~ssPv3(skf3(skf3(U_242)))))). % 12.31/4.45 tff(c_1179, plain, (![U_309]: (ssPv3(skf2(skf3(U_309))) | ssPv1(skf3(U_309)) | ssPv3(skf3(U_309)) | ssPv4(skf3(U_309)) | ssPv1(U_309) | ~ssPv1(skf2(skf3(U_309)))))). % 12.31/4.45 tff(c_2628, plain, (![U_416]: (~ssPv1(skf3(U_416)) | ssPv1(U_416) | ~ssPv1(skf2(skf3(U_416))) | ssPv4(skf3(U_416)) | ~ssPv3(skf3(U_416)) | ~ssPv2(skf3(U_416))))). % 12.31/4.45 tff(c_1178, plain, (![U_309]: (~ssPv2(skf2(skf3(U_309))) | ~ssPv1(skf3(U_309)) | ~ssPv2(skf3(U_309)) | ssPv4(skf3(U_309)) | ssPv1(U_309) | ~ssPv1(skf2(skf3(U_309)))))). % 12.31/4.45 tff(c_2539, plain, (![U_409, U_411]: (~ssPv1(skf2(U_409)) | ~ssPv3(skf2(skf2(U_409))) | ~ssPv4(U_411) | ~ssRr(U_411, skf2(U_409)) | ssPv2(skf2(U_409)) | ~ssPv3(skf2(U_409)) | ~ssPv2(U_409)))). % 12.31/4.45 tff(c_589, plain, (![U_222]: (ssPv3(skf2(skf3(U_222))) | ssPv1(skf3(U_222)) | ssPv3(skf3(U_222)) | ssPv4(skf3(U_222)) | ssPv1(skf2(skf3(U_222))) | ~ssPv1(U_222)))). % 12.31/4.45 tff(c_658, plain, (![U_2, W_235, U_236]: (~ssPv1(skf2(U_2)) | ~ssPv3(W_235) | ~ssRr(skf2(U_2), W_235) | ~ssPv4(U_236) | ~ssRr(U_236, skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2)))). % 12.31/4.45 tff(c_2476, plain, (![U_404]: (~ssPv1(skf3(U_404)) | ssPv1(skf2(skf3(U_404))) | ~ssPv1(U_404) | ssPv4(skf3(U_404)) | ~ssPv3(skf3(U_404)) | ~ssPv2(skf3(U_404))))). % 12.31/4.45 tff(c_588, plain, (![U_222]: (~ssPv2(skf2(skf3(U_222))) | ~ssPv1(skf3(U_222)) | ~ssPv2(skf3(U_222)) | ssPv4(skf3(U_222)) | ssPv1(skf2(skf3(U_222))) | ~ssPv1(U_222)))). % 12.31/4.45 tff(c_573, plain, (![U_221]: (ssPv3(skf2(skf2(U_221))) | ssPv1(skf2(U_221)) | ssPv3(skf2(U_221)) | ssPv2(skf2(U_221)) | ~ssPv1(skf2(skf2(U_221))) | ~ssPv3(U_221)))). % 12.31/4.45 tff(c_2379, plain, (![U_397]: (~ssPv1(skf3(U_397)) | ~ssPv1(U_397) | ~ssPv4(skf3(skf3(U_397))) | ssPv2(skf2(skf3(U_397))) | ~ssPv1(skf2(skf3(U_397))) | ~ssPv2(skf3(U_397))))). % 12.31/4.45 tff(c_904, plain, (![U_280]: (ssPv1(U_280) | ~ssPv2(skf3(U_280)) | ssPv1(skf3(U_280)) | ~ssPv3(skf3(skf3(U_280))) | ssPv2(skf3(skf3(U_280))) | ~ssPv4(skf3(U_280))))). % 12.31/4.45 tff(c_879, plain, (![U_273, U_274]: (~ssPv1(skf3(U_273)) | ~ssPv1(U_273) | ~ssPv4(U_274) | ~ssRr(U_274, skf3(U_273)) | ssPv2(skf2(skf3(U_273))) | ~ssPv1(skf2(skf3(U_273))) | ~ssPv2(skf3(U_273))))). % 12.31/4.45 tff(c_2190, plain, (![U_382]: (ssPv3(skf2(U_382)) | ~ssPv1(skf2(U_382)) | ssPv4(skf2(U_382)) | ssPv2(skf2(U_382)) | ~ssPv1(skf2(skf2(U_382))) | ~ssPv3(U_382)))). % 12.31/4.45 tff(c_1993, plain, (![U_370]: (ssPv3(skf3(U_370)) | ~ssPv1(skf3(U_370)) | ssPv2(skf3(U_370)) | ssPv4(skf3(U_370)) | ssPv1(U_370) | ~ssPv1(skf2(skf3(U_370)))))). % 12.31/4.45 tff(c_936, plain, (![U_201]: (~ssPv2(skf2(U_201)) | ~ssPv1(U_201) | ~ssPv1(skf2(U_201)) | ssPv3(skf2(U_201)) | ssPv1(skf3(skf2(U_201))) | ~ssPv4(skf2(U_201))))). % 12.31/4.45 tff(c_2197, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(U_2) | ssPv2(skf2(skf2(U_2))) | ssPv3(skf2(skf2(U_2))) | ssPv1(skf2(skf2(U_2))) | ssPv2(skf2(U_2))))). % 12.31/4.45 tff(c_1142, plain, (![U_306]: (ssPv3(skf3(U_306)) | ssPv2(skf3(U_306)) | ~ssPv1(skf3(U_306)) | ssPv4(skf3(U_306)) | ssPv1(skf2(skf3(U_306))) | ~ssPv1(U_306)))). % 12.31/4.45 tff(c_1887, plain, (![U_360]: (~ssPv1(skf3(U_360)) | ~ssPv3(U_360) | ~ssPv2(skf3(U_360)) | ssPv3(skf3(U_360)) | ssPv2(skf3(skf3(U_360))) | ~ssPv4(skf3(U_360))))). % 12.31/4.45 tff(c_2210, plain, (![U_386]: (ssPv4(skf3(U_386)) | ~ssPv1(U_386) | ssPv3(skf3(U_386)) | ssPv1(skf3(U_386)) | ssPv2(skf3(skf3(U_386)))))). % 12.31/4.45 tff(c_2196, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf3(U_1)) | ssPv2(skf2(U_1)) | ssPv3(skf2(U_1)) | ssPv1(skf2(U_1)) | ssPv2(U_1)))). % 12.31/4.45 tff(c_1963, plain, (![U_366, U_123]: (ssPv4(U_366) | ssPv2(U_123) | ~ssRr(U_123, U_366) | ssPv2(skf2(U_366)) | ssPv3(skf2(U_366)) | ssPv1(skf2(U_366)) | ssPv2(U_366)))). % 12.31/4.45 tff(c_2155, plain, (![U_379]: (ssPv4(skf2(U_379)) | ssPv2(skf3(skf2(U_379))) | ssPv2(skf2(U_379)) | ~ssPv1(skf2(skf2(U_379))) | ~ssPv3(U_379)))). % 12.31/4.45 tff(c_2156, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.45 tff(c_574, plain, (![U_221, U_123]: (ssPv4(skf2(U_221)) | ssPv2(U_123) | ~ssRr(U_123, skf2(U_221)) | ssPv2(skf2(U_221)) | ~ssPv1(skf2(skf2(U_221))) | ~ssPv3(U_221)))). % 12.31/4.45 tff(c_2085, plain, (![U_374]: (~ssPv1(skf3(U_374)) | ~ssPv1(U_374) | ~ssPv4(skf3(skf3(U_374))) | ssPv4(skf3(U_374)) | ssPv2(skf3(U_374)) | ~ssPv2(skf3(skf3(U_374)))))). % 12.31/4.45 tff(c_855, plain, (![U_272]: (~ssPv1(skf3(U_272)) | ~ssPv1(U_272) | ~ssPv3(U_272) | ssPv2(skf3(U_272)) | ~ssPv3(skf3(skf3(U_272))) | ~ssPv2(skf3(skf3(U_272)))))). % 12.31/4.45 tff(c_2074, plain, (![U_1]: (ssPv1(skf2(U_1)) | ssPv2(skf2(U_1)) | ~ssPv2(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf3(U_1))))). % 12.31/4.45 tff(c_877, plain, (![U_273, U_274]: (~ssPv1(skf3(U_273)) | ~ssPv1(U_273) | ~ssPv4(U_274) | ~ssRr(U_274, skf3(U_273)) | ssPv4(skf3(U_273)) | ssPv2(skf3(U_273)) | ~ssPv2(skf3(skf3(U_273)))))). % 12.31/4.45 tff(c_1990, plain, (![U_370]: (~ssPv3(skf3(U_370)) | ssPv2(skf3(U_370)) | ssPv4(skf3(U_370)) | ssPv1(U_370) | ~ssPv1(skf2(skf3(U_370)))))). % 12.31/4.45 tff(c_1991, plain, (![U_370]: (ssPv3(U_370) | ssPv2(skf3(U_370)) | ssPv4(skf3(U_370)) | ssPv1(U_370) | ~ssPv1(skf2(skf3(U_370)))))). % 12.31/4.45 tff(c_1976, plain, (![U_368]: (ssPv2(skf3(U_368)) | ssPv2(skf3(skf3(U_368))) | ssPv4(skf3(U_368)) | ssPv1(U_368) | ~ssPv1(skf2(skf3(U_368)))))). % 12.31/4.45 tff(c_1180, plain, (![U_309, U_123]: (ssPv2(skf3(U_309)) | ssPv2(U_123) | ~ssRr(U_123, skf3(U_309)) | ssPv4(skf3(U_309)) | ssPv1(U_309) | ~ssPv1(skf2(skf3(U_309)))))). % 12.31/4.45 tff(c_1962, plain, (![U_366]: (ssPv1(U_366) | ssPv3(U_366) | ssPv2(skf2(U_366)) | ssPv3(skf2(U_366)) | ssPv1(skf2(U_366)) | ssPv2(U_366)))). % 12.31/4.45 tff(c_1920, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.31/4.45 tff(c_1893, plain, (![U_361]: (ssPv4(skf3(U_361)) | ssPv2(skf3(skf3(U_361))) | ssPv2(skf3(U_361)) | ~ssPv1(U_361) | ~ssPv3(skf3(skf3(U_361)))))). % 12.31/4.45 tff(c_699, plain, (![U_242, U_123]: (ssPv4(skf3(U_242)) | ssPv2(U_123) | ~ssRr(U_123, skf3(U_242)) | ssPv2(skf3(U_242)) | ~ssPv1(U_242) | ~ssPv3(skf3(skf3(U_242)))))). % 12.31/4.45 tff(c_1713, plain, (![U_345]: (~ssPv1(skf3(U_345)) | ~ssPv3(U_345) | ~ssPv4(skf3(skf3(U_345))) | ssPv3(skf3(U_345)) | ~ssPv4(skf3(U_345)) | ~ssPv2(skf3(U_345))))). % 12.31/4.45 tff(c_1841, plain, (![U_147]: (~ssPv1(skf3(U_147)) | ssPv1(U_147) | ssPv3(U_147) | ssPv2(skf3(U_147)) | ~ssPv4(U_147)))). % 12.31/4.45 tff(c_675, plain, (![U_1, W_238, U_239]: (~ssPv4(U_1) | ~ssPv1(W_238) | ~ssRr(W_238, U_1) | ~ssPv4(U_239) | ~ssRr(U_239, U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf3(U_1))))). % 12.31/4.45 tff(c_1786, plain, (![U_350]: (~ssPv1(U_350) | ~ssPv4(skf3(skf3(U_350))) | ssPv2(skf2(skf3(U_350))) | ~ssPv3(skf3(U_350)) | ~ssPv1(skf3(U_350))))). % 12.31/4.45 tff(c_876, plain, (![U_273, U_274]: (~ssPv1(U_273) | ~ssPv4(U_274) | ~ssRr(U_274, skf3(U_273)) | ssPv2(skf2(skf3(U_273))) | ~ssPv3(skf3(U_273)) | ~ssPv1(skf3(U_273))))). % 12.31/4.45 tff(c_824, plain, (![U_1]: (ssPv3(skf2(U_1)) | ssPv1(U_1) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ssPv3(U_1) | ssPv1(skf3(U_1)) | ~ssPv4(U_1)))). % 12.31/4.45 tff(c_773, plain, (![U_255]: (ssPv2(skf3(U_255)) | ssPv4(U_255) | ~ssPv1(U_255) | ssPv3(skf3(U_255)) | ssPv1(skf3(skf3(U_255))) | ~ssPv4(skf3(U_255))))). % 12.31/4.45 tff(c_1245, plain, (![U_1, U_317]: (~ssPv1(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv4(U_317) | ~ssRr(U_317, skf3(U_1)) | ssPv3(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.31/4.45 tff(c_854, plain, (![U_272]: (~ssPv1(skf3(U_272)) | ~ssPv1(U_272) | ~ssPv3(U_272) | ssPv3(skf3(U_272)) | ssPv2(skf3(skf3(U_272))) | ~ssPv4(skf3(U_272))))). % 12.31/4.45 tff(c_1648, plain, (![U_340]: (~ssPv1(U_340) | ~ssPv4(skf3(skf3(U_340))) | ssPv4(skf3(U_340)) | ~ssPv1(skf3(U_340)) | ~ssPv1(skf3(skf3(U_340)))))). % 12.31/4.45 tff(c_878, plain, (![U_273, U_274]: (~ssPv1(U_273) | ~ssPv4(U_274) | ~ssRr(U_274, skf3(U_273)) | ssPv4(skf3(U_273)) | ~ssPv1(skf3(U_273)) | ~ssPv1(skf3(skf3(U_273)))))). % 12.31/4.45 tff(c_1630, plain, (![U_337]: (ssPv2(skf3(U_337)) | ~ssPv3(skf3(skf3(U_337))) | ssPv3(U_337) | ~ssPv3(skf3(U_337)) | ~ssPv1(skf3(U_337))))). % 12.31/4.46 tff(c_265, plain, (![U_146, U_143]: (ssPv2(skf3(U_146)) | ~ssPv3(U_143) | ~ssRr(U_143, skf3(U_146)) | ssPv3(U_146) | ~ssPv3(skf3(U_146)) | ~ssPv1(skf3(U_146))))). % 12.31/4.46 tff(c_1358, plain, (![U_324]: (ssPv1(skf2(U_324)) | ~ssPv2(U_324) | ssPv3(U_324) | ssPv2(skf3(U_324)) | ssPv3(skf3(U_324)) | ssPv1(skf3(U_324))))). % 12.31/4.46 tff(c_639, plain, (![U_230]: (ssPv1(skf2(U_230)) | ~ssPv3(skf2(U_230)) | ~ssPv4(skf2(U_230)) | ~ssPv1(U_230) | ~ssPv2(skf2(U_230)) | ~ssPv4(U_230)))). % 12.31/4.46 tff(c_1076, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(U_2) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2)))))). % 12.31/4.46 tff(c_737, plain, (![U_248]: (ssPv1(skf2(U_248)) | ~ssPv4(skf2(U_248)) | ~ssPv3(skf2(U_248)) | ssPv2(U_248) | ~ssPv2(skf2(U_248)) | ~ssPv4(U_248)))). % 12.31/4.46 tff(c_1329, plain, (![U_154]: (ssPv3(U_154) | ssPv4(skf3(U_154)) | ssPv2(skf3(U_154)) | ssPv3(skf3(U_154)) | ssPv1(skf3(U_154))))). % 12.31/4.46 tff(c_1309, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf3(U_1))))). % 12.31/4.46 tff(c_1246, plain, (![U_2, U_317]: (~ssPv1(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv4(U_317) | ~ssRr(U_317, U_2) | ssPv3(U_2) | ~ssPv4(U_2) | ~ssPv2(U_2)))). % 12.31/4.46 tff(c_659, plain, (![U_2, W_235, U_236]: (~ssPv1(U_2) | ~ssPv3(W_235) | ~ssRr(U_2, W_235) | ~ssPv4(U_236) | ~ssRr(U_236, U_2) | ssPv3(U_2) | ~ssPv4(U_2) | ~ssPv2(U_2)))). % 12.31/4.46 tff(c_1222, plain, (![U_312]: (~ssPv1(U_312) | ~ssPv4(skf3(skf3(U_312))) | ssPv2(U_312) | ~ssPv3(skf3(U_312)) | ~ssPv1(skf3(U_312))))). % 12.31/4.46 tff(c_874, plain, (![U_190, U_274]: (~ssPv1(U_190) | ~ssPv4(U_274) | ~ssRr(U_274, skf3(U_190)) | ssPv2(U_190) | ~ssPv3(skf3(U_190)) | ~ssPv1(skf3(U_190))))). % 12.31/4.46 tff(c_1141, plain, (![U_306]: (ssPv2(skf3(U_306)) | ~ssPv3(skf3(U_306)) | ssPv4(skf3(U_306)) | ssPv1(skf2(skf3(U_306))) | ~ssPv1(U_306)))). % 12.31/4.46 tff(c_1140, plain, (![U_306]: (ssPv2(skf3(U_306)) | ssPv3(U_306) | ssPv4(skf3(U_306)) | ssPv1(skf2(skf3(U_306))) | ~ssPv1(U_306)))). % 12.31/4.46 tff(c_1150, plain, (![U_307]: (ssPv4(skf3(U_307)) | ssPv1(U_307) | ssPv4(skf2(skf3(U_307))) | ~ssPv1(skf2(skf3(U_307)))))). % 12.31/4.46 tff(c_1102, plain, (![U_300, V_302]: (ssPv4(skf3(U_300)) | ssPv1(U_300) | ssPv4(skf2(skf3(U_300))) | ~ssPv1(V_302) | ~ssRr(skf3(U_300), V_302)))). % 12.31/4.46 tff(c_1094, plain, (![U_299]: (ssPv2(skf3(skf3(U_299))) | ssPv4(skf3(U_299)) | ssPv1(skf2(skf3(U_299))) | ~ssPv1(U_299)))). % 12.31/4.46 tff(c_1112, plain, (![U_303]: (ssPv4(skf3(U_303)) | ssPv1(U_303) | ssPv4(U_303) | ~ssPv1(skf2(skf3(U_303)))))). % 12.31/4.46 tff(c_1101, plain, (![U_1, V_302]: (ssPv4(skf3(U_1)) | ssPv1(U_1) | ssPv4(U_1) | ~ssPv1(V_302) | ~ssRr(skf3(U_1), V_302)))). % 12.31/4.46 tff(c_319, plain, (![U_1, W_162, V_163]: (ssPv4(skf3(U_1)) | ssPv1(U_1) | ssPv4(W_162) | ~ssRr(skf3(U_1), W_162) | ~ssPv1(V_163) | ~ssRr(skf3(U_1), V_163)))). % 12.31/4.46 tff(c_1029, plain, (![U_292, U_1]: (ssPv2(U_292) | ~ssRr(U_292, skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ~ssPv1(U_1)))). % 12.31/4.46 tff(c_1075, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf3(U_1)) | ssPv2(U_1) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.46 tff(c_551, plain, (![U_218, U_123]: (ssPv4(U_218) | ssPv2(U_123) | ~ssRr(U_123, U_218) | ssPv2(U_218) | ~ssPv1(skf2(U_218)) | ~ssPv3(skf3(U_218))))). % 12.31/4.46 tff(c_619, plain, (![U_147]: (ssPv1(skf2(U_147)) | ~ssPv2(U_147) | ssPv1(U_147) | ~ssPv3(skf3(U_147)) | ssPv2(skf3(U_147)) | ~ssPv4(U_147)))). % 12.31/4.46 tff(c_968, plain, (![U_284, U_285]: (ssPv4(skf3(U_284)) | ssPv2(U_285) | ~ssPv1(U_284) | ~ssPv4(skf2(skf3(U_284))) | ~ssRr(U_285, skf3(U_284))))). % 12.31/4.46 tff(c_974, plain, (![U_287]: (ssPv4(skf3(U_287)) | ssPv2(skf3(skf3(U_287))) | ~ssPv1(U_287) | ~ssPv4(U_287)))). % 12.31/4.46 tff(c_967, plain, (![U_1, U_285]: (ssPv4(skf3(U_1)) | ssPv2(U_285) | ~ssPv1(U_1) | ~ssPv4(U_1) | ~ssRr(U_285, skf3(U_1))))). % 12.31/4.46 tff(c_375, plain, (![U_1, U_179, W_181]: (ssPv4(skf3(U_1)) | ssPv2(U_179) | ~ssPv1(U_1) | ~ssPv4(W_181) | ~ssRr(skf3(U_1), W_181) | ~ssRr(U_179, skf3(U_1))))). % 12.31/4.46 tff(c_919, plain, (![U_1]: (~ssPv1(U_1) | ssPv2(skf3(U_1)) | ssPv3(U_1) | ssPv1(skf3(U_1)) | ~ssPv4(U_1)))). % 12.31/4.46 tff(c_889, plain, (![U_278]: (ssPv1(U_278) | ssPv2(skf3(skf3(U_278))) | ~ssPv2(skf3(U_278)) | ~ssPv4(skf3(skf3(U_278)))))). % 12.31/4.46 tff(c_884, plain, (![U_275, U_277]: (ssPv1(U_275) | ssPv2(skf3(skf3(U_275))) | ~ssPv2(skf3(U_275)) | ~ssPv4(U_277) | ~ssRr(U_277, skf3(U_275))))). % 12.31/4.46 tff(c_350, plain, (![U_1, W_169, U_171]: (ssPv1(U_1) | ssPv2(W_169) | ~ssPv2(skf3(U_1)) | ~ssRr(W_169, skf3(U_1)) | ~ssPv4(U_171) | ~ssRr(U_171, skf3(U_1))))). % 12.31/4.46 tff(c_832, plain, (![U_267, U_269]: (~ssPv1(skf3(U_267)) | ~ssPv1(U_267) | ~ssPv3(skf2(skf3(U_267))) | ~ssPv4(U_269) | ~ssRr(U_269, skf3(U_267))))). % 12.31/4.46 tff(c_838, plain, (![U_270]: (~ssPv1(skf3(U_270)) | ~ssPv1(U_270) | ~ssPv3(U_270) | ~ssPv4(skf3(skf3(U_270)))))). % 12.31/4.46 tff(c_831, plain, (![U_1, U_269]: (~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv3(U_1) | ~ssPv4(U_269) | ~ssRr(U_269, skf3(U_1))))). % 12.31/4.46 tff(c_398, plain, (![U_1, W_188, U_189]: (~ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ~ssPv3(W_188) | ~ssRr(skf3(U_1), W_188) | ~ssPv4(U_189) | ~ssRr(U_189, skf3(U_1))))). % 12.31/4.46 tff(c_550, plain, (![U_218]: (ssPv3(skf2(U_218)) | ssPv1(U_218) | ssPv3(U_218) | ssPv2(U_218) | ~ssPv1(skf2(U_218)) | ~ssPv3(skf3(U_218))))). % 12.31/4.46 tff(c_286, plain, (![U_153]: (ssPv1(skf2(skf3(U_153))) | ~ssPv3(skf3(U_153)) | ssPv4(skf3(U_153)) | ssPv2(skf3(U_153)) | ~ssPv4(U_153)))). % 12.31/4.46 tff(c_421, plain, (![U_2]: (ssPv2(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ssPv3(skf2(U_2)) | ~ssPv4(skf2(U_2)) | ~ssPv3(U_2)))). % 12.31/4.46 tff(c_420, plain, (![U_165]: (ssPv2(skf2(U_165)) | ~ssPv1(skf3(skf2(U_165))) | ssPv3(skf2(U_165)) | ssPv1(U_165) | ~ssPv4(skf2(U_165))))). % 12.31/4.46 tff(c_786, plain, (![U_258, U_260]: (~ssPv4(skf3(U_258)) | ~ssPv4(U_258) | ~ssPv1(skf3(skf3(U_258))) | ~ssPv4(U_260) | ~ssRr(U_260, skf3(U_258))))). % 12.31/4.46 tff(c_277, plain, (![U_1, W_151, U_152]: (~ssPv4(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv1(W_151) | ~ssRr(W_151, skf3(U_1)) | ~ssPv4(U_152) | ~ssRr(U_152, skf3(U_1))))). % 12.31/4.46 tff(c_762, plain, (![U_250, U_252]: (ssPv2(skf3(U_250)) | ssPv4(U_250) | ~ssPv1(skf2(skf3(U_250))) | ~ssPv3(U_252) | ~ssRr(U_252, skf3(U_250))))). % 12.31/4.46 tff(c_768, plain, (![U_253]: (ssPv2(skf3(U_253)) | ssPv4(U_253) | ~ssPv1(U_253) | ~ssPv3(skf3(skf3(U_253)))))). % 12.31/4.46 tff(c_761, plain, (![U_1, U_252]: (ssPv2(skf3(U_1)) | ssPv4(U_1) | ~ssPv1(U_1) | ~ssPv3(U_252) | ~ssRr(U_252, skf3(U_1))))). % 12.31/4.46 tff(c_452, plain, (![U_1, W_199, U_200]: (ssPv2(skf3(U_1)) | ssPv4(U_1) | ~ssPv1(W_199) | ~ssRr(skf3(U_1), W_199) | ~ssPv3(U_200) | ~ssRr(U_200, skf3(U_1))))). % 12.31/4.46 tff(c_725, plain, (![U_246]: (ssPv1(skf2(skf2(U_246))) | ssPv2(U_246) | ~ssPv2(skf2(U_246)) | ~ssPv4(skf3(skf2(U_246)))))). % 12.31/4.46 tff(c_726, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2)))). % 12.31/4.46 tff(c_597, plain, (![U_2, U_225]: (ssPv1(skf2(skf2(U_2))) | ssPv2(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_225) | ~ssRr(U_225, skf2(U_2))))). % 12.31/4.46 tff(c_706, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ssPv4(U_1) | ~ssPv1(U_1)))). % 12.31/4.46 tff(c_534, plain, (![U_1, V_217]: (ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ssPv4(U_1) | ~ssPv1(V_217) | ~ssRr(skf3(U_1), V_217)))). % 12.31/4.46 tff(c_680, plain, (![U_240]: (ssPv2(skf3(U_240)) | ssPv4(skf2(skf3(U_240))) | ~ssPv1(U_240) | ~ssPv3(skf3(skf3(U_240)))))). % 12.31/4.46 tff(c_520, plain, (![U_1, U_212]: (ssPv2(skf3(U_1)) | ssPv4(skf2(skf3(U_1))) | ~ssPv1(U_1) | ~ssPv3(U_212) | ~ssRr(U_212, skf3(U_1))))). % 12.31/4.46 tff(c_278, plain, (![U_2, W_151, U_152]: (~ssPv4(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv1(W_151) | ~ssRr(W_151, U_2) | ~ssPv4(U_152) | ~ssRr(U_152, U_2)))). % 12.31/4.46 tff(c_399, plain, (![U_2, W_188, U_189]: (~ssPv1(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv3(W_188) | ~ssRr(U_2, W_188) | ~ssPv4(U_189) | ~ssRr(U_189, U_2)))). % 12.31/4.46 tff(c_376, plain, (![U_2, U_179, W_181]: (ssPv4(U_2) | ssPv2(U_179) | ~ssPv1(skf2(U_2)) | ~ssPv4(W_181) | ~ssRr(U_2, W_181) | ~ssRr(U_179, U_2)))). % 12.31/4.46 tff(c_632, plain, (![U_229]: (~ssPv4(skf2(U_229)) | ~ssPv1(U_229) | ssPv1(skf2(skf2(U_229))) | ~ssPv2(skf2(U_229)) | ~ssPv4(U_229)))). % 12.31/4.46 tff(c_604, plain, (![U_2]: (ssPv1(skf2(skf2(U_2))) | ssPv2(skf3(skf2(U_2))) | ~ssPv2(skf2(U_2)) | ~ssPv4(U_2)))). % 12.31/4.46 tff(c_603, plain, (![U_1]: (ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv4(skf3(U_1))))). % 12.31/4.46 tff(c_596, plain, (![U_1, U_225]: (ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv4(U_225) | ~ssRr(U_225, U_1)))). % 12.31/4.46 tff(c_351, plain, (![U_2, W_169, U_171]: (ssPv1(skf2(U_2)) | ssPv2(W_169) | ~ssPv2(U_2) | ~ssRr(W_169, U_2) | ~ssPv4(U_171) | ~ssRr(U_171, U_2)))). % 12.31/4.46 tff(c_557, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ssPv4(skf2(skf3(U_1))) | ~ssPv1(U_1)))). % 12.31/4.46 tff(c_528, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv4(skf2(skf2(U_2))) | ~ssPv1(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 12.31/4.46 tff(c_535, plain, (![U_2, V_217]: (ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv4(skf2(U_2)) | ~ssPv1(V_217) | ~ssRr(U_2, V_217)))). % 12.31/4.46 tff(c_527, plain, (![U_1]: (ssPv2(U_1) | ssPv4(skf2(U_1)) | ~ssPv1(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 12.31/4.46 tff(c_320, plain, (![U_2, W_162, V_163]: (ssPv4(U_2) | ssPv1(skf2(U_2)) | ssPv4(W_162) | ~ssRr(U_2, W_162) | ~ssPv1(V_163) | ~ssRr(U_2, V_163)))). % 12.31/4.46 tff(c_521, plain, (![U_2, U_212]: (ssPv2(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv3(U_212) | ~ssRr(U_212, U_2)))). % 12.31/4.46 tff(c_453, plain, (![U_2, W_199, U_200]: (ssPv2(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(W_199) | ~ssRr(U_2, W_199) | ~ssPv3(U_200) | ~ssRr(U_200, U_2)))). % 12.31/4.46 tff(c_186, plain, (![U_116]: (ssPv1(skf2(U_116)) | ~ssPv4(skf2(U_116)) | ssPv2(skf2(U_116)) | ~ssPv3(skf2(U_116)) | ~ssPv2(U_116)))). % 12.31/4.46 tff(c_482, plain, (![U_205]: (ssPv3(skf2(U_205)) | ssPv3(U_205) | ~ssPv4(skf2(U_205)) | ~ssPv3(skf3(skf2(U_205)))))). % 12.31/4.46 tff(c_223, plain, (![U_2, U_131]: (ssPv3(skf2(U_2)) | ssPv3(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv3(U_131) | ~ssRr(U_131, skf2(U_2))))). % 12.31/4.46 tff(c_462, plain, (![U_201]: (~ssPv4(skf2(U_201)) | ~ssPv2(skf2(U_201)) | ~ssPv1(U_201) | ~ssPv2(skf3(skf2(U_201)))))). % 12.31/4.46 tff(c_463, plain, (![U_2]: (~ssPv4(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv2(U_2)))). % 12.31/4.46 tff(c_116, plain, (![U_2, U_88]: (~ssPv4(skf2(U_2)) | ~ssPv2(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv2(U_88) | ~ssRr(U_88, skf2(U_2))))). % 12.31/4.46 tff(c_40, plain, (![V_54, X_56, W_55, U_53]: (ssPv2(V_54) | ssPv4(X_56) | ~ssRr(V_54, X_56) | ~ssPv1(W_55) | ~ssRr(V_54, W_55) | ~ssPv3(U_53) | ~ssRr(U_53, V_54)))). % 12.31/4.46 tff(c_429, plain, (![U_194]: (ssPv3(skf3(U_194)) | ssPv1(skf3(U_194)) | ssPv4(U_194) | ssPv2(skf3(skf3(U_194)))))). % 12.31/4.46 tff(c_192, plain, (![U_1, U_119]: (ssPv3(skf3(U_1)) | ssPv1(skf3(U_1)) | ssPv4(U_1) | ssPv2(U_119) | ~ssRr(U_119, skf3(U_1))))). % 12.31/4.46 tff(c_409, plain, (![U_190]: (ssPv2(U_190) | ssPv3(skf2(skf3(U_190))) | ~ssPv3(skf3(U_190)) | ~ssPv1(skf3(U_190))))). % 12.31/4.46 tff(c_408, plain, (![U_1]: (ssPv2(U_1) | ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1))))). % 12.45/4.46 tff(c_241, plain, (![U_1, V_136]: (ssPv2(U_1) | ssPv3(V_136) | ~ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssRr(skf3(U_1), V_136)))). % 12.45/4.46 tff(c_42, plain, (![V_58, X_60, W_59, U_57]: (~ssPv1(V_58) | ~ssPv1(X_60) | ~ssRr(V_58, X_60) | ~ssPv3(W_59) | ~ssRr(V_58, W_59) | ~ssPv4(U_57) | ~ssRr(U_57, V_58)))). % 12.45/4.46 tff(c_391, plain, (![U_183]: (ssPv4(skf3(U_183)) | ssPv3(U_183) | ~ssPv1(skf3(U_183)) | ~ssPv1(skf3(skf3(U_183)))))). % 12.45/4.46 tff(c_95, plain, (![U_1, U_80]: (ssPv4(skf3(U_1)) | ssPv3(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv1(U_80) | ~ssRr(U_80, skf3(U_1))))). % 12.45/4.46 tff(c_369, plain, (![U_147]: (ssPv1(U_147) | ~ssPv3(skf3(U_147)) | ssPv4(skf3(U_147)) | ssPv2(skf3(U_147)) | ~ssPv4(U_147)))). % 12.45/4.46 tff(c_36, plain, (![V_46, U_45, X_48, W_47]: (ssPv4(V_46) | ssPv2(U_45) | ~ssPv1(X_48) | ~ssRr(V_46, X_48) | ~ssPv4(W_47) | ~ssRr(V_46, W_47) | ~ssRr(U_45, V_46)))). % 12.45/4.46 tff(c_364, plain, (![U_175]: (ssPv2(skf3(U_175)) | ssPv1(U_175) | ~ssPv3(skf3(U_175)) | ~ssPv2(skf3(skf3(U_175)))))). % 12.45/4.46 tff(c_172, plain, (![U_1, U_112]: (ssPv2(skf3(U_1)) | ssPv1(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv2(U_112) | ~ssRr(U_112, skf3(U_1))))). % 12.45/4.46 tff(c_343, plain, (![U_2]: (ssPv3(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv2(U_2)))). % 12.45/4.46 tff(c_334, plain, (![U_165]: (ssPv3(skf2(U_165)) | ssPv1(U_165) | ssPv3(skf3(skf2(U_165))) | ~ssPv4(skf2(U_165))))). % 12.45/4.46 tff(c_344, plain, (![U_1]: (ssPv3(skf2(U_1)) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf3(U_1))))). % 12.45/4.46 tff(c_38, plain, (![X_52, W_51, V_50, U_49]: (ssPv1(X_52) | ssPv2(W_51) | ~ssPv2(V_50) | ~ssRr(V_50, X_52) | ~ssRr(W_51, V_50) | ~ssPv4(U_49) | ~ssRr(U_49, V_50)))). % 12.45/4.46 tff(c_335, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv1(U_2) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 12.45/4.46 tff(c_132, plain, (![U_2, U_96]: (ssPv3(skf2(U_2)) | ssPv1(U_2) | ssPv3(U_96) | ~ssPv4(skf2(U_2)) | ~ssRr(U_96, skf2(U_2))))). % 12.45/4.46 tff(c_313, plain, (![U_158]: (ssPv2(skf3(U_158)) | ~ssPv3(skf3(U_158)) | ~ssPv2(U_158) | ~ssPv3(skf3(skf3(U_158)))))). % 12.45/4.46 tff(c_34, plain, (![U_41, X_44, W_43, V_42]: (ssPv4(U_41) | ssPv1(X_44) | ssPv4(W_43) | ~ssRr(U_41, X_44) | ~ssRr(U_41, W_43) | ~ssPv1(V_42) | ~ssRr(U_41, V_42)))). % 12.45/4.46 tff(c_256, plain, (![U_1, U_143]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv3(U_143) | ~ssRr(U_143, skf3(U_1))))). % 12.45/4.47 tff(c_298, plain, (![U_147]: (ssPv3(U_147) | ssPv4(skf3(U_147)) | ssPv2(skf3(U_147)) | ~ssPv4(U_147)))). % 12.45/4.47 tff(c_293, plain, (![U_154]: (ssPv4(skf3(U_154)) | ssPv2(skf3(U_154)) | ssPv3(U_154) | ~ssPv2(skf3(skf3(U_154)))))). % 12.45/4.47 tff(c_156, plain, (![U_1, U_105]: (ssPv4(skf3(U_1)) | ssPv2(skf3(U_1)) | ssPv3(U_1) | ~ssPv2(U_105) | ~ssRr(U_105, skf3(U_1))))). % 12.45/4.47 tff(c_271, plain, (![U_147]: (ssPv4(skf3(U_147)) | ssPv2(skf3(U_147)) | ssPv2(skf3(skf3(U_147))) | ~ssPv4(U_147)))). % 12.45/4.47 tff(c_44, plain, (![V_62, X_64, W_63, U_61]: (~ssPv4(V_62) | ~ssPv4(X_64) | ~ssRr(V_62, X_64) | ~ssPv1(W_63) | ~ssRr(W_63, V_62) | ~ssPv4(U_61) | ~ssRr(U_61, V_62)))). % 12.45/4.47 tff(c_206, plain, (![U_1, U_123]: (ssPv4(skf3(U_1)) | ssPv2(skf3(U_1)) | ssPv2(U_123) | ~ssPv4(U_1) | ~ssRr(U_123, skf3(U_1))))). % 12.45/4.47 tff(c_248, plain, (![U_1]: (ssPv2(skf2(skf3(U_1))) | ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv1(skf3(U_1))))). % 12.45/4.47 tff(c_257, plain, (![U_2, U_143]: (ssPv2(U_2) | ~ssPv3(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv3(U_143) | ~ssRr(U_143, U_2)))). % 12.45/4.47 tff(c_30, plain, (![V_36, W_37, U_35]: (ssPv2(V_36) | ~ssPv3(V_36) | ~ssPv2(W_37) | ~ssRr(V_36, W_37) | ~ssPv3(U_35) | ~ssRr(U_35, V_36)))). % 12.45/4.47 tff(c_249, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv1(U_2)))). % 12.45/4.47 tff(c_242, plain, (![U_2, V_136]: (ssPv2(skf2(U_2)) | ssPv3(V_136) | ~ssPv3(U_2) | ~ssPv1(U_2) | ~ssRr(U_2, V_136)))). % 12.45/4.47 tff(c_22, plain, (![W_25, V_24, U_23]: (ssPv2(W_25) | ssPv3(V_24) | ~ssPv3(U_23) | ~ssPv1(U_23) | ~ssRr(U_23, W_25) | ~ssRr(U_23, V_24)))). % 12.45/4.47 tff(c_230, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv3(skf3(skf2(U_2))) | ~ssPv4(skf2(U_2)) | ~ssPv3(U_2)))). % 12.45/4.47 tff(c_222, plain, (![U_1, U_131]: (ssPv3(U_1) | ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_131) | ~ssRr(U_131, U_1)))). % 12.45/4.47 tff(c_26, plain, (![V_30, W_31, U_29]: (ssPv3(V_30) | ssPv3(W_31) | ~ssPv4(V_30) | ~ssRr(W_31, V_30) | ~ssPv3(U_29) | ~ssRr(U_29, V_30)))). % 12.45/4.47 tff(c_200, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv1(skf2(U_2)) | ssPv4(skf2(skf2(U_2))) | ssPv2(U_2)))). % 12.45/4.47 tff(c_207, plain, (![U_2, U_123]: (ssPv4(U_2) | ssPv2(U_2) | ssPv2(U_123) | ~ssPv4(skf2(U_2)) | ~ssRr(U_123, U_2)))). % 12.45/4.47 tff(c_199, plain, (![U_1]: (ssPv3(U_1) | ssPv1(U_1) | ssPv4(skf2(U_1)) | ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_18, plain, (![V_18, U_17, W_19]: (ssPv4(V_18) | ssPv2(V_18) | ssPv2(U_17) | ~ssPv4(W_19) | ~ssRr(V_18, W_19) | ~ssRr(U_17, V_18)))). % 12.45/4.47 tff(c_193, plain, (![U_2, U_119]: (ssPv3(U_2) | ssPv1(U_2) | ssPv4(skf2(U_2)) | ssPv2(U_119) | ~ssRr(U_119, U_2)))). % 12.45/4.47 tff(c_14, plain, (![V_12, W_13, U_11]: (ssPv3(V_12) | ssPv1(V_12) | ssPv4(W_13) | ssPv2(U_11) | ~ssRr(V_12, W_13) | ~ssRr(U_11, V_12)))). % 12.45/4.47 tff(c_180, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2)))). % 12.45/4.47 tff(c_179, plain, (![U_1]: (ssPv2(U_1) | ssPv1(skf2(U_1)) | ~ssPv3(U_1) | ~ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_173, plain, (![U_2, U_112]: (ssPv2(U_2) | ssPv1(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv2(U_112) | ~ssRr(U_112, U_2)))). % 12.45/4.47 tff(c_28, plain, (![V_33, W_34, U_32]: (ssPv2(V_33) | ssPv1(W_34) | ~ssPv3(V_33) | ~ssRr(V_33, W_34) | ~ssPv2(U_32) | ~ssRr(U_32, V_33)))). % 12.45/4.47 tff(c_164, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ~ssPv2(U_2)))). % 12.45/4.47 tff(c_163, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv3(skf2(U_1)) | ~ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_157, plain, (![U_2, U_105]: (ssPv4(U_2) | ssPv2(U_2) | ssPv3(skf2(U_2)) | ~ssPv2(U_105) | ~ssRr(U_105, U_2)))). % 12.45/4.47 tff(c_20, plain, (![V_21, W_22, U_20]: (ssPv4(V_21) | ssPv2(V_21) | ssPv3(W_22) | ~ssRr(V_21, W_22) | ~ssPv2(U_20) | ~ssRr(U_20, V_21)))). % 12.45/4.47 tff(c_103, plain, (![U_1]: (ssPv1(skf3(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_139, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv1(skf3(skf2(U_2))) | ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 12.45/4.47 tff(c_123, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2)) | ~ssPv1(U_2)))). % 12.45/4.47 tff(c_138, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf3(U_1)) | ssPv3(skf3(U_1)) | ~ssPv4(U_1)))). % 12.45/4.47 tff(c_131, plain, (![U_1, U_96]: (ssPv3(U_1) | ssPv1(skf3(U_1)) | ssPv3(U_96) | ~ssPv4(U_1) | ~ssRr(U_96, U_1)))). % 12.45/4.47 tff(c_16, plain, (![V_15, W_16, U_14]: (ssPv3(V_15) | ssPv1(W_16) | ssPv3(U_14) | ~ssPv4(V_15) | ~ssRr(W_16, V_15) | ~ssRr(U_14, V_15)))). % 12.45/4.47 tff(c_115, plain, (![U_1, U_88]: (~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv2(U_88) | ~ssRr(U_88, U_1)))). % 12.45/4.47 tff(c_122, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf2(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf3(U_1))))). % 12.45/4.47 tff(c_96, plain, (![U_2, U_80]: (ssPv4(U_2) | ssPv3(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv1(U_80) | ~ssRr(U_80, U_2)))). % 12.45/4.47 tff(c_32, plain, (![V_39, W_40, U_38]: (~ssPv4(V_39) | ~ssPv2(V_39) | ~ssPv1(W_40) | ~ssRr(W_40, V_39) | ~ssPv2(U_38) | ~ssRr(U_38, V_39)))). % 12.45/4.47 tff(c_89, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv2(skf2(U_2)) | ~ssPv1(skf2(U_2)) | ~ssPv2(U_2)))). % 12.45/4.47 tff(c_54, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv1(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_64, plain, (![U_1]: (ssPv1(skf3(U_1)) | ~ssPv4(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv1(U_1)))). % 12.45/4.47 tff(c_73, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_88, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv2(skf3(U_1))))). % 12.45/4.47 tff(c_24, plain, (![V_27, W_28, U_26]: (ssPv4(V_27) | ssPv3(W_28) | ~ssPv1(V_27) | ~ssRr(V_27, W_28) | ~ssPv1(U_26) | ~ssRr(U_26, V_27)))). % 12.45/4.47 tff(c_10, plain, (![V_8, U_7]: (ssPv3(V_8) | ssPv2(V_8) | ~ssPv1(V_8) | ~ssPv2(U_7) | ~ssRr(U_7, V_8)))). % 12.45/4.47 tff(c_74, plain, (![U_2]: (ssPv4(U_2) | ssPv2(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv2(U_2)))). % 12.45/4.47 tff(c_65, plain, (![U_2]: (ssPv1(U_2) | ~ssPv4(U_2) | ~ssPv3(U_2) | ~ssPv1(skf2(U_2))))). % 12.45/4.47 tff(c_6, plain, (![U_3, V_4]: (ssPv4(U_3) | ssPv2(V_4) | ~ssPv3(U_3) | ~ssPv2(U_3) | ~ssRr(U_3, V_4)))). % 12.45/4.47 tff(c_12, plain, (![U_9, V_10]: (ssPv1(U_9) | ~ssPv4(U_9) | ~ssPv3(U_9) | ~ssPv1(V_10) | ~ssRr(U_9, V_10)))). % 12.45/4.47 tff(c_55, plain, (![U_2]: (ssPv3(U_2) | ssPv1(skf2(U_2)) | ~ssPv4(U_2) | ~ssPv2(U_2)))). % 12.45/4.47 tff(c_8, plain, (![U_5, V_6]: (ssPv3(U_5) | ssPv1(V_6) | ~ssPv4(U_5) | ~ssPv2(U_5) | ~ssRr(U_5, V_6)))). % 12.45/4.47 tff(c_2, plain, (![U_1]: (ssRr(skf3(U_1), U_1)))). % 12.45/4.47 tff(c_4, plain, (![U_2]: (ssRr(U_2, skf2(U_2))))). % 12.45/4.47 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.45/4.47 %------------------------------------------------------------------------------