The bear eats the squirrel. The bear sees the squirrel. The cat eats the bear. The cat is young. The cat sees the bear. The cat sees the lion. The lion is kind. The lion sees the bear. The lion sees the cat. The squirrel eats the bear. The squirrel eats the cat. The squirrel eats the lion. The squirrel is red. The squirrel needs the bear. The squirrel sees the bear. If someone needs the cat then the cat is red. If someone sees the bear then they see the lion. If someone sees the lion and they need the bear then the lion is blue.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone needs the cat then the cat is red.
((("someone" "needs" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone sees the bear then they see the lion.
((("someone" "sees" "bear" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion and they need the bear then the lion is blue.
((("someone" "sees" "lion" "+") ("someone" "needs" "bear" "+")) -> ("lion" "is" "blue" "+"))
The cat sees the bear.
True
1
proof
[(triple5)]
("cat" "sees" "bear" "+")
triple5
The lion is not kind.
False
1
inv-proof
[(triple7)]
("lion" "is" "kind" "-")
triple7
The lion sees the lion.
True
2
proof
[(((triple8) -> rule2))]
("lion" "sees" "lion" "+")
((triple8) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The squirrel does not see the lion.
False
2
inv-proof
[(((triple15) -> rule2))]
("squirrel" "sees" "lion" "-")
((triple15) -> (rule2 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion is blue.
True
4
proof
[(((((triple15) -> rule2) triple14) -> rule3))]
("lion" "is" "blue" "+")
((((triple15) -> (rule2 % int2)) triple14) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion is not blue.
False
4
inv-proof
[(((((triple15) -> rule2) triple14) -> rule3))]
("lion" "is" "blue" "-")
((((triple15) -> (rule2 % int2)) triple14) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "red" "-")
The bear sees the lion.
Unknown
rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "lion" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The lion does not need the squirrel.
Unknown
inv-random
[@0: The lion needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "squirrel" "-")
The lion eats the squirrel.
Unknown
random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "+")
@0: The bear eats the squirrel.[(triple1)] The bear sees the squirrel.[(triple2)] The cat eats the bear.[(triple3)] The cat is young.[(triple4)] The cat sees the bear.[(triple5)] The cat sees the lion.[(triple6 OR ((triple5) -> rule2))] The lion is kind.[(triple7)] The lion sees the bear.[(triple8)] The lion sees the cat.[(triple9)] The squirrel eats the bear.[(triple10)] The squirrel eats the cat.[(triple11)] The squirrel eats the lion.[(triple12)] The squirrel is red.[(triple13)] The squirrel needs the bear.[(triple14)] The squirrel sees the bear.[(triple15)] @1: The lion sees the lion.[(((triple8) -> rule2))] The squirrel sees the lion.[(((triple15) -> rule2))] @2: The lion is blue.[(((((triple15) -> rule2) triple14) -> rule3))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat sees the bear.
("cat" "sees" "bear" "+")
triple5
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
((triple5) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple7
The lion sees the bear.
("lion" "sees" "bear" "+")
triple8
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple10
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple11
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple12
The squirrel is red.
("squirrel" "is" "red" "+")
triple13
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple14
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple15
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple8) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple15) -> (rule2 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((((triple15) -> (rule2 % int2)) triple14) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2