cnf(a_equals_b_5,negated_conjecture, ( equalish(a,b) )). cnf(c_equals_d_6,negated_conjecture, ( equalish(c,d) )). cnf(add_not_equal_to_add_7,negated_conjecture, ( ~ equalish(add(a,c),add(d,b)) )).

Proof Style

Sentence Format

Lens Magnitude

Lens Width

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

Question:

The resulting equation of the summation of two equations

Query

cnf(a_equals_b_5,negated_conjecture,
    ( equalish(a,b) )).

cnf(c_equals_d_6,negated_conjecture,
    ( equalish(c,d) )).

cnf(add_not_equal_to_add_7,negated_conjecture,
    ( ~ equalish(add(a,c),add(d,b)) )).

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: