%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS084+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n020.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 : 600s % DateTime : Sun Jul 17 03:31:51 EDT 2022 % Result : Unsatisfiable 79.41s 79.61s % Output : Proof 79.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS084+1 : TPTP v8.1.0. Released v3.1.0. % 0.00/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jun 7 07:33:06 EDT 2022 % 0.12/0.34 % CPUTime : % 79.41/79.61 % SZS status Theorem % 79.41/79.61 (* PROOF-FOUND *) % 79.41/79.61 (* BEGIN-PROOF *) % 79.41/79.61 % SZS output start Proof % 79.41/79.61 1. (rf T_0 (i2003_11_14_17_19_35232)) (-. (rf T_0 (i2003_11_14_17_19_35232))) ### Axiom % 79.41/79.61 2. (rf T_0 T_1) (-. (rf T_0 T_1)) ### Axiom % 79.41/79.61 3. ((i2003_11_14_17_19_35232) != T_1) ((i2003_11_14_17_19_35232) = T_1) ### Axiom % 79.41/79.61 4. (((rf T_0 (i2003_11_14_17_19_35232)) /\ (rf T_0 T_1)) => ((i2003_11_14_17_19_35232) = T_1)) ((i2003_11_14_17_19_35232) != T_1) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) ### DisjTree 1 2 3 % 79.41/79.61 5. (All Z, (((rf T_0 (i2003_11_14_17_19_35232)) /\ (rf T_0 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((i2003_11_14_17_19_35232) != T_1) ### All 4 % 79.41/79.61 6. (All Y, (All Z, (((rf T_0 Y) /\ (rf T_0 Z)) => (Y = Z)))) ((i2003_11_14_17_19_35232) != T_1) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) ### All 5 % 79.41/79.61 7. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((i2003_11_14_17_19_35232) != T_1) ### All 6 % 79.41/79.61 8. ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (-. ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232)))))) ### Axiom % 79.41/79.61 9. (-. (cUnsatisfiable (i2003_11_14_17_19_35232))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) ### Definition-Pseudo(cUnsatisfiable) 8 % 79.41/79.61 10. (rf T_0 T_1) (-. (rf T_0 T_1)) ### Axiom % 79.41/79.61 11. (rf T_0 (i2003_11_14_17_19_35232)) (-. (rf T_0 (i2003_11_14_17_19_35232))) ### Axiom % 79.41/79.61 12. (T_1 != (i2003_11_14_17_19_35232)) (T_1 = (i2003_11_14_17_19_35232)) ### Axiom % 79.41/79.61 13. (((rf T_0 T_1) /\ (rf T_0 (i2003_11_14_17_19_35232))) => (T_1 = (i2003_11_14_17_19_35232))) (T_1 != (i2003_11_14_17_19_35232)) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ### DisjTree 10 11 12 % 79.41/79.61 14. (All Z, (((rf T_0 T_1) /\ (rf T_0 Z)) => (T_1 = Z))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (T_1 != (i2003_11_14_17_19_35232)) ### All 13 % 79.41/79.61 15. (All Y, (All Z, (((rf T_0 Y) /\ (rf T_0 Z)) => (Y = Z)))) (T_1 != (i2003_11_14_17_19_35232)) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ### All 14 % 79.41/79.61 16. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (T_1 != (i2003_11_14_17_19_35232)) ### All 15 % 79.41/79.61 17. (rf T_2 T_1) (-. (rf T_2 T_1)) ### Axiom % 79.41/79.61 18. (-. (rinvF T_1 T_2)) (rf T_2 T_1) ### Definition-Pseudo(rinvF) 17 % 79.41/79.61 19. (rf T_2 T_1) (-. (rf T_2 T_1)) ### Axiom % 79.41/79.61 20. (rf T_2 T_3) (-. (rf T_2 T_3)) ### Axiom % 79.41/79.61 21. (T_1 != T_3) (T_1 = T_3) ### Axiom % 79.41/79.61 22. (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (T_1 != T_3) (rf T_2 T_3) (rf T_2 T_1) ### DisjTree 19 20 21 % 79.41/79.61 23. (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (rf T_2 T_3) (T_1 != T_3) ### All 22 % 79.41/79.61 24. (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (T_1 != T_3) (rf T_2 T_3) (rf T_2 T_1) ### All 23 % 79.41/79.61 25. ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (-. ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1))))) ### Axiom % 79.41/79.61 26. (-. (cUnsatisfiable T_1)) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) ### Definition-Pseudo(cUnsatisfiable) 25 % 79.41/79.61 27. (rf T_2 T_1) (-. (rf T_2 T_1)) ### Axiom % 79.41/79.61 28. (rf T_2 (i2003_11_14_17_19_35232)) (-. (rf T_2 (i2003_11_14_17_19_35232))) ### Axiom % 79.41/79.61 29. (T_1 != T_1) ### Refl(=) % 79.41/79.61 30. (T_1 != T_1) ### Refl(=) % 79.41/79.61 31. (rf T_2 (i2003_11_14_17_19_35232)) (-. (rf T_2 (i2003_11_14_17_19_35232))) ### Axiom % 79.41/79.61 32. (rf T_2 T_1) (-. (rf T_2 T_1)) ### Axiom % 79.41/79.61 33. (rf T_2 T_3) (-. (rf T_2 T_3)) ### Axiom % 79.41/79.61 34. (T_1 = T_3) (T_3 != T_1) ### Sym(=) % 79.41/79.61 35. (rf T_4 T_3) (-. (rf T_4 T_3)) ### Axiom % 79.41/79.61 36. (-. (rinvF T_3 T_4)) (rf T_4 T_3) ### Definition-Pseudo(rinvF) 35 % 79.41/79.61 37. (rf T_4 T_1) (-. (rf T_4 T_1)) ### Axiom % 79.41/79.61 38. (rf T_4 T_5) (-. (rf T_4 T_5)) ### Axiom % 79.41/79.61 39. (T_5 != T_1) (T_1 = T_5) ### Sym(=) % 79.41/79.61 40. (((rf T_4 T_1) /\ (rf T_4 T_5)) => (T_1 = T_5)) (T_5 != T_1) (rf T_4 T_5) (rf T_4 T_1) ### DisjTree 37 38 39 % 79.41/79.61 41. (All Z, (((rf T_4 T_1) /\ (rf T_4 Z)) => (T_1 = Z))) (rf T_4 T_1) (rf T_4 T_5) (T_5 != T_1) ### All 40 % 79.41/79.61 42. (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (T_5 != T_1) (rf T_4 T_5) (rf T_4 T_1) ### All 41 % 79.41/79.61 43. (T_3 != T_3) ### Refl(=) % 79.41/79.61 44. (T_3 != T_5) (T_1 = T_3) (rf T_4 T_1) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) ### Trans-sym 42 43 % 79.41/79.61 45. (rf T_2 T_3) (-. (rf T_2 T_3)) ### Axiom % 79.41/79.61 46. (-. (rinvF T_3 T_2)) (rf T_2 T_3) ### Definition-Pseudo(rinvF) 45 % 79.41/79.61 47. (-. (rf T_2 T_5)) (rf T_2 T_5) ### Axiom % 79.41/79.61 48. (rinvF T_5 T_2) (-. (rf T_2 T_5)) ### Definition-Pseudo(rinvF) 47 % 79.41/79.61 49. (((T_3 = T_5) /\ (rinvF T_3 T_2)) => (rinvF T_5 T_2)) (-. (rf T_2 T_5)) (rf T_2 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (rf T_4 T_1) (T_1 = T_3) ### DisjTree 44 46 48 % 79.41/79.61 50. (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (T_1 = T_3) (rf T_4 T_1) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_2 T_3) (-. (rf T_2 T_5)) ### All 49 % 79.41/79.61 51. (rinvF T_1 T_4) (-. (rf T_2 T_5)) (rf T_2 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (T_1 = T_3) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) ### Definition-Pseudo(rinvF) 50 % 79.41/79.61 52. (((T_3 = T_1) /\ (rinvF T_3 T_4)) => (rinvF T_1 T_4)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_2 T_3) (-. (rf T_2 T_5)) (rf T_4 T_3) (T_1 = T_3) ### DisjTree 34 36 51 % 79.41/79.61 53. (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (T_1 = T_3) (rf T_4 T_3) (-. (rf T_2 T_5)) (rf T_2 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) ### All 52 % 79.41/79.61 54. (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (-. (rf T_2 T_5)) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (rf T_2 T_1) ### DisjTree 32 33 53 % 79.41/79.61 55. ((i2003_11_14_17_19_35232) != T_5) ((i2003_11_14_17_19_35232) = T_5) ### Axiom % 79.41/79.61 56. (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 T_5)) => ((i2003_11_14_17_19_35232) = T_5)) ((i2003_11_14_17_19_35232) != T_5) (rf T_2 T_1) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (rf T_2 (i2003_11_14_17_19_35232)) ### DisjTree 31 54 55 % 79.41/79.61 57. (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 (i2003_11_14_17_19_35232)) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (rf T_2 T_1) ((i2003_11_14_17_19_35232) != T_5) ### All 56 % 79.41/79.61 58. (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) ((i2003_11_14_17_19_35232) != T_5) (rf T_2 T_1) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_2 (i2003_11_14_17_19_35232)) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) ### All 57 % 79.41/79.61 59. (T_1 != T_5) (T_1 = (i2003_11_14_17_19_35232)) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 (i2003_11_14_17_19_35232)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) ### TransEq 29 30 58 % 79.41/79.68 60. (((rf T_2 T_1) /\ (rf T_2 (i2003_11_14_17_19_35232))) => (T_1 = (i2003_11_14_17_19_35232))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (T_1 != T_5) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ### DisjTree 27 28 59 % 79.41/79.68 61. (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (T_1 != T_5) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) ### All 60 % 79.41/79.68 62. (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (T_1 != T_5) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ### All 61 % 79.41/79.68 63. (rf T_2 (i2003_11_14_17_19_35232)) (-. (rf T_2 (i2003_11_14_17_19_35232))) ### Axiom % 79.41/79.68 64. (rf T_2 T_3) (-. (rf T_2 T_3)) ### Axiom % 79.41/79.68 65. (rf T_2 (i2003_11_14_17_19_35232)) (-. (rf T_2 (i2003_11_14_17_19_35232))) ### Axiom % 79.41/79.68 66. (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (-. (rf T_2 T_5)) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) ### All 54 % 79.41/79.68 67. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (-. (rf T_2 T_5)) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) ### All 66 % 79.41/79.68 68. (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (-. (rf T_2 T_5)) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 67 % 79.41/79.68 69. (rf T_2 T_1) (-. (rf T_2 T_1)) ### Axiom % 79.41/79.68 70. ((i2003_11_14_17_19_35232) = T_3) (T_3 != (i2003_11_14_17_19_35232)) ### Sym(=) % 79.41/79.68 71. (T_5 != T_5) ### Refl(=) % 79.41/79.68 72. (T_5 != T_3) ((i2003_11_14_17_19_35232) = T_5) ((i2003_11_14_17_19_35232) = T_3) ### Trans-sym 70 71 % 79.41/79.68 73. (rf T_6 T_5) (-. (rf T_6 T_5)) ### Axiom % 79.41/79.68 74. (-. (rinvF T_5 T_6)) (rf T_6 T_5) ### Definition-Pseudo(rinvF) 73 % 79.41/79.68 75. (rf T_2 T_3) (-. (rf T_2 T_3)) ### Axiom % 79.41/79.68 76. (T_1 = T_5) (T_5 != T_1) ### Sym(=) % 79.41/79.68 77. (rf T_6 T_1) (-. (rf T_6 T_1)) ### Axiom % 79.41/79.68 78. (rf T_6 T_7) (-. (rf T_6 T_7)) ### Axiom % 79.41/79.68 79. (T_1 = T_7) (T_1 != T_7) ### Axiom % 79.41/79.68 80. (rf T_2 T_7) (-. (rf T_2 T_7)) ### Axiom % 79.41/79.68 81. (rf T_2 T_3) (-. (rf T_2 T_3)) ### Axiom % 79.41/79.68 82. (T_7 = T_3) (T_3 != T_7) ### Sym(=) % 79.41/79.68 83. ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (-. ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3))))) ### Axiom % 79.41/79.68 84. (-. (cUnsatisfiable T_3)) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) ### Definition-Pseudo(cUnsatisfiable) 83 % 79.41/79.68 85. (rf T_6 T_7) (-. (rf T_6 T_7)) ### Axiom % 79.41/79.68 86. (rf T_6 T_3) (-. (rf T_6 T_3)) ### Axiom % 79.41/79.68 87. (T_1 != T_1) ### Refl(=) % 79.41/79.68 88. (rf T_8 T_9) (-. (rf T_8 T_9)) ### Axiom % 79.41/79.68 89. (T_7 = T_3) (T_7 != T_3) ### Axiom % 79.41/79.68 90. (rf T_8 T_7) (-. (rf T_8 T_7)) ### Axiom % 79.41/79.68 91. (-. (rinvF T_7 T_8)) (rf T_8 T_7) ### Definition-Pseudo(rinvF) 90 % 79.41/79.68 92. (-. (rf T_8 T_3)) (rf T_8 T_3) ### Axiom % 79.41/79.68 93. (rinvF T_3 T_8) (-. (rf T_8 T_3)) ### Definition-Pseudo(rinvF) 92 % 79.41/79.68 94. (((T_7 = T_3) /\ (rinvF T_7 T_8)) => (rinvF T_3 T_8)) (-. (rf T_8 T_3)) (rf T_8 T_7) (T_7 = T_3) ### DisjTree 89 91 93 % 79.41/79.68 95. (All C, (((T_7 = T_3) /\ (rinvF T_7 C)) => (rinvF T_3 C))) (T_7 = T_3) (rf T_8 T_7) (-. (rf T_8 T_3)) ### All 94 % 79.41/79.68 96. (T_9 != T_3) (T_9 = T_3) ### Axiom % 79.41/79.68 97. (((rf T_8 T_9) /\ (rf T_8 T_3)) => (T_9 = T_3)) (T_9 != T_3) (rf T_8 T_7) (T_7 = T_3) (All C, (((T_7 = T_3) /\ (rinvF T_7 C)) => (rinvF T_3 C))) (rf T_8 T_9) ### DisjTree 88 95 96 % 79.41/79.68 98. (All Z, (((rf T_8 T_9) /\ (rf T_8 Z)) => (T_9 = Z))) (rf T_8 T_9) (All C, (((T_7 = T_3) /\ (rinvF T_7 C)) => (rinvF T_3 C))) (T_7 = T_3) (rf T_8 T_7) (T_9 != T_3) ### All 97 % 79.41/79.68 99. (All Y, (All Z, (((rf T_8 Y) /\ (rf T_8 Z)) => (Y = Z)))) (T_9 != T_3) (rf T_8 T_7) (T_7 = T_3) (All C, (((T_7 = T_3) /\ (rinvF T_7 C)) => (rinvF T_3 C))) (rf T_8 T_9) ### All 98 % 79.41/79.68 100. (All B, (All C, (((T_7 = B) /\ (rinvF T_7 C)) => (rinvF B C)))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (T_9 != T_3) (All Y, (All Z, (((rf T_8 Y) /\ (rf T_8 Z)) => (Y = Z)))) ### All 99 % 79.41/79.68 101. (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All Y, (All Z, (((rf T_8 Y) /\ (rf T_8 Z)) => (Y = Z)))) (T_9 != T_3) (rf T_8 T_7) (T_7 = T_3) (rf T_8 T_9) ### All 100 % 79.41/79.68 102. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (T_9 != T_3) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ### All 101 % 79.41/79.68 103. (T_5 != T_5) ### Refl(=) % 79.41/79.68 104. (T_5 != T_9) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (T_7 = T_3) (rf T_8 T_9) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Trans-sym 102 103 % 79.41/79.68 105. (T_1 != T_9) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ### Trans 87 104 % 79.41/79.68 106. (rf T_6 T_7) (-. (rf T_6 T_7)) ### Axiom % 79.41/79.68 107. (rf T_6 T_9) (-. (rf T_6 T_9)) ### Axiom % 79.41/79.68 108. (rf T_4 T_3) (-. (rf T_4 T_3)) ### Axiom % 79.41/79.68 109. (-. (rr T_4 T_3)) (rr T_4 T_3) ### Axiom % 79.41/79.68 110. ((rf T_4 T_3) => (rr T_4 T_3)) (-. (rr T_4 T_3)) (rf T_4 T_3) ### Imply 108 109 % 79.41/79.68 111. (All Y, ((rf T_4 Y) => (rr T_4 Y))) (rf T_4 T_3) (-. (rr T_4 T_3)) ### All 110 % 79.41/79.68 112. (All X, (All Y, ((rf X Y) => (rr X Y)))) (-. (rr T_4 T_3)) (rf T_4 T_3) ### All 111 % 79.41/79.68 113. (T_7 != T_7) ### Refl(=) % 79.41/79.68 114. (-. (rr T_4 T_7)) (T_7 = T_3) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) ### TransEq2 112 112 113 % 79.41/79.68 115. (T_9 != T_9) ### Refl(=) % 79.41/79.68 116. (-. (rr T_4 T_9)) (T_7 = T_9) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (T_7 = T_3) ### TransEq 114 114 115 % 79.41/79.68 117. (-. (rinvR T_9 T_4)) (T_7 = T_3) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (T_7 = T_9) ### Definition-Pseudo(rinvR) 116 % 79.41/79.68 118. (rf T_10 T_11) (-. (rf T_10 T_11)) ### Axiom % 79.41/79.68 119. (rf T_10 T_4) (-. (rf T_10 T_4)) ### Axiom % 79.41/79.68 120. (T_4 != T_11) (T_11 = T_4) ### Sym(=) % 79.41/79.68 121. (((rf T_10 T_11) /\ (rf T_10 T_4)) => (T_11 = T_4)) (T_4 != T_11) (rf T_10 T_4) (rf T_10 T_11) ### DisjTree 118 119 120 % 79.41/79.68 122. (All Z, (((rf T_10 T_11) /\ (rf T_10 Z)) => (T_11 = Z))) (rf T_10 T_11) (rf T_10 T_4) (T_4 != T_11) ### All 121 % 79.41/79.68 123. (All Y, (All Z, (((rf T_10 Y) /\ (rf T_10 Z)) => (Y = Z)))) (T_4 != T_11) (rf T_10 T_4) (rf T_10 T_11) ### All 122 % 79.41/79.68 124. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_10 T_11) (rf T_10 T_4) (T_4 != T_11) ### All 123 % 79.41/79.68 125. (cc T_4) (-. (cc T_4)) ### Axiom % 79.41/79.68 126. (-. (cc T_11)) (cc T_11) ### Axiom % 79.41/79.68 127. (((T_4 = T_11) /\ (cc T_4)) => (cc T_11)) (-. (cc T_11)) (cc T_4) (rf T_10 T_4) (rf T_10 T_11) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### DisjTree 124 125 126 % 79.50/79.71 128. (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_10 T_11) (rf T_10 T_4) (cc T_4) (-. (cc T_11)) ### All 127 % 79.50/79.71 129. ((rf T_10 T_11) /\ (-. (cc T_11))) (cc T_4) (rf T_10 T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) ### And 128 % 79.50/79.71 130. (Ex Y, ((rf T_10 Y) /\ (-. (cc Y)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_10 T_4) (cc T_4) ### Exists 129 % 79.50/79.71 131. ((Ex Y, ((rf T_10 Y) /\ (-. (cc Y)))) /\ (cc T_10)) (cc T_4) (rf T_10 T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) ### And 130 % 79.50/79.71 132. (cd T_10) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_10 T_4) (cc T_4) ### Definition-Pseudo(cd) 131 % 79.50/79.71 133. (rinvF T_4 T_10) (cc T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cd T_10) ### Definition-Pseudo(rinvF) 132 % 79.50/79.71 134. ((rinvF T_4 T_10) /\ (cd T_10)) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (cc T_4) ### And 133 % 79.50/79.71 135. (Ex Y, ((rinvF T_4 Y) /\ (cd Y))) (cc T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) ### Exists 134 % 79.50/79.71 136. ((rinvR T_9 T_4) => (Ex Y, ((rinvF T_4 Y) /\ (cd Y)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (cc T_4) (T_7 = T_9) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (T_7 = T_3) ### Imply 117 135 % 79.50/79.71 137. (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (T_7 = T_3) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (T_7 = T_9) (cc T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) ### All 136 % 79.50/79.72 138. (((rf T_6 T_7) /\ (rf T_6 T_9)) => (T_7 = T_9)) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (T_7 = T_3) (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (rf T_6 T_9) (rf T_6 T_7) ### DisjTree 106 107 137 % 79.50/79.72 139. (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (rf T_6 T_7) (rf T_6 T_9) (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (T_7 = T_3) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) ### All 138 % 79.50/79.72 140. (rinvF T_9 T_6) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (T_7 = T_3) (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (rf T_6 T_7) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) ### Definition-Pseudo(rinvF) 139 % 79.50/79.72 141. (((T_5 = T_9) /\ (rinvF T_5 T_6)) => (rinvF T_9 T_6)) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (rf T_6 T_7) (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ### DisjTree 104 74 140 % 79.50/79.72 142. (All C, (((T_5 = T_9) /\ (rinvF T_5 C)) => (rinvF T_9 C))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (T_7 = T_3) (rf T_8 T_9) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (rf T_6 T_7) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) ### All 141 % 79.50/79.72 143. (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (rf T_6 T_7) (All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ### All 142 % 79.50/79.72 144. ((Ex Z, ((rinvF T_9 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_9 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_9)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (T_7 = T_3) (rf T_8 T_9) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (rf T_6 T_7) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ### ConjTree 143 % 79.50/79.72 145. (cUnsatisfiable T_9) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (rf T_6 T_7) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ### Definition-Pseudo(cUnsatisfiable) 144 % 79.50/79.72 146. (((T_1 = T_9) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable T_9)) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (rf T_6 T_7) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (T_7 = T_3) (rf T_8 T_9) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) ### DisjTree 105 26 145 % 79.50/79.72 147. (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (T_7 = T_3) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (rf T_6 T_7) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) ### All 146 % 79.50/79.72 148. (((rf T_6 T_7) /\ (rf T_6 T_3)) => (T_7 = T_3)) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (rf T_8 T_9) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ### DisjTree 85 86 147 % 79.50/79.72 149. (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_9) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All Z, (((rf T_6 T_7) /\ (rf T_6 Z)) => (T_7 = Z))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) ### All 148 % 79.50/79.77 150. (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (rf T_8 T_9) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ### All 149 % 79.50/79.77 151. ((rf T_8 T_9) /\ (-. (cc T_9))) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) ### And 150 % 79.50/79.77 152. (Ex Y, ((rf T_8 Y) /\ (-. (cc Y)))) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ### Exists 151 % 79.50/79.77 153. ((Ex Y, ((rf T_8 Y) /\ (-. (cc Y)))) /\ (cc T_8)) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_8 T_7) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) ### And 152 % 79.50/79.77 154. (cd T_8) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (rf T_8 T_7) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ### Definition-Pseudo(cd) 153 % 79.50/79.77 155. (rinvF T_7 T_8) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (cd T_8) ### Definition-Pseudo(rinvF) 154 % 79.50/79.77 156. ((rinvF T_7 T_8) /\ (cd T_8)) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ### And 155 % 79.50/79.77 157. (Ex Z, ((rinvF T_7 Z) /\ (cd Z))) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) ### Exists 156 % 79.50/79.77 158. ((Ex Z, ((rinvF T_7 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_7 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_7)))) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ### ConjTree 157 % 79.50/79.77 159. (cUnsatisfiable T_7) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) ### Definition-Pseudo(cUnsatisfiable) 158 % 79.50/79.77 160. (((T_3 = T_7) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable T_7)) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (T_7 = T_3) ### DisjTree 82 84 159 % 79.50/79.77 161. (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (T_7 = T_3) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) ### All 160 % 79.58/79.82 162. (((rf T_2 T_7) /\ (rf T_2 T_3)) => (T_7 = T_3)) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_7) ### DisjTree 80 81 161 % 79.58/79.82 163. (All Z, (((rf T_2 T_7) /\ (rf T_2 Z)) => (T_7 = Z))) (rf T_2 T_7) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) ### All 162 % 79.58/79.82 164. (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_7) ### All 163 % 79.58/79.82 165. (rinvF T_7 T_2) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) ### Definition-Pseudo(rinvF) 164 % 79.58/79.82 166. (((T_1 = T_7) /\ (rinvF T_1 T_2)) => (rinvF T_7 T_2)) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_1) (T_1 = T_7) ### DisjTree 79 18 165 % 79.58/79.82 167. (All C, (((T_1 = T_7) /\ (rinvF T_1 C)) => (rinvF T_7 C))) (T_1 = T_7) (rf T_2 T_1) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_7) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) ### All 166 % 79.58/79.82 168. (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) (rf T_6 T_7) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_1) (T_1 = T_7) ### All 167 % 79.58/79.82 169. (((rf T_6 T_1) /\ (rf T_6 T_7)) => (T_1 = T_7)) (rf T_2 T_1) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_1) ### DisjTree 77 78 168 % 79.58/79.82 170. (All Z, (((rf T_6 T_1) /\ (rf T_6 Z)) => (T_1 = Z))) (rf T_6 T_1) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_1) ### All 169 % 79.58/79.84 171. (rf T_2 T_1) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_6 Y) /\ (rf T_6 Z)) => (Y = Z)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_1) ### All 170 % 79.58/79.84 172. (rf T_6 T_1) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (rf T_6 T_5) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (T_1 = T_5) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_1) ### All 171 % 79.58/79.84 173. (rinvF T_1 T_6) (rf T_2 T_1) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (T_1 = T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (rf T_6 T_5) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) ### Definition-Pseudo(rinvF) 172 % 79.58/79.84 174. (((T_5 = T_1) /\ (rinvF T_5 T_6)) => (rinvF T_1 T_6)) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (rf T_4 T_3) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (T_3 = T_5) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_2 T_3) (rf T_2 T_1) (rf T_6 T_5) (T_1 = T_5) ### DisjTree 76 74 173 % 79.58/79.84 175. (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (T_1 = T_5) (rf T_6 T_5) (rf T_2 T_1) (rf T_2 T_3) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (T_3 = T_5) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (rf T_4 T_3) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) ### All 174 % 79.58/79.84 176. (((rf T_2 T_3) /\ (rf T_2 T_5)) => (T_3 = T_5)) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (rf T_6 T_3) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_6 T_5) (T_1 = T_5) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (rf T_2 T_3) ### DisjTree 75 54 175 % 79.58/79.84 177. (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (rf T_2 T_3) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (T_1 = T_5) (rf T_6 T_5) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (rf T_6 T_3) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) ### All 176 % 79.69/79.89 178. (rinvF T_3 T_6) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (rf T_6 T_5) (T_1 = T_5) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (rf T_2 T_3) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) ### Definition-Pseudo(rinvF) 177 % 79.69/79.89 179. (((T_5 = T_3) /\ (rinvF T_5 T_6)) => (rinvF T_3 T_6)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (rf T_2 T_3) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (T_1 = T_5) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_5) ((i2003_11_14_17_19_35232) = T_3) ((i2003_11_14_17_19_35232) = T_5) ### DisjTree 72 74 178 % 79.69/79.89 180. (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) ((i2003_11_14_17_19_35232) = T_5) ((i2003_11_14_17_19_35232) = T_3) (rf T_6 T_5) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (T_1 = T_5) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (rf T_2 T_3) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) ### All 179 % 79.69/79.89 181. (((rf T_2 T_1) /\ (rf T_2 T_5)) => (T_1 = T_5)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_5) ((i2003_11_14_17_19_35232) = T_3) ((i2003_11_14_17_19_35232) = T_5) (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_1) ### DisjTree 69 68 180 % 79.69/79.89 182. (rf T_2 T_1) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) ((i2003_11_14_17_19_35232) = T_5) ((i2003_11_14_17_19_35232) = T_3) (rf T_6 T_5) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) ### All 181 % 79.69/79.89 183. (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 T_5)) => ((i2003_11_14_17_19_35232) = T_5)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_5) ((i2003_11_14_17_19_35232) = T_3) (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 (i2003_11_14_17_19_35232)) ### DisjTree 65 68 182 % 79.74/79.95 184. (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 (i2003_11_14_17_19_35232)) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) ((i2003_11_14_17_19_35232) = T_3) (rf T_6 T_5) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) ### All 183 % 79.74/79.95 185. (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 T_3)) => ((i2003_11_14_17_19_35232) = T_3)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_5) (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### DisjTree 63 64 184 % 79.74/79.95 186. (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All C, (((T_5 = T_3) /\ (rinvF T_5 C)) => (rinvF T_3 C))) (rf T_6 T_5) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) ### All 185 % 79.74/79.95 187. (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (((rf T_2 T_1) /\ (rf T_2 T_3)) => (T_1 = T_3)) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### All 186 % 79.74/79.95 188. (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_6 T_5) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (((T_4 = B) /\ (cc T_4)) => (cc B))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) ### All 187 % 79.74/79.95 189. (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All C, (((T_3 = T_5) /\ (rinvF T_3 C)) => (rinvF T_5 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_7) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### All 188 % 79.74/79.98 190. (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_6 T_5) (rf T_6 T_7) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ### All 189 % 79.74/79.98 191. ((rf T_6 T_7) /\ (-. (cc T_7))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### And 190 % 79.74/79.98 192. (Ex Y, ((rf T_6 Y) /\ (-. (cc Y)))) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_6 T_5) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ### Exists 191 % 79.74/79.98 193. ((Ex Y, ((rf T_6 Y) /\ (-. (cc Y)))) /\ (cc T_6)) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_6 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### And 192 % 79.74/79.98 194. (cd T_6) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_6 T_5) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ### Definition-Pseudo(cd) 193 % 79.81/80.02 195. (rinvF T_5 T_6) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) (cd T_6) ### Definition-Pseudo(rinvF) 194 % 79.81/80.02 196. ((rinvF T_5 T_6) /\ (cd T_6)) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ### And 195 % 79.81/80.02 197. (Ex Z, ((rinvF T_5 Z) /\ (cd Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### Exists 196 % 79.81/80.02 198. ((Ex Z, ((rinvF T_5 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_5 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_5)))) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_1) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ### ConjTree 197 % 79.81/80.02 199. (cUnsatisfiable T_5) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_1) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) ### Definition-Pseudo(cUnsatisfiable) 198 % 79.81/80.02 200. (((T_1 = T_5) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable T_5)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### DisjTree 62 26 199 % 79.81/80.06 201. (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_5) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All C, (((T_5 = T_1) /\ (rinvF T_5 C)) => (rinvF T_1 C))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 200 % 79.81/80.06 202. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_4 T_5) (All Y, (All Z, (((rf T_4 Y) /\ (rf T_4 Z)) => (Y = Z)))) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### All 201 % 79.81/80.06 203. (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (All Z, (((rf T_2 (i2003_11_14_17_19_35232)) /\ (rf T_2 Z)) => ((i2003_11_14_17_19_35232) = Z))) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 202 % 79.81/80.06 204. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_5 = B) /\ (rinvF T_5 C)) => (rinvF B C)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### All 203 % 79.81/80.06 205. (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All Z, (((rf T_2 T_3) /\ (rf T_2 Z)) => (T_3 = Z))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 204 % 79.81/80.06 206. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_4 T_5) (rf T_4 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_2 T_3) (All Z, (((rf T_2 T_1) /\ (rf T_2 Z)) => (T_1 = Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### All 205 % 79.81/80.06 207. (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_3) (All C, (((T_3 = T_1) /\ (rinvF T_3 C)) => (rinvF T_1 C))) (rf T_4 T_3) (rf T_4 T_5) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 206 % 79.87/80.08 208. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_4 T_5) (rf T_4 T_3) (rf T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### All 207 % 79.87/80.08 209. ((rf T_4 T_5) /\ (-. (cc T_5))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_3) (rf T_4 T_3) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (cc T_4) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### And 208 % 79.87/80.08 210. (Ex Y, ((rf T_4 Y) /\ (-. (cc Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (cc T_4) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_4 T_3) (rf T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### Exists 209 % 79.87/80.08 211. ((Ex Y, ((rf T_4 Y) /\ (-. (cc Y)))) /\ (cc T_4)) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_3) (rf T_4 T_3) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### And 210 % 79.87/80.08 212. (cd T_4) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_4 T_3) (rf T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### Definition-Pseudo(cd) 211 % 79.87/80.08 213. (rinvF T_3 T_4) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (cd T_4) ### Definition-Pseudo(rinvF) 212 % 79.87/80.08 214. ((rinvF T_3 T_4) /\ (cd T_4)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### And 213 % 79.87/80.08 215. (Ex Z, ((rinvF T_3 Z) /\ (cd Z))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Exists 214 % 79.87/80.08 216. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) ((Ex Z, ((rinvF T_3 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_3 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_3)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ### ConjTree 215 % 79.87/80.10 217. (cUnsatisfiable T_3) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 T_3) (rf T_2 (i2003_11_14_17_19_35232)) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Definition-Pseudo(cUnsatisfiable) 216 % 79.87/80.10 218. (((T_1 = T_3) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable T_3)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (rf T_2 (i2003_11_14_17_19_35232)) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 T_3) (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) ### DisjTree 24 26 217 % 79.87/80.10 219. (All Y, (All Z, (((rf T_2 Y) /\ (rf T_2 Z)) => (Y = Z)))) (rf T_2 T_3) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 (i2003_11_14_17_19_35232)) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 218 % 79.87/80.10 220. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All B, (((T_3 = B) /\ (cUnsatisfiable T_3)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (rf T_2 (i2003_11_14_17_19_35232)) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 T_3) ### All 219 % 79.87/80.10 221. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rf T_2 T_3) (rf T_2 T_1) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (rf T_2 (i2003_11_14_17_19_35232)) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 220 % 79.87/80.10 222. (rinvF (i2003_11_14_17_19_35232) T_2) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_1) (rf T_2 T_3) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### Definition-Pseudo(rinvF) 221 % 79.87/80.10 223. (((T_1 = (i2003_11_14_17_19_35232)) /\ (rinvF T_1 T_2)) => (rinvF (i2003_11_14_17_19_35232) T_2)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rf T_2 T_3) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_2 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### DisjTree 16 18 222 % 79.87/80.10 224. (All C, (((T_1 = (i2003_11_14_17_19_35232)) /\ (rinvF T_1 C)) => (rinvF (i2003_11_14_17_19_35232) C))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_2 T_1) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (All C, (((T_3 = B) /\ (rinvF T_3 C)) => (rinvF B C)))) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (rf T_2 T_3) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### All 223 % 79.87/80.10 225. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rf T_2 T_3) ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_2 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All C, (((T_1 = (i2003_11_14_17_19_35232)) /\ (rinvF T_1 C)) => (rinvF (i2003_11_14_17_19_35232) C))) ### All 224 % 79.87/80.10 226. (cUnsatisfiable T_1) (All C, (((T_1 = (i2003_11_14_17_19_35232)) /\ (rinvF T_1 C)) => (rinvF (i2003_11_14_17_19_35232) C))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_2 T_1) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (rf T_2 T_3) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### Definition-Pseudo(cUnsatisfiable) 225 % 79.87/80.10 227. ((((i2003_11_14_17_19_35232) = T_1) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable T_1)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rf T_2 T_3) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_2 T_1) (All C, (((T_1 = (i2003_11_14_17_19_35232)) /\ (rinvF T_1 C)) => (rinvF (i2003_11_14_17_19_35232) C))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### DisjTree 7 9 226 % 79.87/80.12 228. (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All C, (((T_1 = (i2003_11_14_17_19_35232)) /\ (rinvF T_1 C)) => (rinvF (i2003_11_14_17_19_35232) C))) (rf T_2 T_1) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (rf T_2 T_3) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### All 227 % 79.87/80.12 229. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rf T_2 T_3) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_2 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) ### All 228 % 79.87/80.12 230. ((rf T_2 T_3) /\ (-. (cc T_3))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_2 T_1) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### And 229 % 79.87/80.12 231. (Ex Y, ((rf T_2 Y) /\ (-. (cc Y)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_2 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) ### Exists 230 % 79.87/80.12 232. ((Ex Y, ((rf T_2 Y) /\ (-. (cc Y)))) /\ (cc T_2)) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_2 T_1) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### And 231 % 79.87/80.12 233. (cd T_2) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (rf T_2 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) ### Definition-Pseudo(cd) 232 % 79.87/80.12 234. (rinvF T_1 T_2) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (cd T_2) ### Definition-Pseudo(rinvF) 233 % 79.87/80.12 235. ((rinvF T_1 T_2) /\ (cd T_2)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) ### And 234 % 79.87/80.12 236. (Ex Z, ((rinvF T_1 Z) /\ (cd Z))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### Exists 235 % 79.87/80.12 237. ((Ex Z, ((rinvF T_1 Z) /\ (cd Z))) /\ ((All Y, ((rinvR T_1 Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc T_1)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) ### ConjTree 236 % 79.87/80.13 238. (cUnsatisfiable T_1) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### Definition-Pseudo(cUnsatisfiable) 237 % 79.87/80.13 239. ((((i2003_11_14_17_19_35232) = T_1) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable T_1)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### DisjTree 7 9 238 % 79.87/80.13 240. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All B, ((((i2003_11_14_17_19_35232) = B) /\ (cUnsatisfiable (i2003_11_14_17_19_35232))) => (cUnsatisfiable B))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### All 239 % 79.87/80.13 241. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All B, (((T_1 = B) /\ (cUnsatisfiable T_1)) => (cUnsatisfiable B))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 240 % 79.87/80.13 242. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) (rf T_0 T_1) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All B, (All C, (((T_1 = B) /\ (rinvF T_1 C)) => (rinvF B C)))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### All 241 % 79.87/80.13 243. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 T_1) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 242 % 79.87/80.13 244. ((rf T_0 T_1) /\ (-. (cc T_1))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### And 243 % 79.87/80.13 245. (Ex Y, ((rf T_0 Y) /\ (-. (cc Y)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Exists 244 % 79.87/80.13 246. ((Ex Y, ((rf T_0 Y) /\ (-. (cc Y)))) /\ (cc T_0)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf T_0 (i2003_11_14_17_19_35232)) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### And 245 % 79.87/80.13 247. (cd T_0) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (rf T_0 (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Definition-Pseudo(cd) 246 % 79.87/80.13 248. (rinvF (i2003_11_14_17_19_35232) T_0) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (cd T_0) ### Definition-Pseudo(rinvF) 247 % 79.87/80.13 249. ((rinvF (i2003_11_14_17_19_35232) T_0) /\ (cd T_0)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### And 248 % 79.87/80.13 250. (Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### Exists 249 % 79.87/80.13 251. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) ((Ex Y, ((rinvF (i2003_11_14_17_19_35232) Y) /\ (cd Y))) /\ ((All Y, ((rinvR (i2003_11_14_17_19_35232) Y) => (Ex Z, ((rinvF Y Z) /\ (cd Z))))) /\ (-. (cc (i2003_11_14_17_19_35232))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### ConjTree 250 % 79.87/80.13 252. (cUnsatisfiable (i2003_11_14_17_19_35232)) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rf X Y) => (rr X Y)))) (All A, (All B, (All C, (((A = B) /\ (rinvF A C)) => (rinvF B C))))) (All A, (All B, (((A = B) /\ (cc A)) => (cc B)))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### Definition-Pseudo(cUnsatisfiable) 251 % 79.87/80.13 % SZS output end Proof % 79.87/80.13 (* END-PROOF *) %------------------------------------------------------------------------------