The bear likes the squirrel. The squirrel sees the bear. If someone visits the squirrel then they visit the bear. If the squirrel visits the bear then the bear sees the squirrel. If someone likes the squirrel then they like the bear. If the squirrel sees the bear then the bear likes the squirrel. If someone is blue then they like the squirrel. If someone is kind and red then they visit the squirrel. If someone visits the squirrel then they are kind. If the bear visits the squirrel then the bear likes the squirrel.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone visits the squirrel then they visit the bear.
((("someone" "visits" "squirrel" "+")) -> ("someone" "visits" "bear" "+"))
If the squirrel visits the bear then the bear sees the squirrel.
((("squirrel" "visits" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
If someone likes the squirrel then they like the bear.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "bear" "+"))
If the squirrel sees the bear then the bear likes the squirrel.
((("squirrel" "sees" "bear" "+")) -> ("bear" "likes" "squirrel" "+"))
If someone is blue then they like the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone is kind and red then they visit the squirrel.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the squirrel then they are kind.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "kind" "+"))
If the bear visits the squirrel then the bear likes the squirrel.
((("bear" "visits" "squirrel" "+")) -> ("bear" "likes" "squirrel" "+"))
The squirrel sees the bear.
True
1
proof
[(triple2)]
("squirrel" "sees" "bear" "+")
triple2
The squirrel does not see the bear.
False
1
inv-proof
[(triple2)]
("squirrel" "sees" "bear" "-")
triple2
The bear likes the bear.
True
2
proof
[(((triple1) -> rule3) OR ((((triple2) -> rule4)) -> rule3))]
("bear" "likes" "bear" "+")
((triple1) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear does not like the bear.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2) -> rule4)) -> rule3))]
("bear" "likes" "bear" "-")
((triple1) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear does not see the squirrel.
Unknown
inv-rconc
[@3: The bear sees the squirrel.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule6 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The squirrel likes the bear.
Unknown
rconc
[@2: The squirrel likes the bear.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("squirrel" "likes" "bear" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The bear likes the squirrel.[(triple1 OR ((triple2) -> rule4))] The squirrel sees the bear.[(triple2)] @1: The bear likes the bear.[(((triple1) -> rule3) OR ((((triple2) -> rule4)) -> rule3))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
((triple2) -> (rule4 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple2
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple1) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2