NEW URI

Proof Style English Proof Tree Sentence Format English Raw Lens Magnitude 1 2 3 4 5 10 25 max Lens Width 500 600 700 800 900 1000 1100 1200 1300 1400 1500 1600

Question:

• Elimination of multiplicative inverses in an order, part 2

Query

cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
    ( ~ equalish(a,additive_identity) )).

cnf(b_not_equal_to_additive_identity_4,negated_conjecture,
    ( ~ equalish(b,additive_identity) )).

cnf(less_or_equal_5,negated_conjecture,
    ( less_or_equal(multiplicative_inverse(b),multiplicative_inverse(a)) )).

cnf(less_or_equal_6,negated_conjecture,
    ( less_or_equal(multiplicative_inverse(a),additive_identity) )).

cnf(not_less_or_equal_7,negated_conjecture,
    ( ~ less_or_equal(a,b) )).