Step 1

? (((p (e x x)) & (p (e (e x y) (e y x)))) & (p (e (e x y) (e (e y z) (e x z)))))


> ftp.revsk
=============================
Step 2

? (((p (e x x)) & (p (e (e x y) (e y x)))) & (p (e (e x y) (e (e y z) (e x z)))))


> &r
=============================
|Step 3
|
|? ((p (e x x)) & (p (e (e x y) (e y x))))
|
|
|> &r
|=============================
||Step 4
||
||? (p (e x x))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 5
|||
|||? (p (e Var420 (e x x)))
|||
|||1. (~ (p (e x x)))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 6
||||
||||? (p (e Var426 (e Var420 (e x x))))
||||
||||1. (~ (p (e Var420 (e x x))))
||||2. (~ (p (e x x)))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 7
|||
|||? (p (e x Var435))
|||
|||1. (~ (p (e (e x Var435) (e x x))))
|||2. (~ (p (e x x)))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 8
||||
||||? (p (e Var441 (e x Var435)))
||||
||||1. (~ (p (e x Var435)))
||||2. (~ (p (e (e x Var435) (e x x))))
||||3. (~ (p (e x x)))
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
|||||Step 9
|||||
|||||? (p (e Var447 (e Var441 (e x Var435))))
|||||
|||||1. (~ (p (e Var441 (e x Var435))))
|||||2. (~ (p (e x Var435)))
|||||3. (~ (p (e (e x Var435) (e x x))))
|||||4. (~ (p (e x x)))
|||||
|||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
||||||Step 10
||||||
||||||? (p (e Var453 (e Var447 (e Var441 (e x Var435)))))
||||||
||||||1. (~ (p (e Var447 (e Var441 (e x Var435)))))
||||||2. (~ (p (e Var441 (e x Var435))))
||||||3. (~ (p (e x Var435)))
||||||4. (~ (p (e (e x Var435) (e x x))))
||||||5. (~ (p (e x x)))
||||||
||||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||||=============================
|||||Step 11
|||||
|||||? (p (e Var441 Var462))
|||||
|||||1. (~ (p (e (e (e x Var435) Var462) (e Var441 (e x Var435)))))
|||||2. (~ (p (e Var441 (e x Var435))))
|||||3. (~ (p (e x Var435)))
|||||4. (~ (p (e (e x Var435) (e x x))))
|||||5. (~ (p (e x x)))
|||||
|||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
||||||Step 12
||||||
||||||? (p (e Var468 (e Var441 Var462)))
||||||
||||||1. (~ (p (e Var441 Var462)))
||||||2. (~ (p (e (e (e x Var435) Var462) (e Var441 (e x Var435)))))
||||||3. (~ (p (e Var441 (e x Var435))))
||||||4. (~ (p (e x Var435)))
||||||5. (~ (p (e (e x Var435) (e x x))))
||||||6. (~ (p (e x x)))
||||||
||||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||||=============================
|||||Step 13
|||||
|||||? (p (e Var478 Var477))
|||||
|||||1. (~ (p (e (e Var479 Var477) (e Var478 Var479))))
|||||2. (~ (p (e (e (e x Var435) (e Var478 Var479)) (e (e Var479 Var477) (e x Var435)))))
|||||3. (~ (p (e (e Var479 Var477) (e x Var435))))
|||||4. (~ (p (e x Var435)))
|||||5. (~ (p (e (e x Var435) (e x x))))
|||||6. (~ (p (e x x)))
|||||
|||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||||=============================
||||Step 14
||||
||||? (p (e (e x Var435) (e (e Var489 Var488) Var479)))
||||
||||1. (~ (p (e (e Var479 (e (e Var490 Var488) (e Var489 Var490))) (e x Var435))))
||||2. (~ (p (e x Var435)))
||||3. (~ (p (e (e x Var435) (e x x))))
||||4. (~ (p (e x x)))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 15
|||
|||? (p (e (e x Var497) (e (e Var490 Var488) (e Var497 Var490))))
|||
|||1. (~ (p (e x Var488)))
|||2. (~ (p (e (e x Var488) (e x x))))
|||3. (~ (p (e x x)))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 16
||
||? (p (e x x))
||
||1. (~ (p (e x x)))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 17
|||
|||? (p (e Var508 (e x x)))
|||
|||1. (~ (p (e x x)))
|||2. (~ (p (e x x)))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 18
||||
||||? (p (e Var514 (e Var508 (e x x))))
||||
||||1. (~ (p (e Var508 (e x x))))
||||2. (~ (p (e x x)))
||||3. (~ (p (e x x)))
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
|||||Step 19
|||||
|||||? (p (e Var520 (e Var514 (e Var508 (e x x)))))
|||||
|||||1. (~ (p (e Var514 (e Var508 (e x x)))))
|||||2. (~ (p (e Var508 (e x x))))
|||||3. (~ (p (e x x)))
|||||4. (~ (p (e x x)))
|||||
|||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||||=============================
||||Step 20
||||
||||? (p (e Var508 Var529))
||||
||||1. (~ (p (e (e (e x x) Var529) (e Var508 (e x x)))))
||||2. (~ (p (e Var508 (e x x))))
||||3. (~ (p (e x x)))
||||4. (~ (p (e x x)))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 21
|||
|||? (p (e (e x x) (e (e Var540 Var538) (e Var539 Var540))))
|||
|||1. (~ (p (e (e Var539 Var538) (e x x))))
|||2. (~ (p (e x x)))
|||3. (~ (p (e x x)))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 22
||
||? (p (e x x))
||
||1. (~ (p (e x x)))
||2. (~ (p (e x x)))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 23
|||
|||? (p (e Var551 (e x x)))
|||
|||1. (~ (p (e x x)))
|||2. (~ (p (e x x)))
|||3. (~ (p (e x x)))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 24
||||
||||? (p (e Var557 (e Var551 (e x x))))
||||
||||1. (~ (p (e Var551 (e x x))))
||||2. (~ (p (e x x)))
||||3. (~ (p (e x x)))
||||4. (~ (p (e x x)))
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
|||||Step 25
|||||
|||||? (p (e Var563 (e Var557 (e Var551 (e x x)))))
|||||
|||||1. (~ (p (e Var557 (e Var551 (e x x)))))
|||||2. (~ (p (e Var551 (e x x))))
|||||3. (~ (p (e x x)))
|||||4. (~ (p (e x x)))
|||||5. (~ (p (e x x)))
|||||
|||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||||=============================
||||Step 26
||||
||||? (p (e Var551 Var572))
||||
||||1. (~ (p (e (e (e x x) Var572) (e Var551 (e x x)))))
||||2. (~ (p (e Var551 (e x x))))
||||3. (~ (p (e x x)))
||||4. (~ (p (e x x)))
||||5. (~ (p (e x x)))
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
|||||Step 27
|||||
|||||? (p (e Var578 (e Var551 Var572)))
|||||
|||||1. (~ (p (e Var551 Var572)))
|||||2. (~ (p (e (e (e x x) Var572) (e Var551 (e x x)))))
|||||3. (~ (p (e Var551 (e x x))))
|||||4. (~ (p (e x x)))
|||||5. (~ (p (e x x)))
|||||6. (~ (p (e x x)))
|||||
|||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||||=============================
||||Step 28
||||
||||? (p (e Var588 Var587))
||||
||||1. (~ (p (e (e Var589 Var587) (e Var588 Var589))))
||||2. (~ (p (e (e (e x x) (e Var588 Var589)) (e (e Var589 Var587) (e x x)))))
||||3. (~ (p (e (e Var589 Var587) (e x x))))
||||4. (~ (p (e x x)))
||||5. (~ (p (e x x)))
||||6. (~ (p (e x x)))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 29
|||
|||? (p (e (e x x) (e (e Var599 Var598) Var589)))
|||
|||1. (~ (p (e (e Var589 (e (e Var600 Var598) (e Var599 Var600))) (e x x))))
|||2. (~ (p (e x x)))
|||3. (~ (p (e x x)))
|||4. (~ (p (e x x)))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 30
||
||? (p (e (e x Var607) (e (e Var600 x) (e Var607 Var600))))
||
||1. (~ (p (e x x)))
||2. (~ (p (e x x)))
||3. (~ (p (e x x)))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 31
|
|? (p (e (e x y) (e y x)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 32
||
||? (p (e Var618 (e (e x y) (e y x))))
||
||1. (~ (p (e (e x y) (e y x))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 33
|
|? (p (e y y))
|
|1. (~ (p (e (e x y) (e y x))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 34
||
||? (p (e Var631 (e y y)))
||
||1. (~ (p (e y y)))
||2. (~ (p (e (e x y) (e y x))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 35
|||
|||? (p (e Var637 (e Var631 (e y y))))
|||
|||1. (~ (p (e Var631 (e y y))))
|||2. (~ (p (e y y)))
|||3. (~ (p (e (e x y) (e y x))))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 36
||||
||||? (p (e Var643 (e Var637 (e Var631 (e y y)))))
||||
||||1. (~ (p (e Var637 (e Var631 (e y y)))))
||||2. (~ (p (e Var631 (e y y))))
||||3. (~ (p (e y y)))
||||4. (~ (p (e (e x y) (e y x))))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 37
|||
|||? (p (e Var631 Var652))
|||
|||1. (~ (p (e (e (e y y) Var652) (e Var631 (e y y)))))
|||2. (~ (p (e Var631 (e y y))))
|||3. (~ (p (e y y)))
|||4. (~ (p (e (e x y) (e y x))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 38
||
||? (p (e (e y y) (e (e Var663 Var661) (e Var662 Var663))))
||
||1. (~ (p (e (e Var662 Var661) (e y y))))
||2. (~ (p (e y y)))
||3. (~ (p (e (e x y) (e y x))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 39
|
|? (p (e y y))
|
|1. (~ (p (e y y)))
|2. (~ (p (e (e x y) (e y x))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 40
||
||? (p (e Var674 (e y y)))
||
||1. (~ (p (e y y)))
||2. (~ (p (e y y)))
||3. (~ (p (e (e x y) (e y x))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 41
|||
|||? (p (e Var680 (e Var674 (e y y))))
|||
|||1. (~ (p (e Var674 (e y y))))
|||2. (~ (p (e y y)))
|||3. (~ (p (e y y)))
|||4. (~ (p (e (e x y) (e y x))))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 42
||||
||||? (p (e Var686 (e Var680 (e Var674 (e y y)))))
||||
||||1. (~ (p (e Var680 (e Var674 (e y y)))))
||||2. (~ (p (e Var674 (e y y))))
||||3. (~ (p (e y y)))
||||4. (~ (p (e y y)))
||||5. (~ (p (e (e x y) (e y x))))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 43
|||
|||? (p (e Var674 Var695))
|||
|||1. (~ (p (e (e (e y y) Var695) (e Var674 (e y y)))))
|||2. (~ (p (e Var674 (e y y))))
|||3. (~ (p (e y y)))
|||4. (~ (p (e y y)))
|||5. (~ (p (e (e x y) (e y x))))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 44
||||
||||? (p (e Var701 (e Var674 Var695)))
||||
||||1. (~ (p (e Var674 Var695)))
||||2. (~ (p (e (e (e y y) Var695) (e Var674 (e y y)))))
||||3. (~ (p (e Var674 (e y y))))
||||4. (~ (p (e y y)))
||||5. (~ (p (e y y)))
||||6. (~ (p (e (e x y) (e y x))))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 45
|||
|||? (p (e Var711 Var710))
|||
|||1. (~ (p (e (e Var712 Var710) (e Var711 Var712))))
|||2. (~ (p (e (e (e y y) (e Var711 Var712)) (e (e Var712 Var710) (e y y)))))
|||3. (~ (p (e (e Var712 Var710) (e y y))))
|||4. (~ (p (e y y)))
|||5. (~ (p (e y y)))
|||6. (~ (p (e (e x y) (e y x))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 46
||
||? (p (e (e y y) (e (e Var722 Var721) Var712)))
||
||1. (~ (p (e (e Var712 (e (e Var723 Var721) (e Var722 Var723))) (e y y))))
||2. (~ (p (e y y)))
||3. (~ (p (e y y)))
||4. (~ (p (e (e x y) (e y x))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 47
|
|? (p (e (e y Var730) (e (e Var723 y) (e Var730 Var723))))
|
|1. (~ (p (e y y)))
|2. (~ (p (e y y)))
|3. (~ (p (e (e x y) (e y x))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 48

? (p (e (e x y) (e (e y z) (e x z))))


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 49
|
|? (p (e Var741 (e (e x y) (e (e y z) (e x z)))))
|
|1. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 50
||
||? (p (e Var747 (e Var741 (e (e x y) (e (e y z) (e x z))))))
||
||1. (~ (p (e Var741 (e (e x y) (e (e y z) (e x z))))))
||2. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 51
|
|? (p (e (e x y) Var756))
|
|1. (~ (p (e (e (e (e y z) (e x z)) Var756) (e (e x y) (e (e y z) (e x z))))))
|2. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 52

? (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))

1. (~ (p (e (e x y) (e (e y z) (e x z)))))

> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 53
|
|? (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|
|1. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|2. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 54
||
||? (p (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||
||1. (~ (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||2. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||3. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 55
|||
|||? (p (e Var783 (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
|||
|||1. (~ (p (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
|||2. (~ (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||4. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 56
||||
||||? (p (e Var789 (e Var783 (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))))
||||
||||1. (~ (p (e Var783 (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))))
||||2. (~ (p (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
||||3. (~ (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 57
|||
|||? (p (e Var777 Var798))
|||
|||1. (~ (p (e (e (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) Var798) (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))))
|||2. (~ (p (e Var777 (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
|||3. (~ (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 58
||
||? (p (e (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) (e (e Var809 Var807) (e Var808 Var809))))
||
||1. (~ (p (e (e Var808 Var807) (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
||2. (~ (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||4. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 59
|||
|||? (p (e Var815 (e (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) (e (e Var809 Var807) (e Var808 Var809)))))
|||
|||1. (~ (p (e (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) (e (e Var809 Var807) (e Var808 Var809)))))
|||2. (~ (p (e (e Var808 Var807) (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
|||3. (~ (p (e Var771 (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 60
||
||? (p (e (e Var809 Var807) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||
||1. (~ (p (e (e (e Var808 Var809) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) (e (e Var809 Var807) (e Var808 Var809)))))
||2. (~ (p (e (e Var808 Var807) (e (e Var808 Var809) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
||3. (~ (p (e (e Var808 Var809) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 61
|||
|||? (p (e Var828 (e (e Var809 Var807) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||
|||1. (~ (p (e (e Var809 Var807) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||2. (~ (p (e (e (e Var808 Var809) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) (e (e Var809 Var807) (e Var808 Var809)))))
|||3. (~ (p (e (e Var808 Var807) (e (e Var808 Var809) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
|||4. (~ (p (e (e Var808 Var809) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 62
||
||? (p (e (e (e y z) (e x z)) Var807))
||
||1. (~ (p (e (e (e (e Var765 y) (e x Var765)) Var807) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||2. (~ (p (e (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))) (e (e (e (e Var765 y) (e x Var765)) Var807) (e Var808 (e (e Var765 y) (e x Var765)))))))
||3. (~ (p (e (e Var808 Var807) (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))))
||4. (~ (p (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 63
|
|? (p (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844))))
|
|1. (~ (p (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|2. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|3. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 64
||
||? (p (e Var850 (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844)))))
||
||1. (~ (p (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844)))))
||2. (~ (p (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||4. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 65
|||
|||? (p (e Var856 (e Var850 (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844))))))
|||
|||1. (~ (p (e Var850 (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844))))))
|||2. (~ (p (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844)))))
|||3. (~ (p (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 66
||
||? (p (e Var808 Var865))
||
||1. (~ (p (e (e (e (e Var844 (e x z)) (e (e y z) Var844)) Var865) (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844))))))
||2. (~ (p (e Var808 (e (e Var844 (e x z)) (e (e y z) Var844)))))
||3. (~ (p (e (e Var808 (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 67
|
|? (p (e (e (e Var844 (e x z)) (e (e y z) Var844)) (e (e Var876 Var874) (e Var875 Var876))))
|
|1. (~ (p (e (e Var875 Var874) (e (e Var844 (e x z)) (e (e y z) Var844)))))
|2. (~ (p (e (e (e Var875 Var874) (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|4. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 68
||
||? (p (e Var882 (e (e (e Var844 (e x z)) (e (e y z) Var844)) (e (e Var876 Var874) (e Var875 Var876)))))
||
||1. (~ (p (e (e (e Var844 (e x z)) (e (e y z) Var844)) (e (e Var876 Var874) (e Var875 Var876)))))
||2. (~ (p (e (e Var875 Var874) (e (e Var844 (e x z)) (e (e y z) Var844)))))
||3. (~ (p (e (e (e Var875 Var874) (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 69
|
|? (p (e (e (e x z) Var874) (e (e y z) Var875)))
|
|1. (~ (p (e (e (e Var875 (e x z)) (e (e y z) Var875)) (e (e (e x z) Var874) (e Var875 (e x z))))))
|2. (~ (p (e (e Var875 Var874) (e (e Var875 (e x z)) (e (e y z) Var875)))))
|3. (~ (p (e (e (e Var875 Var874) (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 70
||
||? (p (e Var895 (e (e (e x z) Var874) (e (e y z) Var875))))
||
||1. (~ (p (e (e (e x z) Var874) (e (e y z) Var875))))
||2. (~ (p (e (e (e Var875 (e x z)) (e (e y z) Var875)) (e (e (e x z) Var874) (e Var875 (e x z))))))
||3. (~ (p (e (e Var875 Var874) (e (e Var875 (e x z)) (e (e y z) Var875)))))
||4. (~ (p (e (e (e Var875 Var874) (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 71
|
|? (p (e (e y z) Var874))
|
|1. (~ (p (e (e (e x z) Var874) (e (e y z) (e x z)))))
|2. (~ (p (e (e (e (e x z) (e x z)) (e (e y z) (e x z))) (e (e (e x z) Var874) (e (e x z) (e x z))))))
|3. (~ (p (e (e (e x z) Var874) (e (e (e x z) (e x z)) (e (e y z) (e x z))))))
|4. (~ (p (e (e (e (e x z) Var874) (e (e Var765 y) (e x Var765))) (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765))))))
|5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 72

? (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))

1. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
2. (~ (p (e (e x y) (e (e y z) (e x z)))))

> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 73
|
|? (p (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|
|1. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|2. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|3. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 74
||
||? (p (e Var923 (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
||
||1. (~ (p (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
||2. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||4. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 75
|||
|||? (p (e Var929 (e Var923 (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))))
|||
|||1. (~ (p (e Var923 (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))))
|||2. (~ (p (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
|||3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 76
||
||? (p (e Var917 Var938))
||
||1. (~ (p (e (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) Var938) (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))))
||2. (~ (p (e Var917 (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
||3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 77
|
|? (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949))))
|
|1. (~ (p (e (e Var948 Var947) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
|2. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|4. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 78
||
||? (p (e Var955 (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949)))))
||
||1. (~ (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949)))))
||2. (~ (p (e (e Var948 Var947) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
||3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 79
|||
|||? (p (e Var961 (e Var955 (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949))))))
|||
|||1. (~ (p (e Var955 (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949))))))
|||2. (~ (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949)))))
|||3. (~ (p (e (e Var948 Var947) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
|||4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 80
||
||? (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) Var970))
||
||1. (~ (p (e (e (e (e Var949 Var947) (e Var948 Var949)) Var970) (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949))))))
||2. (~ (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949)))))
||3. (~ (p (e (e Var948 Var947) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
||4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 81
|
|? (p (e (e (e Var949 Var947) (e Var948 Var949)) (e (e Var979 (e (e Var765 y) (e x Var765))) (e (e (e x z) (e (e Var911 z) (e y Var911))) Var979))))
|
|1. (~ (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949)))))
|2. (~ (p (e (e Var948 Var947) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
|3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 82
||
||? (p (e Var985 (e (e (e Var949 Var947) (e Var948 Var949)) (e (e Var979 (e (e Var765 y) (e x Var765))) (e (e (e x z) (e (e Var911 z) (e y Var911))) Var979)))))
||
||1. (~ (p (e (e (e Var949 Var947) (e Var948 Var949)) (e (e Var979 (e (e Var765 y) (e x Var765))) (e (e (e x z) (e (e Var911 z) (e y Var911))) Var979)))))
||2. (~ (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e Var949 Var947) (e Var948 Var949)))))
||3. (~ (p (e (e Var948 Var947) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
||4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 83
|
|? (p (e (e Var979 (e (e Var765 y) (e x Var765))) (e Var948 (e (e x z) (e (e Var911 z) (e y Var911))))))
|
|1. (~ (p (e (e (e (e (e x z) (e (e Var911 z) (e y Var911))) Var979) (e Var948 (e (e x z) (e (e Var911 z) (e y Var911))))) (e (e Var979 (e (e Var765 y) (e x Var765))) (e (e (e x z) (e (e Var911 z) (e y Var911))) Var979)))))
|2. (~ (p (e (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))) (e (e (e (e x z) (e (e Var911 z) (e y Var911))) Var979) (e Var948 (e (e x z) (e (e Var911 z) (e y Var911))))))))
|3. (~ (p (e (e Var948 Var979) (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765))))))
|4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 84

? (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z)))

1. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
2. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
3. (~ (p (e (e x y) (e (e y z) (e x z)))))

> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 85
|
|? (p (e Var1005 (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|
|1. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|2. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|4. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 86
||
||? (p (e Var1011 (e Var1005 (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z)))))
||
||1. (~ (p (e Var1005 (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z)))))
||2. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
||3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 87
|
|? (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) Var1020))
|
|1. (~ (p (e (e (e x z) Var1020) (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z)))))
|2. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 88
||
||? (p (e Var1026 (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) Var1020)))
||
||1. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) Var1020)))
||2. (~ (p (e (e (e x z) Var1020) (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z)))))
||3. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
||4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 89
|
|? (p (e Var1034 (e (e Var765 y) (e x Var765))))
|
|1. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e Var1034 (e (e Var911 z) (e y Var911))))))
|2. (~ (p (e (e (e x z) (e Var1034 (e (e Var911 z) (e y Var911)))) (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z)))))
|3. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 90

? (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911)))))

1. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
2. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
3. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
4. (~ (p (e (e x y) (e (e y z) (e x z)))))

> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 91
|
|? (p (e Var1048 (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
|
|1. (~ (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
|2. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 92
||
||? (p (e Var1054 (e Var1048 (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911)))))))
||
||1. (~ (p (e Var1048 (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911)))))))
||2. (~ (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
||3. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
||4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
||5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
||6. (~ (p (e (e x y) (e (e y z) (e x z)))))
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 93
|
|? (p (e (e x z) Var1063))
|
|1. (~ (p (e (e (e (e x y) (e (e Var911 z) (e y Var911))) Var1063) (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911)))))))
|2. (~ (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
|3. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 94

? (p (e (e (e x y) (e (e Var911 z) (e y Var911))) (e (e Var1072 z) (e x Var1072))))

1. (~ (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
2. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
3. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
4. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
5. (~ (p (e (e x y) (e (e y z) (e x z)))))

> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 95
|
|? (p (e Var1078 (e (e (e x y) (e (e Var911 z) (e y Var911))) (e (e Var1072 z) (e x Var1072)))))
|
|1. (~ (p (e (e (e x y) (e (e Var911 z) (e y Var911))) (e (e Var1072 z) (e x Var1072)))))
|2. (~ (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
|3. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
|4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
|5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
|6. (~ (p (e (e x y) (e (e y z) (e x z)))))
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 96

? (p (e (e y z) (e (e Var911 z) (e y Var911))))

1. (~ (p (e (e (e x y) (e (e Var911 z) (e y Var911))) (e (e y z) (e x y)))))
2. (~ (p (e (e x z) (e (e x y) (e (e Var911 z) (e y Var911))))))
3. (~ (p (e (e (e (e Var911 z) (e y Var911)) (e (e Var765 y) (e x Var765))) (e x z))))
4. (~ (p (e (e (e x z) (e (e Var911 z) (e y Var911))) (e (e Var765 y) (e x Var765)))))
5. (~ (p (e (e (e y z) (e x z)) (e (e Var765 y) (e x Var765)))))
6. (~ (p (e (e x y) (e (e y z) (e x z)))))

> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
=============================