| current assets |
|---|
ad51d../61127.. bday: 11752 doc published by PrGVS..Known 68ce2.. : ∀ x0 x1 . (x0 = x1 ⟶ False) ⟶ x1 = x0 ⟶ FalseTheorem 86b2a.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ In (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ In (x3 x4 x5 x6) x0) ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x6 x7 x8 x9) x0) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x7 x8 x9) x0) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ In (x9 x10 x11) x0) ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ In (x11 x12 x13) x0) ⟶ (∀ x12 . In x12 x0 ⟶ (x11 x10 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ (x11 x12 x10 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x9 x12 (x11 x12 x13) = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x1 (x11 x13 x12) x12 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x11 (x1 x13 x12) x12 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ x11 x13 x12 = x11 x14 x12 ⟶ (x13 = x14 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x8 x12 x13 = x11 (x9 x12 x13) (x9 (x9 x12 x10) x10) ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ (x2 x10 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ (x7 x10 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x3 x12 x10 x13 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x6 x12 x10 x13 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x6 x12 x13 (x8 x12 (x2 x13 (x6 x12 x13 (x8 x12 (x2 x13 (x6 x12 x13 (x8 x12 (x2 x13 (x6 x12 x13 (x8 x12 (x2 x13 (x6 x12 x13 (x8 x12 (x2 x13 x14)))))))))))))) = x14 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ (x3 x12 x14 (x7 x13 (x8 x12 (x3 x14 x13 (x3 x12 x14 (x7 x13 (x8 x12 (x3 x14 x13 (x3 x12 x14 (x7 x13 (x8 x12 (x3 x14 x13 (x3 x12 x14 (x7 x13 (x8 x12 (x3 x14 x13 x15))))))))))))))) = x15 ⟶ False) ⟶ False) ⟶ (x11 x4 x5 = x11 x5 x4 ⟶ False) ⟶ False (proof)Known b5371.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ ((∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x1 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x2 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x3 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x7 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ In (x8 x14 x15 x16) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ In (x9 x14 x15 x16) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x10 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x11 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x12 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x13 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ x1 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x1 x14 x4 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x2 x14 (x1 x14 x15) = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x1 x14 (x2 x14 x15) = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x3 (x1 x14 x15) x15 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x1 (x3 x14 x15) x15 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x1 x14 x15 = x1 x14 x16 ⟶ x15 = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x1 x14 x15 = x1 x16 x15 ⟶ x14 = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x5 x14 x15 = x2 (x1 x15 x14) (x1 x14 x15)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x6 x14 x15 x16 = x2 (x1 x14 (x1 x15 x16)) (x1 (x1 x14 x15) x16)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x7 x14 x15 = x2 x14 (x1 x15 x14)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x10 x14 x15 = x1 x14 (x1 x15 (x2 x14 x4))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x11 x14 x15 = x1 (x1 (x3 x4 x14) x15) x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x12 x14 x15 = x1 (x2 x14 x15) (x2 (x2 x14 x4) x4)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x13 x14 x15 = x1 (x3 x4 (x3 x4 x14)) (x3 x15 x14)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x8 x14 x15 x16 = x2 (x1 x15 x14) (x1 x15 (x1 x14 x16))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x9 x14 x15 x16 = x3 (x1 (x1 x16 x14) x15) (x1 x14 x15)) ⟶ (∀ x14 . In x14 x0 ⟶ x2 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x2 x14 x14 = x4) ⟶ (∀ x14 . In x14 x0 ⟶ x3 x14 x4 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x3 x14 x14 = x4) ⟶ (∀ x14 . In x14 x0 ⟶ x7 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x10 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x11 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x12 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x13 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x8 x4 x14 x15 = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x8 x14 x4 x15 = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x9 x4 x14 x15 = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x9 x14 x4 x15 = x15) ⟶ ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x1 x14 x15 = x1 x15 x14) ⟶ FalseKnown b4782..contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0Known notEnotE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ FalseTheorem 775e8.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x9 x14 x15 (x12 x14 (x7 x15 (x9 x14 x15 (x12 x14 (x7 x15 (x9 x14 x15 (x12 x14 (x7 x15 (x9 x14 x15 (x12 x14 (x7 x15 (x9 x14 x15 (x12 x14 (x7 x15 x16)))))))))))))) = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x8 x14 x15 (x10 x16 (x12 x14 (x8 x15 x16 (x8 x14 x15 (x10 x16 (x12 x14 (x8 x15 x16 (x8 x14 x15 (x10 x16 (x12 x14 (x8 x15 x16 (x8 x14 x15 (x10 x16 (x12 x14 (x8 x15 x16 x17))))))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x12 x14 (x12 x15 (x12 x16 x17)) = x12 x15 (x12 x16 (x12 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x9 x14 x15 (x10 x16 (x12 x17 x18)) = x10 x16 (x12 x17 (x9 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x12 x15 (x12 x16 (x7 x17 x18))) = x12 x16 (x7 x17 (x10 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x10 x15 (x7 x16 (x12 x17 x18))) = x7 x16 (x12 x17 (x10 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x10 x15 (x12 x16 (x7 x17 x18))) = x12 x16 (x7 x17 (x12 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x7 x15 (x10 x16 (x12 x17 x18))) = x10 x16 (x12 x17 (x7 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x12 x15 (x7 x16 (x12 x17 x18))) = x7 x16 (x12 x17 (x10 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x9 x14 x15 (x7 x16 (x13 x17 (x12 x18 x19))) = x13 x17 (x12 x18 (x9 x14 x15 (x7 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x13 x16 (x13 x17 (x7 x18 x19))) = x13 x17 (x7 x18 (x8 x14 x15 (x13 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x8 x14 x15 (x12 x16 (x8 x17 x18 (x10 x19 x20))) = x8 x17 x18 (x10 x19 (x8 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x12 x16 (x8 x17 x18 (x10 x19 x20))) = x8 x17 x18 (x10 x19 (x9 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x7 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x8 x14 x15 (x10 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x10 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x10 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x13 x16 (x12 x17 (x8 x18 x19 (x13 x20 x21)))) = x8 x18 x19 (x13 x20 (x8 x14 x15 (x13 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x13 x16 (x12 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x13 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x12 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x8 x14 x15 (x12 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x10 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x12 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x13 x17 (x8 x18 x19 (x7 x20 x21)))) = x8 x18 x19 (x7 x20 (x9 x14 x15 (x12 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x10 x16 (x10 x17 (x8 x18 x19 (x7 x20 x21)))) = x8 x18 x19 (x7 x20 (x9 x14 x15 (x10 x16 (x10 x17 x21))))) ⟶ False (proof)Theorem ff6ab.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x2 x3 x4 x5) x0) ⟶ ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ In (x5 x6 x7) x0) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x6 x7 x8) x0) ⟶ ∀ x7 . In x7 x0 ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0) ⟶ (∀ x9 . In x9 x0 ⟶ (x8 x9 x7 = x9 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x8 x9 (x1 x9 x10) = x10 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x6 x9 x10 = x1 x9 (x8 x10 x9) ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ (x1 x7 x9 = x9 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ (x5 x7 x9 = x9 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x2 x7 x9 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x2 x9 x7 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x2 x9 x11 (x6 x10 (x6 x9 (x2 x11 x10 (x2 x9 x11 (x6 x10 (x6 x9 (x2 x11 x10 (x2 x9 x11 (x6 x10 (x6 x9 (x2 x11 x10 x12))))))))))) = x12 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x2 x9 x10 (x5 x9 (x6 x10 (x2 x9 x10 (x5 x9 (x6 x10 (x2 x9 x10 (x5 x9 (x6 x10 (x2 x9 x10 (x5 x9 (x6 x10 x11))))))))))) = x11 ⟶ False) ⟶ False) ⟶ (x8 x3 x4 = x8 x4 x3 ⟶ False) ⟶ False (proof)Theorem a3916.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x8 x14 x15 (x7 x16 (x7 x14 (x8 x15 x16 (x8 x14 x15 (x7 x16 (x7 x14 (x8 x15 x16 (x8 x14 x15 (x7 x16 (x7 x14 (x8 x15 x16 x17))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x8 x14 x15 (x12 x14 (x7 x15 (x8 x14 x15 (x12 x14 (x7 x15 (x8 x14 x15 (x12 x14 (x7 x15 (x8 x14 x15 (x12 x14 (x7 x15 x16))))))))))) = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x12 x14 (x12 x15 (x13 x16 x17)) = x12 x15 (x13 x16 (x12 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x9 x14 x15 (x10 x16 (x13 x17 x18)) = x10 x16 (x13 x17 (x9 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x12 x15 (x12 x16 (x10 x17 x18))) = x12 x16 (x10 x17 (x13 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x10 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x12 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x12 x15 (x10 x16 (x12 x17 x18))) = x10 x16 (x12 x17 (x12 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x13 x15 (x10 x16 (x13 x17 x18))) = x10 x16 (x13 x17 (x7 x14 (x13 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x7 x15 (x10 x16 (x7 x17 x18))) = x10 x16 (x7 x17 (x12 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x12 x16 (x13 x17 (x7 x18 x19))) = x13 x17 (x7 x18 (x8 x14 x15 (x12 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x12 x16 (x10 x17 (x13 x18 x19))) = x10 x17 (x13 x18 (x8 x14 x15 (x12 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x7 x16 (x8 x17 x18 (x7 x19 x20))) = x8 x17 x18 (x7 x19 (x9 x14 x15 (x7 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x8 x14 x15 (x10 x16 (x9 x17 x18 (x12 x19 x20))) = x9 x17 x18 (x12 x19 (x8 x14 x15 (x10 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x10 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x12 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x13 x16 (x12 x17 (x8 x18 x19 (x7 x20 x21)))) = x8 x18 x19 (x7 x20 (x8 x14 x15 (x13 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x12 x17 (x9 x18 x19 (x13 x20 x21)))) = x9 x18 x19 (x13 x20 (x8 x14 x15 (x12 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x13 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x9 x14 x15 (x12 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x12 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x8 x14 x15 (x10 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x7 x16 (x12 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x7 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x10 x16 (x10 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x10 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x13 x16 (x10 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x13 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x7 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ False (proof)Theorem 1df9f.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ ∀ x4 : ι → ι → ι → ι . (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ In (x4 x5 x6 x7) x0) ⟶ ∀ x5 : ι → ι → ι → ι . (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x5 x6 x7 x8) x0) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x6 x7 x8) x0) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x7 x8 x9) x0) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0) ⟶ ∀ x9 . In x9 x0 ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ In (x10 x11 x12) x0) ⟶ (∀ x11 . In x11 x0 ⟶ (x10 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x10 x11 x9 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x8 x11 (x10 x11 x12) = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x10 x11 (x8 x11 x12) = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x10 (x7 x12 x11) x11 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ x10 x12 x11 = x10 x13 x11 ⟶ (x12 = x13 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x6 x11 x12 = x10 (x8 x11 x12) (x8 (x8 x11 x9) x9) ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x8 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x8 x11 x11 = x9 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x1 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x5 x9 x11 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x5 x11 x9 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x4 x9 x11 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x5 x11 x13 (x6 x12 (x1 x11 (x5 x13 x12 (x5 x11 x13 (x6 x12 (x1 x11 (x5 x13 x12 (x5 x11 x13 (x6 x12 (x1 x11 (x5 x13 x12 (x5 x11 x13 (x6 x12 (x1 x11 (x5 x13 x12 (x5 x11 x13 (x6 x12 (x1 x11 (x5 x13 x12 x14))))))))))))))))))) = x14 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x4 x11 x13 (x6 x12 (x6 x11 (x5 x13 x12 (x4 x11 x13 (x6 x12 (x6 x11 (x5 x13 x12 (x4 x11 x13 (x6 x12 (x6 x11 (x5 x13 x12 x14))))))))))) = x14 ⟶ False) ⟶ False) ⟶ (x10 x2 x3 = x10 x3 x2 ⟶ False) ⟶ False (proof)Theorem 9c369.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x8 x14 x15 (x12 x16 (x13 x14 (x8 x15 x16 (x8 x14 x15 (x12 x16 (x13 x14 (x8 x15 x16 (x8 x14 x15 (x12 x16 (x13 x14 (x8 x15 x16 (x8 x14 x15 (x12 x16 (x13 x14 (x8 x15 x16 (x8 x14 x15 (x12 x16 (x13 x14 (x8 x15 x16 x17))))))))))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x14 (x8 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x8 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x8 x15 x16 x17))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x12 x14 (x7 x15 (x7 x16 x17)) = x7 x15 (x7 x16 (x12 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x8 x14 x15 (x10 x16 (x7 x17 x18)) = x10 x16 (x7 x17 (x8 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x12 x15 (x10 x16 (x7 x17 x18))) = x10 x16 (x7 x17 (x12 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x12 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x10 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x7 x15 (x10 x16 (x12 x17 x18))) = x10 x16 (x12 x17 (x10 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x10 x15 (x10 x16 (x13 x17 x18))) = x10 x16 (x13 x17 (x10 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x10 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x12 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x9 x14 x15 (x10 x16 (x13 x17 (x10 x18 x19))) = x13 x17 (x10 x18 (x9 x14 x15 (x10 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x7 x16 (x7 x17 (x12 x18 x19))) = x7 x17 (x12 x18 (x8 x14 x15 (x7 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x12 x16 (x8 x17 x18 (x10 x19 x20))) = x8 x17 x18 (x10 x19 (x9 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x8 x14 x15 (x10 x16 (x9 x17 x18 (x10 x19 x20))) = x9 x17 x18 (x10 x19 (x8 x14 x15 (x10 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x12 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x8 x14 x15 (x7 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x10 x16 (x7 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x9 x14 x15 (x10 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x13 x16 (x10 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x9 x14 x15 (x13 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x7 x17 (x8 x18 x19 (x13 x20 x21)))) = x8 x18 x19 (x13 x20 (x9 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x13 x16 (x7 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x13 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x10 x17 (x8 x18 x19 (x13 x20 x21)))) = x8 x18 x19 (x13 x20 (x8 x14 x15 (x7 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x7 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x13 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x12 x16 (x13 x17 x21))))) ⟶ False (proof)Theorem 82388.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x2 x3 x4 x5) x0) ⟶ ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x6 x7 x8) x0) ⟶ ∀ x7 : ι → ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x7 x8 x9 x10) x0) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0) ⟶ ∀ x9 . In x9 x0 ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ In (x10 x11 x12) x0) ⟶ (∀ x11 . In x11 x0 ⟶ (x10 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x10 x11 x9 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x8 (x10 x12 x11) x11 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x10 (x8 x12 x11) x11 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x7 x11 x12 x13 = x8 (x10 (x10 x13 x11) x12) (x10 x11 x12) ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x1 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x6 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x2 x9 x11 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x2 x11 x9 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x7 x11 x12 (x1 x11 (x6 x12 (x7 x11 x12 (x1 x11 (x6 x12 (x7 x11 x12 (x1 x11 (x6 x12 (x7 x11 x12 (x1 x11 (x6 x12 (x7 x11 x12 (x1 x11 (x6 x12 x13)))))))))))))) = x13 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x7 x11 x13 (x1 x12 (x6 x11 (x2 x13 x12 (x7 x11 x13 (x1 x12 (x6 x11 (x2 x13 x12 (x7 x11 x13 (x1 x12 (x6 x11 (x2 x13 x12 (x7 x11 x13 (x1 x12 (x6 x11 (x2 x13 x12 x14))))))))))))))) = x14 ⟶ False) ⟶ False) ⟶ (x10 (x10 x3 x4) x5 = x10 x3 (x10 x4 x5) ⟶ False) ⟶ False (proof)Known 7c609.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ ((∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x1 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x2 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x3 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x7 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ In (x8 x14 x15 x16) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ In (x9 x14 x15 x16) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x10 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x11 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x12 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ In (x13 x14 x15) x0) ⟶ (∀ x14 . In x14 x0 ⟶ x1 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x1 x14 x4 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x2 x14 (x1 x14 x15) = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x1 x14 (x2 x14 x15) = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x3 (x1 x14 x15) x15 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x1 (x3 x14 x15) x15 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x1 x14 x15 = x1 x14 x16 ⟶ x15 = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x1 x14 x15 = x1 x16 x15 ⟶ x14 = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x5 x14 x15 = x2 (x1 x15 x14) (x1 x14 x15)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x6 x14 x15 x16 = x2 (x1 x14 (x1 x15 x16)) (x1 (x1 x14 x15) x16)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x7 x14 x15 = x2 x14 (x1 x15 x14)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x10 x14 x15 = x1 x14 (x1 x15 (x2 x14 x4))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x11 x14 x15 = x1 (x1 (x3 x4 x14) x15) x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x12 x14 x15 = x1 (x2 x14 x15) (x2 (x2 x14 x4) x4)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x13 x14 x15 = x1 (x3 x4 (x3 x4 x14)) (x3 x15 x14)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x8 x14 x15 x16 = x2 (x1 x15 x14) (x1 x15 (x1 x14 x16))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x9 x14 x15 x16 = x3 (x1 (x1 x16 x14) x15) (x1 x14 x15)) ⟶ (∀ x14 . In x14 x0 ⟶ x2 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x2 x14 x14 = x4) ⟶ (∀ x14 . In x14 x0 ⟶ x3 x14 x4 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x3 x14 x14 = x4) ⟶ (∀ x14 . In x14 x0 ⟶ x7 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x10 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x11 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x12 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ x13 x4 x14 = x14) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x8 x4 x14 x15 = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x8 x14 x4 x15 = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x9 x4 x14 x15 = x15) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x9 x14 x4 x15 = x15) ⟶ ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x1 x14 (x1 x15 x16) = x1 (x1 x14 x15) x16) ⟶ FalseKnown 15e97..eq_sym_i : ∀ x0 x1 . x0 = x1 ⟶ x1 = x0Theorem 36b47.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x9 x14 x15 (x7 x14 (x10 x15 (x9 x14 x15 (x7 x14 (x10 x15 (x9 x14 x15 (x7 x14 (x10 x15 (x9 x14 x15 (x7 x14 (x10 x15 (x9 x14 x15 (x7 x14 (x10 x15 x16)))))))))))))) = x16) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x7 x16 (x10 x14 (x8 x15 x16 (x9 x14 x15 (x7 x16 (x10 x14 (x8 x15 x16 (x9 x14 x15 (x7 x16 (x10 x14 (x8 x15 x16 (x9 x14 x15 (x7 x16 (x10 x14 (x8 x15 x16 x17))))))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x12 x14 (x12 x15 (x12 x16 x17)) = x12 x15 (x12 x16 (x12 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x8 x14 x15 (x12 x16 (x7 x17 x18)) = x12 x16 (x7 x17 (x8 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x10 x15 (x7 x16 (x10 x17 x18))) = x7 x16 (x10 x17 (x10 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x7 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x12 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x12 x15 (x12 x16 (x13 x17 x18))) = x12 x16 (x13 x17 (x12 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x12 x15 (x7 x16 (x7 x17 x18))) = x7 x16 (x7 x17 (x7 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x7 x15 (x13 x16 (x10 x17 x18))) = x13 x16 (x10 x17 (x7 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x10 x16 (x7 x17 (x7 x18 x19))) = x7 x17 (x7 x18 (x8 x14 x15 (x10 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x12 x16 (x12 x17 (x10 x18 x19))) = x12 x17 (x10 x18 (x8 x14 x15 (x12 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x7 x16 (x9 x17 x18 (x10 x19 x20))) = x9 x17 x18 (x10 x19 (x9 x14 x15 (x7 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x8 x14 x15 (x7 x16 (x9 x17 x18 (x7 x19 x20))) = x9 x17 x18 (x7 x19 (x8 x14 x15 (x7 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x12 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x10 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x10 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x12 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x10 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x8 x14 x15 (x7 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x13 x16 (x13 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x8 x14 x15 (x13 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x7 x16 (x12 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x9 x14 x15 (x7 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x12 x17 (x9 x18 x19 (x13 x20 x21)))) = x9 x18 x19 (x13 x20 (x8 x14 x15 (x10 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x12 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x7 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x10 x16 (x12 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x10 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x13 x17 (x8 x18 x19 (x13 x20 x21)))) = x8 x18 x19 (x13 x20 (x9 x14 x15 (x12 x16 (x13 x17 x21))))) ⟶ False (proof)Theorem 5d2a3.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ In (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x3 x4 x5) x0) ⟶ ∀ x4 : ι → ι → ι → ι . (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ In (x4 x5 x6 x7) x0) ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ ∀ x7 : ι → ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x7 x8 x9 x10) x0) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0) ⟶ ∀ x9 . In x9 x0 ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ In (x10 x11 x12) x0) ⟶ (∀ x11 . In x11 x0 ⟶ (x10 x11 x9 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x1 (x10 x12 x11) x11 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x10 (x1 x12 x11) x11 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x2 x11 x12 = x10 (x1 x9 (x1 x9 x11)) (x1 x12 x11) ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x1 x11 x11 = x9 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x3 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ (x8 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x4 x11 x9 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x7 x9 x11 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x7 x11 x13 (x2 x12 (x8 x11 (x7 x13 x12 (x7 x11 x13 (x2 x12 (x8 x11 (x7 x13 x12 x14))))))) = x14 ⟶ False) ⟶ False) ⟶ (∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x4 x11 x13 (x3 x12 (x2 x11 (x4 x13 x12 (x4 x11 x13 (x3 x12 (x2 x11 (x4 x13 x12 (x4 x11 x13 (x3 x12 (x2 x11 (x4 x13 x12 x14))))))))))) = x14 ⟶ False) ⟶ False) ⟶ (x10 x5 x6 = x10 x6 x5 ⟶ False) ⟶ False (proof)Theorem 9ce88.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x13 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x13 x16 (x12 x14 (x9 x15 x16 x17))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x8 x14 x15 (x10 x16 (x13 x14 (x8 x15 x16 (x8 x14 x15 (x10 x16 (x13 x14 (x8 x15 x16 (x8 x14 x15 (x10 x16 (x13 x14 (x8 x15 x16 x17))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x10 x14 (x7 x15 (x10 x16 x17)) = x7 x15 (x10 x16 (x10 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x8 x14 x15 (x7 x16 (x12 x17 x18)) = x7 x16 (x12 x17 (x8 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x7 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x13 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x10 x15 (x12 x16 (x12 x17 x18))) = x12 x16 (x12 x17 (x12 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x12 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x12 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x12 x15 (x10 x16 (x7 x17 x18))) = x10 x16 (x7 x17 (x13 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x13 x15 (x13 x16 (x12 x17 x18))) = x13 x16 (x12 x17 (x12 x14 (x13 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x10 x16 (x10 x17 (x13 x18 x19))) = x10 x17 (x13 x18 (x8 x14 x15 (x10 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x13 x16 (x12 x17 (x10 x18 x19))) = x12 x17 (x10 x18 (x8 x14 x15 (x13 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x12 x16 (x9 x17 x18 (x12 x19 x20))) = x9 x17 x18 (x12 x19 (x9 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x12 x16 (x8 x17 x18 (x12 x19 x20))) = x8 x17 x18 (x12 x19 (x9 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x10 x17 (x8 x18 x19 (x7 x20 x21)))) = x8 x18 x19 (x7 x20 (x8 x14 x15 (x10 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x13 x16 (x7 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x9 x14 x15 (x13 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x13 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x8 x14 x15 (x7 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x10 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x8 x14 x15 (x10 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x13 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x7 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x10 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x7 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x13 x16 (x13 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x13 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x10 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x7 x17 (x8 x18 x19 (x13 x20 x21)))) = x8 x18 x19 (x13 x20 (x8 x14 x15 (x7 x16 (x7 x17 x21))))) ⟶ False (proof)Theorem 74b5f.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 : ι → ι → ι → ι . (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x5 x6 x7 x8) x0) ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x6 x7 x8 x9) x0) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x7 x8 x9) x0) ⟶ ∀ x8 . In x8 x0 ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ In (x9 x10 x11) x0) ⟶ (∀ x10 . In x10 x0 ⟶ (x9 x8 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ (x9 x10 x8 = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x7 (x9 x11 x10) x10 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x9 (x7 x11 x10) x10 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x6 x10 x11 x12 = x7 (x9 (x9 x12 x10) x11) (x9 x10 x11) ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ (x1 x8 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x5 x8 x10 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x5 x10 x8 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x6 x10 x12 (x1 x11 (x1 x10 (x5 x12 x11 (x6 x10 x12 (x1 x11 (x1 x10 (x5 x12 x11 (x6 x10 x12 (x1 x11 (x1 x10 (x5 x12 x11 x13))))))))))) = x13 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x6 x10 x12 (x1 x11 (x1 x10 (x6 x12 x11 (x6 x10 x12 (x1 x11 (x1 x10 (x6 x12 x11 (x6 x10 x12 (x1 x11 (x1 x10 (x6 x12 x11 (x6 x10 x12 (x1 x11 (x1 x10 (x6 x12 x11 x13))))))))))))))) = x13 ⟶ False) ⟶ False) ⟶ (x9 (x9 x2 x3) x4 = x9 x2 (x9 x3 x4) ⟶ False) ⟶ False (proof)Theorem f0370.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x14 (x8 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x8 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x8 x15 x16 x17))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 x17))))))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x7 x14 (x10 x15 (x12 x16 x17)) = x10 x15 (x12 x16 (x7 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x8 x14 x15 (x12 x16 (x13 x17 x18)) = x12 x16 (x13 x17 (x8 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x12 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x12 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x12 x15 (x12 x16 (x10 x17 x18))) = x12 x16 (x10 x17 (x13 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x10 x14 (x7 x15 (x13 x16 (x13 x17 x18))) = x13 x16 (x13 x17 (x10 x14 (x7 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x10 x15 (x12 x16 (x12 x17 x18))) = x12 x16 (x12 x17 (x7 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x12 x14 (x13 x15 (x7 x16 (x7 x17 x18))) = x7 x16 (x7 x17 (x12 x14 (x13 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x8 x14 x15 (x13 x16 (x10 x17 (x13 x18 x19))) = x10 x17 (x13 x18 (x8 x14 x15 (x13 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x17 (x12 x18 x19))) = x12 x17 (x12 x18 (x9 x14 x15 (x12 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x12 x16 (x8 x17 x18 (x7 x19 x20))) = x8 x17 x18 (x7 x19 (x9 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x10 x16 (x8 x17 x18 (x12 x19 x20))) = x8 x17 x18 (x12 x19 (x9 x14 x15 (x10 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x10 x16 (x7 x17 (x9 x18 x19 (x13 x20 x21)))) = x9 x18 x19 (x13 x20 (x9 x14 x15 (x10 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x10 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x10 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x9 x14 x15 (x12 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x7 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x7 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x10 x16 (x7 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x8 x14 x15 (x10 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x17 (x9 x18 x19 (x13 x20 x21)))) = x9 x18 x19 (x13 x20 (x9 x14 x15 (x12 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x7 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x13 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x8 x14 x15 (x12 x16 (x13 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x10 x16 (x7 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x10 x16 (x7 x17 x21))))) ⟶ False (proof)Theorem edd28.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x2 x3 x4 x5) x0) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x3 x4 x5) x0) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ In (x4 x5 x6) x0) ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ ∀ x8 : ι → ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ In (x8 x9 x10 x11) x0) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ In (x9 x10 x11) x0) ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ In (x11 x12 x13) x0) ⟶ (∀ x12 . In x12 x0 ⟶ (x11 x12 x10 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x1 (x11 x13 x12) x12 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x11 (x1 x13 x12) x12 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ (x2 x12 x13 x14 = x1 (x11 (x11 x14 x12) x13) (x11 x12 x13) ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ (x9 x10 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ (x3 x10 x12 = x12 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x8 x12 x10 x13 = x13 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 x15))))))))))))))) = x15 ⟶ False) ⟶ False) ⟶ (∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ (x2 x12 x14 (x3 x13 (x4 x12 (x2 x14 x13 (x2 x12 x14 (x3 x13 (x4 x12 (x2 x14 x13 (x2 x12 x14 (x3 x13 (x4 x12 (x2 x14 x13 x15))))))))))) = x15 ⟶ False) ⟶ False) ⟶ (x11 (x11 x7 x6) x5 = x11 x7 (x11 x6 x5) ⟶ False) ⟶ False (proof)Theorem fdf62.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ In x4 x0 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x10 x16 (x7 x14 (x8 x15 x16 (x9 x14 x15 (x10 x16 (x7 x14 (x8 x15 x16 (x9 x14 x15 (x10 x16 (x7 x14 (x8 x15 x16 (x9 x14 x15 (x10 x16 (x7 x14 (x8 x15 x16 x17))))))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x9 x14 x15 (x12 x16 (x7 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x7 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x7 x14 (x9 x15 x16 x17))))))))))) = x17) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x12 x14 (x7 x15 (x12 x16 x17)) = x7 x15 (x12 x16 (x12 x14 x17))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x9 x14 x15 (x10 x16 (x13 x17 x18)) = x10 x16 (x13 x17 (x9 x14 x15 x18))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x12 x15 (x7 x16 (x7 x17 x18))) = x7 x16 (x7 x17 (x13 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x10 x15 (x7 x16 (x7 x17 x18))) = x7 x16 (x7 x17 (x7 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x12 x15 (x7 x16 (x10 x17 x18))) = x7 x16 (x10 x17 (x13 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x7 x14 (x12 x15 (x7 x16 (x10 x17 x18))) = x7 x16 (x10 x17 (x7 x14 (x12 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ x13 x14 (x10 x15 (x13 x16 (x12 x17 x18))) = x13 x16 (x12 x17 (x13 x14 (x10 x15 x18)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x9 x14 x15 (x12 x16 (x10 x17 (x7 x18 x19))) = x10 x17 (x7 x18 (x9 x14 x15 (x12 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ x9 x14 x15 (x7 x16 (x10 x17 (x7 x18 x19))) = x10 x17 (x7 x18 (x9 x14 x15 (x7 x16 x19)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x8 x14 x15 (x12 x16 (x8 x17 x18 (x7 x19 x20))) = x8 x17 x18 (x7 x19 (x8 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ x9 x14 x15 (x12 x16 (x8 x17 x18 (x10 x19 x20))) = x8 x17 x18 (x10 x19 (x9 x14 x15 (x12 x16 x20)))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x7 x16 (x7 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x9 x14 x15 (x7 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x12 x16 (x12 x17 (x9 x18 x19 (x13 x20 x21)))) = x9 x18 x19 (x13 x20 (x9 x14 x15 (x12 x16 (x12 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x7 x16 (x7 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x8 x14 x15 (x7 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x7 x17 (x8 x18 x19 (x13 x20 x21)))) = x8 x18 x19 (x13 x20 (x8 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x7 x17 (x8 x18 x19 (x12 x20 x21)))) = x8 x18 x19 (x12 x20 (x8 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x13 x16 (x7 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x9 x14 x15 (x13 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x8 x14 x15 (x12 x16 (x7 x17 (x8 x18 x19 (x7 x20 x21)))) = x8 x18 x19 (x7 x20 (x8 x14 x15 (x12 x16 (x7 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x7 x16 (x10 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x9 x14 x15 (x7 x16 (x10 x17 x21))))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ ∀ x20 . In x20 x0 ⟶ ∀ x21 . In x21 x0 ⟶ x9 x14 x15 (x7 x16 (x7 x17 (x9 x18 x19 (x7 x20 x21)))) = x9 x18 x19 (x7 x20 (x9 x14 x15 (x7 x16 (x7 x17 x21))))) ⟶ False (proof)
|
|