The bear likes the cat. The cat chases the bear. The cat chases the squirrel. The cat is nice. The cat needs the bear. The cat needs the lion. The lion is blue. The lion is nice. The lion is rough. The lion likes the bear. The squirrel is blue. The squirrel is cold. If someone is nice then they need the lion.
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If someone is nice then they need the lion.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "lion" "+"))
The bear likes the cat.
True
1
proof
[(triple1)]
("bear" "likes" "cat" "+")
triple1
The squirrel is not cold.
False
1
inv-proof
[(triple12)]
("squirrel" "is" "cold" "-")
triple12
The lion needs the lion.
True
2
proof
[(((triple8) -> rule1))]
("lion" "needs" "lion" "+")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple8) -> rule1))]
("lion" "needs" "lion" "-")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The bear does not need the lion.
Unknown
inv-rconc
[@1: The bear needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "lion" "-")
The squirrel needs the lion.
Unknown
rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "lion" "+")
The cat does not like the squirrel.
Unknown
inv-random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The bear likes the cat.[(triple1)] The cat chases the bear.[(triple2)] The cat chases the squirrel.[(triple3)] The cat is nice.[(triple4)] The cat needs the bear.[(triple5)] The cat needs the lion.[(triple6 OR ((triple4) -> rule1))] The lion is blue.[(triple7)] The lion is nice.[(triple8)] The lion is rough.[(triple9)] The lion likes the bear.[(triple10)] The squirrel is blue.[(triple11)] The squirrel is cold.[(triple12)] @1: The lion needs the lion.[(((triple8) -> rule1))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat needs the bear.
("cat" "needs" "bear" "+")
triple5
The cat needs the lion.
("cat" "needs" "lion" "+")
triple6
((triple4) -> (rule1 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The lion likes the bear.
("lion" "likes" "bear" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple12
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1