%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n014.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 : Thu Jul 21 12:45:07 EDT 2022 % Result : Theorem 29.10s 29.32s % Output : Proof 29.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0. % 0.10/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n014.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.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jul 12 03:57:04 EDT 2022 % 0.12/0.33 % CPUTime : % 29.10/29.32 % SZS status Theorem % 29.10/29.32 (* PROOF-FOUND *) % 29.10/29.32 (* BEGIN-PROOF *) % 29.10/29.32 % SZS output start Proof % 29.10/29.32 1. (-. (reachable T_0 T_0)) ### Refl(reachable) % 29.10/29.32 2. (reachable T_0 T_1) (-. (reachable T_0 T_1)) ### Axiom % 29.10/29.32 3. (reachable T_0 T_1) (-. (reachable T_0 T_1)) ### Axiom % 29.10/29.32 4. (T_2 != T_2) ### Refl(=) % 29.10/29.32 5. (-. (reachable T_0 T_2)) (reachable T_1 T_2) (reachable T_0 T_1) ### Trans 3 4 % 29.10/29.32 6. (T_3 != T_3) ### Refl(=) % 29.10/29.32 7. (-. (reachable T_0 T_3)) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) ### Trans 5 6 % 29.10/29.32 8. (T_4 != T_4) ### Refl(=) % 29.10/29.32 9. (-. (reachable T_0 T_4)) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) ### Trans 7 8 % 29.10/29.32 10. (T_5 != T_5) ### Refl(=) % 29.10/29.32 11. (-. (reachable T_0 T_5)) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) ### Trans 9 10 % 29.10/29.32 12. (T_6 != T_6) ### Refl(=) % 29.10/29.32 13. (-. (reachable T_0 T_6)) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) ### Trans 11 12 % 29.10/29.32 14. (T_7 != T_7) ### Refl(=) % 29.10/29.32 15. (-. (reachable T_0 T_7)) (reachable T_6 T_7) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) ### Trans 13 14 % 29.10/29.32 16. (reachable (initial_world) T_0) (-. (reachable (initial_world) T_0)) ### Axiom % 29.10/29.32 17. (T_1 != T_1) ### Refl(=) % 29.10/29.32 18. (-. (reachable (initial_world) T_1)) (reachable T_0 T_1) (reachable (initial_world) T_0) ### Trans 16 17 % 29.10/29.32 19. (T_2 != T_2) ### Refl(=) % 29.10/29.32 20. (-. (reachable (initial_world) T_2)) (reachable T_1 T_2) (reachable (initial_world) T_0) (reachable T_0 T_1) ### Trans 18 19 % 29.10/29.32 21. (T_3 != T_3) ### Refl(=) % 29.10/29.32 22. (-. (reachable (initial_world) T_3)) (reachable T_2 T_3) (reachable T_0 T_1) (reachable (initial_world) T_0) (reachable T_1 T_2) ### Trans 20 21 % 29.10/29.32 23. (T_4 != T_4) ### Refl(=) % 29.10/29.32 24. (-. (reachable (initial_world) T_4)) (reachable T_3 T_4) (reachable T_1 T_2) (reachable (initial_world) T_0) (reachable T_0 T_1) (reachable T_2 T_3) ### Trans 22 23 % 29.10/29.32 25. (T_5 != T_5) ### Refl(=) % 29.10/29.32 26. (-. (reachable (initial_world) T_5)) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable (initial_world) T_0) (reachable T_1 T_2) (reachable T_3 T_4) ### Trans 24 25 % 29.10/29.32 27. (T_6 != T_6) ### Refl(=) % 29.10/29.32 28. (-. (reachable (initial_world) T_6)) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable (initial_world) T_0) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) ### Trans 26 27 % 29.10/29.32 29. (T_7 != T_7) ### Refl(=) % 29.10/29.32 30. (-. (reachable (initial_world) T_7)) (reachable T_6 T_7) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable (initial_world) T_0) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) ### Trans 28 29 % 29.10/29.32 31. (T_8 != T_8) ### Refl(=) % 29.10/29.32 32. (-. (reachable (initial_world) T_8)) (reachable T_7 T_8) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable (initial_world) T_0) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (reachable T_6 T_7) ### Trans 30 31 % 29.10/29.32 33. (All W, ((reachable T_8 W) => (p W))) (-. (All W, ((reachable T_8 W) => (p W)))) ### Axiom % 29.10/29.32 34. (-. ((reachable (initial_world) T_8) /\ (All W, ((reachable T_8 W) => (p W))))) (All W, ((reachable T_8 W) => (p W))) (reachable T_6 T_7) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable (initial_world) T_0) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) (reachable T_7 T_8) ### NotAnd 32 33 % 29.10/29.32 35. (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable T_7 T_8) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable (initial_world) T_0) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (reachable T_6 T_7) (All W, ((reachable T_8 W) => (p W))) ### NotExists 34 % 29.10/29.32 36. ((reachable T_7 T_8) /\ (All W, ((reachable T_8 W) => (p W)))) (reachable T_6 T_7) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable (initial_world) T_0) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) ### And 35 % 29.10/29.32 37. (Ex Z, ((reachable T_7 Z) /\ (All W, ((reachable Z W) => (p W))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable (initial_world) T_0) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (reachable T_6 T_7) ### Exists 36 % 29.10/29.32 38. ((reachable T_0 T_7) => (Ex Z, ((reachable T_7 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (reachable T_6 T_7) ### Imply 15 37 % 29.10/29.32 39. (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_6 T_7) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 38 % 29.10/29.32 40. ((reachable T_6 T_7) /\ (All W, ((reachable T_7 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) ### And 39 % 29.10/29.32 41. (Ex Z, ((reachable T_6 Z) /\ (All W, ((reachable Z W) => (p W))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 40 % 29.10/29.32 42. ((reachable T_0 T_6) => (Ex Z, ((reachable T_6 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) (reachable T_5 T_6) ### Imply 13 41 % 29.10/29.32 43. (reachable T_5 T_6) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 42 % 29.10/29.32 44. ((reachable T_5 T_6) /\ (All W, ((reachable T_6 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) ### And 43 % 29.10/29.32 45. (Ex Z, ((reachable T_5 Z) /\ (All W, ((reachable Z W) => (p W))))) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 44 % 29.10/29.32 46. ((reachable T_0 T_5) => (Ex Z, ((reachable T_5 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (reachable T_4 T_5) ### Imply 11 45 % 29.10/29.32 47. (reachable T_4 T_5) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 46 % 29.10/29.33 48. ((reachable T_4 T_5) /\ (All W, ((reachable T_5 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) ### And 47 % 29.10/29.33 49. (Ex Z, ((reachable T_4 Z) /\ (All W, ((reachable Z W) => (p W))))) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 48 % 29.10/29.33 50. ((reachable T_0 T_4) => (Ex Z, ((reachable T_4 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (reachable T_3 T_4) ### Imply 9 49 % 29.10/29.33 51. (reachable T_3 T_4) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 50 % 29.10/29.33 52. ((reachable T_3 T_4) /\ (All W, ((reachable T_4 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) ### And 51 % 29.10/29.33 53. (Ex Z, ((reachable T_3 Z) /\ (All W, ((reachable Z W) => (p W))))) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 52 % 29.10/29.33 54. ((reachable T_0 T_3) => (Ex Z, ((reachable T_3 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_1 T_2) (reachable T_0 T_1) (reachable T_2 T_3) ### Imply 7 53 % 29.10/29.33 55. (reachable T_2 T_3) (reachable T_0 T_1) (reachable T_1 T_2) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 54 % 29.10/29.33 56. ((reachable T_2 T_3) /\ (All W, ((reachable T_3 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_1 T_2) (reachable T_0 T_1) ### And 55 % 29.10/29.33 57. (Ex Z, ((reachable T_2 Z) /\ (All W, ((reachable Z W) => (p W))))) (reachable T_0 T_1) (reachable T_1 T_2) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 56 % 29.10/29.33 58. ((reachable T_0 T_2) => (Ex Z, ((reachable T_2 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_0 T_1) (reachable T_1 T_2) ### Imply 5 57 % 29.10/29.33 59. (reachable T_1 T_2) (reachable T_0 T_1) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 58 % 29.10/29.33 60. ((reachable T_1 T_2) /\ (All W, ((reachable T_2 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_0 T_1) ### And 59 % 29.10/29.33 61. (Ex Z, ((reachable T_1 Z) /\ (All W, ((reachable Z W) => (p W))))) (reachable T_0 T_1) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 60 % 29.10/29.33 62. ((reachable T_0 T_1) => (Ex Z, ((reachable T_1 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_0 T_1) ### Imply 2 61 % 29.10/29.33 63. (reachable T_0 T_1) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 62 % 29.10/29.33 64. ((reachable T_0 T_1) /\ (All W, ((reachable T_1 W) => (p W)))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) ### And 63 % 29.10/29.33 65. (Ex Z, ((reachable T_0 Z) /\ (All W, ((reachable Z W) => (p W))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### Exists 64 % 29.10/29.33 66. ((reachable T_0 T_0) => (Ex Z, ((reachable T_0 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable (initial_world) T_0) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) ### Imply 1 65 % 29.10/29.33 67. (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) (reachable (initial_world) T_0) ### All 66 % 29.10/29.33 68. ((reachable (initial_world) T_0) /\ (All Y, ((reachable T_0 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) ### And 67 % 29.10/29.33 69. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y)))))) ### Exists 68 % 29.10/29.33 70. (reachable (initial_world) T_9) (-. (reachable (initial_world) T_9)) ### Axiom % 29.10/29.33 71. (reachable (initial_world) T_9) (-. (reachable (initial_world) T_9)) ### Axiom % 29.10/29.33 72. (T_10 != T_10) ### Refl(=) % 29.10/29.33 73. (-. (reachable (initial_world) T_10)) (reachable T_9 T_10) (reachable (initial_world) T_9) ### Trans 71 72 % 29.10/29.33 74. (T_11 != T_11) ### Refl(=) % 29.10/29.33 75. (-. (reachable (initial_world) T_11)) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) ### Trans 73 74 % 29.10/29.33 76. (T_12 != T_12) ### Refl(=) % 29.10/29.33 77. (-. (reachable (initial_world) T_12)) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) ### Trans 75 76 % 29.10/29.33 78. (T_13 != T_13) ### Refl(=) % 29.10/29.33 79. (-. (reachable (initial_world) T_13)) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) ### Trans 77 78 % 29.10/29.33 80. (T_14 != T_14) ### Refl(=) % 29.10/29.33 81. (-. (reachable (initial_world) T_14)) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) ### Trans 79 80 % 29.10/29.36 82. (T_15 != T_15) ### Refl(=) % 29.10/29.36 83. (-. (reachable (initial_world) T_15)) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) ### Trans 81 82 % 29.10/29.36 84. (T_16 != T_16) ### Refl(=) % 29.10/29.36 85. (-. (reachable (initial_world) T_16)) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) ### Trans 83 84 % 29.10/29.36 86. (T_17 != T_17) ### Refl(=) % 29.10/29.36 87. (-. (reachable (initial_world) T_17)) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) ### Trans 85 86 % 29.10/29.36 88. (T_18 != T_18) ### Refl(=) % 29.10/29.36 89. (-. (reachable (initial_world) T_18)) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) ### Trans 87 88 % 29.10/29.36 90. (T_19 != T_19) ### Refl(=) % 29.10/29.36 91. (-. (reachable (initial_world) T_19)) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) ### Trans 89 90 % 29.10/29.36 92. (T_20 != T_20) ### Refl(=) % 29.10/29.36 93. (-. (reachable (initial_world) T_20)) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) ### Trans 91 92 % 29.10/29.36 94. (T_21 != T_21) ### Refl(=) % 29.10/29.36 95. (-. (reachable (initial_world) T_21)) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) ### Trans 93 94 % 29.10/29.36 96. (T_22 != T_22) ### Refl(=) % 29.10/29.36 97. (-. (reachable (initial_world) T_22)) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) ### Trans 95 96 % 29.10/29.36 98. (T_23 != T_23) ### Refl(=) % 29.10/29.36 99. (-. (reachable (initial_world) T_23)) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) ### Trans 97 98 % 29.10/29.36 100. (T_24 != T_24) ### Refl(=) % 29.10/29.36 101. (-. (reachable (initial_world) T_24)) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) ### Trans 99 100 % 29.10/29.36 102. (T_25 != T_25) ### Refl(=) % 29.10/29.36 103. (-. (reachable (initial_world) T_25)) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) ### Trans 101 102 % 29.10/29.36 104. (T_26 != T_26) ### Refl(=) % 29.10/29.36 105. (-. (reachable (initial_world) T_26)) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) ### Trans 103 104 % 29.10/29.36 106. (T_27 != T_27) ### Refl(=) % 29.10/29.36 107. (-. (reachable (initial_world) T_27)) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) ### Trans 105 106 % 29.10/29.36 108. (T_28 != T_28) ### Refl(=) % 29.10/29.36 109. (-. (reachable (initial_world) T_28)) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) ### Trans 107 108 % 29.10/29.36 110. (T_29 != T_29) ### Refl(=) % 29.10/29.36 111. (-. (reachable (initial_world) T_29)) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) ### Trans 109 110 % 29.10/29.36 112. (T_30 != T_30) ### Refl(=) % 29.10/29.36 113. (-. (reachable (initial_world) T_30)) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) ### Trans 111 112 % 29.10/29.36 114. (reachable T_25 T_26) (-. (reachable T_25 T_26)) ### Axiom % 29.10/29.36 115. (T_27 != T_27) ### Refl(=) % 29.10/29.36 116. (-. (reachable T_25 T_27)) (reachable T_26 T_27) (reachable T_25 T_26) ### Trans 114 115 % 29.10/29.36 117. (T_28 != T_28) ### Refl(=) % 29.10/29.36 118. (-. (reachable T_25 T_28)) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_26 T_27) ### Trans 116 117 % 29.10/29.36 119. (T_29 != T_29) ### Refl(=) % 29.10/29.36 120. (-. (reachable T_25 T_29)) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_25 T_26) (reachable T_27 T_28) ### Trans 118 119 % 29.10/29.36 121. (T_30 != T_30) ### Refl(=) % 29.10/29.36 122. (-. (reachable T_25 T_30)) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_26 T_27) (reachable T_28 T_29) ### Trans 120 121 % 29.10/29.36 123. (T_31 != T_31) ### Refl(=) % 29.10/29.36 124. (-. (reachable T_25 T_31)) (reachable T_30 T_31) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) ### Trans 122 123 % 29.10/29.36 125. (reachable T_9 T_10) (-. (reachable T_9 T_10)) ### Axiom % 29.10/29.36 126. (T_11 != T_11) ### Refl(=) % 29.10/29.36 127. (-. (reachable T_9 T_11)) (reachable T_10 T_11) (reachable T_9 T_10) ### Trans 125 126 % 29.10/29.36 128. (T_12 != T_12) ### Refl(=) % 29.10/29.36 129. (-. (reachable T_9 T_12)) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) ### Trans 127 128 % 29.24/29.43 130. (T_13 != T_13) ### Refl(=) % 29.24/29.43 131. (-. (reachable T_9 T_13)) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) ### Trans 129 130 % 29.24/29.43 132. (T_14 != T_14) ### Refl(=) % 29.24/29.43 133. (-. (reachable T_9 T_14)) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) ### Trans 131 132 % 29.24/29.43 134. (T_15 != T_15) ### Refl(=) % 29.24/29.43 135. (-. (reachable T_9 T_15)) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) ### Trans 133 134 % 29.24/29.43 136. (T_16 != T_16) ### Refl(=) % 29.24/29.43 137. (-. (reachable T_9 T_16)) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) ### Trans 135 136 % 29.24/29.43 138. (T_17 != T_17) ### Refl(=) % 29.24/29.43 139. (-. (reachable T_9 T_17)) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) ### Trans 137 138 % 29.24/29.43 140. (T_18 != T_18) ### Refl(=) % 29.24/29.43 141. (-. (reachable T_9 T_18)) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) ### Trans 139 140 % 29.24/29.43 142. (T_19 != T_19) ### Refl(=) % 29.24/29.43 143. (-. (reachable T_9 T_19)) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) ### Trans 141 142 % 29.24/29.43 144. (T_20 != T_20) ### Refl(=) % 29.24/29.43 145. (-. (reachable T_9 T_20)) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) ### Trans 143 144 % 29.24/29.43 146. (T_21 != T_21) ### Refl(=) % 29.24/29.43 147. (-. (reachable T_9 T_21)) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) ### Trans 145 146 % 29.24/29.43 148. (T_22 != T_22) ### Refl(=) % 29.24/29.43 149. (-. (reachable T_9 T_22)) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) ### Trans 147 148 % 29.24/29.43 150. (T_23 != T_23) ### Refl(=) % 29.24/29.43 151. (-. (reachable T_9 T_23)) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) ### Trans 149 150 % 29.24/29.43 152. (T_24 != T_24) ### Refl(=) % 29.24/29.43 153. (-. (reachable T_9 T_24)) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) ### Trans 151 152 % 29.24/29.43 154. (T_25 != T_25) ### Refl(=) % 29.24/29.43 155. (-. (reachable T_9 T_25)) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) ### Trans 153 154 % 29.24/29.43 156. (T_26 != T_26) ### Refl(=) % 29.24/29.43 157. (-. (reachable T_9 T_26)) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) ### Trans 155 156 % 29.24/29.43 158. (T_27 != T_27) ### Refl(=) % 29.24/29.43 159. (-. (reachable T_9 T_27)) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) ### Trans 157 158 % 29.24/29.43 160. (T_28 != T_28) ### Refl(=) % 29.24/29.43 161. (-. (reachable T_9 T_28)) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) ### Trans 159 160 % 29.24/29.43 162. (T_29 != T_29) ### Refl(=) % 29.24/29.43 163. (-. (reachable T_9 T_29)) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) ### Trans 161 162 % 29.24/29.43 164. (T_30 != T_30) ### Refl(=) % 29.24/29.43 165. (-. (reachable T_9 T_30)) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) ### Trans 163 164 % 29.24/29.43 166. (T_31 != T_31) ### Refl(=) % 29.24/29.43 167. (-. (reachable T_9 T_31)) (reachable T_30 T_31) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) ### Trans 165 166 % 29.24/29.43 168. (T_32 != T_32) ### Refl(=) % 29.24/29.43 169. (-. (reachable T_9 T_32)) (reachable T_31 T_32) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) (reachable T_30 T_31) ### Trans 167 168 % 29.24/29.43 170. (-. (p T_32)) (p T_32) ### Axiom % 29.24/29.43 171. ((reachable T_9 T_32) => (p T_32)) (-. (p T_32)) (reachable T_30 T_31) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) (reachable T_31 T_32) ### Imply 169 170 % 29.24/29.46 172. (All Y, ((reachable T_9 Y) => (p Y))) (reachable T_31 T_32) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) (reachable T_30 T_31) (-. (p T_32)) ### All 171 % 29.24/29.46 173. (-. ((reachable T_31 T_32) => (p T_32))) (reachable T_30 T_31) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) (All Y, ((reachable T_9 Y) => (p Y))) ### NotImply 172 % 29.24/29.46 174. (-. (All W, ((reachable T_31 W) => (p W)))) (All Y, ((reachable T_9 Y) => (p Y))) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) (reachable T_30 T_31) ### NotAllEx 173 % 29.24/29.46 175. (-. ((reachable T_25 T_31) /\ (All W, ((reachable T_31 W) => (p W))))) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (All Y, ((reachable T_9 Y) => (p Y))) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_26 T_27) (reachable T_28 T_29) (reachable T_30 T_31) ### NotAnd 124 174 % 29.24/29.46 176. (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable T_30 T_31) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) (All Y, ((reachable T_9 Y) => (p Y))) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) ### NotExists 175 % 29.24/29.46 177. (-. ((reachable T_30 T_31) => (Ex Z, ((reachable T_31 Z) /\ (All W, ((reachable Z W) => (p W))))))) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (All Y, ((reachable T_9 Y) => (p Y))) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_26 T_27) (reachable T_28 T_29) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) ### NotImply 176 % 29.24/29.46 178. (-. (All Y, ((reachable T_30 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) (All Y, ((reachable T_9 Y) => (p Y))) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) ### NotAllEx 177 % 29.24/29.46 179. (-. ((reachable (initial_world) T_30) /\ (All Y, ((reachable T_30 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (reachable T_29 T_30) ### NotAnd 113 178 % 29.24/29.46 180. (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_29 T_30) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 179 % 29.24/29.46 181. (-. ((reachable T_29 T_30) => (Ex Z, ((reachable T_30 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) ### NotImply 180 % 29.24/29.46 182. (-. (All Y, ((reachable T_29 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 181 % 29.24/29.46 183. (-. ((reachable (initial_world) T_29) /\ (All Y, ((reachable T_29 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (reachable T_28 T_29) ### NotAnd 111 182 % 29.24/29.49 184. (reachable T_28 T_29) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 183 % 29.24/29.49 185. (-. ((reachable T_28 T_29) => (Ex Z, ((reachable T_29 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) ### NotImply 184 % 29.24/29.49 186. (-. (All Y, ((reachable T_28 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 185 % 29.24/29.49 187. (-. ((reachable (initial_world) T_28) /\ (All Y, ((reachable T_28 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (reachable T_27 T_28) ### NotAnd 109 186 % 29.24/29.49 188. (reachable T_27 T_28) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 187 % 29.24/29.49 189. (-. ((reachable T_27 T_28) => (Ex Z, ((reachable T_28 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) ### NotImply 188 % 29.24/29.49 190. (-. (All Y, ((reachable T_27 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 189 % 29.24/29.49 191. (-. ((reachable (initial_world) T_27) /\ (All Y, ((reachable T_27 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (reachable T_26 T_27) ### NotAnd 107 190 % 29.24/29.49 192. (reachable T_26 T_27) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 191 % 29.24/29.49 193. (-. ((reachable T_26 T_27) => (Ex Z, ((reachable T_27 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) ### NotImply 192 % 29.33/29.52 194. (-. (All Y, ((reachable T_26 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 193 % 29.33/29.52 195. (-. ((reachable (initial_world) T_26) /\ (All Y, ((reachable T_26 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (reachable T_25 T_26) ### NotAnd 105 194 % 29.33/29.52 196. (reachable T_25 T_26) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 195 % 29.33/29.52 197. (-. ((reachable T_25 T_26) => (Ex Z, ((reachable T_26 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) ### NotImply 196 % 29.33/29.52 198. (-. (All Y, ((reachable T_25 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 197 % 29.33/29.52 199. (-. ((reachable (initial_world) T_25) /\ (All Y, ((reachable T_25 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (reachable T_24 T_25) ### NotAnd 103 198 % 29.33/29.52 200. (reachable T_24 T_25) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (-. (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W)))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 199 % 29.33/29.53 201. (-. ((reachable T_24 T_25) => (Ex Z, ((reachable T_25 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) ### NotImply 200 % 29.33/29.53 202. (-. (All Y, ((reachable T_24 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 201 % 29.33/29.53 203. (-. ((reachable (initial_world) T_24) /\ (All Y, ((reachable T_24 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (reachable T_23 T_24) ### NotAnd 101 202 % 29.33/29.53 204. (reachable T_23 T_24) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 203 % 29.33/29.53 205. (-. ((reachable T_23 T_24) => (Ex Z, ((reachable T_24 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) ### NotImply 204 % 29.33/29.56 206. (-. (All Y, ((reachable T_23 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 205 % 29.33/29.56 207. (-. ((reachable (initial_world) T_23) /\ (All Y, ((reachable T_23 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (reachable T_22 T_23) ### NotAnd 99 206 % 29.33/29.56 208. (reachable T_22 T_23) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 207 % 29.33/29.56 209. (-. ((reachable T_22 T_23) => (Ex Z, ((reachable T_23 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) ### NotImply 208 % 29.33/29.56 210. (-. (All Y, ((reachable T_22 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 209 % 29.33/29.56 211. (-. ((reachable (initial_world) T_22) /\ (All Y, ((reachable T_22 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (reachable T_21 T_22) ### NotAnd 97 210 % 29.33/29.56 212. (reachable T_21 T_22) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 211 % 29.33/29.56 213. (-. ((reachable T_21 T_22) => (Ex Z, ((reachable T_22 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) ### NotImply 212 % 29.33/29.56 214. (-. (All Y, ((reachable T_21 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 213 % 29.33/29.56 215. (-. ((reachable (initial_world) T_21) /\ (All Y, ((reachable T_21 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (reachable T_20 T_21) ### NotAnd 95 214 % 29.33/29.56 216. (reachable T_20 T_21) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 215 % 29.33/29.56 217. (-. ((reachable T_20 T_21) => (Ex Z, ((reachable T_21 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) ### NotImply 216 % 29.33/29.56 218. (-. (All Y, ((reachable T_20 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 217 % 29.41/29.59 219. (-. ((reachable (initial_world) T_20) /\ (All Y, ((reachable T_20 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (reachable T_19 T_20) ### NotAnd 93 218 % 29.41/29.59 220. (reachable T_19 T_20) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 219 % 29.41/29.59 221. (-. ((reachable T_19 T_20) => (Ex Z, ((reachable T_20 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) ### NotImply 220 % 29.41/29.59 222. (-. (All Y, ((reachable T_19 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 221 % 29.41/29.59 223. (-. ((reachable (initial_world) T_19) /\ (All Y, ((reachable T_19 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (reachable T_18 T_19) ### NotAnd 91 222 % 29.41/29.59 224. (reachable T_18 T_19) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 223 % 29.41/29.59 225. (-. ((reachable T_18 T_19) => (Ex Z, ((reachable T_19 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) ### NotImply 224 % 29.41/29.59 226. (-. (All Y, ((reachable T_18 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 225 % 29.41/29.59 227. (-. ((reachable (initial_world) T_18) /\ (All Y, ((reachable T_18 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (reachable T_17 T_18) ### NotAnd 89 226 % 29.41/29.59 228. (reachable T_17 T_18) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 227 % 29.41/29.59 229. (-. ((reachable T_17 T_18) => (Ex Z, ((reachable T_18 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) ### NotImply 228 % 29.41/29.59 230. (-. (All Y, ((reachable T_17 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 229 % 29.41/29.59 231. (-. ((reachable (initial_world) T_17) /\ (All Y, ((reachable T_17 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (reachable T_16 T_17) ### NotAnd 87 230 % 29.41/29.59 232. (reachable T_16 T_17) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 231 % 29.41/29.59 233. (-. ((reachable T_16 T_17) => (Ex Z, ((reachable T_17 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) ### NotImply 232 % 29.41/29.59 234. (-. (All Y, ((reachable T_16 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 233 % 29.41/29.61 235. (-. ((reachable (initial_world) T_16) /\ (All Y, ((reachable T_16 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (reachable T_15 T_16) ### NotAnd 85 234 % 29.41/29.61 236. (reachable T_15 T_16) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 235 % 29.41/29.61 237. (-. ((reachable T_15 T_16) => (Ex Z, ((reachable T_16 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) ### NotImply 236 % 29.41/29.61 238. (-. (All Y, ((reachable T_15 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 237 % 29.41/29.61 239. (-. ((reachable (initial_world) T_15) /\ (All Y, ((reachable T_15 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (reachable T_14 T_15) ### NotAnd 83 238 % 29.41/29.61 240. (reachable T_14 T_15) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 239 % 29.41/29.61 241. (-. ((reachable T_14 T_15) => (Ex Z, ((reachable T_15 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) ### NotImply 240 % 29.41/29.61 242. (-. (All Y, ((reachable T_14 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 241 % 29.41/29.61 243. (-. ((reachable (initial_world) T_14) /\ (All Y, ((reachable T_14 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (reachable T_13 T_14) ### NotAnd 81 242 % 29.41/29.61 244. (reachable T_13 T_14) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 243 % 29.41/29.61 245. (-. ((reachable T_13 T_14) => (Ex Z, ((reachable T_14 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) ### NotImply 244 % 29.41/29.61 246. (-. (All Y, ((reachable T_13 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 245 % 29.41/29.61 247. (-. ((reachable (initial_world) T_13) /\ (All Y, ((reachable T_13 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (reachable T_12 T_13) ### NotAnd 79 246 % 29.41/29.61 248. (reachable T_12 T_13) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 247 % 29.41/29.61 249. (-. ((reachable T_12 T_13) => (Ex Z, ((reachable T_13 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) ### NotImply 248 % 29.41/29.61 250. (-. (All Y, ((reachable T_12 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 249 % 29.41/29.61 251. (-. ((reachable (initial_world) T_12) /\ (All Y, ((reachable T_12 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (reachable T_11 T_12) ### NotAnd 77 250 % 29.41/29.61 252. (reachable T_11 T_12) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 251 % 29.41/29.61 253. (-. ((reachable T_11 T_12) => (Ex Z, ((reachable T_12 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) ### NotImply 252 % 29.41/29.62 254. (-. (All Y, ((reachable T_11 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 253 % 29.41/29.62 255. (-. ((reachable (initial_world) T_11) /\ (All Y, ((reachable T_11 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_9 T_10) (reachable (initial_world) T_9) (reachable T_10 T_11) ### NotAnd 75 254 % 29.41/29.62 256. (reachable T_10 T_11) (reachable (initial_world) T_9) (reachable T_9 T_10) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 255 % 29.41/29.62 257. (-. ((reachable T_10 T_11) => (Ex Z, ((reachable T_11 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable T_9 T_10) (reachable (initial_world) T_9) ### NotImply 256 % 29.41/29.62 258. (-. (All Y, ((reachable T_10 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable (initial_world) T_9) (reachable T_9 T_10) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 257 % 29.41/29.62 259. (-. ((reachable (initial_world) T_10) /\ (All Y, ((reachable T_10 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable (initial_world) T_9) (reachable T_9 T_10) ### NotAnd 73 258 % 29.41/29.62 260. (reachable T_9 T_10) (reachable (initial_world) T_9) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 259 % 29.41/29.62 261. (-. ((reachable T_9 T_10) => (Ex Z, ((reachable T_10 Z) /\ (All W, ((reachable Z W) => (p W))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable (initial_world) T_9) ### NotImply 260 % 29.41/29.62 262. (-. (All Y, ((reachable T_9 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))) (reachable (initial_world) T_9) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotAllEx 261 % 29.41/29.62 263. (-. ((reachable (initial_world) T_9) /\ (All Y, ((reachable T_9 Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))) (All Y, ((reachable T_9 Y) => (p Y))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (reachable (initial_world) T_9) ### NotAnd 70 262 % 29.41/29.62 264. (reachable (initial_world) T_9) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) (All Y, ((reachable T_9 Y) => (p Y))) ### NotExists 263 % 29.41/29.62 265. ((reachable (initial_world) T_9) /\ (All Y, ((reachable T_9 Y) => (p Y)))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) ### And 264 % 29.41/29.62 266. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y))))) (-. (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W)))))))))) ### Exists 265 % 29.41/29.62 267. (-. ((Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (p Y))))) <=> (Ex X, ((reachable (initial_world) X) /\ (All Y, ((reachable X Y) => (Ex Z, ((reachable Y Z) /\ (All W, ((reachable Z W) => (p W))))))))))) ### NotEquiv 69 266 % 29.41/29.62 % SZS output end Proof % 29.41/29.62 (* END-PROOF *) %------------------------------------------------------------------------------