CalcCheck: Test/Test001.ltx: No syntax errors.
CalcCheck: Now checking...

    p ≢ q
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    ¬(p ≡ q)
  =   〈 (3.9 〉
       ─ CalcCheck: Could not extract information; could not justify this step!
    ¬p ≡ q

 ─ CalcCheck: 1 out of 2 steps not justified



=======================

    (p ≢ q) ≡ r
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    ¬(p ≡ q) ≡ r
  =   〈 (3.9) 〉
       ─ CalcCheck: (3.9) Distributivity of ¬ over ≡   ─   OK
    ¬p ≡ q ≡ r
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢; could not justify this step!
    (p ≢ q) ≡ r
  =   〈 (3.1) 〉
       ─ CalcCheck: (3.1) Associativity of ≡; could not justify this step!
    p ≢ (q ≡ r)

 ─ CalcCheck: 2 out of 4 steps not justified



=======================

    (p ≢ q) ≡ r
  =   〈 (3.16) 〉
       ─ CalcCheck: (3.16) Symmetry of ≢   ─   OK
    (q ≢ p) ≡ r
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢; could not justify this step!
    ¬q ≡ p ≡ r
  =   〈 3.2 〉
       ─ CalcCheck: Could not extract information   ─   OK (no change)
    p ≡ ¬q ≡ r
  =   〈 (3.9) 〉
       ─ CalcCheck: (3.9) Distributivity of ¬ over ≡   ─   OK
    p ≡ ¬(q ≡ r)
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    p ≡ (q ≢ r)
  =   〈 (3.17) 〉
       ─ CalcCheck: (3.17) Associativity of ≢; could not justify this step!
    (p ≡ q) ≢ r

 ─ CalcCheck: 2 out of 6 steps not justified



=======================

    p ∨ q ∨ r ≡ p ∨ q ∨ p ∨ r

    p ∨ q ∨ p ∨ r
  =   〈 (3.25) 〉
       ─ CalcCheck: (3.25) Associativity of ∨   ─   OK
    p ∨ q ∨ p ∨ r
  =   〈 (3.24) 〉
       ─ CalcCheck: (3.24) Symmetry of ∨   ─   OK
    p ∨ p ∨ q ∨ r
  =   〈 (3.25) 〉
       ─ CalcCheck: (3.25) Associativity of ∨   ─   OK
    p ∨ p ∨ q ∨ r
  =   〈 (3.26) 〉
       ─ CalcCheck: (3.26) Idempotency of ∨   ─   OK
    p ∨ q ∨ r
  =   〈 (3.25) 〉
       ─ CalcCheck: (3.25) Associativity of ∨   ─   OK
    p ∨ q ∨ r

 ─ CalcCheck: All steps OK



=======================

    p ∧ q ≡ q ∧ p

    p ∧ q
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    p ≡ q ≡ p ∧ q
  =   〈 (3.2) 〉
       ─ CalcCheck: (3.2) Symmetry of ≡   ─   OK (no change)
    p ≡ q ≡ q ∧ p
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    q ∧ p

 ─ CalcCheck: 2 out of 3 steps not justified



=======================

    p ∧ p ≡ p

    p ∧ p
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule   ─   OK
    p ≡ p ≡ p ∨ p
  =   〈 (3.26) 〉
       ─ CalcCheck: (3.26) Idempotency of ∨   ─   OK
    p ≡ p ≡ p
  =   〈 (3.2) 〉
       ─ CalcCheck: (3.2) Symmetry of ≡   ─   OK
    p

 ─ CalcCheck: All steps OK



=======================

    p ∧ false ≡ false

    p ∧ false
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule   ─   OK
    p ≡ false ≡ p ∨ false
  =   〈 (3.30) 〉
       ─ CalcCheck: (3.30) Identity of ∨   ─   OK
    p ≡ false ≡ p
  =   〈 3.15 〉
       ─ CalcCheck: Could not extract information; could not justify this step!
    ¬p ≡ p
  =   〈 (3.15) 〉
       ─ CalcCheck: (3.15) ¬p ≡ p ≡ false   ─   OK
    false

 ─ CalcCheck: 1 out of 4 steps not justified



=======================

    p ∨ (¬p ∧ q) ≡ p ∨ q

    p ∨ (¬p ∧ q)
  =   〈 (3.32) 〉
       ─ CalcCheck: (3.32) p ∨ q ≡ p ∨ ¬q ≡ p; could not justify this step!
    p ∨ (p ∧ q) ≡ p
  =   〈 (3.32) 〉
       ─ CalcCheck: (3.32) p ∨ q ≡ p ∨ ¬q ≡ p; could not justify this step!
    ¬p ∨ q

 ─ CalcCheck: 2 out of 2 steps not justified



=======================

    p ∧ q ≡ p ∧ ¬q ≡ ¬p

    p ∧ q ≡ p ∧ ¬q
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    p ≡ q ≡ p ∨ q
  =   〈 3.32 〉
       ─ CalcCheck: Could not extract information; could not justify this step!
    q ≡ p ∨ ¬q
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    p ≡ p ∧ q
  =   〈 (3.40) 〉
       ─ CalcCheck: (3.40) Zero of ∧; could not justify this step!
    p ≡ false
  =   〈 (3.15) 〉
       ─ CalcCheck: (3.15) ¬p ≡ p ≡ false   ─   OK
    ¬p

 ─ CalcCheck: 4 out of 5 steps not justified



CalcCheck: Finished checking Test/Test001.ltx
CalcCheck: 8 out of 15 calculations fully checked
CalcCheck: 7 out of 15 calculations not fully justified
CalcCheck: Wrote Test/Test001.ltx.html
