The dog is young. The lion is rough. The lion is young. The lion needs the dog. The lion needs the squirrel. The lion sees the dog. The squirrel eats the dog. The squirrel is cold. The squirrel needs the lion. The squirrel sees the lion. If something sees the dog then the dog needs the lion. If the squirrel sees the dog and the squirrel is nice then the dog sees the lion.
The dog is young.
("dog" "is" "young" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something sees the dog then the dog needs the lion.
((("something" "sees" "dog" "+")) -> ("dog" "needs" "lion" "+"))
If the squirrel sees the dog and the squirrel is nice then the dog sees the lion.
((("squirrel" "sees" "dog" "+") ("squirrel" "is" "nice" "+")) -> ("dog" "sees" "lion" "+"))
The lion is rough.
True
1
proof
[(triple2)]
("lion" "is" "rough" "+")
triple2
The squirrel is not cold.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "cold" "-")
triple8
The dog needs the lion.
True
2
proof
[(((triple6) -> rule1))]
("dog" "needs" "lion" "+")
((triple6) -> (rule1 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog does not need the lion.
False
2
inv-proof
[(((triple6) -> rule1))]
("dog" "needs" "lion" "-")
((triple6) -> (rule1 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog does not see the lion.
Unknown
inv-rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The dog is young.[(triple1)] The lion is rough.[(triple2)] The lion is young.[(triple3)] The lion needs the dog.[(triple4)] The lion needs the squirrel.[(triple5)] The lion sees the dog.[(triple6)] The squirrel eats the dog.[(triple7)] The squirrel is cold.[(triple8)] The squirrel needs the lion.[(triple9)] The squirrel sees the lion.[(triple10)] @1: The dog needs the lion.[(((triple6) -> rule1))]
The dog is young.
("dog" "is" "young" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion needs the dog.
("lion" "needs" "dog" "+")
triple4
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple5
The lion sees the dog.
("lion" "sees" "dog" "+")
triple6
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple6) -> (rule1 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1