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