cnf(a_equals_x_5,negated_conjecture, ( equalish(a,x) )). cnf(add_equals_c_6,negated_conjecture, ( equalish(add(a,b),c) )). cnf(add_not_equal_to_c_7,negated

Proof Style

Sentence Format

Lens Magnitude

Lens Width

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

Question:

Substitution of an element in additive equations

Query

cnf(a_equals_x_5,negated_conjecture,
    ( equalish(a,x) )).

cnf(add_equals_c_6,negated_conjecture,
    ( equalish(add(a,b),c) )).

cnf(add_not_equal_to_c_7,negated_conjecture,
    ( ~ equalish(add(x,b),c) )).

Answers:

```
$false
```
(by EP 1.1)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]
```
$false
```
(by SPASS 3.5)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]

NEW URI

Question:

Query

Answers: