Proofgold Proposition

∀ x0 x1 x2 . atleastp (setsum (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x1 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x1 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod x1 x2))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) x1)) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) x2)) (setsum (setprod c0b45.. (setexp x0 50a6b..)) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x1 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x1 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod x1 x2))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) x1)) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) x2)) (setsum (setprod c0b45.. (setexp x0 33cc2..)) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 50a6b..) x2))) (setsum (setprod c0b45.. (setprod x0 (setexp x1 50a6b..))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 33cc2..) x2))) (setsum (setprod c0b45.. (setprod x0 (setexp x1 33cc2..))) (setsum (setprod c0b45.. (setprod x0 (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod x0 (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod x0 (setprod x1 x2))) (setsum (setprod c0b45.. (setprod x0 x1)) (setsum (setprod c0b45.. (setprod x0 (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod x0 (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod x0 x2)) (setsum (setprod c0b45.. x0) (setsum (setprod c0b45.. (setprod (setexp x1 50a6b..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x1 50a6b..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x1 50a6b..) x2)) (setsum (setprod c0b45.. (setexp x1 50a6b..)) (setsum (setprod c0b45.. (setprod (setexp x1 33cc2..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x1 33cc2..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x1 33cc2..) x2)) (setsum (setprod c0b45.. (setexp x1 33cc2..)) (setsum (setprod c0b45.. (setprod x1 (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod x1 (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod x1 x2)) (setsum (setprod c0b45.. x1) (setsum (setprod c0b45.. (setexp x2 50a6b..)) (setsum (setprod c0b45.. (setexp x2 33cc2..)) (setsum (setprod c0b45.. x2) c0b45..))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 6a551..) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x1 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x1 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setprod x1 x2))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) x1)) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 50a6b..) x2)) (setsum (setprod c0b45.. (setexp x0 50a6b..)) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x1 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x1 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setprod x1 x2))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) x1)) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x0 33cc2..) x2)) (setsum (setprod c0b45.. (setexp x0 33cc2..)) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 50a6b..) x2))) (setsum (setprod c0b45.. (setprod x0 (setexp x1 50a6b..))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod x0 (setprod (setexp x1 33cc2..) x2))) (setsum (setprod c0b45.. (setprod x0 (setexp x1 33cc2..))) (setsum (setprod c0b45.. (setprod x0 (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod c0b45.. (setprod x0 (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod c0b45.. (setprod x0 (setprod x1 x2))) (setsum (setprod c0b45.. (setprod x0 x1)) (setsum (setprod c0b45.. (setprod x0 (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod x0 (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod x0 x2)) (setsum (setprod c0b45.. x0) (setsum (setprod c0b45.. (setprod (setexp x1 50a6b..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x1 50a6b..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x1 50a6b..) x2)) (setsum (setprod c0b45.. (setexp x1 50a6b..)) (setsum (setprod c0b45.. (setprod (setexp x1 33cc2..) (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod (setexp x1 33cc2..) (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod (setexp x1 33cc2..) x2)) (setsum (setprod c0b45.. (setexp x1 33cc2..)) (setsum (setprod c0b45.. (setprod x1 (setexp x2 50a6b..))) (setsum (setprod c0b45.. (setprod x1 (setexp x2 33cc2..))) (setsum (setprod c0b45.. (setprod x1 x2)) (setsum (setprod c0b45.. x1) (setsum (setprod c0b45.. (setexp x2 50a6b..)) (setsum (setprod c0b45.. (setexp x2 33cc2..)) (setsum (setprod c0b45.. x2) c0b45..))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ⟶ False

type
prop

theory
HF

name
-

proof
PUbQq..

Megalodon
-

proofgold address
TMXhz..

creator
3149 PrGxv../5bbf8..

owner
3177 PrGxv../168fa..

term root
c46d6..