The bear likes the squirrel. The squirrel eats the bear. If something eats the bear and it is kind then it eats the squirrel. If something is kind and it sees the bear then it eats the bear. If the bear likes the squirrel then the bear sees the squirrel. If something eats the bear and the bear likes the squirrel then the bear eats the squirrel. If the squirrel eats the bear then the bear eats the squirrel. If something eats the squirrel and it likes the bear then it is young.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
If something eats the bear and it is kind then it eats the squirrel.
((("something" "eats" "bear" "+") ("something" "is" "kind" "+")) -> ("something" "eats" "squirrel" "+"))
If something is kind and it sees the bear then it eats the bear.
((("something" "is" "kind" "+") ("something" "sees" "bear" "+")) -> ("something" "eats" "bear" "+"))
If the bear likes the squirrel then the bear sees the squirrel.
((("bear" "likes" "squirrel" "+")) -> ("bear" "sees" "squirrel" "+"))
If something eats the bear and the bear likes the squirrel then the bear eats the squirrel.
((("something" "eats" "bear" "+") ("bear" "likes" "squirrel" "+")) -> ("bear" "eats" "squirrel" "+"))
If the squirrel eats the bear then the bear eats the squirrel.
((("squirrel" "eats" "bear" "+")) -> ("bear" "eats" "squirrel" "+"))
If something eats the squirrel and it likes the bear then it is young.
((("something" "eats" "squirrel" "+") ("something" "likes" "bear" "+")) -> ("something" "is" "young" "+"))
The bear likes the squirrel.
True
1
proof
[(triple1)]
("bear" "likes" "squirrel" "+")
triple1
The squirrel does not eat the bear.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "bear" "-")
triple2
The bear sees the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("bear" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "sees" "squirrel" "-")
((triple1) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "young" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The bear likes the squirrel.[(triple1)] The squirrel eats the bear.[(triple2)] @1: The bear eats the squirrel.[(((triple2) -> rule5) OR ((triple2 triple1) -> rule4))] The bear sees the squirrel.[(((triple1) -> rule3))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
((triple2) -> (rule5 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
((triple2 triple1) -> (rule4 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1