Step 1 ? (((tpp a b) & (ec b c)) => ((dc a c) v (ec a c))) > revsk ============================= Step 2 ? (((~ (tpp a b)) v (~ (ec b c))) v ((dc a c) v (ec a c))) > assocv ============================= Step 3 ? ((~ (tpp a b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) > demodulate+revsk ============================= Step 4 ? (((~ (pp a b)) v ((~ (ec c23206 a)) v (~ (ec c23206 b)))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) > assocv ============================= Step 5 ? ((~ (pp a b)) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) > demodulate+revsk ============================= Step 6 ? (((~ (p a b)) v (p b a)) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) > assocv ============================= Step 7 ? ((~ (p a b)) v ((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))) > demodulate+revsk ============================= Step 8 ? (exists x23207 ((((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) v (c x23207 a)) & (((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) v (~ (c x23207 b))))) > eR ============================= Step 9 ? ((((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) v (c Var1630 a)) & (((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) v (~ (c Var1630 b)))) > &r ============================= |Step 10 | |? (((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) v (c Var1630 a)) | | |> assocv |============================= |Step 11 | |? ((p b a) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (c Var1630 a))) | | |> demodulate+revsk |============================= |Step 12 | |? (((~ (c c23209 b)) v (c c23209 a)) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (c Var1630 a))) | | |> assocv |============================= |Step 13 | |? ((~ (c c23209 b)) v ((c c23209 a) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (c Var1630 a)))) | | |> supp- |============================= |Step 14 | |? ((c c23209 a) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (c Var1630 a))) | |1. (c c23209 b) | |> supp+ |============================= |Step 15 | |? ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (c Var1630 a)) | |1. (~ (c c23209 a)) |2. (c c23209 b) | |> assocv |============================= |Step 16 | |? (((~ (ec c23206 a)) v (~ (ec c23206 b))) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))) | |1. (~ (c c23209 a)) |2. (c c23209 b) | |> assocv |============================= |Step 17 | |? ((~ (ec c23206 a)) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)))) | |1. (~ (c c23209 a)) |2. (c c23209 b) | |> demodulate+revsk |============================= |Step 18 | |? (((~ (c c23206 a)) v (o c23206 a)) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)))) | |1. (~ (c c23209 a)) |2. (c c23209 b) | |> assocv |============================= |Step 19 | |? ((~ (c c23206 a)) v ((o c23206 a) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))))) | |1. (~ (c c23209 a)) |2. (c c23209 b) | |> supp- |============================= |Step 20 | |? ((o c23206 a) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)))) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> demodulate+revsk |============================= |Step 21 | |? (exists x23210 ((((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))) v (p x23210 c23206)) & (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))) v (p x23210 a)))) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> eR |============================= |Step 22 | |? ((((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))) v (p Var1727 c23206)) & (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))) v (p Var1727 a))) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> &r |============================= ||Step 23 || ||? (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a))) v (p Var1727 c23206)) || ||1. (c c23206 a) ||2. (~ (c c23209 a)) ||3. (c c23209 b) || ||> assocv ||============================= ||Step 24 || ||? ((~ (ec c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206))) || ||1. (c c23206 a) ||2. (~ (c c23209 a)) ||3. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 25 || ||? (((~ (c c23206 b)) v (o c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206))) || ||1. (c c23206 a) ||2. (~ (c c23209 a)) ||3. (c c23209 b) || ||> assocv ||============================= ||Step 26 || ||? ((~ (c c23206 b)) v ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206)))) || ||1. (c c23206 a) ||2. (~ (c c23209 a)) ||3. (c c23209 b) || ||> supp- ||============================= ||Step 27 || ||? ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 28 || ||? (exists x23211 ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206)) v (p x23211 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206)) v (p x23211 b)))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> eR ||============================= ||Step 29 || ||? ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206)) v (p Var1773 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206)) v (p Var1773 b))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> &r ||============================= |||Step 30 ||| |||? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v (p Var1727 c23206)) v (p Var1773 c23206)) ||| |||1. (c c23206 b) |||2. (c c23206 a) |||3. (~ (c c23209 a)) |||4. (c c23209 b) ||| |||> assocv |||============================= |||Step 31 ||| |||? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var1630 a)) v ((p Var1727 c23206) v (p Var1773 c23206))) ||| |||1. (c c23206 b) |||2. (c c23206 a) |||3. (~ (c c23209 a)) |||4. (c c23209 b) ||| |||> assocv |||============================= |||Step 32 ||| |||? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) ||| |||1. (c c23206 b) |||2. (c c23206 a) |||3. (~ (c c23209 a)) |||4. (c c23209 b) ||| |||> assocv |||============================= |||Step 33 ||| |||? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))))) ||| |||1. (c c23206 b) |||2. (c c23206 a) |||3. (~ (c c23209 a)) |||4. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 34 ||| |||? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))))) ||| |||1. (c c23206 b) |||2. (c c23206 a) |||3. (~ (c c23209 a)) |||4. (c c23209 b) ||| |||> assocv |||============================= |||Step 35 ||| |||? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))))) ||| |||1. (c c23206 b) |||2. (c c23206 a) |||3. (~ (c c23209 a)) |||4. (c c23209 b) ||| |||> supp- |||============================= |||Step 36 ||| |||? ((o b c) v (((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 37 ||| |||? (exists x23212 (((((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) v (p x23212 b)) & ((((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) v (p x23212 c)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> eR |||============================= |||Step 38 ||| |||? (((((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) v (p Var1829 b)) & ((((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) v (p Var1829 c))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> &r |||============================= ||||Step 39 |||| ||||? ((((dc a c) v (ec a c)) v ((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) v (p Var1829 b)) |||| ||||1. (c b c) ||||2. (c c23206 b) ||||3. (c c23206 a) ||||4. (~ (c c23209 a)) ||||5. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 40 |||| ||||? (((dc a c) v (ec a c)) v (((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b))) |||| ||||1. (c b c) ||||2. (c c23206 b) ||||3. (c c23206 a) ||||4. (~ (c c23209 a)) ||||5. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 41 |||| ||||? ((dc a c) v ((ec a c) v (((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b)))) |||| ||||1. (c b c) ||||2. (c c23206 b) ||||3. (c c23206 a) ||||4. (~ (c c23209 a)) ||||5. (c c23209 b) |||| ||||> demodulate+revsk ||||============================= ||||Step 42 |||| ||||? ((~ (c a c)) v ((ec a c) v (((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b)))) |||| ||||1. (c b c) ||||2. (c c23206 b) ||||3. (c c23206 a) ||||4. (~ (c c23209 a)) ||||5. (c c23209 b) |||| ||||> supp- ||||============================= ||||Step 43 |||| ||||? ((ec a c) v (((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> demodulate+revsk ||||============================= ||||Step 44 |||| ||||? (((((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b)) v (c a c)) & ((((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b)) v (~ (o a c)))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> &r ||||============================= |||||Step 45 ||||| |||||? ((((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b)) v (c a c)) ||||| |||||1. (c a c) |||||2. (c b c) |||||3. (c c23206 b) |||||4. (c c23206 a) |||||5. (~ (c c23209 a)) |||||6. (c c23209 b) ||||| |||||> assocv |||||============================= |||||Step 46 ||||| |||||? (((c Var1630 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v ((p Var1829 b) v (c a c))) ||||| |||||1. (c a c) |||||2. (c b c) |||||3. (c c23206 b) |||||4. (c c23206 a) |||||5. (~ (c c23209 a)) |||||6. (c c23209 b) ||||| |||||> assocv |||||============================= |||||Step 47 ||||| |||||? ((c Var1630 a) v (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 b) v (c a c)))) ||||| |||||1. (c a c) |||||2. (c b c) |||||3. (c c23206 b) |||||4. (c c23206 a) |||||5. (~ (c c23209 a)) |||||6. (c c23209 b) ||||| |||||> supp+ |||||============================= |||||Step 48 ||||| |||||? (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 b) v (c a c))) ||||| |||||1. (all x23213 (~ (c x23213 a))) |||||2. (c a c) |||||3. (c b c) |||||4. (c c23206 b) |||||5. (c c23206 a) |||||6. (~ (c c23209 a)) |||||7. (c c23209 b) ||||| |||||> contradiction |||||============================= ||||Step 49 |||| ||||? ((((c Var1905 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 b)) v (~ (o a c))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 50 |||| ||||? (((c Var1905 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v ((p Var1829 b) v (~ (o a c)))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 51 |||| ||||? ((c Var1905 a) v (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 b) v (~ (o a c))))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> supp+ ||||============================= ||||Step 52 |||| ||||? (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 b) v (~ (o a c)))) |||| ||||1. (all x23214 (~ (c x23214 a))) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23209 a)) ||||7. (c c23209 b) |||| ||||> contradiction ||||============================= |||Step 53 ||| |||? ((((dc a c) v (ec a c)) v ((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206)))) v (p Var1829 c)) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> assocv |||============================= |||Step 54 ||| |||? (((dc a c) v (ec a c)) v (((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> assocv |||============================= |||Step 55 ||| |||? ((dc a c) v ((ec a c) v (((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 56 ||| |||? ((~ (c a c)) v ((ec a c) v (((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> supp- |||============================= |||Step 57 ||| |||? ((ec a c) v (((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 58 ||| |||? (((((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c)) v (c a c)) & ((((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c)) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> &r |||============================= ||||Step 59 |||| ||||? ((((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c)) v (c a c)) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 60 |||| ||||? (((c Var1941 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v ((p Var1829 c) v (c a c))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 61 |||| ||||? ((c Var1941 a) v (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 c) v (c a c)))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> supp+ ||||============================= ||||Step 62 |||| ||||? (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 c) v (c a c))) |||| ||||1. (all x23215 (~ (c x23215 a))) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23209 a)) ||||7. (c c23209 b) |||| ||||> contradiction ||||============================= |||Step 63 ||| |||? ((((c Var2017 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v (p Var1829 c)) v (~ (o a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 64 ||| |||? (((c Var2017 a) v ((p Var1727 c23206) v (p Var1773 c23206))) v ((p Var1829 c) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 65 ||| |||? ((c Var2017 a) v (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 c) v (~ (o a c))))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> supp+ |||============================= |||Step 66 ||| |||? (((p Var1727 c23206) v (p Var1773 c23206)) v ((p Var1829 c) v (~ (o a c)))) ||| |||1. (all x23216 (~ (c x23216 a))) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23209 a)) |||7. (c c23209 b) ||| |||> contradiction |||============================= ||Step 67 || ||? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2053 a)) v (p Var1727 c23206)) v (p Var1773 b)) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 68 || ||? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2053 a)) v ((p Var1727 c23206) v (p Var1773 b))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 69 || ||? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 70 || ||? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 71 || ||? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 72 || ||? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> supp- ||============================= ||Step 73 || ||? ((o b c) v (((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 74 || ||? (exists x23217 (((((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))) v (p x23217 b)) & ((((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))) v (p x23217 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> eR ||============================= ||Step 75 || ||? (((((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))) v (p Var2109 b)) & ((((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))) v (p Var2109 c))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> &r ||============================= |||Step 76 ||| |||? ((((dc a c) v (ec a c)) v ((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b)))) v (p Var2109 b)) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> assocv |||============================= |||Step 77 ||| |||? (((dc a c) v (ec a c)) v (((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> assocv |||============================= |||Step 78 ||| |||? ((dc a c) v ((ec a c) v (((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 79 ||| |||? ((~ (c a c)) v ((ec a c) v (((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> supp- |||============================= |||Step 80 ||| |||? ((ec a c) v (((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 81 ||| |||? (((((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b)) v (c a c)) & ((((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b)) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> &r |||============================= ||||Step 82 |||| ||||? ((((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b)) v (c a c)) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 83 |||| ||||? (((c Var2053 a) v ((p Var1727 c23206) v (p Var1773 b))) v ((p Var2109 b) v (c a c))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 84 |||| ||||? ((c Var2053 a) v (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 b) v (c a c)))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> supp+ ||||============================= ||||Step 85 |||| ||||? (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 b) v (c a c))) |||| ||||1. (all x23218 (~ (c x23218 a))) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23209 a)) ||||7. (c c23209 b) |||| ||||> contradiction ||||============================= |||Step 86 ||| |||? ((((c Var2185 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 b)) v (~ (o a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 87 ||| |||? (((c Var2185 a) v ((p Var1727 c23206) v (p Var1773 b))) v ((p Var2109 b) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 88 ||| |||? ((c Var2185 a) v (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 b) v (~ (o a c))))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> supp+ |||============================= |||Step 89 ||| |||? (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 b) v (~ (o a c)))) ||| |||1. (all x23219 (~ (c x23219 a))) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23209 a)) |||7. (c c23209 b) ||| |||> contradiction |||============================= ||Step 90 || ||? ((((dc a c) v (ec a c)) v ((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b)))) v (p Var2109 c)) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> assocv ||============================= ||Step 91 || ||? (((dc a c) v (ec a c)) v (((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> assocv ||============================= ||Step 92 || ||? ((dc a c) v ((ec a c) v (((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 93 || ||? ((~ (c a c)) v ((ec a c) v (((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> supp- ||============================= ||Step 94 || ||? ((ec a c) v (((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 95 || ||? (((((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c)) v (c a c)) & ((((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c)) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> &r ||============================= |||Step 96 ||| |||? ((((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c)) v (c a c)) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 97 ||| |||? (((c Var2221 a) v ((p Var1727 c23206) v (p Var1773 b))) v ((p Var2109 c) v (c a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 98 ||| |||? ((c Var2221 a) v (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 c) v (c a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> supp+ |||============================= |||Step 99 ||| |||? (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 c) v (c a c))) ||| |||1. (all x23220 (~ (c x23220 a))) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23209 a)) |||7. (c c23209 b) ||| |||> contradiction |||============================= ||Step 100 || ||? ((((c Var2297 a) v ((p Var1727 c23206) v (p Var1773 b))) v (p Var2109 c)) v (~ (o a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 101 || ||? (((c Var2297 a) v ((p Var1727 c23206) v (p Var1773 b))) v ((p Var2109 c) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 102 || ||? ((c Var2297 a) v (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 c) v (~ (o a c))))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> supp+ ||============================= ||Step 103 || ||? (((p Var1727 c23206) v (p Var1773 b)) v ((p Var2109 c) v (~ (o a c)))) || ||1. (all x23221 (~ (c x23221 a))) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23209 a)) ||7. (c c23209 b) || ||> contradiction ||============================= |Step 104 | |? (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a))) v (p Var1727 a)) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> assocv |============================= |Step 105 | |? ((~ (ec c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a))) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> demodulate+revsk |============================= |Step 106 | |? (((~ (c c23206 b)) v (o c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a))) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> assocv |============================= |Step 107 | |? ((~ (c c23206 b)) v ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a)))) | |1. (c c23206 a) |2. (~ (c c23209 a)) |3. (c c23209 b) | |> supp- |============================= |Step 108 | |? ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> demodulate+revsk |============================= |Step 109 | |? (exists x23222 ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a)) v (p x23222 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a)) v (p x23222 b)))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> eR |============================= |Step 110 | |? ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a)) v (p Var2379 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a)) v (p Var2379 b))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> &r |============================= ||Step 111 || ||? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v (p Var1727 a)) v (p Var2379 c23206)) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 112 || ||? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2333 a)) v ((p Var1727 a) v (p Var2379 c23206))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 113 || ||? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 114 || ||? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 115 || ||? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> assocv ||============================= ||Step 116 || ||? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23209 a)) ||4. (c c23209 b) || ||> supp- ||============================= ||Step 117 || ||? ((o b c) v (((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 118 || ||? (exists x23223 (((((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))) v (p x23223 b)) & ((((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))) v (p x23223 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> eR ||============================= ||Step 119 || ||? (((((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))) v (p Var2435 b)) & ((((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))) v (p Var2435 c))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> &r ||============================= |||Step 120 ||| |||? ((((dc a c) v (ec a c)) v ((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206)))) v (p Var2435 b)) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> assocv |||============================= |||Step 121 ||| |||? (((dc a c) v (ec a c)) v (((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> assocv |||============================= |||Step 122 ||| |||? ((dc a c) v ((ec a c) v (((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 123 ||| |||? ((~ (c a c)) v ((ec a c) v (((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23209 a)) |||5. (c c23209 b) ||| |||> supp- |||============================= |||Step 124 ||| |||? ((ec a c) v (((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> demodulate+revsk |||============================= |||Step 125 ||| |||? (((((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b)) v (c a c)) & ((((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b)) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> &r |||============================= ||||Step 126 |||| ||||? ((((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b)) v (c a c)) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 127 |||| ||||? (((c Var2333 a) v ((p Var1727 a) v (p Var2379 c23206))) v ((p Var2435 b) v (c a c))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> assocv ||||============================= ||||Step 128 |||| ||||? ((c Var2333 a) v (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 b) v (c a c)))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23209 a)) ||||6. (c c23209 b) |||| ||||> supp+ ||||============================= ||||Step 129 |||| ||||? (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 b) v (c a c))) |||| ||||1. (all x23224 (~ (c x23224 a))) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23209 a)) ||||7. (c c23209 b) |||| ||||> contradiction ||||============================= |||Step 130 ||| |||? ((((c Var2511 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 b)) v (~ (o a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 131 ||| |||? (((c Var2511 a) v ((p Var1727 a) v (p Var2379 c23206))) v ((p Var2435 b) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 132 ||| |||? ((c Var2511 a) v (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 b) v (~ (o a c))))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> supp+ |||============================= |||Step 133 ||| |||? (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 b) v (~ (o a c)))) ||| |||1. (all x23225 (~ (c x23225 a))) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23209 a)) |||7. (c c23209 b) ||| |||> contradiction |||============================= ||Step 134 || ||? ((((dc a c) v (ec a c)) v ((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206)))) v (p Var2435 c)) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> assocv ||============================= ||Step 135 || ||? (((dc a c) v (ec a c)) v (((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> assocv ||============================= ||Step 136 || ||? ((dc a c) v ((ec a c) v (((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 137 || ||? ((~ (c a c)) v ((ec a c) v (((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> supp- ||============================= ||Step 138 || ||? ((ec a c) v (((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 139 || ||? (((((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c)) v (c a c)) & ((((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c)) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> &r ||============================= |||Step 140 ||| |||? ((((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c)) v (c a c)) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 141 ||| |||? (((c Var2547 a) v ((p Var1727 a) v (p Var2379 c23206))) v ((p Var2435 c) v (c a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 142 ||| |||? ((c Var2547 a) v (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 c) v (c a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> supp+ |||============================= |||Step 143 ||| |||? (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 c) v (c a c))) ||| |||1. (all x23226 (~ (c x23226 a))) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23209 a)) |||7. (c c23209 b) ||| |||> contradiction |||============================= ||Step 144 || ||? ((((c Var2623 a) v ((p Var1727 a) v (p Var2379 c23206))) v (p Var2435 c)) v (~ (o a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 145 || ||? (((c Var2623 a) v ((p Var1727 a) v (p Var2379 c23206))) v ((p Var2435 c) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 146 || ||? ((c Var2623 a) v (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 c) v (~ (o a c))))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> supp+ ||============================= ||Step 147 || ||? (((p Var1727 a) v (p Var2379 c23206)) v ((p Var2435 c) v (~ (o a c)))) || ||1. (all x23227 (~ (c x23227 a))) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23209 a)) ||7. (c c23209 b) || ||> contradiction ||============================= |Step 148 | |? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2659 a)) v (p Var1727 a)) v (p Var2379 b)) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> assocv |============================= |Step 149 | |? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (c Var2659 a)) v ((p Var1727 a) v (p Var2379 b))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> assocv |============================= |Step 150 | |? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> assocv |============================= |Step 151 | |? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> demodulate+revsk |============================= |Step 152 | |? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> assocv |============================= |Step 153 | |? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23209 a)) |4. (c c23209 b) | |> supp- |============================= |Step 154 | |? ((o b c) v (((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> demodulate+revsk |============================= |Step 155 | |? (exists x23228 (((((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))) v (p x23228 b)) & ((((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))) v (p x23228 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> eR |============================= |Step 156 | |? (((((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))) v (p Var2715 b)) & ((((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))) v (p Var2715 c))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> &r |============================= ||Step 157 || ||? ((((dc a c) v (ec a c)) v ((c Var2659 a) v ((p Var1727 a) v (p Var2379 b)))) v (p Var2715 b)) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> assocv ||============================= ||Step 158 || ||? (((dc a c) v (ec a c)) v (((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> assocv ||============================= ||Step 159 || ||? ((dc a c) v ((ec a c) v (((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 160 || ||? ((~ (c a c)) v ((ec a c) v (((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23209 a)) ||5. (c c23209 b) || ||> supp- ||============================= ||Step 161 || ||? ((ec a c) v (((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> demodulate+revsk ||============================= ||Step 162 || ||? (((((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b)) v (c a c)) & ((((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b)) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> &r ||============================= |||Step 163 ||| |||? ((((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b)) v (c a c)) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 164 ||| |||? (((c Var2659 a) v ((p Var1727 a) v (p Var2379 b))) v ((p Var2715 b) v (c a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> assocv |||============================= |||Step 165 ||| |||? ((c Var2659 a) v (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 b) v (c a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23209 a)) |||6. (c c23209 b) ||| |||> supp+ |||============================= |||Step 166 ||| |||? (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 b) v (c a c))) ||| |||1. (all x23229 (~ (c x23229 a))) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23209 a)) |||7. (c c23209 b) ||| |||> contradiction |||============================= ||Step 167 || ||? ((((c Var2791 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 b)) v (~ (o a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 168 || ||? (((c Var2791 a) v ((p Var1727 a) v (p Var2379 b))) v ((p Var2715 b) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 169 || ||? ((c Var2791 a) v (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 b) v (~ (o a c))))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> supp+ ||============================= ||Step 170 || ||? (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 b) v (~ (o a c)))) || ||1. (all x23230 (~ (c x23230 a))) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23209 a)) ||7. (c c23209 b) || ||> contradiction ||============================= |Step 171 | |? ((((dc a c) v (ec a c)) v ((c Var2827 a) v ((p Var1727 a) v (p Var2379 b)))) v (p Var2715 c)) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> assocv |============================= |Step 172 | |? (((dc a c) v (ec a c)) v (((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> assocv |============================= |Step 173 | |? ((dc a c) v ((ec a c) v (((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> demodulate+revsk |============================= |Step 174 | |? ((~ (c a c)) v ((ec a c) v (((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23209 a)) |5. (c c23209 b) | |> supp- |============================= |Step 175 | |? ((ec a c) v (((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23209 a)) |6. (c c23209 b) | |> demodulate+revsk |============================= |Step 176 | |? (((((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c)) v (c a c)) & ((((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c)) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23209 a)) |6. (c c23209 b) | |> &r |============================= ||Step 177 || ||? ((((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c)) v (c a c)) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 178 || ||? (((c Var2827 a) v ((p Var1727 a) v (p Var2379 b))) v ((p Var2715 c) v (c a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> assocv ||============================= ||Step 179 || ||? ((c Var2827 a) v (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 c) v (c a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23209 a)) ||6. (c c23209 b) || ||> supp+ ||============================= ||Step 180 || ||? (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 c) v (c a c))) || ||1. (all x23231 (~ (c x23231 a))) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23209 a)) ||7. (c c23209 b) || ||> contradiction ||============================= |Step 181 | |? ((((c Var2903 a) v ((p Var1727 a) v (p Var2379 b))) v (p Var2715 c)) v (~ (o a c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23209 a)) |6. (c c23209 b) | |> assocv |============================= |Step 182 | |? (((c Var2903 a) v ((p Var1727 a) v (p Var2379 b))) v ((p Var2715 c) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23209 a)) |6. (c c23209 b) | |> assocv |============================= |Step 183 | |? ((c Var2903 a) v (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 c) v (~ (o a c))))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23209 a)) |6. (c c23209 b) | |> supp+ |============================= |Step 184 | |? (((p Var1727 a) v (p Var2379 b)) v ((p Var2715 c) v (~ (o a c)))) | |1. (all x23232 (~ (c x23232 a))) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23209 a)) |7. (c c23209 b) | |> contradiction |============================= Step 185 ? (((p b a) v (((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) v (~ (c Var2939 b))) > assocv ============================= Step 186 ? ((p b a) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (~ (c Var2939 b)))) > demodulate+revsk ============================= Step 187 ? (((~ (c c23234 b)) v (c c23234 a)) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (~ (c Var2939 b)))) > assocv ============================= Step 188 ? ((~ (c c23234 b)) v ((c c23234 a) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (~ (c Var2939 b))))) > supp- ============================= Step 189 ? ((c c23234 a) v ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (~ (c Var2939 b)))) 1. (c c23234 b) > supp+ ============================= Step 190 ? ((((~ (ec c23206 a)) v (~ (ec c23206 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))) v (~ (c Var2939 b))) 1. (~ (c c23234 a)) 2. (c c23234 b) > assocv ============================= Step 191 ? (((~ (ec c23206 a)) v (~ (ec c23206 b))) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))) 1. (~ (c c23234 a)) 2. (c c23234 b) > assocv ============================= Step 192 ? ((~ (ec c23206 a)) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))))) 1. (~ (c c23234 a)) 2. (c c23234 b) > demodulate+revsk ============================= Step 193 ? (((~ (c c23206 a)) v (o c23206 a)) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))))) 1. (~ (c c23234 a)) 2. (c c23234 b) > assocv ============================= Step 194 ? ((~ (c c23206 a)) v ((o c23206 a) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))))) 1. (~ (c c23234 a)) 2. (c c23234 b) > supp- ============================= Step 195 ? ((o c23206 a) v ((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))))) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > demodulate+revsk ============================= Step 196 ? (exists x23235 ((((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))) v (p x23235 c23206)) & (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))) v (p x23235 a)))) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > eR ============================= Step 197 ? ((((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))) v (p Var3036 c23206)) & (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))) v (p Var3036 a))) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > &r ============================= |Step 198 | |? (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b)))) v (p Var3036 c23206)) | |1. (c c23206 a) |2. (~ (c c23234 a)) |3. (c c23234 b) | |> assocv |============================= |Step 199 | |? ((~ (ec c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206))) | |1. (c c23206 a) |2. (~ (c c23234 a)) |3. (c c23234 b) | |> demodulate+revsk |============================= |Step 200 | |? (((~ (c c23206 b)) v (o c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206))) | |1. (c c23206 a) |2. (~ (c c23234 a)) |3. (c c23234 b) | |> assocv |============================= |Step 201 | |? ((~ (c c23206 b)) v ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206)))) | |1. (c c23206 a) |2. (~ (c c23234 a)) |3. (c c23234 b) | |> supp- |============================= |Step 202 | |? ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> demodulate+revsk |============================= |Step 203 | |? (exists x23236 ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206)) v (p x23236 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206)) v (p x23236 b)))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> eR |============================= |Step 204 | |? ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206)) v (p Var3082 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206)) v (p Var3082 b))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> &r |============================= ||Step 205 || ||? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v (p Var3036 c23206)) v (p Var3082 c23206)) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23234 a)) ||4. (c c23234 b) || ||> assocv ||============================= ||Step 206 || ||? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var2939 b))) v ((p Var3036 c23206) v (p Var3082 c23206))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23234 a)) ||4. (c c23234 b) || ||> assocv ||============================= ||Step 207 || ||? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23234 a)) ||4. (c c23234 b) || ||> assocv ||============================= ||Step 208 || ||? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23234 a)) ||4. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 209 || ||? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23234 a)) ||4. (c c23234 b) || ||> assocv ||============================= ||Step 210 || ||? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))))) || ||1. (c c23206 b) ||2. (c c23206 a) ||3. (~ (c c23234 a)) ||4. (c c23234 b) || ||> supp- ||============================= ||Step 211 || ||? ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 212 || ||? (exists x23237 (((((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))) v (p x23237 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))) v (p x23237 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> eR ||============================= ||Step 213 || ||? (((((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))) v (p Var3138 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))) v (p Var3138 c))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> &r ||============================= |||Step 214 ||| |||? ((((dc a c) v (ec a c)) v ((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206)))) v (p Var3138 b)) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23234 a)) |||5. (c c23234 b) ||| |||> assocv |||============================= |||Step 215 ||| |||? (((dc a c) v (ec a c)) v (((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23234 a)) |||5. (c c23234 b) ||| |||> assocv |||============================= |||Step 216 ||| |||? ((dc a c) v ((ec a c) v (((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23234 a)) |||5. (c c23234 b) ||| |||> demodulate+revsk |||============================= |||Step 217 ||| |||? ((~ (c a c)) v ((ec a c) v (((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b)))) ||| |||1. (c b c) |||2. (c c23206 b) |||3. (c c23206 a) |||4. (~ (c c23234 a)) |||5. (c c23234 b) ||| |||> supp- |||============================= |||Step 218 ||| |||? ((ec a c) v (((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> demodulate+revsk |||============================= |||Step 219 ||| |||? (((((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b)) v (c a c)) & ((((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b)) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> &r |||============================= ||||Step 220 |||| ||||? ((((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v (p Var3138 b)) v (c a c)) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23234 a)) ||||6. (c c23234 b) |||| ||||> assocv ||||============================= ||||Step 221 |||| ||||? (((~ (c Var2939 b)) v ((p Var3036 c23206) v (p Var3082 c23206))) v ((p Var3138 b) v (c a c))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23234 a)) ||||6. (c c23234 b) |||| ||||> assocv ||||============================= ||||Step 222 |||| ||||? ((~ (c Var2939 b)) v (((p Var3036 c23206) v (p Var3082 c23206)) v ((p Var3138 b) v (c a c)))) |||| ||||1. (c a c) ||||2. (c b c) ||||3. (c c23206 b) ||||4. (c c23206 a) ||||5. (~ (c c23234 a)) ||||6. (c c23234 b) |||| ||||> supp- ||||============================= ||||Step 223 |||| ||||? (((p Var3036 c23206) v (p Var3082 c23206)) v ((p Var3138 b) v (c a c))) |||| ||||1. (all x23238 (c x23238 b)) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23234 a)) ||||7. (c c23234 b) |||| ||||> assocv ||||============================= ||||Step 224 |||| ||||? ((p Var3036 c23206) v ((p Var3082 c23206) v ((p Var3138 b) v (c a c)))) |||| ||||1. (all x23238 (c x23238 b)) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23234 a)) ||||7. (c c23234 b) |||| ||||> demodulate+revsk ||||============================= ||||Step 225 |||| ||||? (((~ (c c23240 Var3036)) v (c c23240 c23206)) v ((p Var3082 c23206) v ((p Var3138 b) v (c a c)))) |||| ||||1. (all x23238 (c x23238 b)) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23234 a)) ||||7. (c c23234 b) |||| ||||> assocv ||||============================= ||||Step 226 |||| ||||? ((~ (c c23240 Var3036)) v ((c c23240 c23206) v ((p Var3082 c23206) v ((p Var3138 b) v (c a c))))) |||| ||||1. (all x23238 (c x23238 b)) ||||2. (c a c) ||||3. (c b c) ||||4. (c c23206 b) ||||5. (c c23206 a) ||||6. (~ (c c23234 a)) ||||7. (c c23234 b) |||| ||||> supp- ||||============================= ||||Step 227 |||| ||||? ((c c23240 c23206) v ((p Var3082 c23206) v ((p Var3138 b) v (c a c)))) |||| ||||1. (all x23241 (c c23240 x23241)) ||||2. (all x23238 (c x23238 b)) ||||3. (c a c) ||||4. (c b c) ||||5. (c c23206 b) ||||6. (c c23206 a) ||||7. (~ (c c23234 a)) ||||8. (c c23234 b) |||| ||||> supp+ ||||============================= ||||Step 228 |||| ||||? ((p Var3082 c23206) v ((p Var3138 b) v (c a c))) |||| ||||1. (~ (c c23240 c23206)) ||||2. (all x23241 (c c23240 x23241)) ||||3. (all x23238 (c x23238 b)) ||||4. (c a c) ||||5. (c b c) ||||6. (c c23206 b) ||||7. (c c23206 a) ||||8. (~ (c c23234 a)) ||||9. (c c23234 b) |||| ||||> contradiction ||||============================= |||Step 229 ||| |||? ((((~ (c Var3210 b)) v ((p Var3242 c23206) v (p Var3082 c23206))) v (p Var3138 b)) v (~ (o a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 230 ||| |||? (((~ (c Var3210 b)) v ((p Var3242 c23206) v (p Var3082 c23206))) v ((p Var3138 b) v (~ (o a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 231 ||| |||? ((~ (c Var3210 b)) v (((p Var3242 c23206) v (p Var3082 c23206)) v ((p Var3138 b) v (~ (o a c))))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> supp- |||============================= |||Step 232 ||| |||? (((p Var3242 c23206) v (p Var3082 c23206)) v ((p Var3138 b) v (~ (o a c)))) ||| |||1. (all x23242 (c x23242 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 233 ||| |||? ((p Var3242 c23206) v ((p Var3082 c23206) v ((p Var3138 b) v (~ (o a c))))) ||| |||1. (all x23242 (c x23242 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> demodulate+revsk |||============================= |||Step 234 ||| |||? (((~ (c c23244 Var3242)) v (c c23244 c23206)) v ((p Var3082 c23206) v ((p Var3138 b) v (~ (o a c))))) ||| |||1. (all x23242 (c x23242 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 235 ||| |||? ((~ (c c23244 Var3242)) v ((c c23244 c23206) v ((p Var3082 c23206) v ((p Var3138 b) v (~ (o a c)))))) ||| |||1. (all x23242 (c x23242 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> supp- |||============================= |||Step 236 ||| |||? ((c c23244 c23206) v ((p Var3082 c23206) v ((p Var3138 b) v (~ (o a c))))) ||| |||1. (all x23245 (c c23244 x23245)) |||2. (all x23242 (c x23242 b)) |||3. (c a c) |||4. (c b c) |||5. (c c23206 b) |||6. (c c23206 a) |||7. (~ (c c23234 a)) |||8. (c c23234 b) ||| |||> supp+ |||============================= |||Step 237 ||| |||? ((p Var3082 c23206) v ((p Var3138 b) v (~ (o a c)))) ||| |||1. (~ (c c23244 c23206)) |||2. (all x23245 (c c23244 x23245)) |||3. (all x23242 (c x23242 b)) |||4. (c a c) |||5. (c b c) |||6. (c c23206 b) |||7. (c c23206 a) |||8. (~ (c c23234 a)) |||9. (c c23234 b) ||| |||> contradiction |||============================= ||Step 238 || ||? ((((dc a c) v (ec a c)) v ((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206)))) v (p Var3138 c)) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> assocv ||============================= ||Step 239 || ||? (((dc a c) v (ec a c)) v (((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> assocv ||============================= ||Step 240 || ||? ((dc a c) v ((ec a c) v (((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 241 || ||? ((~ (c a c)) v ((ec a c) v (((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> supp- ||============================= ||Step 242 || ||? ((ec a c) v (((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 243 || ||? (((((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c)) v (c a c)) & ((((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c)) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> &r ||============================= |||Step 244 ||| |||? ((((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v (p Var3138 c)) v (c a c)) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 245 ||| |||? (((~ (c Var3288 b)) v ((p Var3320 c23206) v (p Var3082 c23206))) v ((p Var3138 c) v (c a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 246 ||| |||? ((~ (c Var3288 b)) v (((p Var3320 c23206) v (p Var3082 c23206)) v ((p Var3138 c) v (c a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> supp- |||============================= |||Step 247 ||| |||? (((p Var3320 c23206) v (p Var3082 c23206)) v ((p Var3138 c) v (c a c))) ||| |||1. (all x23246 (c x23246 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 248 ||| |||? ((p Var3320 c23206) v ((p Var3082 c23206) v ((p Var3138 c) v (c a c)))) ||| |||1. (all x23246 (c x23246 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> demodulate+revsk |||============================= |||Step 249 ||| |||? (((~ (c c23248 Var3320)) v (c c23248 c23206)) v ((p Var3082 c23206) v ((p Var3138 c) v (c a c)))) ||| |||1. (all x23246 (c x23246 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 250 ||| |||? ((~ (c c23248 Var3320)) v ((c c23248 c23206) v ((p Var3082 c23206) v ((p Var3138 c) v (c a c))))) ||| |||1. (all x23246 (c x23246 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> supp- |||============================= |||Step 251 ||| |||? ((c c23248 c23206) v ((p Var3082 c23206) v ((p Var3138 c) v (c a c)))) ||| |||1. (all x23249 (c c23248 x23249)) |||2. (all x23246 (c x23246 b)) |||3. (c a c) |||4. (c b c) |||5. (c c23206 b) |||6. (c c23206 a) |||7. (~ (c c23234 a)) |||8. (c c23234 b) ||| |||> supp+ |||============================= |||Step 252 ||| |||? ((p Var3082 c23206) v ((p Var3138 c) v (c a c))) ||| |||1. (~ (c c23248 c23206)) |||2. (all x23249 (c c23248 x23249)) |||3. (all x23246 (c x23246 b)) |||4. (c a c) |||5. (c b c) |||6. (c c23206 b) |||7. (c c23206 a) |||8. (~ (c c23234 a)) |||9. (c c23234 b) ||| |||> contradiction |||============================= ||Step 253 || ||? ((((~ (c Var3406 b)) v ((p Var3438 c23206) v (p Var3082 c23206))) v (p Var3138 c)) v (~ (o a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 254 || ||? (((~ (c Var3406 b)) v ((p Var3438 c23206) v (p Var3082 c23206))) v ((p Var3138 c) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 255 || ||? ((~ (c Var3406 b)) v (((p Var3438 c23206) v (p Var3082 c23206)) v ((p Var3138 c) v (~ (o a c))))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> supp- ||============================= ||Step 256 || ||? (((p Var3438 c23206) v (p Var3082 c23206)) v ((p Var3138 c) v (~ (o a c)))) || ||1. (all x23250 (c x23250 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 257 || ||? ((p Var3438 c23206) v ((p Var3082 c23206) v ((p Var3138 c) v (~ (o a c))))) || ||1. (all x23250 (c x23250 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 258 || ||? (((~ (c c23252 Var3438)) v (c c23252 c23206)) v ((p Var3082 c23206) v ((p Var3138 c) v (~ (o a c))))) || ||1. (all x23250 (c x23250 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 259 || ||? ((~ (c c23252 Var3438)) v ((c c23252 c23206) v ((p Var3082 c23206) v ((p Var3138 c) v (~ (o a c)))))) || ||1. (all x23250 (c x23250 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> supp- ||============================= ||Step 260 || ||? ((c c23252 c23206) v ((p Var3082 c23206) v ((p Var3138 c) v (~ (o a c))))) || ||1. (all x23253 (c c23252 x23253)) ||2. (all x23250 (c x23250 b)) ||3. (c a c) ||4. (c b c) ||5. (c c23206 b) ||6. (c c23206 a) ||7. (~ (c c23234 a)) ||8. (c c23234 b) || ||> supp+ ||============================= ||Step 261 || ||? ((p Var3082 c23206) v ((p Var3138 c) v (~ (o a c)))) || ||1. (~ (c c23252 c23206)) ||2. (all x23253 (c c23252 x23253)) ||3. (all x23250 (c x23250 b)) ||4. (c a c) ||5. (c b c) ||6. (c c23206 b) ||7. (c c23206 a) ||8. (~ (c c23234 a)) ||9. (c c23234 b) || ||> contradiction ||============================= |Step 262 | |? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3484 b))) v (p Var3516 c23206)) v (p Var3082 b)) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 263 | |? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3484 b))) v ((p Var3516 c23206) v (p Var3082 b))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 264 | |? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 265 | |? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> demodulate+revsk |============================= |Step 266 | |? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 267 | |? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> supp- |============================= |Step 268 | |? ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> demodulate+revsk |============================= |Step 269 | |? (exists x23254 (((((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))) v (p x23254 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))) v (p x23254 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> eR |============================= |Step 270 | |? (((((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))) v (p Var3586 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))) v (p Var3586 c))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> &r |============================= ||Step 271 || ||? ((((dc a c) v (ec a c)) v ((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b)))) v (p Var3586 b)) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> assocv ||============================= ||Step 272 || ||? (((dc a c) v (ec a c)) v (((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> assocv ||============================= ||Step 273 || ||? ((dc a c) v ((ec a c) v (((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 274 || ||? ((~ (c a c)) v ((ec a c) v (((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> supp- ||============================= ||Step 275 || ||? ((ec a c) v (((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 276 || ||? (((((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b)) v (c a c)) & ((((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b)) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> &r ||============================= |||Step 277 ||| |||? ((((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v (p Var3586 b)) v (c a c)) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 278 ||| |||? (((~ (c Var3484 b)) v ((p Var3516 c23206) v (p Var3082 b))) v ((p Var3586 b) v (c a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 279 ||| |||? ((~ (c Var3484 b)) v (((p Var3516 c23206) v (p Var3082 b)) v ((p Var3586 b) v (c a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> supp- |||============================= |||Step 280 ||| |||? (((p Var3516 c23206) v (p Var3082 b)) v ((p Var3586 b) v (c a c))) ||| |||1. (all x23255 (c x23255 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 281 ||| |||? ((p Var3516 c23206) v ((p Var3082 b) v ((p Var3586 b) v (c a c)))) ||| |||1. (all x23255 (c x23255 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> demodulate+revsk |||============================= |||Step 282 ||| |||? (((~ (c c23257 Var3516)) v (c c23257 c23206)) v ((p Var3082 b) v ((p Var3586 b) v (c a c)))) ||| |||1. (all x23255 (c x23255 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 283 ||| |||? ((~ (c c23257 Var3516)) v ((c c23257 c23206) v ((p Var3082 b) v ((p Var3586 b) v (c a c))))) ||| |||1. (all x23255 (c x23255 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> supp- |||============================= |||Step 284 ||| |||? ((c c23257 c23206) v ((p Var3082 b) v ((p Var3586 b) v (c a c)))) ||| |||1. (all x23258 (c c23257 x23258)) |||2. (all x23255 (c x23255 b)) |||3. (c a c) |||4. (c b c) |||5. (c c23206 b) |||6. (c c23206 a) |||7. (~ (c c23234 a)) |||8. (c c23234 b) ||| |||> supp+ |||============================= |||Step 285 ||| |||? ((p Var3082 b) v ((p Var3586 b) v (c a c))) ||| |||1. (~ (c c23257 c23206)) |||2. (all x23258 (c c23257 x23258)) |||3. (all x23255 (c x23255 b)) |||4. (c a c) |||5. (c b c) |||6. (c c23206 b) |||7. (c c23206 a) |||8. (~ (c c23234 a)) |||9. (c c23234 b) ||| |||> contradiction |||============================= ||Step 286 || ||? ((((~ (c Var3658 b)) v ((p Var3690 c23206) v (p Var3082 b))) v (p Var3586 b)) v (~ (o a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 287 || ||? (((~ (c Var3658 b)) v ((p Var3690 c23206) v (p Var3082 b))) v ((p Var3586 b) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 288 || ||? ((~ (c Var3658 b)) v (((p Var3690 c23206) v (p Var3082 b)) v ((p Var3586 b) v (~ (o a c))))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> supp- ||============================= ||Step 289 || ||? (((p Var3690 c23206) v (p Var3082 b)) v ((p Var3586 b) v (~ (o a c)))) || ||1. (all x23259 (c x23259 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 290 || ||? ((p Var3690 c23206) v ((p Var3082 b) v ((p Var3586 b) v (~ (o a c))))) || ||1. (all x23259 (c x23259 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 291 || ||? (((~ (c c23261 Var3690)) v (c c23261 c23206)) v ((p Var3082 b) v ((p Var3586 b) v (~ (o a c))))) || ||1. (all x23259 (c x23259 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 292 || ||? ((~ (c c23261 Var3690)) v ((c c23261 c23206) v ((p Var3082 b) v ((p Var3586 b) v (~ (o a c)))))) || ||1. (all x23259 (c x23259 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> supp- ||============================= ||Step 293 || ||? ((c c23261 c23206) v ((p Var3082 b) v ((p Var3586 b) v (~ (o a c))))) || ||1. (all x23262 (c c23261 x23262)) ||2. (all x23259 (c x23259 b)) ||3. (c a c) ||4. (c b c) ||5. (c c23206 b) ||6. (c c23206 a) ||7. (~ (c c23234 a)) ||8. (c c23234 b) || ||> supp+ ||============================= ||Step 294 || ||? ((p Var3082 b) v ((p Var3586 b) v (~ (o a c)))) || ||1. (~ (c c23261 c23206)) ||2. (all x23262 (c c23261 x23262)) ||3. (all x23259 (c x23259 b)) ||4. (c a c) ||5. (c b c) ||6. (c c23206 b) ||7. (c c23206 a) ||8. (~ (c c23234 a)) ||9. (c c23234 b) || ||> contradiction ||============================= |Step 295 | |? ((((dc a c) v (ec a c)) v ((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b)))) v (p Var3586 c)) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> assocv |============================= |Step 296 | |? (((dc a c) v (ec a c)) v (((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> assocv |============================= |Step 297 | |? ((dc a c) v ((ec a c) v (((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> demodulate+revsk |============================= |Step 298 | |? ((~ (c a c)) v ((ec a c) v (((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> supp- |============================= |Step 299 | |? ((ec a c) v (((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> demodulate+revsk |============================= |Step 300 | |? (((((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c)) v (c a c)) & ((((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c)) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> &r |============================= ||Step 301 || ||? ((((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v (p Var3586 c)) v (c a c)) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 302 || ||? (((~ (c Var3736 b)) v ((p Var3768 c23206) v (p Var3082 b))) v ((p Var3586 c) v (c a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 303 || ||? ((~ (c Var3736 b)) v (((p Var3768 c23206) v (p Var3082 b)) v ((p Var3586 c) v (c a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> supp- ||============================= ||Step 304 || ||? (((p Var3768 c23206) v (p Var3082 b)) v ((p Var3586 c) v (c a c))) || ||1. (all x23263 (c x23263 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 305 || ||? ((p Var3768 c23206) v ((p Var3082 b) v ((p Var3586 c) v (c a c)))) || ||1. (all x23263 (c x23263 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 306 || ||? (((~ (c c23265 Var3768)) v (c c23265 c23206)) v ((p Var3082 b) v ((p Var3586 c) v (c a c)))) || ||1. (all x23263 (c x23263 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 307 || ||? ((~ (c c23265 Var3768)) v ((c c23265 c23206) v ((p Var3082 b) v ((p Var3586 c) v (c a c))))) || ||1. (all x23263 (c x23263 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> supp- ||============================= ||Step 308 || ||? ((c c23265 c23206) v ((p Var3082 b) v ((p Var3586 c) v (c a c)))) || ||1. (all x23266 (c c23265 x23266)) ||2. (all x23263 (c x23263 b)) ||3. (c a c) ||4. (c b c) ||5. (c c23206 b) ||6. (c c23206 a) ||7. (~ (c c23234 a)) ||8. (c c23234 b) || ||> supp+ ||============================= ||Step 309 || ||? ((p Var3082 b) v ((p Var3586 c) v (c a c))) || ||1. (~ (c c23265 c23206)) ||2. (all x23266 (c c23265 x23266)) ||3. (all x23263 (c x23263 b)) ||4. (c a c) ||5. (c b c) ||6. (c c23206 b) ||7. (c c23206 a) ||8. (~ (c c23234 a)) ||9. (c c23234 b) || ||> contradiction ||============================= |Step 310 | |? ((((~ (c Var3854 b)) v ((p Var3886 c23206) v (p Var3082 b))) v (p Var3586 c)) v (~ (o a c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 311 | |? (((~ (c Var3854 b)) v ((p Var3886 c23206) v (p Var3082 b))) v ((p Var3586 c) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 312 | |? ((~ (c Var3854 b)) v (((p Var3886 c23206) v (p Var3082 b)) v ((p Var3586 c) v (~ (o a c))))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> supp- |============================= |Step 313 | |? (((p Var3886 c23206) v (p Var3082 b)) v ((p Var3586 c) v (~ (o a c)))) | |1. (all x23267 (c x23267 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 314 | |? ((p Var3886 c23206) v ((p Var3082 b) v ((p Var3586 c) v (~ (o a c))))) | |1. (all x23267 (c x23267 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> demodulate+revsk |============================= |Step 315 | |? (((~ (c c23269 Var3886)) v (c c23269 c23206)) v ((p Var3082 b) v ((p Var3586 c) v (~ (o a c))))) | |1. (all x23267 (c x23267 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 316 | |? ((~ (c c23269 Var3886)) v ((c c23269 c23206) v ((p Var3082 b) v ((p Var3586 c) v (~ (o a c)))))) | |1. (all x23267 (c x23267 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> supp- |============================= |Step 317 | |? ((c c23269 c23206) v ((p Var3082 b) v ((p Var3586 c) v (~ (o a c))))) | |1. (all x23270 (c c23269 x23270)) |2. (all x23267 (c x23267 b)) |3. (c a c) |4. (c b c) |5. (c c23206 b) |6. (c c23206 a) |7. (~ (c c23234 a)) |8. (c c23234 b) | |> supp+ |============================= |Step 318 | |? ((p Var3082 b) v ((p Var3586 c) v (~ (o a c)))) | |1. (~ (c c23269 c23206)) |2. (all x23270 (c c23269 x23270)) |3. (all x23267 (c x23267 b)) |4. (c a c) |5. (c b c) |6. (c c23206 b) |7. (c c23206 a) |8. (~ (c c23234 a)) |9. (c c23234 b) | |> contradiction |============================= Step 319 ? (((~ (ec c23206 b)) v (((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b)))) v (p Var3964 a)) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > assocv ============================= Step 320 ? ((~ (ec c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a))) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > demodulate+revsk ============================= Step 321 ? (((~ (c c23206 b)) v (o c23206 b)) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a))) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > assocv ============================= Step 322 ? ((~ (c c23206 b)) v ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a)))) 1. (c c23206 a) 2. (~ (c c23234 a)) 3. (c c23234 b) > supp- ============================= Step 323 ? ((o c23206 b) v ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > demodulate+revsk ============================= Step 324 ? (exists x23271 ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a)) v (p x23271 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a)) v (p x23271 b)))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > eR ============================= Step 325 ? ((((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a)) v (p Var4024 c23206)) & (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a)) v (p Var4024 b))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > &r ============================= |Step 326 | |? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v (p Var3964 a)) v (p Var4024 c23206)) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 327 | |? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var3932 b))) v ((p Var3964 a) v (p Var4024 c23206))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 328 | |? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 329 | |? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> demodulate+revsk |============================= |Step 330 | |? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> assocv |============================= |Step 331 | |? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))))) | |1. (c c23206 b) |2. (c c23206 a) |3. (~ (c c23234 a)) |4. (c c23234 b) | |> supp- |============================= |Step 332 | |? ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> demodulate+revsk |============================= |Step 333 | |? (exists x23272 (((((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))) v (p x23272 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))) v (p x23272 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> eR |============================= |Step 334 | |? (((((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))) v (p Var4080 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))) v (p Var4080 c))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> &r |============================= ||Step 335 || ||? ((((dc a c) v (ec a c)) v ((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206)))) v (p Var4080 b)) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> assocv ||============================= ||Step 336 || ||? (((dc a c) v (ec a c)) v (((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> assocv ||============================= ||Step 337 || ||? ((dc a c) v ((ec a c) v (((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 338 || ||? ((~ (c a c)) v ((ec a c) v (((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b)))) || ||1. (c b c) ||2. (c c23206 b) ||3. (c c23206 a) ||4. (~ (c c23234 a)) ||5. (c c23234 b) || ||> supp- ||============================= ||Step 339 || ||? ((ec a c) v (((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 340 || ||? (((((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b)) v (c a c)) & ((((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b)) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> &r ||============================= |||Step 341 ||| |||? ((((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v (p Var4080 b)) v (c a c)) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 342 ||| |||? (((~ (c Var3932 b)) v ((p Var3964 a) v (p Var4024 c23206))) v ((p Var4080 b) v (c a c))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> assocv |||============================= |||Step 343 ||| |||? ((~ (c Var3932 b)) v (((p Var3964 a) v (p Var4024 c23206)) v ((p Var4080 b) v (c a c)))) ||| |||1. (c a c) |||2. (c b c) |||3. (c c23206 b) |||4. (c c23206 a) |||5. (~ (c c23234 a)) |||6. (c c23234 b) ||| |||> supp- |||============================= |||Step 344 ||| |||? (((p Var3964 a) v (p Var4024 c23206)) v ((p Var4080 b) v (c a c))) ||| |||1. (all x23273 (c x23273 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 345 ||| |||? ((p Var3964 a) v ((p Var4024 c23206) v ((p Var4080 b) v (c a c)))) ||| |||1. (all x23273 (c x23273 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> demodulate+revsk |||============================= |||Step 346 ||| |||? (((~ (c c23275 Var3964)) v (c c23275 a)) v ((p Var4024 c23206) v ((p Var4080 b) v (c a c)))) ||| |||1. (all x23273 (c x23273 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> assocv |||============================= |||Step 347 ||| |||? ((~ (c c23275 Var3964)) v ((c c23275 a) v ((p Var4024 c23206) v ((p Var4080 b) v (c a c))))) ||| |||1. (all x23273 (c x23273 b)) |||2. (c a c) |||3. (c b c) |||4. (c c23206 b) |||5. (c c23206 a) |||6. (~ (c c23234 a)) |||7. (c c23234 b) ||| |||> supp- |||============================= |||Step 348 ||| |||? ((c c23275 a) v ((p Var4024 c23206) v ((p Var4080 b) v (c a c)))) ||| |||1. (all x23276 (c c23275 x23276)) |||2. (all x23273 (c x23273 b)) |||3. (c a c) |||4. (c b c) |||5. (c c23206 b) |||6. (c c23206 a) |||7. (~ (c c23234 a)) |||8. (c c23234 b) ||| |||> supp+ |||============================= |||Step 349 ||| |||? ((p Var4024 c23206) v ((p Var4080 b) v (c a c))) ||| |||1. (~ (c c23275 a)) |||2. (all x23276 (c c23275 x23276)) |||3. (all x23273 (c x23273 b)) |||4. (c a c) |||5. (c b c) |||6. (c c23206 b) |||7. (c c23206 a) |||8. (~ (c c23234 a)) |||9. (c c23234 b) ||| |||> contradiction |||============================= ||Step 350 || ||? ((((~ (c Var4152 b)) v ((p Var4184 a) v (p Var4024 c23206))) v (p Var4080 b)) v (~ (o a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 351 || ||? (((~ (c Var4152 b)) v ((p Var4184 a) v (p Var4024 c23206))) v ((p Var4080 b) v (~ (o a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 352 || ||? ((~ (c Var4152 b)) v (((p Var4184 a) v (p Var4024 c23206)) v ((p Var4080 b) v (~ (o a c))))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> supp- ||============================= ||Step 353 || ||? (((p Var4184 a) v (p Var4024 c23206)) v ((p Var4080 b) v (~ (o a c)))) || ||1. (all x23277 (c x23277 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 354 || ||? ((p Var4184 a) v ((p Var4024 c23206) v ((p Var4080 b) v (~ (o a c))))) || ||1. (all x23277 (c x23277 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 355 || ||? (((~ (c c23279 Var4184)) v (c c23279 a)) v ((p Var4024 c23206) v ((p Var4080 b) v (~ (o a c))))) || ||1. (all x23277 (c x23277 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 356 || ||? ((~ (c c23279 Var4184)) v ((c c23279 a) v ((p Var4024 c23206) v ((p Var4080 b) v (~ (o a c)))))) || ||1. (all x23277 (c x23277 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> supp- ||============================= ||Step 357 || ||? ((c c23279 a) v ((p Var4024 c23206) v ((p Var4080 b) v (~ (o a c))))) || ||1. (all x23280 (c c23279 x23280)) ||2. (all x23277 (c x23277 b)) ||3. (c a c) ||4. (c b c) ||5. (c c23206 b) ||6. (c c23206 a) ||7. (~ (c c23234 a)) ||8. (c c23234 b) || ||> supp+ ||============================= ||Step 358 || ||? ((p Var4024 c23206) v ((p Var4080 b) v (~ (o a c)))) || ||1. (~ (c c23279 a)) ||2. (all x23280 (c c23279 x23280)) ||3. (all x23277 (c x23277 b)) ||4. (c a c) ||5. (c b c) ||6. (c c23206 b) ||7. (c c23206 a) ||8. (~ (c c23234 a)) ||9. (c c23234 b) || ||> contradiction ||============================= |Step 359 | |? ((((dc a c) v (ec a c)) v ((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206)))) v (p Var4080 c)) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> assocv |============================= |Step 360 | |? (((dc a c) v (ec a c)) v (((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> assocv |============================= |Step 361 | |? ((dc a c) v ((ec a c) v (((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> demodulate+revsk |============================= |Step 362 | |? ((~ (c a c)) v ((ec a c) v (((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> supp- |============================= |Step 363 | |? ((ec a c) v (((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> demodulate+revsk |============================= |Step 364 | |? (((((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c)) v (c a c)) & ((((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c)) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> &r |============================= ||Step 365 || ||? ((((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v (p Var4080 c)) v (c a c)) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 366 || ||? (((~ (c Var4230 b)) v ((p Var4262 a) v (p Var4024 c23206))) v ((p Var4080 c) v (c a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 367 || ||? ((~ (c Var4230 b)) v (((p Var4262 a) v (p Var4024 c23206)) v ((p Var4080 c) v (c a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> supp- ||============================= ||Step 368 || ||? (((p Var4262 a) v (p Var4024 c23206)) v ((p Var4080 c) v (c a c))) || ||1. (all x23281 (c x23281 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 369 || ||? ((p Var4262 a) v ((p Var4024 c23206) v ((p Var4080 c) v (c a c)))) || ||1. (all x23281 (c x23281 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 370 || ||? (((~ (c c23283 Var4262)) v (c c23283 a)) v ((p Var4024 c23206) v ((p Var4080 c) v (c a c)))) || ||1. (all x23281 (c x23281 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 371 || ||? ((~ (c c23283 Var4262)) v ((c c23283 a) v ((p Var4024 c23206) v ((p Var4080 c) v (c a c))))) || ||1. (all x23281 (c x23281 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> supp- ||============================= ||Step 372 || ||? ((c c23283 a) v ((p Var4024 c23206) v ((p Var4080 c) v (c a c)))) || ||1. (all x23284 (c c23283 x23284)) ||2. (all x23281 (c x23281 b)) ||3. (c a c) ||4. (c b c) ||5. (c c23206 b) ||6. (c c23206 a) ||7. (~ (c c23234 a)) ||8. (c c23234 b) || ||> supp+ ||============================= ||Step 373 || ||? ((p Var4024 c23206) v ((p Var4080 c) v (c a c))) || ||1. (~ (c c23283 a)) ||2. (all x23284 (c c23283 x23284)) ||3. (all x23281 (c x23281 b)) ||4. (c a c) ||5. (c b c) ||6. (c c23206 b) ||7. (c c23206 a) ||8. (~ (c c23234 a)) ||9. (c c23234 b) || ||> contradiction ||============================= |Step 374 | |? ((((~ (c Var4348 b)) v ((p Var4380 a) v (p Var4024 c23206))) v (p Var4080 c)) v (~ (o a c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 375 | |? (((~ (c Var4348 b)) v ((p Var4380 a) v (p Var4024 c23206))) v ((p Var4080 c) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 376 | |? ((~ (c Var4348 b)) v (((p Var4380 a) v (p Var4024 c23206)) v ((p Var4080 c) v (~ (o a c))))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> supp- |============================= |Step 377 | |? (((p Var4380 a) v (p Var4024 c23206)) v ((p Var4080 c) v (~ (o a c)))) | |1. (all x23285 (c x23285 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 378 | |? ((p Var4380 a) v ((p Var4024 c23206) v ((p Var4080 c) v (~ (o a c))))) | |1. (all x23285 (c x23285 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> demodulate+revsk |============================= |Step 379 | |? (((~ (c c23287 Var4380)) v (c c23287 a)) v ((p Var4024 c23206) v ((p Var4080 c) v (~ (o a c))))) | |1. (all x23285 (c x23285 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 380 | |? ((~ (c c23287 Var4380)) v ((c c23287 a) v ((p Var4024 c23206) v ((p Var4080 c) v (~ (o a c)))))) | |1. (all x23285 (c x23285 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> supp- |============================= |Step 381 | |? ((c c23287 a) v ((p Var4024 c23206) v ((p Var4080 c) v (~ (o a c))))) | |1. (all x23288 (c c23287 x23288)) |2. (all x23285 (c x23285 b)) |3. (c a c) |4. (c b c) |5. (c c23206 b) |6. (c c23206 a) |7. (~ (c c23234 a)) |8. (c c23234 b) | |> supp+ |============================= |Step 382 | |? ((p Var4024 c23206) v ((p Var4080 c) v (~ (o a c)))) | |1. (~ (c c23287 a)) |2. (all x23288 (c c23287 x23288)) |3. (all x23285 (c x23285 b)) |4. (c a c) |5. (c b c) |6. (c c23206 b) |7. (c c23206 a) |8. (~ (c c23234 a)) |9. (c c23234 b) | |> contradiction |============================= Step 383 ? (((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var4426 b))) v (p Var4458 a)) v (p Var4024 b)) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > assocv ============================= Step 384 ? ((((~ (ec b c)) v ((dc a c) v (ec a c))) v (~ (c Var4426 b))) v ((p Var4458 a) v (p Var4024 b))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > assocv ============================= Step 385 ? (((~ (ec b c)) v ((dc a c) v (ec a c))) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > assocv ============================= Step 386 ? ((~ (ec b c)) v (((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > demodulate+revsk ============================= Step 387 ? (((~ (c b c)) v (o b c)) v (((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > assocv ============================= Step 388 ? ((~ (c b c)) v ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))))) 1. (c c23206 b) 2. (c c23206 a) 3. (~ (c c23234 a)) 4. (c c23234 b) > supp- ============================= Step 389 ? ((o b c) v (((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))))) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > demodulate+revsk ============================= Step 390 ? (exists x23289 (((((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))) v (p x23289 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))) v (p x23289 c)))) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > eR ============================= Step 391 ? (((((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))) v (p Var4528 b)) & ((((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))) v (p Var4528 c))) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > &r ============================= |Step 392 | |? ((((dc a c) v (ec a c)) v ((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b)))) v (p Var4528 b)) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> assocv |============================= |Step 393 | |? (((dc a c) v (ec a c)) v (((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> assocv |============================= |Step 394 | |? ((dc a c) v ((ec a c) v (((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> demodulate+revsk |============================= |Step 395 | |? ((~ (c a c)) v ((ec a c) v (((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b)))) | |1. (c b c) |2. (c c23206 b) |3. (c c23206 a) |4. (~ (c c23234 a)) |5. (c c23234 b) | |> supp- |============================= |Step 396 | |? ((ec a c) v (((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> demodulate+revsk |============================= |Step 397 | |? (((((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b)) v (c a c)) & ((((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b)) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> &r |============================= ||Step 398 || ||? ((((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v (p Var4528 b)) v (c a c)) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 399 || ||? (((~ (c Var4426 b)) v ((p Var4458 a) v (p Var4024 b))) v ((p Var4528 b) v (c a c))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> assocv ||============================= ||Step 400 || ||? ((~ (c Var4426 b)) v (((p Var4458 a) v (p Var4024 b)) v ((p Var4528 b) v (c a c)))) || ||1. (c a c) ||2. (c b c) ||3. (c c23206 b) ||4. (c c23206 a) ||5. (~ (c c23234 a)) ||6. (c c23234 b) || ||> supp- ||============================= ||Step 401 || ||? (((p Var4458 a) v (p Var4024 b)) v ((p Var4528 b) v (c a c))) || ||1. (all x23290 (c x23290 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 402 || ||? ((p Var4458 a) v ((p Var4024 b) v ((p Var4528 b) v (c a c)))) || ||1. (all x23290 (c x23290 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> demodulate+revsk ||============================= ||Step 403 || ||? (((~ (c c23292 Var4458)) v (c c23292 a)) v ((p Var4024 b) v ((p Var4528 b) v (c a c)))) || ||1. (all x23290 (c x23290 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> assocv ||============================= ||Step 404 || ||? ((~ (c c23292 Var4458)) v ((c c23292 a) v ((p Var4024 b) v ((p Var4528 b) v (c a c))))) || ||1. (all x23290 (c x23290 b)) ||2. (c a c) ||3. (c b c) ||4. (c c23206 b) ||5. (c c23206 a) ||6. (~ (c c23234 a)) ||7. (c c23234 b) || ||> supp- ||============================= ||Step 405 || ||? ((c c23292 a) v ((p Var4024 b) v ((p Var4528 b) v (c a c)))) || ||1. (all x23293 (c c23292 x23293)) ||2. (all x23290 (c x23290 b)) ||3. (c a c) ||4. (c b c) ||5. (c c23206 b) ||6. (c c23206 a) ||7. (~ (c c23234 a)) ||8. (c c23234 b) || ||> supp+ ||============================= ||Step 406 || ||? ((p Var4024 b) v ((p Var4528 b) v (c a c))) || ||1. (~ (c c23292 a)) ||2. (all x23293 (c c23292 x23293)) ||3. (all x23290 (c x23290 b)) ||4. (c a c) ||5. (c b c) ||6. (c c23206 b) ||7. (c c23206 a) ||8. (~ (c c23234 a)) ||9. (c c23234 b) || ||> contradiction ||============================= |Step 407 | |? ((((~ (c Var4600 b)) v ((p Var4632 a) v (p Var4024 b))) v (p Var4528 b)) v (~ (o a c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 408 | |? (((~ (c Var4600 b)) v ((p Var4632 a) v (p Var4024 b))) v ((p Var4528 b) v (~ (o a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 409 | |? ((~ (c Var4600 b)) v (((p Var4632 a) v (p Var4024 b)) v ((p Var4528 b) v (~ (o a c))))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> supp- |============================= |Step 410 | |? (((p Var4632 a) v (p Var4024 b)) v ((p Var4528 b) v (~ (o a c)))) | |1. (all x23294 (c x23294 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 411 | |? ((p Var4632 a) v ((p Var4024 b) v ((p Var4528 b) v (~ (o a c))))) | |1. (all x23294 (c x23294 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> demodulate+revsk |============================= |Step 412 | |? (((~ (c c23296 Var4632)) v (c c23296 a)) v ((p Var4024 b) v ((p Var4528 b) v (~ (o a c))))) | |1. (all x23294 (c x23294 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 413 | |? ((~ (c c23296 Var4632)) v ((c c23296 a) v ((p Var4024 b) v ((p Var4528 b) v (~ (o a c)))))) | |1. (all x23294 (c x23294 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> supp- |============================= |Step 414 | |? ((c c23296 a) v ((p Var4024 b) v ((p Var4528 b) v (~ (o a c))))) | |1. (all x23297 (c c23296 x23297)) |2. (all x23294 (c x23294 b)) |3. (c a c) |4. (c b c) |5. (c c23206 b) |6. (c c23206 a) |7. (~ (c c23234 a)) |8. (c c23234 b) | |> supp+ |============================= |Step 415 | |? ((p Var4024 b) v ((p Var4528 b) v (~ (o a c)))) | |1. (~ (c c23296 a)) |2. (all x23297 (c c23296 x23297)) |3. (all x23294 (c x23294 b)) |4. (c a c) |5. (c b c) |6. (c c23206 b) |7. (c c23206 a) |8. (~ (c c23234 a)) |9. (c c23234 b) | |> contradiction |============================= Step 416 ? ((((dc a c) v (ec a c)) v ((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b)))) v (p Var4528 c)) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > assocv ============================= Step 417 ? (((dc a c) v (ec a c)) v (((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c))) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > assocv ============================= Step 418 ? ((dc a c) v ((ec a c) v (((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c)))) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > demodulate+revsk ============================= Step 419 ? ((~ (c a c)) v ((ec a c) v (((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c)))) 1. (c b c) 2. (c c23206 b) 3. (c c23206 a) 4. (~ (c c23234 a)) 5. (c c23234 b) > supp- ============================= Step 420 ? ((ec a c) v (((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c))) 1. (c a c) 2. (c b c) 3. (c c23206 b) 4. (c c23206 a) 5. (~ (c c23234 a)) 6. (c c23234 b) > demodulate+revsk ============================= Step 421 ? (((((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c)) v (c a c)) & ((((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c)) v (~ (o a c)))) 1. (c a c) 2. (c b c) 3. (c c23206 b) 4. (c c23206 a) 5. (~ (c c23234 a)) 6. (c c23234 b) > &r ============================= |Step 422 | |? ((((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v (p Var4528 c)) v (c a c)) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 423 | |? (((~ (c Var4678 b)) v ((p Var4710 a) v (p Var4024 b))) v ((p Var4528 c) v (c a c))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> assocv |============================= |Step 424 | |? ((~ (c Var4678 b)) v (((p Var4710 a) v (p Var4024 b)) v ((p Var4528 c) v (c a c)))) | |1. (c a c) |2. (c b c) |3. (c c23206 b) |4. (c c23206 a) |5. (~ (c c23234 a)) |6. (c c23234 b) | |> supp- |============================= |Step 425 | |? (((p Var4710 a) v (p Var4024 b)) v ((p Var4528 c) v (c a c))) | |1. (all x23298 (c x23298 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 426 | |? ((p Var4710 a) v ((p Var4024 b) v ((p Var4528 c) v (c a c)))) | |1. (all x23298 (c x23298 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> demodulate+revsk |============================= |Step 427 | |? (((~ (c c23300 Var4710)) v (c c23300 a)) v ((p Var4024 b) v ((p Var4528 c) v (c a c)))) | |1. (all x23298 (c x23298 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> assocv |============================= |Step 428 | |? ((~ (c c23300 Var4710)) v ((c c23300 a) v ((p Var4024 b) v ((p Var4528 c) v (c a c))))) | |1. (all x23298 (c x23298 b)) |2. (c a c) |3. (c b c) |4. (c c23206 b) |5. (c c23206 a) |6. (~ (c c23234 a)) |7. (c c23234 b) | |> supp- |============================= |Step 429 | |? ((c c23300 a) v ((p Var4024 b) v ((p Var4528 c) v (c a c)))) | |1. (all x23301 (c c23300 x23301)) |2. (all x23298 (c x23298 b)) |3. (c a c) |4. (c b c) |5. (c c23206 b) |6. (c c23206 a) |7. (~ (c c23234 a)) |8. (c c23234 b) | |> supp+ |============================= |Step 430 | |? ((p Var4024 b) v ((p Var4528 c) v (c a c))) | |1. (~ (c c23300 a)) |2. (all x23301 (c c23300 x23301)) |3. (all x23298 (c x23298 b)) |4. (c a c) |5. (c b c) |6. (c c23206 b) |7. (c c23206 a) |8. (~ (c c23234 a)) |9. (c c23234 b) | |> contradiction |============================= Step 431 ? ((((~ (c Var4796 b)) v ((p Var4828 a) v (p Var4024 b))) v (p Var4528 c)) v (~ (o a c))) 1. (c a c) 2. (c b c) 3. (c c23206 b) 4. (c c23206 a) 5. (~ (c c23234 a)) 6. (c c23234 b) > assocv ============================= Step 432 ? (((~ (c Var4796 b)) v ((p Var4828 a) v (p Var4024 b))) v ((p Var4528 c) v (~ (o a c)))) 1. (c a c) 2. (c b c) 3. (c c23206 b) 4. (c c23206 a) 5. (~ (c c23234 a)) 6. (c c23234 b) > assocv ============================= Step 433 ? ((~ (c Var4796 b)) v (((p Var4828 a) v (p Var4024 b)) v ((p Var4528 c) v (~ (o a c))))) 1. (c a c) 2. (c b c) 3. (c c23206 b) 4. (c c23206 a) 5. (~ (c c23234 a)) 6. (c c23234 b) > supp- ============================= Step 434 ? (((p Var4828 a) v (p Var4024 b)) v ((p Var4528 c) v (~ (o a c)))) 1. (all x23302 (c x23302 b)) 2. (c a c) 3. (c b c) 4. (c c23206 b) 5. (c c23206 a) 6. (~ (c c23234 a)) 7. (c c23234 b) > assocv ============================= Step 435 ? ((p Var4828 a) v ((p Var4024 b) v ((p Var4528 c) v (~ (o a c))))) 1. (all x23302 (c x23302 b)) 2. (c a c) 3. (c b c) 4. (c c23206 b) 5. (c c23206 a) 6. (~ (c c23234 a)) 7. (c c23234 b) > demodulate+revsk ============================= Step 436 ? (((~ (c c23304 Var4828)) v (c c23304 a)) v ((p Var4024 b) v ((p Var4528 c) v (~ (o a c))))) 1. (all x23302 (c x23302 b)) 2. (c a c) 3. (c b c) 4. (c c23206 b) 5. (c c23206 a) 6. (~ (c c23234 a)) 7. (c c23234 b) > assocv ============================= Step 437 ? ((~ (c c23304 Var4828)) v ((c c23304 a) v ((p Var4024 b) v ((p Var4528 c) v (~ (o a c)))))) 1. (all x23302 (c x23302 b)) 2. (c a c) 3. (c b c) 4. (c c23206 b) 5. (c c23206 a) 6. (~ (c c23234 a)) 7. (c c23234 b) > supp- ============================= Step 438 ? ((c c23304 a) v ((p Var4024 b) v ((p Var4528 c) v (~ (o a c))))) 1. (all x23305 (c c23304 x23305)) 2. (all x23302 (c x23302 b)) 3. (c a c) 4. (c b c) 5. (c c23206 b) 6. (c c23206 a) 7. (~ (c c23234 a)) 8. (c c23234 b) > supp+ ============================= Step 439 ? ((p Var4024 b) v ((p Var4528 c) v (~ (o a c)))) 1. (~ (c c23304 a)) 2. (all x23305 (c c23304 x23305)) 3. (all x23302 (c x23302 b)) 4. (c a c) 5. (c b c) 6. (c c23206 b) 7. (c c23206 a) 8. (~ (c c23234 a)) 9. (c c23234 b) > contradiction =============================