The dog is round. The dog is young. The dog needs the mouse. The dog needs the tiger. The mouse is not nice. The mouse is not young. The mouse sees the tiger. The mouse visits the dog. The mouse visits the tiger. The squirrel is blue. The squirrel is young. The squirrel visits the tiger. The tiger needs the squirrel. The tiger sees the dog. The tiger sees the squirrel. If the tiger needs the squirrel then the tiger is nice.
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If the tiger needs the squirrel then the tiger is nice.
((("tiger" "needs" "squirrel" "+")) -> ("tiger" "is" "nice" "+"))
The tiger sees the squirrel.
True
1
proof
[(triple15)]
("tiger" "sees" "squirrel" "+")
triple15
The dog does not need the mouse.
False
1
inv-proof
[(triple3)]
("dog" "needs" "mouse" "-")
triple3
The tiger is nice.
True
2
proof
[(((triple13) -> rule1))]
("tiger" "is" "nice" "+")
((triple13) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple13) -> rule1))]
("tiger" "is" "nice" "-")
((triple13) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The dog does not need the squirrel.
Unknown
inv-random
[@0: The dog needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "squirrel" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The mouse does not need the tiger.
Unknown
inv-random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is round.[(triple1)] The dog is young.[(triple2)] The dog needs the mouse.[(triple3)] The dog needs the tiger.[(triple4)] The mouse is not nice.[(triple5)] The mouse is not young.[(triple6)] The mouse sees the tiger.[(triple7)] The mouse visits the dog.[(triple8)] The mouse visits the tiger.[(triple9)] The squirrel is blue.[(triple10)] The squirrel is young.[(triple11)] The squirrel visits the tiger.[(triple12)] The tiger needs the squirrel.[(triple13)] The tiger sees the dog.[(triple14)] The tiger sees the squirrel.[(triple15)] @1: The tiger is nice.[(((triple13) -> rule1))]
The dog is round.
("dog" "is" "round" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple4
The mouse is not nice.
("mouse" "is" "nice" "-")
triple5
The mouse is not young.
("mouse" "is" "young" "-")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple8
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel is young.
("squirrel" "is" "young" "+")
triple11
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple12
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
((triple13) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1