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)))))


> 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 Var322 (e x x)))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 6
||||
||||? (p (e Var328 (e Var322 (e x x))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
|||||Step 7
|||||
|||||? (p (e Var334 (e Var328 (e Var322 (e x x)))))
|||||
|||||
|||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||||=============================
||||Step 8
||||
||||? (p (e Var322 Var343))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
|||||Step 9
|||||
|||||? (p (e Var349 (e Var322 Var343)))
|||||
|||||
|||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||||=============================
||||Step 10
||||
||||? (p (e Var359 Var358))
||||
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 11
|||
|||? (p (e (e x x) (e (e Var370 Var369) Var360)))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 12
||
||? (p (e (e x Var378) (e (e Var371 x) (e Var378 Var371))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 13
|
|? (p (e (e x y) (e y x)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 14
||
||? (p (e Var389 (e (e x y) (e y x))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 15
|
|? (p (e y y))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 16
||
||? (p (e Var402 (e y y)))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 17
|||
|||? (p (e Var408 (e Var402 (e y y))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 18
||||
||||? (p (e Var414 (e Var408 (e Var402 (e y y)))))
||||
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 19
|||
|||? (p (e Var402 Var423))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 20
||||
||||? (p (e Var429 (e Var402 Var423)))
||||
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 21
|||
|||? (p (e Var439 Var438))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 22
||
||? (p (e (e y y) (e (e Var450 Var449) Var440)))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 23
|
|? (p (e (e y Var458) (e (e Var451 y) (e Var458 Var451))))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 24

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


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 25
|
|? (p (e Var469 (e (e x y) (e (e y z) (e x z)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 26
||
||? (p (e Var475 (e Var469 (e (e x y) (e (e y z) (e x z))))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 27
|
|? (p (e (e x y) Var484))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 28

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


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 29
|
|? (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 30
||
||? (p (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 31
|||
|||? (p (e Var511 (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
||||Step 32
||||
||||? (p (e Var517 (e Var511 (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))))
||||
||||
||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||||=============================
|||Step 33
|||
|||? (p (e Var505 Var526))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 34
||
||? (p (e (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) (e (e Var537 Var535) (e Var536 Var537))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 35
|||
|||? (p (e Var543 (e (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) (e (e Var537 Var535) (e Var536 Var537)))))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 36
||
||? (p (e (e Var537 Var535) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 37
|||
|||? (p (e Var556 (e (e Var537 Var535) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 38
||
||? (p (e (e (e y z) (e x z)) Var535))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 39
|
|? (p (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 40
||
||? (p (e Var578 (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572)))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 41
|||
|||? (p (e Var584 (e Var578 (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572))))))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 42
||
||? (p (e Var536 Var593))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 43
|
|? (p (e (e (e Var572 (e x z)) (e (e y z) Var572)) (e (e Var604 Var602) (e Var603 Var604))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 44
||
||? (p (e Var610 (e (e (e Var572 (e x z)) (e (e y z) Var572)) (e (e Var604 Var602) (e Var603 Var604)))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 45
|
|? (p (e (e (e x z) Var602) (e (e y z) Var603)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 46
||
||? (p (e Var623 (e (e (e x z) Var602) (e (e y z) Var603))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 47
|
|? (p (e (e y z) Var602))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 48

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


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 49
|
|? (p (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 50
||
||? (p (e Var651 (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 51
|||
|||? (p (e Var657 (e Var651 (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 52
||
||? (p (e Var645 Var666))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 53
|
|? (p (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) (e (e Var677 Var675) (e Var676 Var677))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 54
||
||? (p (e Var683 (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) (e (e Var677 Var675) (e Var676 Var677)))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
||=============================
|||Step 55
|||
|||? (p (e Var689 (e Var683 (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) (e (e Var677 Var675) (e Var676 Var677))))))
|||
|||
|||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|||=============================
||Step 56
||
||? (p (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) Var698))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 57
|
|? (p (e (e (e Var677 Var675) (e Var676 Var677)) (e (e Var707 (e (e Var493 y) (e x Var493))) (e (e (e x z) (e (e Var639 z) (e y Var639))) Var707))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 58
||
||? (p (e Var713 (e (e (e Var677 Var675) (e Var676 Var677)) (e (e Var707 (e (e Var493 y) (e x Var493))) (e (e (e x z) (e (e Var639 z) (e y Var639))) Var707)))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 59
|
|? (p (e (e Var707 (e (e Var493 y) (e x Var493))) (e Var676 (e (e x z) (e (e Var639 z) (e y Var639))))))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 60

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


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 61
|
|? (p (e Var733 (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 62
||
||? (p (e Var739 (e Var733 (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 63
|
|? (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) Var748))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 64
||
||? (p (e Var754 (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) Var748)))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 65
|
|? (p (e Var762 (e (e Var493 y) (e x Var493))))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 66

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


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 67
|
|? (p (e Var776 (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639))))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
|=============================
||Step 68
||
||? (p (e Var782 (e Var776 (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))))
||
||
||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
||=============================
|Step 69
|
|? (p (e (e x z) Var791))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 70

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


> ((p X) <-- (p (e Y X)) (p Y))
=============================
|Step 71
|
|? (p (e Var806 (e (e (e x y) (e (e Var639 z) (e y Var639))) (e (e Var800 z) (e x Var800)))))
|
|
|> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--)
|=============================
Step 72

? (p (e (e y z) (e (e Var639 z) (e y Var639))))


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