cnf(a_times_b,negated_conjecture, ( product(a,b,additive_identity) )). cnf(a_not_additive_identity,negated_conjecture, ( a != additive_identity )). cnf(prove_b_is_additive_identity,negated_conjecture, ( b != additive

Proof Style

Sentence Format

Lens Magnitude

Lens Width

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

Question:

```
Unknown
```

Query

cnf(a_times_b,negated_conjecture,
    ( product(a,b,additive_identity) )).

cnf(a_not_additive_identity,negated_conjecture,
    ( a != additive_identity )).

cnf(prove_b_is_additive_identity,negated_conjecture,
    ( b != additive_identity )).

Answers:

```
$false
```
(by EP 1.0pre)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]
```
$false
```
(by Otter 3.3)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]
```
$false
```
(by SNARK 20070805r043)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]
```
$false
```
(by SOS 2.0)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]
```
$false
```
(by SPASS 3.01)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]

~ product(X1,X2,additive_identity)
 | product(X1,multiplicative_identity,additive_identity)
 | X2 = additive_identity

(by Vampire 9.0)
[Browse Answer][Browse Proof] [ProbeIt][Tabulator]

NEW URI

Question:

Query

Answers: