MODULE ( HEADER ( SPEC ( NAME ("prophilbert3"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("Further Theorems of Propositional Calculus"), DESCRIPTION ( "This module includes proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)" ), EMAIL ("module@qedeq.org"), AUTHORS ( AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org")) ) ), IMPORTS ( IMPORT ( SPEC ( NAME ("prophilbert2"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ) ), USEDBY ( SPEC ( NAME ("predtheo2"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION (".") ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("hilb36"), "First distributive law (first direction):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(1)), ADDSENTENCE ( LINK ("hilb24")) ), LINE ( IMPL(AND(PROP(1), PROP(3)), PROP(1)), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(AND(PROP(4), PROP(3)), PROP(4)), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(AND(PROP(2), PROP(3)), PROP(2)), REPLACEPROP ( 3, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(2)))), REPLACEPROP ( 5, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 6, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 7, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 8, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(2)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(2)))), REPLACEPROP ( 9, PROP(5), PROP(2) ) ), LINE ( IMPL(IMPL(AND(PROP(2), PROP(3)), PROP(2)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 10, PROP(6), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2))), MODUSPONENS (4, 11) ), LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(2)), ADDSENTENCE ( LINK ("hilb25")) ), LINE ( IMPL(AND(PROP(1), PROP(3)), PROP(3)), REPLACEPROP ( 13, PROP(2), PROP(3) ) ), LINE ( IMPL(AND(PROP(4), PROP(3)), PROP(3)), REPLACEPROP ( 14, PROP(1), PROP(4) ) ), LINE ( IMPL(AND(PROP(2), PROP(3)), PROP(3)), REPLACEPROP ( 15, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(3)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(3)))), REPLACEPROP ( 9, PROP(5), PROP(3) ) ), LINE ( IMPL(IMPL(AND(PROP(2), PROP(3)), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3)))), REPLACEPROP ( 17, PROP(6), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3))), MODUSPONENS (16, 18) ), LINE ( IMPL(PROP(1), IMPL(PROP(2), AND(PROP(1), PROP(2)))), ADDSENTENCE ( LINK ("hilb28")) ), LINE ( IMPL(PROP(1), IMPL(PROP(3), AND(PROP(1), PROP(3)))), REPLACEPROP ( 20, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(4), IMPL(PROP(3), AND(PROP(4), PROP(3)))), REPLACEPROP ( 21, PROP(1), PROP(4) ) ), LINE ( IMPL(PROP(4), IMPL(OR(PROP(1), PROP(3)), AND(PROP(4), OR(PROP(1), PROP(3))))), REPLACEPROP ( 22, PROP(3), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), REPLACEPROP ( 23, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(2)))), REPLACEPROP ( 25, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 26, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 27, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(5)))), REPLACEPROP ( 28, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 29, PROP(5), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 30, PROP(6), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), MODUSPONENS (24, 31) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (12, 32) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb16")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(4))), IMPL(PROP(2), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 34, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 35, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(6), PROP(4)))), REPLACEPROP ( 36, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(PROP(5), IMPL(PROP(6), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 37, PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(6), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 38, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 39, PROP(6), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (33, 40) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 29, PROP(5), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 42, PROP(6), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), MODUSPONENS (41, 43) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (19, 44) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(2))), IMPL(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("hilb33")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), PROP(3))), REPLACEPROP ( 46, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), IMPL(PROP(4), PROP(3))), IMPL(PROP(4), PROP(3))), REPLACEPROP ( 47, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), IMPL(PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), REPLACEPROP ( 48, PROP(3), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), REPLACEPROP ( 49, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), MODUSPONENS (45, 50) ) ) ) ), PARAGRAPH ( LABEL ("hilb37"), "First distributive law (second direction):", PROPOSITION ( SENTENCE ( IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))) ), PROOF ( LINE ( IMPL(PROP(1), IMPL(PROP(2), AND(PROP(1), PROP(2)))), ADDSENTENCE ( LINK ("hilb28")) ), LINE ( IMPL(PROP(1), IMPL(PROP(3), AND(PROP(1), PROP(3)))), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(4), IMPL(PROP(3), AND(PROP(4), PROP(3)))), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(PROP(2), IMPL(PROP(3), AND(PROP(2), PROP(3)))), REPLACEPROP ( 3, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(2)))), REPLACEPROP ( 5, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 6, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 7, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 8, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 9, PROP(5), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(3), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 10, PROP(6), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(2)))), REPLACEPROP ( 12, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 13, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 14, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(2), PROP(6)), IMPL(PROP(2), PROP(5)))), REPLACEPROP ( 15, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(PROP(2), PROP(6)), IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 16, PROP(5), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(PROP(3), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(PROP(2), IMPL(PROP(3), AND(PROP(2), PROP(3)))), IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 17, PROP(6), IMPL(PROP(3), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(2), IMPL(PROP(3), AND(PROP(2), PROP(3)))), IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (11, 18) ), LINE ( IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (4, 19) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb16")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(4))), IMPL(PROP(2), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 21, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 22, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(6), PROP(4)))), REPLACEPROP ( 23, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(PROP(5), IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 24, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 25, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 26, PROP(6), PROP(2) ) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (20, 27) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 9, PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 29, PROP(6), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), PROP(3)), PROP(6)), IMPL(OR(PROP(1), PROP(3)), PROP(5)))), REPLACEPROP ( 15, PROP(4), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), PROP(6)), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 31, PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 32, PROP(6), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))))), MODUSPONENS (30, 33) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (28, 34) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))), ADDSENTENCE ( LINK ("hilb14")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(4))), OR(OR(PROP(1), PROP(2)), PROP(4))), REPLACEPROP ( 36, PROP(3), PROP(4) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(5), PROP(4))), OR(OR(PROP(1), PROP(5)), PROP(4))), REPLACEPROP ( 37, PROP(2), PROP(5) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(4))), OR(OR(PROP(6), PROP(5)), PROP(4))), REPLACEPROP ( 38, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), AND(PROP(2), PROP(3)))), OR(OR(PROP(6), PROP(5)), AND(PROP(2), PROP(3)))), REPLACEPROP ( 39, PROP(4), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))), OR(OR(PROP(6), PROP(1)), AND(PROP(2), PROP(3)))), REPLACEPROP ( 40, PROP(5), PROP(1) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), REPLACEPROP ( 41, PROP(6), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))), ADDSENTENCE ( LINK ("defimpl1")) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("defimpl2")) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(OR(PROP(1), PROP(2))), PROP(6)), OR(NOT(OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 8, PROP(4), NOT(OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), PROP(6)), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 45, PROP(5), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 46, PROP(6), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), MODUSPONENS (42, 47) ), LINE ( IMPL(IMPL(PROP(1), PROP(4)), OR(NOT(PROP(1)), PROP(4))), REPLACEPROP ( 43, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(4)), OR(NOT(PROP(5)), PROP(4))), REPLACEPROP ( 49, PROP(1), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(5), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(PROP(5)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 50, PROP(4), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 51, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), PROP(5)))), REPLACEPROP ( 15, PROP(4), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 53, PROP(5), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 54, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), MODUSPONENS (48, 55) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), MODUSPONENS (52, 56) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(4)), IMPL(PROP(1), PROP(4))), REPLACEPROP ( 44, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(NOT(PROP(5)), PROP(4)), IMPL(PROP(5), PROP(4))), REPLACEPROP ( 58, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(PROP(5), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), REPLACEPROP ( 59, PROP(4), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), REPLACEPROP ( 60, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 53, PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 62, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), MODUSPONENS (61, 63) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), MODUSPONENS (57, 64) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(OR(PROP(1), PROP(3))), PROP(6)), OR(NOT(OR(PROP(1), PROP(3))), PROP(5)))), REPLACEPROP ( 8, PROP(4), NOT(OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(NOT(OR(PROP(1), PROP(3))), PROP(6)), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 66, PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 67, PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), MODUSPONENS (65, 68) ), LINE ( IMPL(IMPL(PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(PROP(5)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 50, PROP(4), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 70, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), PROP(5)))), REPLACEPROP ( 15, PROP(4), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 72, PROP(5), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 73, PROP(6), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), MODUSPONENS (69, 74) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), MODUSPONENS (71, 75) ), LINE ( IMPL(OR(NOT(PROP(5)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 59, PROP(4), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 77, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 72, PROP(5), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 79, PROP(6), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))))), MODUSPONENS (78, 80) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), MODUSPONENS (76, 81) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), MODUSPONENS (35, 82) ), LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("hilb11")) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(AND(PROP(2), PROP(3)), PROP(6)), OR(AND(PROP(2), PROP(3)), PROP(5)))), REPLACEPROP ( 8, PROP(4), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(1)), IMPL(OR(AND(PROP(2), PROP(3)), PROP(6)), OR(AND(PROP(2), PROP(3)), PROP(1)))), REPLACEPROP ( 85, PROP(5), PROP(1) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(1)), PROP(1)), IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(AND(PROP(2), PROP(3)), PROP(1)))), REPLACEPROP ( 86, PROP(6), OR(PROP(1), PROP(1)) ) ), LINE ( IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(AND(PROP(2), PROP(3)), PROP(1))), MODUSPONENS (84, 87) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(PROP(1), PROP(4)), OR(PROP(4), PROP(1))), REPLACEPROP ( 89, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(PROP(5), PROP(4)), OR(PROP(4), PROP(5))), REPLACEPROP ( 90, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(PROP(5), PROP(1)), OR(PROP(1), PROP(5))), REPLACEPROP ( 91, PROP(4), PROP(1) ) ), LINE ( IMPL(OR(AND(PROP(2), PROP(3)), PROP(1)), OR(PROP(1), AND(PROP(2), PROP(3)))), REPLACEPROP ( 92, PROP(5), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), PROP(6)), IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), PROP(5)))), REPLACEPROP ( 15, PROP(4), OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), PROP(6)), IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 94, PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(AND(PROP(2), PROP(3)), PROP(1)), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(AND(PROP(2), PROP(3)), PROP(1))), IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 95, PROP(6), OR(AND(PROP(2), PROP(3)), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(AND(PROP(2), PROP(3)), PROP(1))), IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (93, 96) ), LINE ( IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(PROP(1), AND(PROP(2), PROP(3)))), MODUSPONENS (88, 97) ), LINE ( IMPL(OR(PROP(5), AND(PROP(2), PROP(3))), OR(AND(PROP(2), PROP(3)), PROP(5))), REPLACEPROP ( 91, PROP(4), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1)))), REPLACEPROP ( 99, PROP(5), OR(PROP(1), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), PROP(5)))), REPLACEPROP ( 15, PROP(4), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 101, PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1)))), IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 102, PROP(6), OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(AND(PROP(2), PROP(3)), OR(PROP(1), PROP(1)))), IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (98, 103) ), LINE ( IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), MODUSPONENS (100, 104) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), PROP(6)), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 45, PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 106, PROP(6), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (105, 107) ), LINE ( IMPL(IMPL(PROP(5), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(PROP(5)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), REPLACEPROP ( 50, PROP(4), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), REPLACEPROP ( 109, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), PROP(5)))), REPLACEPROP ( 15, PROP(4), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 111, PROP(5), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 112, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (108, 113) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (110, 114) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 59, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 116, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 111, PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 118, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), OR(NOT(OR(PROP(1), PROP(2))), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (117, 119) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (115, 120) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(NOT(OR(PROP(1), PROP(3))), PROP(6)), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 66, PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 122, PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (121, 123) ), LINE ( IMPL(IMPL(PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(PROP(5)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 50, PROP(4), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 125, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), PROP(5)))), REPLACEPROP ( 15, PROP(4), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 127, PROP(5), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 128, PROP(6), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))))), MODUSPONENS (124, 129) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (126, 130) ), LINE ( IMPL(OR(NOT(PROP(5)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 59, PROP(4), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 132, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 127, PROP(5), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 134, PROP(6), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), OR(NOT(OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))))), MODUSPONENS (133, 135) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (131, 136) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (83, 137) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 25, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 139, PROP(6), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (138, 140) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(AND(PROP(1), PROP(2)), PROP(3))), ADDSENTENCE ( LINK ("hilb29")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(4))), IMPL(AND(PROP(1), PROP(2)), PROP(4))), REPLACEPROP ( 142, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(AND(PROP(1), PROP(5)), PROP(4))), REPLACEPROP ( 143, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(AND(PROP(6), PROP(5)), PROP(4))), REPLACEPROP ( 144, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(AND(PROP(6), PROP(5)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 145, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(AND(PROP(6), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 146, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 147, PROP(6), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), MODUSPONENS (141, 148) ) ) ) ), PARAGRAPH ( LABEL ("hilb38"), "A form for the abbreviation rule form for disjunction (first direction):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(2)), NOT(AND(NOT(PROP(1)), NOT(PROP(2))))) ), PROOF ( LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb5")) ), LINE ( IMPL(PROP(3), NOT(NOT(PROP(3)))), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), REPLACEPROP ( 2, PROP(3), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))), ADDSENTENCE ( LINK ("defimpl1")) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("defimpl2")) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), OR(NOT(PROP(1)), PROP(3))), REPLACEPROP ( 4, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), OR(NOT(PROP(4)), PROP(3))), REPLACEPROP ( 6, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(2)))), REPLACEPROP ( 8, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 9, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 10, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(3)), IMPL(PROP(1), PROP(3))), REPLACEPROP ( 5, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(NOT(PROP(4)), PROP(3)), IMPL(PROP(4), PROP(3))), REPLACEPROP ( 12, PROP(1), PROP(4) ) ), LINE ( IMPL(PROP(2), NOT(NOT(PROP(2)))), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(2)))), REPLACEPROP ( 15, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 16, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 17, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(2), PROP(6)), OR(PROP(2), PROP(5)))), REPLACEPROP ( 18, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(PROP(1)))), IMPL(OR(PROP(2), PROP(6)), OR(PROP(2), NOT(NOT(PROP(1)))))), REPLACEPROP ( 19, PROP(5), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(1), NOT(NOT(PROP(1)))), IMPL(OR(PROP(2), PROP(1)), OR(PROP(2), NOT(NOT(PROP(1)))))), REPLACEPROP ( 20, PROP(6), PROP(1) ) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(2), NOT(NOT(PROP(1))))), MODUSPONENS (1, 21) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(PROP(1), PROP(3)), OR(PROP(3), PROP(1))), REPLACEPROP ( 23, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(4), PROP(3)), OR(PROP(3), PROP(4))), REPLACEPROP ( 24, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(PROP(4), NOT(NOT(PROP(1)))), OR(NOT(NOT(PROP(1))), PROP(4))), REPLACEPROP ( 25, PROP(3), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(NOT(NOT(PROP(1))), PROP(2))), REPLACEPROP ( 26, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(2), PROP(1)), PROP(6)), IMPL(OR(PROP(2), PROP(1)), PROP(5)))), REPLACEPROP ( 11, PROP(4), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(IMPL(OR(PROP(2), PROP(1)), PROP(6)), IMPL(OR(PROP(2), PROP(1)), OR(NOT(NOT(PROP(1))), PROP(2))))), REPLACEPROP ( 28, PROP(5), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(IMPL(OR(PROP(2), PROP(1)), OR(PROP(2), NOT(NOT(PROP(1))))), IMPL(OR(PROP(2), PROP(1)), OR(NOT(NOT(PROP(1))), PROP(2))))), REPLACEPROP ( 29, PROP(6), OR(PROP(2), NOT(NOT(PROP(1)))) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(1)), OR(PROP(2), NOT(NOT(PROP(1))))), IMPL(OR(PROP(2), PROP(1)), OR(NOT(NOT(PROP(1))), PROP(2)))), MODUSPONENS (27, 30) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(NOT(NOT(PROP(1))), PROP(2))), MODUSPONENS (22, 31) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), PROP(2)), PROP(6)), IMPL(OR(PROP(1), PROP(2)), PROP(5)))), REPLACEPROP ( 11, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(IMPL(OR(PROP(1), PROP(2)), PROP(6)), IMPL(OR(PROP(1), PROP(2)), OR(NOT(NOT(PROP(1))), PROP(2))))), REPLACEPROP ( 33, PROP(5), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(1)), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(OR(PROP(1), PROP(2)), OR(NOT(NOT(PROP(1))), PROP(2))))), REPLACEPROP ( 34, PROP(6), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(OR(PROP(1), PROP(2)), OR(NOT(NOT(PROP(1))), PROP(2)))), MODUSPONENS (32, 35) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(NOT(NOT(PROP(1))), PROP(2))), MODUSPONENS (23, 36) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(1)))), REPLACEPROP ( 38, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(4)))), REPLACEPROP ( 39, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(PROP(4)))), REPLACEPROP ( 40, PROP(3), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(PROP(1), PROP(2))))), REPLACEPROP ( 41, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(PROP(1), PROP(2)))), MODUSPONENS (37, 42) ), LINE ( IMPL(IMPL(PROP(4), NOT(OR(PROP(1), PROP(2)))), IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(PROP(4)))), REPLACEPROP ( 40, PROP(3), NOT(OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(PROP(1), PROP(2)))), IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), REPLACEPROP ( 44, PROP(4), NOT(OR(NOT(NOT(PROP(1))), PROP(2))) ) ), LINE ( IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), MODUSPONENS (43, 45) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(OR(PROP(1), PROP(2))), PROP(6)), OR(NOT(OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 18, PROP(4), NOT(OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), PROP(6)), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), REPLACEPROP ( 47, PROP(5), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), REPLACEPROP ( 48, PROP(6), NOT(NOT(OR(PROP(1), PROP(2)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), MODUSPONENS (46, 49) ), LINE ( IMPL(IMPL(PROP(4), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(PROP(4)), NOT(NOT(OR(PROP(1), PROP(2)))))), REPLACEPROP ( 7, PROP(3), NOT(NOT(OR(PROP(1), PROP(2)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2)))))), REPLACEPROP ( 51, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), PROP(5)))), REPLACEPROP ( 11, PROP(4), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))))), REPLACEPROP ( 53, PROP(5), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))))), REPLACEPROP ( 54, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(PROP(1), PROP(2)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), MODUSPONENS (50, 55) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), MODUSPONENS (52, 56) ), LINE ( IMPL(OR(NOT(PROP(4)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), REPLACEPROP ( 13, PROP(3), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), REPLACEPROP ( 58, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))))), REPLACEPROP ( 53, PROP(5), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))))), REPLACEPROP ( 60, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), MODUSPONENS (59, 61) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), MODUSPONENS (57, 62) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), MODUSPONENS (3, 63) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(NOT(PROP(1))), PROP(6)), OR(NOT(NOT(PROP(1))), PROP(5)))), REPLACEPROP ( 18, PROP(4), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(PROP(2)))), IMPL(OR(NOT(NOT(PROP(1))), PROP(6)), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), REPLACEPROP ( 65, PROP(5), NOT(NOT(PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(2), NOT(NOT(PROP(2)))), IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), REPLACEPROP ( 66, PROP(6), PROP(2) ) ), LINE ( IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), MODUSPONENS (14, 67) ), LINE ( IMPL(IMPL(PROP(4), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), IMPL(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), NOT(PROP(4)))), REPLACEPROP ( 40, PROP(3), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), IMPL(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), REPLACEPROP ( 69, PROP(4), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), MODUSPONENS (68, 70) ), LINE ( IMPL(IMPL(PROP(4), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(PROP(4)))), REPLACEPROP ( 40, PROP(3), NOT(OR(NOT(NOT(PROP(1))), PROP(2))) ) ), LINE ( IMPL(IMPL(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), REPLACEPROP ( 72, PROP(4), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))) ) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), MODUSPONENS (71, 73) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), PROP(6)), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), REPLACEPROP ( 47, PROP(5), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))) ) ), LINE ( IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), REPLACEPROP ( 75, PROP(6), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), MODUSPONENS (74, 76) ), LINE ( IMPL(IMPL(PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(PROP(4)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), REPLACEPROP ( 7, PROP(3), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), REPLACEPROP ( 78, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), PROP(5)))), REPLACEPROP ( 11, PROP(4), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))))), REPLACEPROP ( 80, PROP(5), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))))), REPLACEPROP ( 81, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), MODUSPONENS (77, 82) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), MODUSPONENS (79, 83) ), LINE ( IMPL(OR(NOT(PROP(4)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), IMPL(PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), REPLACEPROP ( 13, PROP(3), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), REPLACEPROP ( 85, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), PROP(6)), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))))), REPLACEPROP ( 80, PROP(5), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))))), REPLACEPROP ( 87, PROP(6), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(NOT(OR(PROP(1), PROP(2))), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), MODUSPONENS (86, 88) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), MODUSPONENS (84, 89) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), MODUSPONENS (64, 90) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(AND(NOT(PROP(1)), NOT(PROP(2))))), REVERSEABBREVIATION (91, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb39"), "A form for the abbreviation rule form for disjunction (second direction):", PROPOSITION ( SENTENCE ( IMPL(NOT(AND(NOT(PROP(1)), NOT(PROP(2)))), OR(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(NOT(NOT(PROP(1))), PROP(1)), ADDSENTENCE ( LINK ("hilb6")) ), LINE ( IMPL(NOT(NOT(PROP(3))), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))), ADDSENTENCE ( LINK ("defimpl1")) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("defimpl2")) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(PROP(1), PROP(3)), OR(PROP(3), PROP(1))), REPLACEPROP ( 6, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(4), PROP(3)), OR(PROP(3), PROP(4))), REPLACEPROP ( 7, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(2)))), REPLACEPROP ( 9, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 10, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 11, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(PROP(4), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), PROP(4))), REPLACEPROP ( 8, PROP(3), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), OR(NOT(PROP(1)), PROP(3))), REPLACEPROP ( 4, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), OR(NOT(PROP(4)), PROP(3))), REPLACEPROP ( 14, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(PROP(1), PROP(2))), OR(NOT(PROP(4)), OR(PROP(1), PROP(2)))), REPLACEPROP ( 15, PROP(3), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(3)), IMPL(PROP(1), PROP(3))), REPLACEPROP ( 5, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(NOT(PROP(4)), PROP(3)), IMPL(PROP(4), PROP(3))), REPLACEPROP ( 17, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(NOT(PROP(4)), OR(PROP(1), PROP(2))), IMPL(PROP(4), OR(PROP(1), PROP(2)))), REPLACEPROP ( 18, PROP(3), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(NOT(NOT(PROP(2))), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(2)))), REPLACEPROP ( 21, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 22, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 23, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(2), PROP(6)), OR(PROP(2), PROP(5)))), REPLACEPROP ( 24, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(1)), IMPL(OR(PROP(2), PROP(6)), OR(PROP(2), PROP(1)))), REPLACEPROP ( 25, PROP(5), PROP(1) ) ), LINE ( IMPL(IMPL(NOT(NOT(PROP(1))), PROP(1)), IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(2), PROP(1)))), REPLACEPROP ( 26, PROP(6), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(2), PROP(1))), MODUSPONENS (1, 27) ), LINE ( IMPL(OR(PROP(4), PROP(1)), OR(PROP(1), PROP(4))), REPLACEPROP ( 8, PROP(3), PROP(1) ) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))), REPLACEPROP ( 29, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), PROP(6)), IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), PROP(5)))), REPLACEPROP ( 12, PROP(4), OR(PROP(2), NOT(NOT(PROP(1)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), PROP(2))), IMPL(IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), PROP(6)), IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(1), PROP(2))))), REPLACEPROP ( 31, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))), IMPL(IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(2), PROP(1))), IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(1), PROP(2))))), REPLACEPROP ( 32, PROP(6), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(2), PROP(1))), IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(1), PROP(2)))), MODUSPONENS (30, 33) ), LINE ( IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(1), PROP(2))), MODUSPONENS (28, 34) ), LINE ( IMPL(OR(PROP(4), PROP(2)), OR(PROP(2), PROP(4))), REPLACEPROP ( 8, PROP(3), PROP(2) ) ), LINE ( IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(2), NOT(NOT(PROP(1))))), REPLACEPROP ( 36, PROP(4), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), PROP(6)), IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), PROP(5)))), REPLACEPROP ( 12, PROP(4), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), PROP(2))), IMPL(IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), PROP(6)), IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(1), PROP(2))))), REPLACEPROP ( 38, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), NOT(NOT(PROP(1)))), OR(PROP(1), PROP(2))), IMPL(IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(2), NOT(NOT(PROP(1))))), IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(1), PROP(2))))), REPLACEPROP ( 39, PROP(6), OR(PROP(2), NOT(NOT(PROP(1)))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(2), NOT(NOT(PROP(1))))), IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(1), PROP(2)))), MODUSPONENS (35, 40) ), LINE ( IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(1), PROP(2))), MODUSPONENS (37, 41) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(1)))), REPLACEPROP ( 43, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(4)))), REPLACEPROP ( 44, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(PROP(1), PROP(2))), IMPL(NOT(OR(PROP(1), PROP(2))), NOT(PROP(4)))), REPLACEPROP ( 45, PROP(3), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(PROP(1))), PROP(2)), OR(PROP(1), PROP(2))), IMPL(NOT(OR(PROP(1), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), REPLACEPROP ( 46, PROP(4), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(NOT(OR(PROP(1), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), MODUSPONENS (42, 47) ), LINE ( IMPL(IMPL(PROP(4), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(PROP(4)))), REPLACEPROP ( 45, PROP(3), NOT(OR(NOT(NOT(PROP(1))), PROP(2))) ) ), LINE ( IMPL(IMPL(NOT(OR(PROP(1), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(2)))))), REPLACEPROP ( 49, PROP(4), NOT(OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(2))))), MODUSPONENS (48, 50) ), LINE ( IMPL(IMPL(PROP(4), NOT(NOT(OR(PROP(1), PROP(2))))), IMPL(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), NOT(PROP(4)))), REPLACEPROP ( 45, PROP(3), NOT(NOT(OR(PROP(1), PROP(2)))) ) ), LINE ( IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(2))))), IMPL(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), REPLACEPROP ( 52, PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), MODUSPONENS (51, 53) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(OR(PROP(1), PROP(2)), PROP(6)), OR(OR(PROP(1), PROP(2)), PROP(5)))), REPLACEPROP ( 24, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(6)), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))))), REPLACEPROP ( 55, PROP(5), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))))), REPLACEPROP ( 56, PROP(6), NOT(NOT(NOT(OR(PROP(1), PROP(2))))) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), MODUSPONENS (54, 57) ), LINE ( IMPL(OR(PROP(4), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), PROP(4))), REPLACEPROP ( 8, PROP(3), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 59, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), PROP(6)), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), PROP(5)))), REPLACEPROP ( 12, PROP(4), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), PROP(6)), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 61, PROP(5), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 62, PROP(6), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))))), MODUSPONENS (60, 63) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), MODUSPONENS (58, 64) ), LINE ( IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2))))))), REPLACEPROP ( 13, PROP(4), NOT(NOT(NOT(OR(PROP(1), PROP(2))))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 12, PROP(4), OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 67, PROP(5), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2))))))), IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 68, PROP(6), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2)))))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(PROP(1), PROP(2))))))), IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))))), MODUSPONENS (65, 69) ), LINE ( IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), MODUSPONENS (66, 70) ), LINE ( IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 16, PROP(4), NOT(NOT(OR(PROP(1), PROP(2)))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 12, PROP(4), IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 73, PROP(5), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 74, PROP(6), OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(PROP(1), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))))), MODUSPONENS (71, 75) ), LINE ( IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), MODUSPONENS (72, 76) ), LINE ( IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 19, PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 73, PROP(5), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 79, PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))))), MODUSPONENS (78, 80) ), LINE ( IMPL(IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2)))), MODUSPONENS (77, 81) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), MODUSPONENS (3, 82) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(NOT(PROP(1))), PROP(6)), OR(NOT(NOT(PROP(1))), PROP(5)))), REPLACEPROP ( 24, PROP(4), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(2)), IMPL(OR(NOT(NOT(PROP(1))), PROP(6)), OR(NOT(NOT(PROP(1))), PROP(2)))), REPLACEPROP ( 84, PROP(5), PROP(2) ) ), LINE ( IMPL(IMPL(NOT(NOT(PROP(2))), PROP(2)), IMPL(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(1))), PROP(2)))), REPLACEPROP ( 85, PROP(6), NOT(NOT(PROP(2))) ) ), LINE ( IMPL(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(1))), PROP(2))), MODUSPONENS (20, 86) ), LINE ( IMPL(IMPL(PROP(4), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(PROP(4)))), REPLACEPROP ( 45, PROP(3), OR(NOT(NOT(PROP(1))), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(1))), PROP(2))), IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), REPLACEPROP ( 88, PROP(4), OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), MODUSPONENS (87, 89) ), LINE ( IMPL(IMPL(PROP(4), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), NOT(PROP(4)))), REPLACEPROP ( 45, PROP(3), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))) ) ), LINE ( IMPL(IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), REPLACEPROP ( 91, PROP(4), NOT(OR(NOT(NOT(PROP(1))), PROP(2))) ) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), MODUSPONENS (90, 92) ), LINE ( IMPL(IMPL(PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), NOT(PROP(4)))), REPLACEPROP ( 45, PROP(3), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPL(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), REPLACEPROP ( 94, PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))) ) ), LINE ( IMPL(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), MODUSPONENS (93, 95) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(6)), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))))), REPLACEPROP ( 55, PROP(5), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))) ) ), LINE ( IMPL(IMPL(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))))), REPLACEPROP ( 97, PROP(6), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), MODUSPONENS (96, 98) ), LINE ( IMPL(OR(PROP(4), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), PROP(4))), REPLACEPROP ( 8, PROP(3), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 100, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), PROP(6)), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), PROP(5)))), REPLACEPROP ( 12, PROP(4), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), PROP(6)), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 102, PROP(5), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 103, PROP(6), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))))), IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))))), MODUSPONENS (101, 104) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), MODUSPONENS (99, 105) ), LINE ( IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), REPLACEPROP ( 13, PROP(4), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 12, PROP(4), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 108, PROP(5), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 109, PROP(6), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))))), IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))))), MODUSPONENS (106, 110) ), LINE ( IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), MODUSPONENS (107, 111) ), LINE ( IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 16, PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 12, PROP(4), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 114, PROP(5), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 115, PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))))), MODUSPONENS (112, 116) ), LINE ( IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), MODUSPONENS (113, 117) ), LINE ( IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 19, PROP(4), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), PROP(6)), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 114, PROP(5), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 120, PROP(6), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), OR(NOT(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), OR(PROP(1), PROP(2)))), IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2))))), MODUSPONENS (119, 121) ), LINE ( IMPL(IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2)))), MODUSPONENS (118, 122) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2))), MODUSPONENS (83, 123) ), LINE ( IMPL(NOT(AND(NOT(PROP(1)), NOT(PROP(2)))), OR(PROP(1), PROP(2))), REVERSEABBREVIATION (124, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb40"), "By duality we get the second distributive law (first direction):", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), OR(PROP(2), PROP(3))), OR(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), ADDSENTENCE ( LINK ("hilb37")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(1)))), REPLACEPROP ( 2, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(4)))), REPLACEPROP ( 3, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(NOT(OR(PROP(1), AND(PROP(2), PROP(3)))), NOT(PROP(4)))), REPLACEPROP ( 4, PROP(3), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(NOT(OR(PROP(1), AND(PROP(2), PROP(3)))), NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)