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 Var322 (e x x))) ||| |||1. (~ (p (e x x))) ||| |||> ((p X) <-- (p (e Y X)) (p Y)) |||============================= ||||Step 6 |||| ||||? (p (e Var328 (e Var322 (e x x)))) |||| ||||1. (~ (p (e Var322 (e x x)))) ||||2. (~ (p (e x x))) |||| ||||> ((p X) <-- (p (e Y X)) (p Y)) ||||============================= |||||Step 7 ||||| |||||? (p (e Var334 (e Var328 (e Var322 (e x x))))) ||||| |||||1. (~ (p (e Var328 (e Var322 (e x x))))) |||||2. (~ (p (e Var322 (e x x)))) |||||3. (~ (p (e x x))) ||||| |||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--) |||||============================= ||||Step 8 |||| ||||? (p (e Var322 Var343)) |||| ||||1. (~ (p (e (e (e x x) Var343) (e Var322 (e x x))))) ||||2. (~ (p (e Var322 (e x x)))) ||||3. (~ (p (e x x))) |||| ||||> ((p X) <-- (p (e Y X)) (p Y)) ||||============================= |||||Step 9 ||||| |||||? (p (e Var349 (e Var322 Var343))) ||||| |||||1. (~ (p (e Var322 Var343))) |||||2. (~ (p (e (e (e x x) Var343) (e Var322 (e x x))))) |||||3. (~ (p (e Var322 (e x x)))) |||||4. (~ (p (e x x))) ||||| |||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--) |||||============================= ||||Step 10 |||| ||||? (p (e Var359 Var358)) |||| ||||1. (~ (p (e (e Var360 Var358) (e Var359 Var360)))) ||||2. (~ (p (e (e (e x x) (e Var359 Var360)) (e (e Var360 Var358) (e x x))))) ||||3. (~ (p (e (e Var360 Var358) (e x x)))) ||||4. (~ (p (e x x))) |||| ||||> ((p (e (e Y X) (e (e Z X) (e Y Z)))) <--) ||||============================= |||Step 11 ||| |||? (p (e (e x x) (e (e Var370 Var369) Var360))) ||| |||1. (~ (p (e (e Var360 (e (e Var371 Var369) (e Var370 Var371))) (e x x)))) |||2. (~ (p (e x x))) ||| |||> ((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)))) || ||1. (~ (p (e x x))) || ||> ((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)))) || ||1. (~ (p (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)) | |1. (~ (p (e (e x y) (e y x)))) | |> ((p X) <-- (p (e Y X)) (p Y)) |============================= ||Step 16 || ||? (p (e Var402 (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 17 ||| |||? (p (e Var408 (e Var402 (e y y)))) ||| |||1. (~ (p (e Var402 (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 18 |||| ||||? (p (e Var414 (e Var408 (e Var402 (e y y))))) |||| ||||1. (~ (p (e Var408 (e Var402 (e y y))))) ||||2. (~ (p (e Var402 (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 19 ||| |||? (p (e Var402 Var423)) ||| |||1. (~ (p (e (e (e y y) Var423) (e Var402 (e y y))))) |||2. (~ (p (e Var402 (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 20 |||| ||||? (p (e Var429 (e Var402 Var423))) |||| ||||1. (~ (p (e Var402 Var423))) ||||2. (~ (p (e (e (e y y) Var423) (e Var402 (e y y))))) ||||3. (~ (p (e Var402 (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 21 ||| |||? (p (e Var439 Var438)) ||| |||1. (~ (p (e (e Var440 Var438) (e Var439 Var440)))) |||2. (~ (p (e (e (e y y) (e Var439 Var440)) (e (e Var440 Var438) (e y y))))) |||3. (~ (p (e (e Var440 Var438) (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 22 || ||? (p (e (e y y) (e (e Var450 Var449) Var440))) || ||1. (~ (p (e (e Var440 (e (e Var451 Var449) (e Var450 Var451))) (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 23 | |? (p (e (e y Var458) (e (e Var451 y) (e Var458 Var451)))) | |1. (~ (p (e y y))) |2. (~ (p (e (e x y) (e y x)))) | |> ((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))))) | |1. (~ (p (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)))))) || ||1. (~ (p (e Var469 (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 27 | |? (p (e (e x y) Var484)) | |1. (~ (p (e (e (e (e y z) (e x z)) Var484) (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 28 ? (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) 1. (~ (p (e (e x y) (e (e y z) (e x z))))) > ((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))))) | |1. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |2. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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)))))) || ||1. (~ (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||2. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||3. (~ (p (e (e x y) (e (e y z) (e x z))))) || ||> ((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))))))) ||| |||1. (~ (p (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) |||2. (~ (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |||3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||4. (~ (p (e (e x y) (e (e y z) (e x z))))) ||| |||> ((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)))))))) |||| ||||1. (~ (p (e Var511 (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))))) ||||2. (~ (p (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) ||||3. (~ (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||||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 33 ||| |||? (p (e Var505 Var526)) ||| |||1. (~ (p (e (e (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) Var526) (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))))) |||2. (~ (p (e Var505 (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) |||3. (~ (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||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 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)))) || ||1. (~ (p (e (e Var536 Var535) (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) ||2. (~ (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||4. (~ (p (e (e x y) (e (e y z) (e x z))))) || ||> ((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))))) ||| |||1. (~ (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))))) |||2. (~ (p (e (e Var536 Var535) (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) |||3. (~ (p (e Var499 (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||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 36 || ||? (p (e (e Var537 Var535) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) || ||1. (~ (p (e (e (e Var536 Var537) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) (e (e Var537 Var535) (e Var536 Var537))))) ||2. (~ (p (e (e Var536 Var535) (e (e Var536 Var537) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) ||3. (~ (p (e (e Var536 Var537) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||5. (~ (p (e (e x y) (e (e y z) (e x z))))) || ||> ((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)))))) ||| |||1. (~ (p (e (e Var537 Var535) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |||2. (~ (p (e (e (e Var536 Var537) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) (e (e Var537 Var535) (e Var536 Var537))))) |||3. (~ (p (e (e Var536 Var535) (e (e Var536 Var537) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) |||4. (~ (p (e (e Var536 Var537) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||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 38 || ||? (p (e (e (e y z) (e x z)) Var535)) || ||1. (~ (p (e (e (e (e Var493 y) (e x Var493)) Var535) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||2. (~ (p (e (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))) (e (e (e (e Var493 y) (e x Var493)) Var535) (e Var536 (e (e Var493 y) (e x Var493))))))) ||3. (~ (p (e (e Var536 Var535) (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))))) ||4. (~ (p (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 39 | |? (p (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572)))) | |1. (~ (p (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |2. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |3. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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))))) || ||1. (~ (p (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572))))) ||2. (~ (p (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||4. (~ (p (e (e x y) (e (e y z) (e x z))))) || ||> ((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)))))) ||| |||1. (~ (p (e Var578 (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572)))))) |||2. (~ (p (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572))))) |||3. (~ (p (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||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 42 || ||? (p (e Var536 Var593)) || ||1. (~ (p (e (e (e (e Var572 (e x z)) (e (e y z) Var572)) Var593) (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572)))))) ||2. (~ (p (e Var536 (e (e Var572 (e x z)) (e (e y z) Var572))))) ||3. (~ (p (e (e Var536 (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 43 | |? (p (e (e (e Var572 (e x z)) (e (e y z) Var572)) (e (e Var604 Var602) (e Var603 Var604)))) | |1. (~ (p (e (e Var603 Var602) (e (e Var572 (e x z)) (e (e y z) Var572))))) |2. (~ (p (e (e (e Var603 Var602) (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |4. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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))))) || ||1. (~ (p (e (e (e Var572 (e x z)) (e (e y z) Var572)) (e (e Var604 Var602) (e Var603 Var604))))) ||2. (~ (p (e (e Var603 Var602) (e (e Var572 (e x z)) (e (e y z) Var572))))) ||3. (~ (p (e (e (e Var603 Var602) (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 45 | |? (p (e (e (e x z) Var602) (e (e y z) Var603))) | |1. (~ (p (e (e (e Var603 (e x z)) (e (e y z) Var603)) (e (e (e x z) Var602) (e Var603 (e x z)))))) |2. (~ (p (e (e Var603 Var602) (e (e Var603 (e x z)) (e (e y z) Var603))))) |3. (~ (p (e (e (e Var603 Var602) (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((p X) <-- (p (e Y X)) (p Y)) |============================= ||Step 46 || ||? (p (e Var623 (e (e (e x z) Var602) (e (e y z) Var603)))) || ||1. (~ (p (e (e (e x z) Var602) (e (e y z) Var603)))) ||2. (~ (p (e (e (e Var603 (e x z)) (e (e y z) Var603)) (e (e (e x z) Var602) (e Var603 (e x z)))))) ||3. (~ (p (e (e Var603 Var602) (e (e Var603 (e x z)) (e (e y z) Var603))))) ||4. (~ (p (e (e (e Var603 Var602) (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) ||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 47 | |? (p (e (e y z) Var602)) | |1. (~ (p (e (e (e x z) Var602) (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) Var602) (e (e x z) (e x z)))))) |3. (~ (p (e (e (e x z) Var602) (e (e (e x z) (e x z)) (e (e y z) (e x z)))))) |4. (~ (p (e (e (e (e x z) Var602) (e (e Var493 y) (e x Var493))) (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493)))))) |5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |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 48 ? (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))) 1. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) 2. (~ (p (e (e x y) (e (e y z) (e x z))))) > ((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))))) | |1. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |2. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |3. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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)))))) || ||1. (~ (p (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) ||2. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||4. (~ (p (e (e x y) (e (e y z) (e x z))))) || ||> ((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))))))) ||| |||1. (~ (p (e Var651 (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))))) |||2. (~ (p (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) |||3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||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 52 || ||? (p (e Var645 Var666)) || ||1. (~ (p (e (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) Var666) (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))))) ||2. (~ (p (e Var645 (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) ||3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 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)))) | |1. (~ (p (e (e Var676 Var675) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) |2. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |4. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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))))) || ||1. (~ (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))))) ||2. (~ (p (e (e Var676 Var675) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) ||3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||5. (~ (p (e (e x y) (e (e y z) (e x z))))) || ||> ((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)))))) ||| |||1. (~ (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)))))) |||2. (~ (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))))) |||3. (~ (p (e (e Var676 Var675) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) |||4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |||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 56 || ||? (p (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) Var698)) || ||1. (~ (p (e (e (e (e Var677 Var675) (e Var676 Var677)) Var698) (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)))))) ||2. (~ (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))))) ||3. (~ (p (e (e Var676 Var675) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) ||4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 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)))) | |1. (~ (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))))) |2. (~ (p (e (e Var676 Var675) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) |3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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))))) || ||1. (~ (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))))) ||2. (~ (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))))) ||3. (~ (p (e (e Var676 Var675) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) ||4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 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)))))) | |1. (~ (p (e (e (e (e (e x z) (e (e Var639 z) (e y Var639))) Var707) (e Var676 (e (e x z) (e (e Var639 z) (e y Var639))))) (e (e Var707 (e (e Var493 y) (e x Var493))) (e (e (e x z) (e (e Var639 z) (e y Var639))) Var707))))) |2. (~ (p (e (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))) (e (e (e (e x z) (e (e Var639 z) (e y Var639))) Var707) (e Var676 (e (e x z) (e (e Var639 z) (e y Var639)))))))) |3. (~ (p (e (e Var676 Var707) (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493)))))) |4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |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 60 ? (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z))) 1. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) 2. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) 3. (~ (p (e (e x y) (e (e y z) (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)))) | |1. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) |2. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |4. (~ (p (e (e x y) (e (e y z) (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))))) || ||1. (~ (p (e Var733 (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z))))) ||2. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) ||3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 63 | |? (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) Var748)) | |1. (~ (p (e (e (e x z) Var748) (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z))))) |2. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) |3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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))) || ||1. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) Var748))) ||2. (~ (p (e (e (e x z) Var748) (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z))))) ||3. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) ||4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 65 | |? (p (e Var762 (e (e Var493 y) (e x Var493)))) | |1. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e Var762 (e (e Var639 z) (e y Var639)))))) |2. (~ (p (e (e (e x z) (e Var762 (e (e Var639 z) (e y Var639)))) (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z))))) |3. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) |4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |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 66 ? (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639))))) 1. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) 2. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) 3. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) 4. (~ (p (e (e x y) (e (e y z) (e x z))))) > ((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)))))) | |1. (~ (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))) |2. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) |3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e x y) (e (e y z) (e x z))))) | |> ((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))))))) || ||1. (~ (p (e Var776 (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639))))))) ||2. (~ (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))) ||3. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) ||4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) ||5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) ||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 69 | |? (p (e (e x z) Var791)) | |1. (~ (p (e (e (e (e x y) (e (e Var639 z) (e y Var639))) Var791) (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639))))))) |2. (~ (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))) |3. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) |4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |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 70 ? (p (e (e (e x y) (e (e Var639 z) (e y Var639))) (e (e Var800 z) (e x Var800)))) 1. (~ (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))) 2. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) 3. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) 4. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) 5. (~ (p (e (e x y) (e (e y z) (e x z))))) > ((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))))) | |1. (~ (p (e (e (e x y) (e (e Var639 z) (e y Var639))) (e (e Var800 z) (e x Var800))))) |2. (~ (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))) |3. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) |4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) |5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) |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 y z) (e (e Var639 z) (e y Var639)))) 1. (~ (p (e (e (e x y) (e (e Var639 z) (e y Var639))) (e (e y z) (e x y))))) 2. (~ (p (e (e x z) (e (e x y) (e (e Var639 z) (e y Var639)))))) 3. (~ (p (e (e (e (e Var639 z) (e y Var639)) (e (e Var493 y) (e x Var493))) (e x z)))) 4. (~ (p (e (e (e x z) (e (e Var639 z) (e y Var639))) (e (e Var493 y) (e x Var493))))) 5. (~ (p (e (e (e y z) (e x z)) (e (e Var493 y) (e x Var493))))) 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)))) <--) =============================