MODULE ( HEADER ( SPEC ( NAME ("prophilbert1"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("First theorems of Propositional Calculus"), DESCRIPTION ( "This module includes first proofs of propositional 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 ("propaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ) ), USEDBY ( SPEC ( NAME ("prophilbert2"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("hilb1"), "First we prove a simple implication, that follows directly from the fourth axiom:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))) ), PROOF ( 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(NOT(PROP(3)), PROP(1)), OR(NOT(PROP(3)), PROP(2)))), REPLACEPROP ( 1, PROP(3), NOT(PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), OR(NOT(PROP(3)), PROP(2)))), REVERSEABBREVIATION (2, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), REVERSEABBREVIATION (3, LINK ("impl"), 1) ) ) ), "This proposition is the form for the Hypothetical Syllogism." ), PARAGRAPH ( LABEL ("hilb2"), "The self implication could be derived:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(1) ) ), LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ), 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 ( 4, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 5, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 6, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(1), PROP(6)), IMPL(PROP(1), PROP(5)))), REPLACEPROP ( 7, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(1)), IMPL(IMPL(PROP(1), PROP(6)), IMPL(PROP(1), PROP(1)))), REPLACEPROP ( 8, PROP(5), PROP(1) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(1)), PROP(1)), IMPL(IMPL(PROP(1), OR(PROP(1), PROP(1))), IMPL(PROP(1), PROP(1)))), REPLACEPROP ( 9, PROP(6), OR(PROP(1), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(1), PROP(1))), IMPL(PROP(1), PROP(1))), MODUSPONENS (3, 10) ), LINE ( IMPL(PROP(1), PROP(1)), MODUSPONENS (2, 11) ) ) ) ), PARAGRAPH ( LABEL ("hilb3"), "One form of the classical `tertium non datur'", PROPOSITION ( SENTENCE ( OR(NOT(PROP(1)), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( OR(NOT(PROP(1)), PROP(1)), USEABBREVIATION (1, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb4"), "The standard form of the excluded middle:", PROPOSITION ( SENTENCE ( OR(PROP(1), NOT(PROP(1))) ), PROOF ( LINE ( OR(NOT(PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("hilb3")) ), 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 ( 2, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(4), PROP(3)), OR(PROP(3), PROP(4))), REPLACEPROP ( 3, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(PROP(4), PROP(1)), OR(PROP(1), PROP(4))), REPLACEPROP ( 4, PROP(3), PROP(1) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(1)), OR(PROP(1), NOT(PROP(1)))), REPLACEPROP ( 5, PROP(4), NOT(PROP(1)) ) ), LINE ( OR(PROP(1), NOT(PROP(1))), MODUSPONENS (1, 6) ) ) ) ), PARAGRAPH ( LABEL ("hilb5"), "Double negation is implicated:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), NOT(NOT(PROP(1)))) ), PROOF ( LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("hilb4")) ), LINE ( OR(NOT(PROP(1)), NOT(NOT(PROP(1)))), REPLACEPROP ( 1, PROP(1), NOT(PROP(1)) ) ), LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), REVERSEABBREVIATION (2, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb6"), "The reverse is also true:", PROPOSITION ( SENTENCE ( IMPL(NOT(NOT(PROP(1))), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb5")) ), LINE ( IMPL(NOT(PROP(1)), NOT(NOT(NOT(PROP(1))))), REPLACEPROP ( 1, PROP(1), NOT(PROP(1)) ) ), 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 ( 3, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 4, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 5, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 6, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(NOT(PROP(1))))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), NOT(NOT(NOT(PROP(1))))))), REPLACEPROP ( 7, PROP(5), NOT(NOT(NOT(PROP(1)))) ) ), LINE ( IMPL(IMPL(NOT(PROP(1)), NOT(NOT(NOT(PROP(1))))), IMPL(OR(PROP(1), NOT(PROP(1))), OR(PROP(1), NOT(NOT(NOT(PROP(1))))))), REPLACEPROP ( 8, PROP(6), NOT(PROP(1)) ) ), LINE ( IMPL(OR(PROP(1), NOT(PROP(1))), OR(PROP(1), NOT(NOT(NOT(PROP(1)))))), MODUSPONENS (2, 9) ), LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("hilb4")) ), LINE ( OR(PROP(1), NOT(NOT(NOT(PROP(1))))), MODUSPONENS (11, 10) ), 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 ( 13, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(4), PROP(3)), OR(PROP(3), PROP(4))), REPLACEPROP ( 14, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(PROP(4), NOT(NOT(NOT(PROP(1))))), OR(NOT(NOT(NOT(PROP(1)))), PROP(4))), REPLACEPROP ( 15, PROP(3), NOT(NOT(NOT(PROP(1)))) ) ), LINE ( IMPL(OR(PROP(1), NOT(NOT(NOT(PROP(1))))), OR(NOT(NOT(NOT(PROP(1)))), PROP(1))), REPLACEPROP ( 16, PROP(4), PROP(1) ) ), LINE ( OR(NOT(NOT(NOT(PROP(1)))), PROP(1)), MODUSPONENS (12, 17) ), LINE ( IMPL(NOT(NOT(PROP(1))), PROP(1)), REVERSEABBREVIATION (18, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb7"), "The correct reverse of an implication:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))) ), PROOF ( LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb5")) ), 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 ( 3, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 4, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 5, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(PROP(1)), PROP(6)), OR(NOT(PROP(1)), PROP(5)))), REPLACEPROP ( 6, PROP(4), NOT(PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(NOT(PROP(2)))), IMPL(OR(NOT(PROP(1)), PROP(6)), OR(NOT(PROP(1)), NOT(NOT(PROP(2)))))), REPLACEPROP ( 7, PROP(5), NOT(NOT(PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(2), NOT(NOT(PROP(2)))), IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(PROP(1)), NOT(NOT(PROP(2)))))), REPLACEPROP ( 8, PROP(6), PROP(2) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(PROP(1)), NOT(NOT(PROP(2))))), MODUSPONENS (2, 9) ), 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 ( 11, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(4), PROP(3)), OR(PROP(3), PROP(4))), REPLACEPROP ( 12, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(PROP(4), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(2))), PROP(4))), REPLACEPROP ( 13, PROP(3), NOT(NOT(PROP(2))) ) ), LINE ( IMPL(OR(NOT(PROP(1)), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), REPLACEPROP ( 14, PROP(4), NOT(PROP(1)) ) ), 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 ( 16, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 17, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 18, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(NOT(PROP(1)), PROP(2)), PROP(6)), IMPL(OR(NOT(PROP(1)), PROP(2)), PROP(5)))), REPLACEPROP ( 19, PROP(4), OR(NOT(PROP(1)), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), IMPL(IMPL(OR(NOT(PROP(1)), PROP(2)), PROP(6)), IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))))), REPLACEPROP ( 20, PROP(5), OR(NOT(NOT(PROP(2))), NOT(PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(PROP(1)), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), IMPL(IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(PROP(1)), NOT(NOT(PROP(2))))), IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))))), REPLACEPROP ( 21, PROP(6), OR(NOT(PROP(1)), NOT(NOT(PROP(2)))) ) ), LINE ( IMPL(IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(PROP(1)), NOT(NOT(PROP(2))))), IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1))))), MODUSPONENS (15, 22) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), MODUSPONENS (10, 23) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), REVERSEABBREVIATION (24, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), REVERSEABBREVIATION (25, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("defimpl1"), "Definition of an Implication 1. part:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(3), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), IMPL(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))), USEABBREVIATION (3, LINK ("impl"), 3) ) ) ) ), PARAGRAPH ( LABEL ("defimpl2"), "Definition of an Implication 2. part:", PROPOSITION ( SENTENCE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(3), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), IMPL(PROP(1), PROP(2)) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))), USEABBREVIATION (3, LINK ("impl"), 2) ) ) ) ), PARAGRAPH ( LABEL ("defand1"), "Definition of a Conjunction 1. part:", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(3), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), AND(PROP(1), PROP(2)) ) ), LINE ( IMPL(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), USEABBREVIATION (3, LINK ("and"), 2) ) ) ) ), PARAGRAPH ( LABEL ("defand2"), "Definition of a Conjunction 2. part:", PROPOSITION ( SENTENCE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), AND(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(3), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), AND(PROP(1), PROP(2)) ) ), LINE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), AND(PROP(1), PROP(2))), USEABBREVIATION (3, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("defequi1"), "Definition of an Equivalence 1. part:", PROPOSITION ( SENTENCE ( IMPL(EQUI(PROP(1), PROP(2)), AND(IMPL(PROP(1), PROP(2)), IMPL(PROP(2), PROP(1)))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(3), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(EQUI(PROP(1), PROP(2)), EQUI(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), EQUI(PROP(1), PROP(2)) ) ), LINE ( IMPL(EQUI(PROP(1), PROP(2)), AND(IMPL(PROP(1), PROP(2)), IMPL(PROP(2), PROP(1)))), USEABBREVIATION (3, LINK ("equi"), 2) ) ) ) ), PARAGRAPH ( LABEL ("defequi2"), "Definition of an Equivalence 2. part:", PROPOSITION ( SENTENCE ( IMPL(AND(IMPL(PROP(1), PROP(2)), IMPL(PROP(2), PROP(1))), EQUI(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(3), PROP(3)), REPLACEPROP ( 1, PROP(1), PROP(3) ) ), LINE ( IMPL(EQUI(PROP(1), PROP(2)), EQUI(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(3), EQUI(PROP(1), PROP(2)) ) ), LINE ( IMPL(AND(IMPL(PROP(1), PROP(2)), IMPL(PROP(2), PROP(1))), EQUI(PROP(1), PROP(2))), USEABBREVIATION (3, LINK ("equi"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb8"), "A simular formulation for the second axiom:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), OR(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), 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 ( 3, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 4, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 5, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(1), PROP(6)), IMPL(PROP(1), PROP(5)))), REPLACEPROP ( 6, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), PROP(1))), IMPL(IMPL(PROP(1), PROP(6)), IMPL(PROP(1), OR(PROP(2), PROP(1))))), REPLACEPROP ( 7, PROP(5), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(IMPL(PROP(1), OR(PROP(1), PROP(2))), IMPL(PROP(1), OR(PROP(2), PROP(1))))), REPLACEPROP ( 8, PROP(6), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(1), PROP(2))), IMPL(PROP(1), OR(PROP(2), PROP(1)))), MODUSPONENS (2, 9) ), LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), MODUSPONENS (1, 10) ) ) ) ), PARAGRAPH ( LABEL ("hilb9"), "A technical lemma (equal to the third axiom):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ) ) ) ), PARAGRAPH ( LABEL ("hilb10"), "And another technical lemma (simular to the third axiom):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))) ), PROOF ( 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 ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(4), PROP(3)), OR(PROP(3), PROP(4))), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(PROP(4), PROP(1)), OR(PROP(1), PROP(4))), REPLACEPROP ( 3, PROP(3), PROP(1) ) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))), REPLACEPROP ( 4, PROP(4), PROP(2) ) ) ) ) ), PARAGRAPH ( LABEL ("hilb11"), "A technical lemma (equal to the first axiom):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ) ) ) ), PARAGRAPH ( LABEL ("hilb12"), "A simple propositon that follows directly from the second axiom:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), OR(PROP(1), PROP(1))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(1) ) ) ) ) ), PARAGRAPH ( LABEL ("hilb13"), "This is a pre form for the associative law:", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("hilb8")) ), LINE ( IMPL(PROP(1), OR(PROP(4), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(4) ) ), LINE ( IMPL(PROP(5), OR(PROP(4), PROP(5))), REPLACEPROP ( 2, PROP(1), PROP(5) ) ), LINE ( IMPL(PROP(5), OR(PROP(1), PROP(5))), REPLACEPROP ( 3, PROP(4), PROP(1) ) ), LINE ( IMPL(PROP(3), OR(PROP(1), PROP(3))), REPLACEPROP ( 4, PROP(5), PROP(3) ) ), 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 ( 6, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 7, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 8, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(2), PROP(6)), OR(PROP(2), PROP(5)))), REPLACEPROP ( 9, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), PROP(3))), IMPL(OR(PROP(2), PROP(6)), OR(PROP(2), OR(PROP(1), PROP(3))))), REPLACEPROP ( 10, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(3), OR(PROP(1), PROP(3))), IMPL(OR(PROP(2), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3))))), REPLACEPROP ( 11, PROP(6), PROP(3) ) ), LINE ( IMPL(OR(PROP(2), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3)))), MODUSPONENS (5, 12) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 9, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 14, PROP(5), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 15, PROP(6), OR(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (13, 16) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("hilb9")) ), LINE ( IMPL(OR(PROP(1), PROP(4)), OR(PROP(4), PROP(1))), REPLACEPROP ( 18, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(PROP(5), PROP(4)), OR(PROP(4), PROP(5))), REPLACEPROP ( 19, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(PROP(5), OR(PROP(2), OR(PROP(1), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(5))), REPLACEPROP ( 20, PROP(4), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), REPLACEPROP ( 21, PROP(5), 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), OR(PROP(2), PROP(3)))), PROP(6)), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), PROP(5)))), REPLACEPROP ( 9, PROP(4), NOT(OR(PROP(1), OR(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), PROP(6)), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))))), REPLACEPROP ( 25, PROP(5), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))))), REPLACEPROP ( 26, PROP(6), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), MODUSPONENS (22, 27) ), LINE ( IMPL(IMPL(PROP(1), PROP(4)), OR(NOT(PROP(1)), PROP(4))), REPLACEPROP ( 23, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(4)), OR(NOT(PROP(5)), PROP(4))), REPLACEPROP ( 29, PROP(1), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(5), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(PROP(5)), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 30, PROP(4), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 31, PROP(5), OR(PROP(1), OR(PROP(2), 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 ( 33, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 34, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 35, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(5)))), REPLACEPROP ( 36, PROP(4), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))))), REPLACEPROP ( 37, PROP(5), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))))), REPLACEPROP ( 38, PROP(6), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))))), MODUSPONENS (28, 39) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), MODUSPONENS (32, 40) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(4)), IMPL(PROP(1), PROP(4))), REPLACEPROP ( 24, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(NOT(PROP(5)), PROP(4)), IMPL(PROP(5), PROP(4))), REPLACEPROP ( 42, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(PROP(5), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), REPLACEPROP ( 43, PROP(4), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), REPLACEPROP ( 44, PROP(5), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(6)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))))), REPLACEPROP ( 37, PROP(5), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))))), REPLACEPROP ( 46, PROP(6), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))))), MODUSPONENS (45, 47) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)))), MODUSPONENS (41, 48) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), MODUSPONENS (17, 49) ), LINE ( IMPL(OR(PROP(1), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3)))), REPLACEPROP ( 1, PROP(1), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(3))), REPLACEPROP ( 52, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(1), PROP(6)), IMPL(PROP(1), PROP(5)))), REPLACEPROP ( 36, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(IMPL(PROP(1), PROP(6)), IMPL(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 54, PROP(5), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(IMPL(PROP(1), OR(PROP(1), PROP(3))), IMPL(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 55, PROP(6), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(1), PROP(3))), IMPL(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (51, 56) ), LINE ( IMPL(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))), MODUSPONENS (53, 57) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(6)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(5)))), REPLACEPROP ( 9, PROP(4), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(6)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 59, PROP(5), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 60, PROP(6), PROP(1) ) ), LINE ( IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (58, 61) ), LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("hilb11")) ), LINE ( IMPL(OR(PROP(4), PROP(4)), PROP(4)), REPLACEPROP ( 63, PROP(1), PROP(4) ) ), LINE ( IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), OR(PROP(2), OR(PROP(1), PROP(3)))), REPLACEPROP ( 64, PROP(4), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), PROP(6)), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), PROP(5)))), REPLACEPROP ( 9, PROP(4), NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), PROP(6)), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 66, PROP(5), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 67, PROP(6), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (65, 68) ), LINE ( IMPL(IMPL(PROP(5), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(PROP(5)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 30, PROP(4), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 70, PROP(5), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(6)), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(5)))), REPLACEPROP ( 36, PROP(4), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(6)), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 72, PROP(5), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 73, PROP(6), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))))), MODUSPONENS (69, 74) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (71, 75) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(PROP(5), OR(PROP(2), OR(PROP(1), PROP(3))))), REPLACEPROP ( 43, PROP(4), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3))))), REPLACEPROP ( 77, PROP(5), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), PROP(6)), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 72, PROP(5), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 79, PROP(6), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), OR(NOT(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3)))))), MODUSPONENS (78, 80) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (76, 81) ), LINE ( IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3)))), MODUSPONENS (62, 82) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), PROP(5)))), REPLACEPROP ( 36, PROP(4), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 84, PROP(5), OR(PROP(2), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 85, PROP(6), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), MODUSPONENS (83, 86) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), MODUSPONENS (50, 87) ) ) ) ), PARAGRAPH ( LABEL ("hilb14"), "The associative law for the disjunction (first direction):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("hilb9")) ), LINE ( IMPL(OR(PROP(1), PROP(4)), OR(PROP(4), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(PROP(5), PROP(4)), OR(PROP(4), PROP(5))), REPLACEPROP ( 2, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(PROP(5), PROP(3)), OR(PROP(3), PROP(5))), REPLACEPROP ( 3, PROP(4), PROP(3) ) ), LINE ( IMPL(OR(PROP(2), PROP(3)), OR(PROP(3), PROP(2))), REPLACEPROP ( 4, PROP(5), 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 ( 6, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 7, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 8, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 9, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(3), PROP(2))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), OR(PROP(3), PROP(2))))), REPLACEPROP ( 10, PROP(5), OR(PROP(3), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(3)), OR(PROP(3), PROP(2))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), REPLACEPROP ( 11, PROP(6), OR(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), MODUSPONENS (5, 12) ), 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(4)), OR(NOT(PROP(1)), PROP(4))), REPLACEPROP ( 14, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(4)), OR(NOT(PROP(5)), PROP(4))), REPLACEPROP ( 16, PROP(1), PROP(5) ) ), 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 ( 18, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 19, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 20, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(4)), IMPL(PROP(1), PROP(4))), REPLACEPROP ( 15, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(NOT(PROP(5)), PROP(4)), IMPL(PROP(5), PROP(4))), REPLACEPROP ( 22, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb13")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(4))), OR(PROP(2), OR(PROP(1), PROP(4)))), REPLACEPROP ( 24, PROP(3), PROP(4) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(5), PROP(4))), OR(PROP(5), OR(PROP(1), PROP(4)))), REPLACEPROP ( 25, PROP(2), PROP(5) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(4))), OR(PROP(5), OR(PROP(6), PROP(4)))), REPLACEPROP ( 26, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(2))), OR(PROP(5), OR(PROP(6), PROP(2)))), REPLACEPROP ( 27, PROP(4), PROP(2) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(3), PROP(2))), OR(PROP(3), OR(PROP(6), PROP(2)))), REPLACEPROP ( 28, PROP(5), PROP(3) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(3), PROP(2))), OR(PROP(3), OR(PROP(1), PROP(2)))), REPLACEPROP ( 29, PROP(6), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), PROP(5)))), REPLACEPROP ( 21, PROP(4), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 31, PROP(5), OR(PROP(3), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(3), PROP(2))), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))))), REPLACEPROP ( 32, PROP(6), OR(PROP(1), OR(PROP(3), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2))))), MODUSPONENS (30, 33) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), MODUSPONENS (13, 34) ), LINE ( IMPL(OR(PROP(5), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), PROP(5))), REPLACEPROP ( 3, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), PROP(3))), REPLACEPROP ( 36, PROP(5), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), PROP(6)), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), PROP(5)))), REPLACEPROP ( 9, PROP(4), NOT(OR(PROP(1), OR(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), PROP(6)), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))))), REPLACEPROP ( 38, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))))), REPLACEPROP ( 39, PROP(6), OR(PROP(3), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))), MODUSPONENS (37, 40) ), LINE ( IMPL(IMPL(PROP(5), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(PROP(5)), OR(PROP(3), OR(PROP(1), PROP(2))))), REPLACEPROP ( 17, PROP(4), OR(PROP(3), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2))))), REPLACEPROP ( 42, PROP(5), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), PROP(6)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), PROP(5)))), REPLACEPROP ( 21, PROP(4), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), PROP(6)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))))), REPLACEPROP ( 44, PROP(5), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2))))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))))), REPLACEPROP ( 45, PROP(6), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(PROP(3), OR(PROP(1), PROP(2))))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))))), MODUSPONENS (41, 46) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))), MODUSPONENS (43, 47) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPL(PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)))), REPLACEPROP ( 23, PROP(4), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3)))), REPLACEPROP ( 49, PROP(5), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), PROP(6)), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3)))))), REPLACEPROP ( 44, PROP(5), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3)))))), REPLACEPROP ( 51, PROP(6), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), OR(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))))), MODUSPONENS (50, 52) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3)))), MODUSPONENS (48, 53) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))), MODUSPONENS (35, 54) ) ) ) ), PARAGRAPH ( LABEL ("hilb15"), "The associative law for the disjunction (second direction):", PROPOSITION ( SENTENCE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))) ), PROOF ( 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 ( 1, PROP(3), PROP(4) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(5), PROP(4))), OR(OR(PROP(1), PROP(5)), PROP(4))), REPLACEPROP ( 2, PROP(2), PROP(5) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(4))), OR(OR(PROP(6), PROP(5)), PROP(4))), REPLACEPROP ( 3, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(1))), OR(OR(PROP(6), PROP(5)), PROP(1))), REPLACEPROP ( 4, PROP(4), PROP(1) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(2), PROP(1))), OR(OR(PROP(6), PROP(2)), PROP(1))), REPLACEPROP ( 5, PROP(5), PROP(2) ) ), LINE ( IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), REPLACEPROP ( 6, PROP(6), PROP(3) ) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("hilb10")) ), LINE ( IMPL(OR(PROP(4), PROP(1)), OR(PROP(1), PROP(4))), REPLACEPROP ( 8, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(PROP(4), PROP(5)), OR(PROP(5), PROP(4))), REPLACEPROP ( 9, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(OR(PROP(2), PROP(1)), PROP(5)), OR(PROP(5), OR(PROP(2), PROP(1)))), REPLACEPROP ( 10, PROP(4), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(PROP(3), OR(PROP(2), PROP(1)))), REPLACEPROP ( 11, PROP(5), PROP(3) ) ), 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(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(1), PROP(4)), IMPL(NOT(PROP(4)), NOT(PROP(1)))), REPLACEPROP ( 15, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(4)), IMPL(NOT(PROP(4)), NOT(PROP(5)))), REPLACEPROP ( 16, PROP(1), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(5), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), NOT(PROP(5)))), REPLACEPROP ( 17, PROP(4), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), REPLACEPROP ( 18, PROP(5), OR(OR(PROP(2), PROP(1)), PROP(3)) ) ), LINE ( IMPL(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), MODUSPONENS (12, 19) ), 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(OR(OR(PROP(3), PROP(2)), PROP(1)), PROP(6)), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), PROP(5)))), REPLACEPROP ( 24, PROP(4), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), PROP(6)), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))))), REPLACEPROP ( 25, PROP(5), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))) ) ), LINE ( IMPL(IMPL(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))))), REPLACEPROP ( 26, PROP(6), NOT(OR(PROP(3), OR(PROP(2), PROP(1)))) ) ), LINE ( IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), MODUSPONENS (20, 27) ), 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 ( 29, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(PROP(5), PROP(4)), OR(PROP(4), PROP(5))), REPLACEPROP ( 30, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(PROP(5), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), PROP(5))), REPLACEPROP ( 31, PROP(4), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))) ) ), LINE ( IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 32, PROP(5), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), 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 ( 34, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 35, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 36, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), PROP(6)), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), PROP(5)))), REPLACEPROP ( 37, PROP(4), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), PROP(6)), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 38, PROP(5), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 39, PROP(6), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (33, 40) ), LINE ( IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (28, 41) ), LINE ( IMPL(OR(PROP(5), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), PROP(5))), REPLACEPROP ( 31, PROP(4), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), LINE ( IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1)))))), REPLACEPROP ( 43, PROP(5), NOT(OR(PROP(3), OR(PROP(2), PROP(1)))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(5)))), REPLACEPROP ( 37, PROP(4), OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 45, PROP(5), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1)))))), IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 46, PROP(6), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1))))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(PROP(3), OR(PROP(2), PROP(1)))))), IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (42, 47) ), LINE ( IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (44, 48) ), LINE ( IMPL(IMPL(PROP(1), PROP(4)), OR(NOT(PROP(1)), PROP(4))), REPLACEPROP ( 13, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(4)), OR(NOT(PROP(5)), PROP(4))), REPLACEPROP ( 50, PROP(1), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(5), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(PROP(5)), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 51, PROP(4), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 52, PROP(5), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(5)))), REPLACEPROP ( 37, PROP(4), IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 54, PROP(5), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 55, PROP(6), OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (49, 56) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (53, 57) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(4)), IMPL(PROP(1), PROP(4))), REPLACEPROP ( 14, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(NOT(PROP(5)), PROP(4)), IMPL(PROP(5), PROP(4))), REPLACEPROP ( 59, PROP(1), PROP(5) ) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(PROP(5), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 60, PROP(4), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 61, PROP(5), OR(OR(PROP(2), PROP(1)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 54, PROP(5), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 63, PROP(6), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (62, 64) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (58, 65) ), LINE ( IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), MODUSPONENS (7, 66) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(3), PROP(6)), OR(PROP(3), PROP(5)))), REPLACEPROP ( 24, PROP(4), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), PROP(1))), IMPL(OR(PROP(3), PROP(6)), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 68, PROP(5), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 69, PROP(6), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1)))), MODUSPONENS (29, 70) ), LINE ( IMPL(OR(PROP(5), OR(PROP(2), PROP(1))), OR(OR(PROP(2), PROP(1)), PROP(5))), REPLACEPROP ( 31, PROP(4), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(2), PROP(1)), PROP(3))), REPLACEPROP ( 72, PROP(5), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), PROP(6)), IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), PROP(5)))), REPLACEPROP ( 37, PROP(4), OR(PROP(3), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(OR(PROP(2), PROP(1)), PROP(3))), IMPL(IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), PROP(6)), IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(2), PROP(1)), PROP(3))))), REPLACEPROP ( 74, PROP(5), OR(OR(PROP(2), PROP(1)), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(2), PROP(1)), PROP(3))), IMPL(IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(2), PROP(1)), PROP(3))))), REPLACEPROP ( 75, PROP(6), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(2), PROP(1)), PROP(3)))), MODUSPONENS (73, 76) ), LINE ( IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(2), PROP(1)), PROP(3))), MODUSPONENS (71, 77) ), LINE ( IMPL(OR(PROP(5), PROP(3)), OR(PROP(3), PROP(5))), REPLACEPROP ( 31, PROP(4), PROP(3) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(3), OR(PROP(1), PROP(2)))), REPLACEPROP ( 79, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), PROP(6)), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), PROP(5)))), REPLACEPROP ( 37, PROP(4), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), OR(OR(PROP(2), PROP(1)), PROP(3))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), PROP(6)), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(2), PROP(1)), PROP(3))))), REPLACEPROP ( 81, PROP(5), OR(OR(PROP(2), PROP(1)), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(OR(PROP(2), PROP(1)), PROP(3))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(2), PROP(1)), PROP(3))))), REPLACEPROP ( 82, PROP(6), OR(PROP(3), OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(3), OR(PROP(1), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(2), PROP(1)), PROP(3)))), MODUSPONENS (78, 83) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(2), PROP(1)), PROP(3))), MODUSPONENS (80, 84) ), LINE ( IMPL(IMPL(PROP(5), OR(OR(PROP(2), PROP(1)), PROP(3))), IMPL(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), NOT(PROP(5)))), REPLACEPROP ( 17, PROP(4), OR(OR(PROP(2), PROP(1)), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(2), PROP(1)), PROP(3))), IMPL(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))))), REPLACEPROP ( 86, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), MODUSPONENS (85, 87) ), LINE ( IMPL(IMPL(PROP(6), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), PROP(6)), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))))), REPLACEPROP ( 25, PROP(5), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))) ) ), LINE ( IMPL(IMPL(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))))), REPLACEPROP ( 89, PROP(6), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))) ) ), LINE ( IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))))), MODUSPONENS (88, 90) ), LINE ( IMPL(OR(PROP(5), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), PROP(5))), REPLACEPROP ( 31, PROP(4), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))) ) ), LINE ( IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 92, PROP(5), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), PROP(6)), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), PROP(5)))), REPLACEPROP ( 37, PROP(4), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), PROP(6)), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 94, PROP(5), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 95, PROP(6), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))))), IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (93, 96) ), LINE ( IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (91, 97) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), REPLACEPROP ( 43, PROP(5), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(5)))), REPLACEPROP ( 37, PROP(4), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 100, PROP(5), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 101, PROP(6), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(OR(OR(PROP(3), PROP(2)), PROP(1)), NOT(OR(OR(PROP(2), PROP(1)), PROP(3))))), IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (98, 102) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (99, 103) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 52, PROP(5), OR(OR(PROP(2), PROP(1)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(5)))), REPLACEPROP ( 37, PROP(4), IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 106, PROP(5), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 107, PROP(6), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(2), PROP(1)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (104, 108) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (105, 109) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 61, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 106, PROP(5), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))))), REPLACEPROP ( 112, PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))))), MODUSPONENS (111, 113) ), LINE ( IMPL(IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1)))), MODUSPONENS (110, 114) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), MODUSPONENS (67, 115) ), LINE ( IMPL(OR(PROP(5), PROP(1)), OR(PROP(1), PROP(5))), REPLACEPROP ( 31, PROP(4), PROP(1) ) ), LINE ( IMPL(OR(OR(PROP(3), PROP(2)), PROP(1)), OR(PROP(1), OR(PROP(3), PROP(2)))), REPLACEPROP ( 117, PROP(5), OR(PROP(3), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), PROP(6)), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), PROP(5)))), REPLACEPROP ( 24, PROP(4), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), PROP(6)), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))))), REPLACEPROP ( 119, PROP(5), OR(PROP(1), OR(PROP(3), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), PROP(2)), PROP(1)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))))), REPLACEPROP ( 120, PROP(6), OR(OR(PROP(3), PROP(2)), PROP(1)) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), MODUSPONENS (118, 121) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), REPLACEPROP ( 52, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(5)))), REPLACEPROP ( 37, PROP(4), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))))), REPLACEPROP ( 124, PROP(5), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))))), REPLACEPROP ( 125, PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(OR(PROP(3), PROP(2)), PROP(1)))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))))), MODUSPONENS (122, 126) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), MODUSPONENS (123, 127) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(PROP(5), OR(PROP(1), OR(PROP(3), PROP(2))))), REPLACEPROP ( 60, PROP(4), OR(PROP(1), OR(PROP(3), PROP(2))) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2))))), REPLACEPROP ( 129, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), PROP(6)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2))))))), REPLACEPROP ( 124, PROP(5), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2))))))), REPLACEPROP ( 131, PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))))), MODUSPONENS (130, 132) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2))))), MODUSPONENS (128, 133) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), MODUSPONENS (116, 134) ), LINE ( IMPL(OR(PROP(5), PROP(2)), OR(PROP(2), PROP(5))), REPLACEPROP ( 31, PROP(4), PROP(2) ) ), LINE ( IMPL(OR(PROP(3), PROP(2)), OR(PROP(2), PROP(3))), REPLACEPROP ( 136, PROP(5), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 24, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), OR(PROP(2), PROP(3))))), REPLACEPROP ( 138, PROP(5), OR(PROP(2), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(3), PROP(2)), OR(PROP(2), PROP(3))), IMPL(OR(PROP(1), OR(PROP(3), PROP(2))), OR(PROP(1), OR(PROP(2), PROP(3))))), REPLACEPROP ( 139, PROP(6), OR(PROP(3), PROP(2)) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(3), PROP(2))), OR(PROP(1), OR(PROP(2), PROP(3)))), MODUSPONENS (137, 140) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), PROP(6)), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))))), REPLACEPROP ( 119, PROP(5), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(3), PROP(2))), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))))), REPLACEPROP ( 142, PROP(6), OR(PROP(1), OR(PROP(3), PROP(2))) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))), MODUSPONENS (141, 143) ), LINE ( IMPL(IMPL(PROP(5), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(PROP(5)), OR(PROP(1), OR(PROP(3), PROP(2))))), REPLACEPROP ( 51, PROP(4), OR(PROP(1), OR(PROP(3), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), REPLACEPROP ( 145, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), PROP(6)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), PROP(5)))), REPLACEPROP ( 37, PROP(4), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))) ) ), LINE ( IMPL(IMPL(PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), PROP(6)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))))), REPLACEPROP ( 147, PROP(5), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))))), REPLACEPROP ( 148, PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2))))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))))), MODUSPONENS (144, 149) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))), MODUSPONENS (146, 150) ), LINE ( IMPL(OR(NOT(PROP(5)), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPL(PROP(5), OR(PROP(1), OR(PROP(2), PROP(3))))), REPLACEPROP ( 60, PROP(4), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3))))), REPLACEPROP ( 152, PROP(5), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), PROP(6)), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3))))))), REPLACEPROP ( 147, PROP(5), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3))))), IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3))))))), REPLACEPROP ( 154, PROP(6), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), OR(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3))))), IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))))), MODUSPONENS (153, 155) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3))))), MODUSPONENS (151, 156) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))), MODUSPONENS (135, 157) ) ) ) ), PARAGRAPH ( LABEL ("hilb16"), "Another consequence from hilb13 is the exchange of preconditions:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb13")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(4))), OR(PROP(2), OR(PROP(1), PROP(4)))), REPLACEPROP ( 1, PROP(3), PROP(4) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(5), PROP(4))), OR(PROP(5), OR(PROP(1), PROP(4)))), REPLACEPROP ( 2, PROP(2), PROP(5) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(4))), OR(PROP(5), OR(PROP(6), PROP(4)))), REPLACEPROP ( 3, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(5), PROP(3))), OR(PROP(5), OR(PROP(6), PROP(3)))), REPLACEPROP ( 4, PROP(4), PROP(3) ) ), LINE ( IMPL(OR(PROP(6), OR(NOT(PROP(2)), PROP(3))), OR(NOT(PROP(2)), OR(PROP(6), PROP(3)))), REPLACEPROP ( 5, PROP(5), NOT(PROP(2)) ) ), LINE ( IMPL(OR(NOT(PROP(1)), OR(NOT(PROP(2)), PROP(3))), OR(NOT(PROP(2)), OR(NOT(PROP(1)), PROP(3)))), REPLACEPROP ( 6, PROP(6), NOT(PROP(1)) ) ), LINE ( IMPL(IMPL(PROP(1), OR(NOT(PROP(2)), PROP(3))), OR(NOT(PROP(2)), OR(NOT(PROP(1)), PROP(3)))), REVERSEABBREVIATION (7, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), OR(NOT(PROP(2)), OR(NOT(PROP(1)), PROP(3)))), REVERSEABBREVIATION (8, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), OR(NOT(PROP(1)), PROP(3)))), REVERSEABBREVIATION (9, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))), REVERSEABBREVIATION (10, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb17"), "An analogus form for \hyperref[hilb16]{hilb16}:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(2), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))) ), PROOF ( 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 ( 1, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 2, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(6), PROP(4)))), REPLACEPROP ( 3, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(3))), IMPL(PROP(5), IMPL(PROP(6), PROP(3)))), REPLACEPROP ( 4, PROP(4), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), IMPL(PROP(6), PROP(3)))), REPLACEPROP ( 5, PROP(5), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(2), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), REPLACEPROP ( 6, PROP(6), PROP(2) ) ) ) ) ) ) )