cnf(add_equals_b_5,negated_conjecture, ( equalish(add(a,u),b) )). cnf(add_equals_b_6,negated_conjecture, ( equalish(add(a,v),b) )). cnf(u_not_equal_to_v_7,negated

Proof Style

Sentence Format

Lens Magnitude

Lens Width

Current URI: http://inference-web.org/proofs/tptp/Problems/FLD/FLD016-1/query.owl#query

Question:

Solutions of linear equations in the additive group are unique

Query

cnf(add_equals_b_5,negated_conjecture,
    ( equalish(add(a,u),b) )).

cnf(add_equals_b_6,negated_conjecture,
    ( equalish(add(a,v),b) )).

cnf(u_not_equal_to_v_7,negated_conjecture,
    ( ~ equalish(u,v) )).

Answer:

```
$false
```
(by Vampire 11.0)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]

NEW URI

Question:

Query

Answer: