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