%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN749-1 : TPTP v9.0.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n004.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:21 PM UTC 2025 % Result : Satisfiable 11.01s 4.01s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.12 % Problem : SYN749-1 : TPTP v9.0.0. Released v2.5.0. % 0.13/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.34 % Computer : n004.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 08:14:22 EDT 2025 % 0.14/0.34 % CPUTime : % 11.01/4.01 % 11.01/4.01 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.01/4.01 % 11.01/4.01 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.01/4.01 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 11.01/4.01 % 11.01/4.01 %Foreground sorts: % 11.01/4.01 % 11.01/4.01 % 11.01/4.01 %Background operators: % 11.01/4.01 % 11.01/4.01 % 11.01/4.01 %Foreground operators: % 11.01/4.01 tff(skf1, type, skf1: $i > $i). % 11.01/4.01 tff(ssPv1, type, ssPv1: $i > $o). % 11.01/4.01 tff(ssPv3, type, ssPv3: $i > $o). % 11.01/4.01 tff(ssPv7, type, ssPv7: $i > $o). % 11.01/4.01 tff(ssPv6, type, ssPv6: $i > $o). % 11.01/4.01 tff(ssPv5, type, ssPv5: $i > $o). % 11.01/4.01 tff(ssRr, type, ssRr: ($i * $i) > $o). % 11.01/4.01 tff(ssPv4, type, ssPv4: $i > $o). % 11.01/4.01 tff(ssPv2, type, ssPv2: $i > $o). % 11.01/4.01 tff(ssPv8, type, ssPv8: $i > $o). % 11.01/4.01 % 11.01/4.01 %Saturated clause set: % 11.01/4.02 tff(c_3270, plain, (![U_1]: (~ssPv2(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_3269, plain, (![U_1]: (ssPv6(U_1) | ~ssPv2(U_1) | ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_7789, plain, (![U_1]: (ssPv6(U_1) | ~ssPv2(U_1) | ssPv7(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.02 tff(c_6725, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 11.01/4.02 tff(c_6721, plain, (![U_1, V_160]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(V_160) | ~ssRr(U_1, V_160) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 11.01/4.02 tff(c_6674, plain, (![U_662]: (ssPv1(U_662) | ~ssPv2(U_662) | ssPv7(U_662) | ~ssPv3(U_662) | ssPv4(U_662) | ~ssPv5(U_662)))). % 11.01/4.02 tff(c_4470, plain, (![U_608]: (ssPv2(U_608) | ~ssPv6(U_608) | ~ssPv4(U_608) | ssPv7(U_608) | ~ssPv5(U_608) | ~ssPv2(skf1(U_608)) | ssPv1(skf1(U_608)) | ~ssPv3(skf1(U_608)) | ssPv1(U_608) | ssPv5(skf1(U_608)) | ~ssPv3(U_608)))). % 11.01/4.02 tff(c_6401, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_3274, plain, (![U_1, V_160]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(V_160) | ~ssRr(U_1, V_160) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_6190, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_669, plain, (![U_1, V_160]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(V_160) | ~ssRr(U_1, V_160) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_4116, plain, (![U_592]: (ssPv7(U_592) | ssPv4(skf1(U_592)) | ~ssPv6(U_592) | ~ssPv5(U_592) | ~ssPv4(U_592) | ~ssPv2(U_592) | ~ssPv2(skf1(U_592)) | ssPv1(skf1(U_592)) | ~ssPv3(skf1(U_592)) | ~ssPv3(U_592)))). % 11.01/4.02 tff(c_6133, plain, (![U_643]: (ssPv4(skf1(U_643)) | ssPv7(U_643) | ~ssPv2(skf1(U_643)) | ssPv1(skf1(U_643)) | ~ssPv3(skf1(U_643)) | ssPv4(U_643) | ssPv5(skf1(U_643)) | ~ssPv5(U_643)))). % 11.01/4.02 tff(c_6097, plain, (![U_1]: (ssPv7(U_1) | ~ssPv2(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.02 tff(c_6051, plain, (![U_1]: (ssPv2(U_1) | ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.02 tff(c_6047, plain, (![U_284]: (ssPv2(U_284) | ~ssPv2(skf1(U_284)) | ssPv4(skf1(U_284)) | ~ssPv3(skf1(U_284)) | ~ssPv6(U_284) | ssPv3(U_284) | ~ssPv4(U_284) | ssPv8(U_284) | ~ssPv5(U_284)))). % 11.01/4.02 tff(c_5928, plain, (![U_636]: (ssPv2(U_636) | ~ssPv6(U_636) | ssPv8(U_636) | ssPv3(U_636) | ~ssPv4(U_636) | ~ssPv2(skf1(U_636)) | ssPv4(skf1(U_636)) | ~ssPv5(skf1(U_636)) | ~ssPv3(skf1(U_636))))). % 11.01/4.02 tff(c_3273, plain, (![U_1]: (~ssPv6(U_1) | ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_3272, plain, (![U_1]: (~ssPv6(U_1) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.02 tff(c_5830, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv5(U_1) | ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1)))). % 11.01/4.02 tff(c_5748, plain, (![U_1]: (ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.02 tff(c_4542, plain, (![U_610]: (ssPv4(skf1(U_610)) | ~ssPv6(U_610) | ssPv8(U_610) | ssPv3(U_610) | ~ssPv4(U_610) | ~ssPv2(skf1(U_610)) | ~ssPv5(skf1(U_610)) | ssPv1(skf1(U_610)) | ~ssPv3(skf1(U_610))))). % 11.01/4.02 tff(c_5540, plain, (![U_1]: (ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv7(skf1(U_1)) | ssPv7(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv8(U_1) | ~ssPv5(U_1)))). % 11.01/4.02 tff(c_2210, plain, (![U_491, V_255]: (ssPv6(U_491) | ~ssPv2(U_491) | ~ssPv7(V_255) | ~ssRr(U_491, V_255) | ssPv7(U_491) | ssPv2(skf1(U_491)) | ~ssPv1(U_491) | ssPv3(U_491) | ssPv3(skf1(U_491)) | ssPv8(U_491) | ~ssPv5(U_491)))). % 11.01/4.02 tff(c_5519, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 11.01/4.02 tff(c_5428, plain, (![U_1]: (~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.02 tff(c_4769, plain, (![U_614]: (ssPv4(skf1(U_614)) | ~ssPv6(U_614) | ~ssPv5(U_614) | ~ssPv4(U_614) | ~ssPv2(U_614) | ~ssPv2(skf1(U_614)) | ~ssPv5(skf1(U_614)) | ssPv1(skf1(U_614)) | ~ssPv3(skf1(U_614))))). % 11.01/4.03 tff(c_4547, plain, (![U_610]: (~ssPv4(skf1(U_610)) | ~ssPv6(U_610) | ssPv8(U_610) | ssPv3(U_610) | ~ssPv4(U_610) | ~ssPv2(skf1(U_610)) | ~ssPv5(skf1(U_610)) | ssPv1(skf1(U_610)) | ~ssPv3(skf1(U_610))))). % 11.01/4.03 tff(c_5055, plain, (![U_618]: (~ssPv2(U_618) | ssPv4(skf1(U_618)) | ssPv7(U_618) | ~ssPv5(U_618) | ~ssPv2(skf1(U_618)) | ssPv1(skf1(U_618)) | ~ssPv3(skf1(U_618)) | ssPv1(U_618) | ~ssPv3(U_618)))). % 11.01/4.03 tff(c_4465, plain, (![U_608]: (ssPv4(skf1(U_608)) | ssPv7(U_608) | ~ssPv5(U_608) | ~ssPv2(skf1(U_608)) | ssPv1(skf1(U_608)) | ~ssPv3(skf1(U_608)) | ssPv1(U_608) | ssPv5(skf1(U_608)) | ~ssPv3(U_608)))). % 11.01/4.03 tff(c_4774, plain, (![U_614]: (~ssPv4(skf1(U_614)) | ~ssPv6(U_614) | ~ssPv5(U_614) | ~ssPv4(U_614) | ~ssPv2(U_614) | ~ssPv2(skf1(U_614)) | ~ssPv5(skf1(U_614)) | ssPv1(skf1(U_614)) | ~ssPv3(skf1(U_614))))). % 11.01/4.03 tff(c_667, plain, (![U_1]: (~ssPv6(U_1) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.03 tff(c_4550, plain, (![U_610]: (ssPv2(U_610) | ~ssPv6(U_610) | ssPv8(U_610) | ssPv3(U_610) | ~ssPv4(U_610) | ~ssPv2(skf1(U_610)) | ~ssPv5(skf1(U_610)) | ssPv1(skf1(U_610)) | ~ssPv3(skf1(U_610))))). % 11.01/4.03 tff(c_668, plain, (![U_1]: (~ssPv6(U_1) | ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.03 tff(c_4422, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv1(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.03 tff(c_2820, plain, (![U_525, V_160]: (ssPv7(U_525) | ~ssPv8(V_160) | ~ssRr(U_525, V_160) | ~ssPv6(skf1(U_525)) | ~ssPv5(skf1(U_525)) | ~ssPv4(skf1(U_525)) | ~ssPv2(skf1(U_525)) | ~ssPv5(U_525) | ~ssPv3(U_525)))). % 11.01/4.03 tff(c_4397, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.03 tff(c_1683, plain, (![U_447, V_160]: (ssPv7(U_447) | ~ssPv5(U_447) | ~ssPv8(V_160) | ~ssRr(U_447, V_160) | ~ssPv2(skf1(U_447)) | ssPv1(skf1(U_447)) | ~ssPv3(skf1(U_447)) | ssPv6(skf1(U_447)) | ~ssPv3(U_447)))). % 11.01/4.03 tff(c_2818, plain, (![U_525]: (~ssPv6(U_525) | ~ssPv4(U_525) | ~ssPv2(U_525) | ~ssPv6(skf1(U_525)) | ~ssPv5(skf1(U_525)) | ~ssPv4(skf1(U_525)) | ~ssPv2(skf1(U_525)) | ~ssPv5(U_525) | ~ssPv3(U_525)))). % 11.01/4.03 tff(c_4271, plain, (![U_1]: (~ssPv7(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_4266, plain, (![V_255, U_598]: (~ssPv7(V_255) | ~ssRr(U_598, V_255) | ssPv6(U_598) | ssPv3(U_598) | ssPv3(skf1(U_598)) | ~ssPv2(U_598) | ssPv4(U_598) | ~ssPv5(U_598)))). % 11.01/4.03 tff(c_4250, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_4222, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv6(U_1) | ssPv3(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.03 tff(c_4217, plain, (![V_209, U_594]: (~ssPv8(V_209) | ~ssRr(U_594, V_209) | ssPv6(U_594) | ssPv3(U_594) | ssPv4(U_594) | ~ssPv5(U_594) | ssPv3(skf1(U_594)) | ~ssPv2(U_594)))). % 11.01/4.03 tff(c_4201, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.03 tff(c_1681, plain, (![U_447]: (~ssPv6(U_447) | ~ssPv5(U_447) | ~ssPv4(U_447) | ~ssPv2(U_447) | ~ssPv2(skf1(U_447)) | ssPv1(skf1(U_447)) | ~ssPv3(skf1(U_447)) | ssPv6(skf1(U_447)) | ~ssPv3(U_447)))). % 11.01/4.03 tff(c_3992, plain, (![U_1]: (~ssPv7(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_3987, plain, (![V_255, U_586]: (~ssPv7(V_255) | ~ssRr(U_586, V_255) | ssPv6(U_586) | ssPv7(U_586) | ssPv3(skf1(U_586)) | ~ssPv2(U_586) | ssPv4(U_586) | ~ssPv5(U_586)))). % 11.01/4.03 tff(c_3971, plain, (![U_1]: (ssPv6(U_1) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_3943, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv6(U_1) | ssPv7(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.03 tff(c_3938, plain, (![V_209, U_582]: (~ssPv8(V_209) | ~ssRr(U_582, V_209) | ssPv6(U_582) | ssPv7(U_582) | ssPv4(U_582) | ~ssPv5(U_582) | ssPv3(skf1(U_582)) | ~ssPv2(U_582)))). % 11.01/4.03 tff(c_3922, plain, (![U_1]: (ssPv6(U_1) | ssPv7(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.03 tff(c_655, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.03 tff(c_656, plain, (![U_1]: (ssPv7(U_1) | ssPv4(U_1) | ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 11.01/4.03 tff(c_2137, plain, (![U_486]: (ssPv2(skf1(U_486)) | ssPv4(skf1(U_486)) | ssPv7(U_486) | ~ssPv5(U_486) | ~ssPv8(U_486) | ~ssPv6(U_486) | ~ssPv3(skf1(U_486)) | ssPv1(U_486) | ~ssPv3(U_486)))). % 11.01/4.03 tff(c_3638, plain, (![U_1]: (ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_3604, plain, (![U_566]: (~ssPv6(U_566) | ssPv4(U_566) | ~ssPv2(U_566) | ~ssPv5(U_566) | ssPv1(U_566) | ~ssPv3(U_566)))). % 11.01/4.03 tff(c_3525, plain, (![U_1]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.03 tff(c_1282, plain, (![U_414, V_209]: (ssPv4(U_414) | ~ssPv5(U_414) | ~ssPv8(V_209) | ~ssRr(U_414, V_209) | ssPv7(U_414) | ssPv1(skf1(U_414)) | ssPv3(U_414) | ssPv3(skf1(U_414)) | ~ssPv2(U_414)))). % 11.01/4.03 tff(c_2734, plain, (![U_519]: (ssPv2(skf1(U_519)) | ssPv7(U_519) | ssPv1(skf1(U_519)) | ssPv4(skf1(U_519)) | ssPv3(U_519) | ssPv3(skf1(U_519)) | ssPv8(U_519) | ~ssPv5(U_519)))). % 11.01/4.03 tff(c_3226, plain, (![U_546]: (ssPv6(U_546) | ~ssPv2(U_546) | ssPv7(U_546) | ssPv4(U_546) | ~ssPv5(U_546) | ~ssPv3(U_546)))). % 11.01/4.03 tff(c_2895, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.03 tff(c_3025, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_2997, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_1928, plain, (![V_209, U_471]: (~ssPv8(V_209) | ~ssRr(U_471, V_209) | ssPv2(skf1(U_471)) | ssPv3(U_471) | ssPv3(skf1(U_471)) | ~ssPv2(U_471) | ssPv4(U_471) | ~ssPv5(U_471)))). % 11.01/4.03 tff(c_2964, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_2035, plain, (![V_209, U_477]: (~ssPv8(V_209) | ~ssRr(U_477, V_209) | ssPv2(skf1(U_477)) | ssPv3(U_477) | ssPv3(skf1(U_477)) | ssPv8(U_477) | ssPv4(U_477) | ~ssPv5(U_477)))). % 11.01/4.03 tff(c_410, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_2896, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_2868, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.03 tff(c_1904, plain, (![V_209, U_468]: (~ssPv8(V_209) | ~ssRr(U_468, V_209) | ssPv2(skf1(U_468)) | ssPv7(U_468) | ssPv3(skf1(U_468)) | ~ssPv2(U_468) | ssPv4(U_468) | ~ssPv5(U_468)))). % 11.01/4.03 tff(c_411, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv8(U_1) | ssPv6(U_1) | ~ssPv7(U_1)))). % 11.01/4.03 tff(c_1509, plain, (![U_434]: (ssPv2(skf1(U_434)) | ssPv4(skf1(U_434)) | ~ssPv5(U_434) | ssPv7(U_434) | ssPv6(U_434) | ~ssPv1(skf1(U_434)) | ssPv1(U_434) | ~ssPv3(U_434)))). % 11.01/4.04 tff(c_568, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_2209, plain, (![U_491]: (ssPv4(skf1(U_491)) | ssPv7(U_491) | ssPv2(skf1(U_491)) | ~ssPv1(U_491) | ssPv3(U_491) | ssPv3(skf1(U_491)) | ssPv8(U_491) | ~ssPv5(U_491)))). % 11.01/4.04 tff(c_1334, plain, (![U_419]: (ssPv2(skf1(U_419)) | ssPv4(skf1(U_419)) | ssPv7(U_419) | ~ssPv8(U_419) | ~ssPv6(U_419) | ~ssPv3(skf1(U_419)) | ssPv4(U_419) | ~ssPv5(U_419)))). % 11.01/4.04 tff(c_1346, plain, (![U_420]: (ssPv2(skf1(U_420)) | ssPv4(skf1(U_420)) | ssPv3(U_420) | ssPv6(U_420) | ssPv3(skf1(U_420)) | ~ssPv7(U_420) | ssPv4(U_420) | ~ssPv5(U_420)))). % 11.01/4.04 tff(c_2752, plain, (![U_520]: (ssPv7(U_520) | ~ssPv5(U_520) | ssPv3(skf1(U_520)) | ssPv4(skf1(U_520)) | ~ssPv2(U_520) | ssPv1(U_520) | ~ssPv3(U_520)))). % 11.01/4.04 tff(c_1191, plain, (![U_405]: (ssPv7(U_405) | ssPv1(skf1(U_405)) | ssPv4(skf1(U_405)) | ssPv3(U_405) | ssPv3(skf1(U_405)) | ssPv8(U_405) | ssPv5(skf1(U_405)) | ~ssPv5(U_405)))). % 11.01/4.04 tff(c_2691, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ssPv5(U_1) | ssPv2(U_1) | ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1752, plain, (![V_247, U_455]: (~ssPv6(V_247) | ~ssRr(U_455, V_247) | ssPv5(U_455) | ssPv2(U_455) | ssPv7(U_455) | ssPv1(skf1(U_455)) | ssPv2(skf1(U_455)) | ~ssPv3(U_455)))). % 11.01/4.04 tff(c_2630, plain, (![U_1]: (ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_2629, plain, (![U_1]: (ssPv4(U_1) | ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_2602, plain, (![U_1]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1043, plain, (![U_391, V_209]: (ssPv4(U_391) | ~ssPv5(U_391) | ~ssPv8(V_209) | ~ssRr(U_391, V_209) | ssPv7(U_391) | ssPv1(skf1(U_391)) | ssPv2(skf1(U_391)) | ~ssPv3(U_391)))). % 11.01/4.04 tff(c_1170, plain, (![U_404]: (ssPv7(U_404) | ssPv2(skf1(U_404)) | ~ssPv1(U_404) | ssPv3(U_404) | ssPv3(skf1(U_404)) | ssPv5(U_404) | ~ssPv8(U_404) | ~ssPv1(skf1(U_404))))). % 11.01/4.04 tff(c_2571, plain, (![U_401]: (~ssPv8(U_401) | ssPv5(U_401) | ssPv2(U_401) | ~ssPv6(U_401) | ~ssPv4(U_401) | ssPv2(skf1(U_401)) | ~ssPv3(U_401)))). % 11.01/4.04 tff(c_2429, plain, (![U_1]: (~ssPv5(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv8(U_1) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv7(U_1)))). % 11.01/4.04 tff(c_570, plain, (![U_1]: (~ssPv6(skf1(U_1)) | ~ssPv5(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv8(U_1) | ssPv6(U_1) | ~ssPv7(U_1)))). % 11.01/4.04 tff(c_2396, plain, (![U_1]: (~ssPv2(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.04 tff(c_2281, plain, (![U_1]: (~ssPv7(skf1(U_1)) | ssPv5(U_1) | ssPv2(U_1) | ~ssPv6(U_1) | ~ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1407, plain, (![V_265, U_426]: (~ssPv7(V_265) | ~ssRr(U_426, V_265) | ssPv5(U_426) | ssPv2(U_426) | ~ssPv6(U_426) | ~ssPv4(U_426) | ssPv2(skf1(U_426)) | ~ssPv3(U_426)))). % 11.01/4.04 tff(c_2199, plain, (![U_1]: (ssPv6(U_1) | ~ssPv7(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_1194, plain, (![U_405]: (ssPv7(U_405) | ssPv2(skf1(U_405)) | ~ssPv1(U_405) | ssPv3(U_405) | ssPv3(skf1(U_405)) | ssPv8(U_405) | ssPv5(skf1(U_405)) | ~ssPv5(U_405)))). % 11.01/4.04 tff(c_1240, plain, (![U_409, V_255]: (ssPv6(U_409) | ~ssPv7(V_255) | ~ssRr(U_409, V_255) | ssPv1(U_409) | ~ssPv2(U_409) | ~ssPv1(skf1(U_409)) | ssPv4(U_409) | ~ssPv5(U_409)))). % 11.01/4.04 tff(c_1172, plain, (![U_404]: (ssPv2(U_404) | ~ssPv6(U_404) | ~ssPv4(U_404) | ssPv3(U_404) | ssPv3(skf1(U_404)) | ssPv5(U_404) | ~ssPv8(U_404) | ~ssPv1(skf1(U_404))))). % 11.01/4.04 tff(c_2139, plain, (![U_486]: (~ssPv2(U_486) | ssPv7(U_486) | ~ssPv5(U_486) | ~ssPv8(U_486) | ~ssPv6(U_486) | ~ssPv3(skf1(U_486)) | ssPv1(U_486) | ~ssPv3(U_486)))). % 11.01/4.04 tff(c_1312, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv3(skf1(U_1)) | ssPv1(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1171, plain, (![U_404]: (ssPv2(U_404) | ~ssPv4(U_404) | ~ssPv1(U_404) | ssPv3(U_404) | ssPv3(skf1(U_404)) | ssPv5(U_404) | ~ssPv8(U_404) | ~ssPv1(skf1(U_404))))). % 11.01/4.04 tff(c_1147, plain, (![U_403]: (ssPv2(U_403) | ~ssPv4(U_403) | ~ssPv1(U_403) | ssPv3(U_403) | ssPv3(skf1(U_403)) | ssPv7(U_403) | ssPv6(U_403) | ~ssPv1(skf1(U_403))))). % 11.01/4.04 tff(c_2072, plain, (![U_1]: (ssPv7(U_1) | ~ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_2071, plain, (![U_1]: (ssPv4(U_1) | ssPv7(U_1) | ~ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_2044, plain, (![U_1]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ~ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1035, plain, (![U_390, V_209]: (ssPv4(U_390) | ~ssPv5(U_390) | ~ssPv8(V_209) | ~ssRr(U_390, V_209) | ssPv7(U_390) | ~ssPv1(U_390) | ssPv2(skf1(U_390)) | ~ssPv3(U_390)))). % 11.01/4.04 tff(c_1742, plain, (![U_453]: (ssPv2(skf1(U_453)) | ssPv4(skf1(U_453)) | ssPv3(U_453) | ssPv3(skf1(U_453)) | ssPv8(U_453) | ssPv4(U_453) | ~ssPv5(U_453)))). % 11.01/4.04 tff(c_1915, plain, (![U_469]: (ssPv2(skf1(U_469)) | ssPv3(U_469) | ssPv3(skf1(U_469)) | ssPv4(skf1(U_469)) | ~ssPv2(U_469) | ssPv4(U_469) | ~ssPv5(U_469)))). % 11.01/4.04 tff(c_1274, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_1887, plain, (![U_466]: (ssPv2(skf1(U_466)) | ssPv7(U_466) | ssPv3(skf1(U_466)) | ssPv4(skf1(U_466)) | ~ssPv2(U_466) | ssPv4(U_466) | ~ssPv5(U_466)))). % 11.01/4.04 tff(c_979, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_1591, plain, (![U_1]: (ssPv7(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_1823, plain, (![U_1]: (ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv7(skf1(U_1)) | ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_622, plain, (![U_300, V_255]: (ssPv6(U_300) | ~ssPv2(U_300) | ~ssPv7(V_255) | ~ssRr(U_300, V_255) | ssPv7(U_300) | ssPv8(U_300) | ssPv4(U_300) | ~ssPv5(U_300)))). % 11.01/4.04 tff(c_1789, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.04 tff(c_1144, plain, (![V_345, U_403]: (~ssPv8(V_345) | ~ssRr(U_403, V_345) | ssPv3(U_403) | ssPv3(skf1(U_403)) | ssPv7(U_403) | ssPv6(U_403) | ~ssPv1(skf1(U_403))))). % 11.01/4.04 tff(c_1756, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv5(U_1) | ~ssPv8(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.04 tff(c_1168, plain, (![V_345, U_404]: (~ssPv8(V_345) | ~ssRr(U_404, V_345) | ssPv3(U_404) | ssPv3(skf1(U_404)) | ssPv5(U_404) | ~ssPv8(U_404) | ~ssPv1(skf1(U_404))))). % 11.01/4.04 tff(c_1044, plain, (![U_391]: (ssPv5(U_391) | ssPv2(U_391) | ssPv3(skf1(U_391)) | ssPv7(U_391) | ssPv1(skf1(U_391)) | ssPv2(skf1(U_391)) | ~ssPv3(U_391)))). % 11.01/4.04 tff(c_1229, plain, (![U_1]: (ssPv4(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ssPv8(U_1) | ssPv6(U_1) | ~ssPv7(U_1)))). % 11.01/4.04 tff(c_1731, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv8(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_1695, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv8(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.04 tff(c_985, plain, (![U_244]: (ssPv2(skf1(U_244)) | ssPv4(skf1(U_244)) | ~ssPv5(U_244) | ssPv7(U_244) | ssPv6(U_244) | ~ssPv8(U_244) | ssPv1(U_244) | ~ssPv3(U_244)))). % 11.01/4.04 tff(c_1192, plain, (![V_345, U_405]: (~ssPv8(V_345) | ~ssRr(U_405, V_345) | ssPv3(U_405) | ssPv3(skf1(U_405)) | ssPv8(U_405) | ssPv5(skf1(U_405)) | ~ssPv5(U_405)))). % 11.01/4.04 tff(c_1098, plain, (![U_399]: (ssPv7(U_399) | ssPv2(skf1(U_399)) | ~ssPv1(U_399) | ssPv3(U_399) | ssPv3(skf1(U_399)) | ssPv4(skf1(U_399)) | ~ssPv2(U_399)))). % 11.01/4.04 tff(c_775, plain, (![U_327]: (~ssPv2(skf1(U_327)) | ssPv1(skf1(U_327)) | ~ssPv3(skf1(U_327)) | ssPv6(skf1(U_327)) | ssPv7(skf1(U_327)) | ~ssPv3(U_327)))). % 11.01/4.04 tff(c_1146, plain, (![U_403]: (ssPv2(skf1(U_403)) | ~ssPv1(U_403) | ssPv3(U_403) | ssPv3(skf1(U_403)) | ssPv7(U_403) | ssPv6(U_403) | ~ssPv1(skf1(U_403))))). % 11.01/4.04 tff(c_1561, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1378, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv6(U_1) | ssPv6(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1)))). % 11.01/4.04 tff(c_1379, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.05 tff(c_1534, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.05 tff(c_1530, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_1076, plain, (![U_398, V_160]: (ssPv7(U_398) | ~ssPv5(U_398) | ~ssPv8(V_160) | ~ssRr(U_398, V_160) | ssPv3(skf1(U_398)) | ssPv4(skf1(U_398)) | ~ssPv2(U_398)))). % 11.01/4.05 tff(c_1123, plain, (![V_209, U_402]: (~ssPv8(V_209) | ~ssRr(U_402, V_209) | ssPv2(skf1(U_402)) | ssPv7(U_402) | ssPv8(U_402) | ssPv4(U_402) | ~ssPv5(U_402)))). % 11.01/4.05 tff(c_980, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ~ssPv3(U_1)))). % 11.01/4.05 tff(c_1108, plain, (![U_400]: (ssPv5(U_400) | ssPv3(skf1(U_400)) | ssPv2(U_400) | ~ssPv4(U_400) | ~ssPv1(U_400) | ssPv2(skf1(U_400)) | ~ssPv3(U_400)))). % 11.01/4.05 tff(c_694, plain, (![U_1]: (~ssPv5(U_1) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1)) | ssPv1(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.05 tff(c_1036, plain, (![U_390]: (ssPv5(U_390) | ssPv2(U_390) | ssPv3(skf1(U_390)) | ssPv7(U_390) | ~ssPv1(U_390) | ssPv2(skf1(U_390)) | ~ssPv3(U_390)))). % 11.01/4.05 tff(c_982, plain, (![U_284]: (ssPv2(skf1(U_284)) | ssPv4(skf1(U_284)) | ~ssPv6(U_284) | ssPv3(U_284) | ~ssPv4(U_284) | ssPv8(U_284) | ~ssPv5(U_284)))). % 11.01/4.05 tff(c_1413, plain, (![U_1]: (~ssPv2(U_1) | ~ssPv7(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_439, plain, (![U_174, V_260]: (~ssPv2(U_174) | ~ssPv7(V_260) | ~ssRr(U_174, V_260) | ssPv7(U_174) | ssPv6(U_174) | ~ssPv8(U_174) | ssPv4(U_174) | ~ssPv5(U_174)))). % 11.01/4.05 tff(c_1116, plain, (![U_401]: (ssPv5(U_401) | ssPv3(skf1(U_401)) | ssPv2(U_401) | ~ssPv6(U_401) | ~ssPv4(U_401) | ssPv2(skf1(U_401)) | ~ssPv3(U_401)))). % 11.01/4.05 tff(c_983, plain, (![U_284]: (ssPv2(skf1(U_284)) | ssPv4(skf1(U_284)) | ~ssPv6(U_284) | ~ssPv4(U_284) | ~ssPv2(U_284) | ssPv8(U_284) | ~ssPv5(U_284)))). % 11.01/4.05 tff(c_1380, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_1352, plain, (![U_1]: (ssPv4(U_1) | ~ssPv8(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.05 tff(c_995, plain, (![U_383, V_209]: (ssPv4(U_383) | ~ssPv8(V_209) | ~ssRr(U_383, V_209) | ssPv2(skf1(U_383)) | ~ssPv5(U_383) | ~ssPv7(U_383) | ~ssPv6(U_383)))). % 11.01/4.05 tff(c_857, plain, (![U_1]: (ssPv3(U_1) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv7(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_1315, plain, (![U_1]: (ssPv7(U_1) | ~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_987, plain, (![U_174]: (ssPv2(skf1(U_174)) | ssPv4(skf1(U_174)) | ssPv7(U_174) | ssPv6(U_174) | ~ssPv8(U_174) | ssPv4(U_174) | ~ssPv5(U_174)))). % 11.01/4.05 tff(c_1287, plain, (![U_1]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv3(skf1(U_1))))). % 11.01/4.05 tff(c_172, plain, (![U_1, V_165]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv8(V_165) | ~ssRr(U_1, V_165) | ~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv3(skf1(U_1))))). % 11.01/4.05 tff(c_1095, plain, (![U_399]: (ssPv7(U_399) | ssPv1(skf1(U_399)) | ssPv3(U_399) | ssPv3(skf1(U_399)) | ssPv4(skf1(U_399)) | ~ssPv2(U_399)))). % 11.01/4.05 tff(c_1246, plain, (![U_1]: (~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.05 tff(c_1096, plain, (![V_345, U_399]: (~ssPv8(V_345) | ~ssRr(U_399, V_345) | ssPv3(U_399) | ssPv3(skf1(U_399)) | ssPv4(skf1(U_399)) | ~ssPv2(U_399)))). % 11.01/4.05 tff(c_1241, plain, (![U_409]: (~ssPv3(U_409) | ssPv1(U_409) | ~ssPv2(U_409) | ~ssPv1(skf1(U_409)) | ssPv4(U_409) | ~ssPv5(U_409)))). % 11.01/4.05 tff(c_1228, plain, (![U_1]: (ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_1200, plain, (![U_1]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.05 tff(c_290, plain, (![U_1, V_212]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(V_212) | ~ssRr(U_1, V_212) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.05 tff(c_926, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv8(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_927, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv5(U_1) | ~ssPv8(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.05 tff(c_928, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.05 tff(c_981, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_1028, plain, (![U_389]: (ssPv2(U_389) | ~ssPv6(U_389) | ~ssPv4(U_389) | ssPv2(skf1(U_389)) | ssPv4(skf1(U_389)) | ~ssPv3(U_389)))). % 11.01/4.05 tff(c_1027, plain, (![U_389]: (ssPv2(U_389) | ~ssPv4(U_389) | ~ssPv1(U_389) | ssPv2(skf1(U_389)) | ssPv4(skf1(U_389)) | ~ssPv3(U_389)))). % 11.01/4.05 tff(c_1073, plain, (![U_398]: (ssPv3(U_398) | ssPv6(skf1(U_398)) | ssPv3(skf1(U_398)) | ssPv4(skf1(U_398)) | ~ssPv2(U_398)))). % 11.01/4.05 tff(c_1060, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv2(U_1)))). % 11.01/4.05 tff(c_1056, plain, (![U_1, V_395]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv7(V_395) | ~ssPv2(U_1) | ~ssRr(U_1, V_395)))). % 11.01/4.05 tff(c_817, plain, (![U_1, W_340, V_341]: (ssPv3(skf1(U_1)) | ssPv4(W_340) | ssPv7(V_341) | ~ssPv2(U_1) | ~ssRr(U_1, W_340) | ~ssRr(U_1, V_341)))). % 11.01/4.05 tff(c_988, plain, (![U_174]: (ssPv2(skf1(U_174)) | ssPv4(skf1(U_174)) | ssPv7(U_174) | ssPv2(U_174) | ssPv4(U_174) | ~ssPv5(U_174)))). % 11.01/4.05 tff(c_1023, plain, (![U_389]: (ssPv7(U_389) | ssPv1(skf1(U_389)) | ssPv2(skf1(U_389)) | ssPv4(skf1(U_389)) | ~ssPv3(U_389)))). % 11.01/4.05 tff(c_1026, plain, (![U_389]: (ssPv7(U_389) | ~ssPv1(U_389) | ssPv2(skf1(U_389)) | ssPv4(skf1(U_389)) | ~ssPv3(U_389)))). % 11.01/4.05 tff(c_1004, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.05 tff(c_1000, plain, (![U_1, V_386]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv6(V_386) | ~ssPv3(U_1) | ~ssRr(U_1, V_386)))). % 11.01/4.05 tff(c_869, plain, (![U_1, W_353, V_354]: (ssPv2(skf1(U_1)) | ssPv4(W_353) | ssPv6(V_354) | ~ssPv3(U_1) | ~ssRr(U_1, W_353) | ~ssRr(U_1, V_354)))). % 11.01/4.05 tff(c_986, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv5(U_1) | ssPv4(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.05 tff(c_947, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv5(skf1(U_1))))). % 11.01/4.05 tff(c_943, plain, (![U_1, V_379]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv5(V_379) | ~ssRr(U_1, V_379)))). % 11.01/4.05 tff(c_886, plain, (![U_1, W_363, V_365]: (ssPv2(skf1(U_1)) | ssPv4(W_363) | ~ssPv5(U_1) | ~ssRr(U_1, W_363) | ~ssPv5(V_365) | ~ssRr(U_1, V_365)))). % 11.01/4.05 tff(c_935, plain, (![U_1, V_374]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(V_374) | ~ssRr(U_1, V_374)))). % 11.01/4.05 tff(c_635, plain, (![U_1, W_303, V_305]: (ssPv1(skf1(U_1)) | ssPv3(W_303) | ~ssPv2(U_1) | ~ssRr(U_1, W_303) | ~ssPv3(V_305) | ~ssRr(U_1, V_305)))). % 11.01/4.05 tff(c_894, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv7(skf1(U_1))))). % 11.01/4.05 tff(c_890, plain, (![U_1, V_368]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv7(V_368) | ~ssRr(U_1, V_368)))). % 11.01/4.05 tff(c_536, plain, (![U_1, W_287, V_288]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv6(W_287) | ~ssRr(U_1, W_287) | ~ssPv7(V_288) | ~ssRr(U_1, V_288)))). % 11.01/4.05 tff(c_82, plain, (![X_120, W_119, U_117, V_118]: (ssPv2(X_120) | ssPv4(W_119) | ~ssPv5(U_117) | ~ssRr(U_117, X_120) | ~ssRr(U_117, W_119) | ~ssPv5(V_118) | ~ssRr(U_117, V_118)))). % 11.01/4.05 tff(c_877, plain, (![U_1]: (ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 11.01/4.05 tff(c_873, plain, (![U_1, V_358]: (ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv6(V_358) | ~ssRr(U_1, V_358)))). % 11.01/4.05 tff(c_594, plain, (![U_1, W_297, V_298]: (ssPv7(U_1) | ssPv1(skf1(U_1)) | ssPv4(W_297) | ~ssRr(U_1, W_297) | ~ssPv6(V_298) | ~ssRr(U_1, V_298)))). % 11.01/4.05 tff(c_68, plain, (![X_92, W_91, V_90, U_89]: (ssPv2(X_92) | ssPv4(W_91) | ssPv6(V_90) | ~ssPv3(U_89) | ~ssRr(U_89, X_92) | ~ssRr(U_89, W_91) | ~ssRr(U_89, V_90)))). % 11.01/4.05 tff(c_858, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv8(U_1) | ssPv6(U_1) | ~ssPv7(U_1)))). % 11.01/4.05 tff(c_829, plain, (![U_1]: (ssPv3(U_1) | ~ssPv8(skf1(U_1)) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv7(U_1)))). % 11.01/4.05 tff(c_825, plain, (![U_1, V_347]: (ssPv3(U_1) | ~ssPv8(V_347) | ~ssRr(U_1, V_347) | ssPv6(U_1) | ssPv3(skf1(U_1)) | ~ssPv7(U_1)))). % 11.01/4.05 tff(c_821, plain, (![U_1, V_345]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv6(skf1(U_1)) | ~ssPv8(V_345) | ~ssRr(U_1, V_345)))). % 11.01/4.05 tff(c_727, plain, (![U_1, W_314, V_315]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv6(W_314) | ~ssRr(U_1, W_314) | ~ssPv8(V_315) | ~ssRr(U_1, V_315)))). % 11.01/4.05 tff(c_70, plain, (![X_96, W_95, V_94, U_93]: (ssPv3(X_96) | ssPv4(W_95) | ssPv7(V_94) | ~ssPv2(U_93) | ~ssRr(U_93, X_96) | ~ssRr(U_93, W_95) | ~ssRr(U_93, V_94)))). % 11.01/4.05 tff(c_809, plain, (![U_1, V_336]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv6(V_336) | ~ssRr(U_1, V_336)))). % 11.01/4.05 tff(c_793, plain, (![U_1, W_331, V_332]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv6(W_331) | ~ssRr(U_1, W_331) | ~ssPv6(V_332) | ~ssRr(U_1, V_332)))). % 11.01/4.05 tff(c_777, plain, (![U_327]: (ssPv7(U_327) | ssPv4(U_327) | ssPv2(U_327) | ssPv6(skf1(U_327)) | ssPv7(skf1(U_327)) | ~ssPv3(U_327)))). % 11.01/4.05 tff(c_76, plain, (![U_105, X_108, W_107, V_106]: (ssPv2(U_105) | ssPv2(X_108) | ssPv6(W_107) | ~ssRr(U_105, X_108) | ~ssRr(U_105, W_107) | ~ssPv6(V_106) | ~ssRr(U_105, V_106)))). % 11.01/4.05 tff(c_776, plain, (![U_327]: (ssPv7(U_327) | ssPv6(U_327) | ~ssPv8(U_327) | ssPv6(skf1(U_327)) | ssPv7(skf1(U_327)) | ~ssPv3(U_327)))). % 11.01/4.05 tff(c_752, plain, (![U_1]: (ssPv6(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.05 tff(c_748, plain, (![U_1, V_324]: (ssPv6(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv8(V_324) | ~ssPv3(U_1) | ~ssRr(U_1, V_324)))). % 11.01/4.05 tff(c_744, plain, (![U_1, W_319, V_320]: (ssPv6(skf1(U_1)) | ssPv7(W_319) | ssPv8(V_320) | ~ssPv3(U_1) | ~ssRr(U_1, W_319) | ~ssRr(U_1, V_320)))). % 11.01/4.05 tff(c_66, plain, (![X_88, W_87, V_86, U_85]: (ssPv6(X_88) | ssPv7(W_87) | ssPv8(V_86) | ~ssPv3(U_85) | ~ssRr(U_85, X_88) | ~ssRr(U_85, W_87) | ~ssRr(U_85, V_86)))). % 11.01/4.05 tff(c_697, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_720, plain, (![U_311]: (ssPv1(U_311) | ~ssPv3(U_311) | ~ssPv6(U_311) | ~ssPv4(U_311) | ~ssPv2(U_311) | ~ssPv5(U_311)))). % 11.01/4.05 tff(c_78, plain, (![U_109, X_112, W_111, V_110]: (ssPv3(U_109) | ssPv3(X_112) | ~ssRr(U_109, X_112) | ~ssPv6(W_111) | ~ssRr(U_109, W_111) | ~ssPv8(V_110) | ~ssRr(U_109, V_110)))). % 11.01/4.05 tff(c_673, plain, (![U_1]: (~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.05 tff(c_286, plain, (![U_210, V_160]: (~ssPv5(U_210) | ~ssPv8(V_160) | ~ssRr(U_210, V_160) | ssPv7(U_210) | ssPv6(U_210) | ~ssPv1(skf1(U_210))))). % 11.01/4.05 tff(c_654, plain, (![U_306]: (ssPv6(U_306) | ~ssPv2(U_306) | ssPv7(U_306) | ~ssPv5(U_306) | ssPv1(U_306) | ~ssPv3(U_306)))). % 11.01/4.05 tff(c_631, plain, (![U_301]: (~ssPv2(U_301) | ssPv7(U_301) | ssPv8(U_301) | ~ssPv5(U_301) | ssPv1(U_301) | ~ssPv3(U_301)))). % 11.01/4.05 tff(c_80, plain, (![X_116, W_115, U_113, V_114]: (ssPv1(X_116) | ssPv3(W_115) | ~ssPv2(U_113) | ~ssRr(U_113, X_116) | ~ssRr(U_113, W_115) | ~ssPv3(V_114) | ~ssRr(U_113, V_114)))). % 11.01/4.05 tff(c_611, plain, (![U_1]: (ssPv7(U_1) | ssPv8(U_1) | ~ssPv5(U_1) | ssPv1(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.05 tff(c_614, plain, (![U_1]: (ssPv7(U_1) | ssPv8(U_1) | ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_590, plain, (![U_1]: (ssPv7(U_1) | ~ssPv8(skf1(U_1)) | ssPv8(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.05 tff(c_72, plain, (![U_97, X_100, W_99, V_98]: (ssPv7(U_97) | ssPv1(X_100) | ssPv4(W_99) | ~ssRr(U_97, X_100) | ~ssRr(U_97, W_99) | ~ssPv6(V_98) | ~ssRr(U_97, V_98)))). % 11.01/4.05 tff(c_532, plain, (![U_284, V_160]: (ssPv7(U_284) | ~ssPv8(V_160) | ~ssRr(U_284, V_160) | ssPv8(U_284) | ssPv5(skf1(U_284)) | ~ssPv5(U_284)))). % 11.01/4.06 tff(c_531, plain, (![U_284]: (~ssPv6(U_284) | ssPv3(U_284) | ~ssPv4(U_284) | ssPv8(U_284) | ssPv5(skf1(U_284)) | ~ssPv5(U_284)))). % 11.01/4.06 tff(c_530, plain, (![U_284]: (~ssPv6(U_284) | ~ssPv4(U_284) | ~ssPv2(U_284) | ssPv8(U_284) | ssPv5(skf1(U_284)) | ~ssPv5(U_284)))). % 11.01/4.06 tff(c_549, plain, (![U_1]: (~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 11.01/4.06 tff(c_74, plain, (![U_101, X_104, W_103, V_102]: (ssPv3(U_101) | ssPv3(X_104) | ssPv6(W_103) | ~ssRr(U_101, X_104) | ~ssRr(U_101, W_103) | ~ssPv7(V_102) | ~ssRr(U_101, V_102)))). % 11.01/4.06 tff(c_520, plain, (![U_1]: (ssPv8(U_1) | ssPv5(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.06 tff(c_495, plain, (![U_1, V_280]: (ssPv8(U_1) | ssPv5(skf1(U_1)) | ssPv7(V_280) | ~ssPv5(U_1) | ~ssRr(U_1, V_280)))). % 11.01/4.06 tff(c_491, plain, (![U_1]: (~ssPv6(U_1) | ~ssPv7(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 11.01/4.06 tff(c_24, plain, (![U_22, W_24, V_23]: (ssPv8(U_22) | ssPv5(W_24) | ssPv7(V_23) | ~ssPv5(U_22) | ~ssRr(U_22, W_24) | ~ssRr(U_22, V_23)))). % 11.01/4.06 tff(c_459, plain, (![U_1, V_270]: (~ssPv6(U_1) | ~ssPv7(V_270) | ~ssRr(U_1, V_270) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 11.01/4.06 tff(c_465, plain, (![U_1]: (~ssPv6(U_1) | ~ssPv7(skf1(U_1)) | ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1)))). % 11.01/4.06 tff(c_458, plain, (![U_1, V_270]: (~ssPv6(U_1) | ~ssPv7(V_270) | ~ssRr(U_1, V_270) | ssPv8(U_1) | ssPv3(U_1) | ~ssPv4(U_1)))). % 11.01/4.06 tff(c_449, plain, (![U_1, V_268]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv6(V_268) | ~ssRr(U_1, V_268)))). % 11.01/4.06 tff(c_445, plain, (![U_1, V_265]: (~ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv7(V_265) | ~ssRr(U_1, V_265)))). % 11.01/4.06 tff(c_54, plain, (![U_67, W_69, V_68]: (ssPv7(U_67) | ~ssPv5(U_67) | ~ssPv1(W_69) | ~ssRr(U_67, W_69) | ~ssPv6(V_68) | ~ssRr(U_67, V_68)))). % 11.01/4.06 tff(c_64, plain, (![U_82, W_84, V_83]: (~ssPv6(U_82) | ~ssPv4(U_82) | ~ssPv3(W_84) | ~ssRr(U_82, W_84) | ~ssPv7(V_83) | ~ssRr(U_82, V_83)))). % 11.01/4.06 tff(c_424, plain, (![U_1, V_258]: (ssPv3(U_1) | ~ssPv6(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv7(V_258) | ~ssRr(U_1, V_258)))). % 11.01/4.06 tff(c_420, plain, (![U_1, V_255]: (ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv5(skf1(U_1)) | ~ssPv7(V_255) | ~ssRr(U_1, V_255)))). % 11.01/4.06 tff(c_60, plain, (![U_76, W_78, V_77]: (ssPv3(U_76) | ~ssPv6(U_76) | ~ssPv1(W_78) | ~ssRr(U_76, W_78) | ~ssPv7(V_77) | ~ssRr(U_76, V_77)))). % 11.01/4.06 tff(c_56, plain, (![U_70, W_72, V_71]: (ssPv6(U_70) | ~ssPv2(U_70) | ~ssPv5(W_72) | ~ssRr(U_70, W_72) | ~ssPv7(V_71) | ~ssRr(U_70, V_71)))). % 11.01/4.06 tff(c_371, plain, (![U_244]: (ssPv7(U_244) | ssPv4(U_244) | ssPv2(U_244) | ssPv1(U_244) | ssPv5(skf1(U_244)) | ~ssPv3(U_244)))). % 11.01/4.06 tff(c_390, plain, (![U_250]: (~ssPv2(U_250) | ssPv7(U_250) | ssPv6(U_250) | ~ssPv8(U_250) | ssPv1(U_250) | ~ssPv3(U_250)))). % 11.01/4.06 tff(c_370, plain, (![U_244]: (ssPv7(U_244) | ssPv6(U_244) | ~ssPv8(U_244) | ssPv1(U_244) | ssPv5(skf1(U_244)) | ~ssPv3(U_244)))). % 11.01/4.06 tff(c_375, plain, (![U_1, V_247]: (ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv6(V_247) | ~ssRr(U_1, V_247)))). % 11.01/4.06 tff(c_62, plain, (![U_79, W_81, V_80]: (ssPv2(U_79) | ~ssPv3(U_79) | ~ssPv3(W_81) | ~ssRr(U_79, W_81) | ~ssPv6(V_80) | ~ssRr(U_79, V_80)))). % 11.01/4.06 tff(c_362, plain, (![U_1]: (ssPv1(U_1) | ssPv5(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv3(U_1)))). % 11.01/4.06 tff(c_353, plain, (![U_1, V_240]: (ssPv1(U_1) | ssPv5(skf1(U_1)) | ssPv8(V_240) | ~ssPv3(U_1) | ~ssRr(U_1, V_240)))). % 11.01/4.06 tff(c_349, plain, (![U_1]: (ssPv7(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 11.01/4.06 tff(c_34, plain, (![U_37, W_39, V_38]: (ssPv1(U_37) | ssPv5(W_39) | ssPv8(V_38) | ~ssPv3(U_37) | ~ssRr(U_37, W_39) | ~ssRr(U_37, V_38)))). % 11.01/4.06 tff(c_345, plain, (![U_1, V_235]: (ssPv7(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv6(V_235) | ~ssRr(U_1, V_235)))). % 11.01/4.06 tff(c_42, plain, (![U_49, W_51, V_50]: (ssPv7(U_49) | ssPv2(W_51) | ~ssPv1(U_49) | ~ssRr(U_49, W_51) | ~ssPv6(V_50) | ~ssRr(U_49, V_50)))). % 11.01/4.06 tff(c_316, plain, (![U_225]: (ssPv1(U_225) | ~ssPv3(U_225) | ~ssPv2(U_225) | ssPv4(skf1(U_225)) | ~ssPv7(U_225) | ~ssPv6(U_225)))). % 11.01/4.06 tff(c_324, plain, (![U_1]: (ssPv6(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv3(U_1)))). % 11.01/4.06 tff(c_320, plain, (![U_1, V_227]: (ssPv6(skf1(U_1)) | ssPv8(V_227) | ~ssPv7(U_1) | ~ssPv3(U_1) | ~ssRr(U_1, V_227)))). % 11.01/4.06 tff(c_38, plain, (![W_45, V_44, U_43]: (ssPv6(W_45) | ssPv8(V_44) | ~ssPv7(U_43) | ~ssPv3(U_43) | ~ssRr(U_43, W_45) | ~ssRr(U_43, V_44)))). % 11.01/4.06 tff(c_311, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.06 tff(c_303, plain, (![U_1, V_220]: (ssPv4(skf1(U_1)) | ssPv5(V_220) | ~ssPv7(U_1) | ~ssPv6(U_1) | ~ssRr(U_1, V_220)))). % 11.01/4.06 tff(c_299, plain, (![U_1]: (ssPv5(U_1) | ssPv7(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.06 tff(c_36, plain, (![W_42, V_41, U_40]: (ssPv4(W_42) | ssPv5(V_41) | ~ssPv7(U_40) | ~ssPv6(U_40) | ~ssRr(U_40, W_42) | ~ssRr(U_40, V_41)))). % 11.01/4.06 tff(c_295, plain, (![U_1, V_216]: (ssPv5(U_1) | ssPv7(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv1(V_216) | ~ssRr(U_1, V_216)))). % 11.01/4.06 tff(c_44, plain, (![U_52, W_54, V_53]: (ssPv5(U_52) | ssPv7(W_54) | ~ssPv8(U_52) | ~ssRr(U_52, W_54) | ~ssPv1(V_53) | ~ssRr(U_52, V_53)))). % 11.01/4.06 tff(c_273, plain, (![U_204]: (ssPv2(U_204) | ~ssPv4(U_204) | ~ssPv1(U_204) | ssPv6(U_204) | ssPv3(skf1(U_204)) | ~ssPv7(U_204)))). % 11.01/4.06 tff(c_282, plain, (![U_1, V_209]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv8(V_209) | ~ssRr(U_1, V_209)))). % 11.01/4.06 tff(c_278, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ssPv7(skf1(U_1)) | ~ssPv1(skf1(U_1))))). % 11.01/4.06 tff(c_58, plain, (![U_73, W_75, V_74]: (ssPv4(U_73) | ~ssPv5(U_73) | ~ssPv4(W_75) | ~ssRr(U_73, W_75) | ~ssPv8(V_74) | ~ssRr(U_73, V_74)))). % 11.01/4.06 tff(c_261, plain, (![U_1, V_201]: (ssPv7(U_1) | ssPv6(U_1) | ssPv7(skf1(U_1)) | ~ssPv1(V_201) | ~ssRr(U_1, V_201)))). % 11.01/4.06 tff(c_265, plain, (![U_1]: (ssPv6(U_1) | ssPv3(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv7(U_1)))). % 11.01/4.06 tff(c_257, plain, (![U_1, V_198]: (ssPv6(U_1) | ssPv3(skf1(U_1)) | ssPv6(V_198) | ~ssPv7(U_1) | ~ssRr(U_1, V_198)))). % 11.01/4.06 tff(c_28, plain, (![U_28, W_30, V_29]: (ssPv7(U_28) | ssPv6(U_28) | ssPv7(W_30) | ~ssRr(U_28, W_30) | ~ssPv1(V_29) | ~ssRr(U_28, V_29)))). % 11.01/4.06 tff(c_26, plain, (![U_25, W_27, V_26]: (ssPv6(U_25) | ssPv3(W_27) | ssPv6(V_26) | ~ssPv7(U_25) | ~ssRr(U_25, W_27) | ~ssRr(U_25, V_26)))). % 11.01/4.06 tff(c_224, plain, (![U_185]: (ssPv7(U_185) | ssPv6(U_185) | ~ssPv8(U_185) | ssPv7(skf1(U_185)) | ~ssPv5(U_185) | ~ssPv3(U_185)))). % 11.01/4.06 tff(c_225, plain, (![U_185]: (ssPv7(U_185) | ssPv4(U_185) | ssPv2(U_185) | ssPv7(skf1(U_185)) | ~ssPv5(U_185) | ~ssPv3(U_185)))). % 11.01/4.06 tff(c_233, plain, (![U_1, V_190]: (ssPv8(U_1) | ~ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv8(V_190) | ~ssRr(U_1, V_190)))). % 11.01/4.06 tff(c_229, plain, (![U_1]: (ssPv1(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 11.01/4.06 tff(c_50, plain, (![U_61, W_63, V_62]: (ssPv8(U_61) | ~ssPv3(U_61) | ~ssPv2(W_63) | ~ssRr(U_61, W_63) | ~ssPv8(V_62) | ~ssRr(U_61, V_62)))). % 11.01/4.06 tff(c_212, plain, (![U_1, V_182]: (ssPv1(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(V_182) | ~ssRr(U_1, V_182)))). % 11.01/4.06 tff(c_216, plain, (![U_1]: (ssPv7(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv3(U_1)))). % 11.01/4.06 tff(c_208, plain, (![U_1, V_178]: (ssPv7(skf1(U_1)) | ssPv8(V_178) | ~ssPv5(U_1) | ~ssPv3(U_1) | ~ssRr(U_1, V_178)))). % 11.01/4.06 tff(c_46, plain, (![U_55, W_57, V_56]: (ssPv1(U_55) | ssPv4(W_57) | ~ssPv2(U_55) | ~ssRr(U_55, W_57) | ~ssPv1(V_56) | ~ssRr(U_55, V_56)))). % 11.01/4.06 tff(c_40, plain, (![W_48, V_47, U_46]: (ssPv7(W_48) | ssPv8(V_47) | ~ssPv5(U_46) | ~ssPv3(U_46) | ~ssRr(U_46, W_48) | ~ssRr(U_46, V_47)))). % 11.01/4.06 tff(c_193, plain, (![U_174]: (ssPv7(U_174) | ssPv6(U_174) | ~ssPv8(U_174) | ssPv4(U_174) | ssPv5(skf1(U_174)) | ~ssPv5(U_174)))). % 11.01/4.06 tff(c_194, plain, (![U_174]: (ssPv7(U_174) | ssPv2(U_174) | ssPv4(U_174) | ssPv5(skf1(U_174)) | ~ssPv5(U_174)))). % 11.01/4.06 tff(c_185, plain, (![U_1]: (ssPv4(U_1) | ssPv5(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv5(U_1)))). % 11.01/4.06 tff(c_181, plain, (![U_1, V_171]: (ssPv4(U_1) | ssPv5(skf1(U_1)) | ssPv8(V_171) | ~ssPv5(U_1) | ~ssRr(U_1, V_171)))). % 11.01/4.06 tff(c_30, plain, (![U_31, W_33, V_32]: (ssPv4(U_31) | ssPv5(W_33) | ssPv8(V_32) | ~ssPv5(U_31) | ~ssRr(U_31, W_33) | ~ssRr(U_31, V_32)))). % 11.01/4.06 tff(c_176, plain, (![U_1]: (ssPv5(U_1) | ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 11.01/4.06 tff(c_168, plain, (![U_1, V_163]: (ssPv5(U_1) | ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(V_163) | ~ssRr(U_1, V_163)))). % 11.01/4.06 tff(c_164, plain, (![U_1, V_160]: (ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv7(skf1(U_1)) | ~ssPv8(V_160) | ~ssRr(U_1, V_160)))). % 11.01/4.06 tff(c_32, plain, (![U_34, W_36, V_35]: (ssPv5(U_34) | ssPv2(U_34) | ssPv3(W_36) | ~ssRr(U_34, W_36) | ~ssPv4(V_35) | ~ssRr(U_34, V_35)))). % 11.01/4.06 tff(c_52, plain, (![U_64, W_66, V_65]: (ssPv7(U_64) | ~ssPv5(U_64) | ~ssPv7(W_66) | ~ssRr(U_64, W_66) | ~ssPv8(V_65) | ~ssRr(U_64, V_65)))). % 11.01/4.06 tff(c_159, plain, (![U_1]: (ssPv7(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv3(skf1(U_1))))). % 11.01/4.06 tff(c_155, plain, (![U_1, V_154]: (ssPv7(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv6(U_1) | ~ssPv3(V_154) | ~ssRr(U_1, V_154)))). % 11.01/4.06 tff(c_48, plain, (![W_60, U_58, V_59]: (ssPv7(W_60) | ~ssPv8(U_58) | ~ssPv6(U_58) | ~ssRr(U_58, W_60) | ~ssPv3(V_59) | ~ssRr(U_58, V_59)))). % 11.01/4.06 tff(c_142, plain, (![U_1]: (ssPv8(U_1) | ssPv6(U_1) | ssPv8(skf1(U_1)) | ~ssPv7(U_1)))). % 11.01/4.06 tff(c_4, plain, (![U_2, V_3]: (ssPv8(U_2) | ssPv6(U_2) | ssPv8(V_3) | ~ssPv7(U_2) | ~ssRr(U_2, V_3)))). % 11.01/4.06 tff(c_136, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv8(skf1(U_1))))). % 11.01/4.06 tff(c_10, plain, (![U_8, V_9]: (ssPv7(U_8) | ssPv6(U_8) | ~ssPv8(U_8) | ~ssPv8(V_9) | ~ssRr(U_8, V_9)))). % 11.01/4.06 tff(c_130, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv6(U_1)))). % 11.01/4.06 tff(c_12, plain, (![V_11, U_10]: (ssPv2(V_11) | ~ssPv8(U_10) | ~ssPv7(U_10) | ~ssPv6(U_10) | ~ssRr(U_10, V_11)))). % 11.01/4.06 tff(c_124, plain, (![U_1]: (ssPv8(U_1) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1)))). % 11.01/4.06 tff(c_6, plain, (![U_4, V_5]: (ssPv8(U_4) | ssPv3(U_4) | ssPv3(V_5) | ~ssPv4(U_4) | ~ssRr(U_4, V_5)))). % 11.01/4.06 tff(c_118, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv7(U_1) | ~ssPv4(U_1)))). % 11.01/4.06 tff(c_14, plain, (![V_13, U_12]: (ssPv2(V_13) | ~ssPv8(U_12) | ~ssPv7(U_12) | ~ssPv4(U_12) | ~ssRr(U_12, V_13)))). % 11.01/4.06 tff(c_112, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 11.01/4.06 tff(c_16, plain, (![V_15, U_14]: (ssPv3(V_15) | ~ssPv5(U_14) | ~ssPv4(U_14) | ~ssPv2(U_14) | ~ssRr(U_14, V_15)))). % 11.01/4.06 tff(c_106, plain, (![U_1]: (ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssPv6(skf1(U_1))))). % 11.01/4.06 tff(c_20, plain, (![U_18, V_19]: (ssPv2(U_18) | ~ssPv4(U_18) | ~ssPv1(U_18) | ~ssPv6(V_19) | ~ssRr(U_18, V_19)))). % 11.01/4.06 tff(c_100, plain, (![U_1]: (ssPv7(U_1) | ssPv4(U_1) | ssPv2(U_1) | ~ssPv8(skf1(U_1))))). % 11.01/4.06 tff(c_8, plain, (![U_6, V_7]: (ssPv7(U_6) | ssPv4(U_6) | ssPv2(U_6) | ~ssPv8(V_7) | ~ssRr(U_6, V_7)))). % 11.01/4.06 tff(c_94, plain, (![U_1]: (ssPv2(U_1) | ~ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv6(skf1(U_1))))). % 11.01/4.06 tff(c_18, plain, (![U_16, V_17]: (ssPv2(U_16) | ~ssPv6(U_16) | ~ssPv4(U_16) | ~ssPv6(V_17) | ~ssRr(U_16, V_17)))). % 11.01/4.07 tff(c_88, plain, (![U_1]: (ssPv1(U_1) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv5(skf1(U_1))))). % 11.01/4.07 tff(c_22, plain, (![U_20, V_21]: (ssPv1(U_20) | ~ssPv3(U_20) | ~ssPv2(U_20) | ~ssPv5(V_21) | ~ssRr(U_20, V_21)))). % 11.01/4.07 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 11.01/4.07 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.01/4.07 %------------------------------------------------------------------------------