The bear is green. The mouse is young. The mouse visits the bear. The mouse visits the squirrel. The rabbit visits the mouse. The rabbit visits the squirrel. The squirrel is green. If someone sees the squirrel and the squirrel is round then they see the bear. If someone chases the bear then they see the squirrel. If someone visits the mouse then they chase the bear. If someone visits the mouse then the mouse visits the bear. If someone is big then they chase the bear. If the mouse sees the bear then the bear is green.
The bear is green.
("bear" "is" "green" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
If someone sees the squirrel and the squirrel is round then they see the bear.
((("someone" "sees" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("someone" "sees" "bear" "+"))
If someone chases the bear then they see the squirrel.
((("someone" "chases" "bear" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the mouse then they chase the bear.
((("someone" "visits" "mouse" "+")) -> ("someone" "chases" "bear" "+"))
If someone visits the mouse then the mouse visits the bear.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If someone is big then they chase the bear.
((("someone" "is" "big" "+")) -> ("someone" "chases" "bear" "+"))
If the mouse sees the bear then the bear is green.
((("mouse" "sees" "bear" "+")) -> ("bear" "is" "green" "+"))
The bear is green.
True
1
proof
[(triple1)]
("bear" "is" "green" "+")
triple1
The mouse does not visit the bear.
False
1
inv-proof
[(triple3 OR ((triple5) -> rule4))]
("mouse" "visits" "bear" "-")
triple3
((triple5) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The rabbit chases the bear.
True
2
proof
[(((triple5) -> rule3))]
("rabbit" "chases" "bear" "+")
((triple5) -> (rule3 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit does not chase the bear.
False
2
inv-proof
[(((triple5) -> rule3))]
("rabbit" "chases" "bear" "-")
((triple5) -> (rule3 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit sees the squirrel.
True
3
proof
[(((((triple5) -> rule3)) -> rule2))]
("rabbit" "sees" "squirrel" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit does not see the squirrel.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2))]
("rabbit" "sees" "squirrel" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The squirrel does not chase the bear.
Unknown
inv-rconc
[@1: The squirrel chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "bear" "-")
The mouse chases the bear.
Unknown
rconc
[@1: The mouse chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "bear" "+")
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not visit the rabbit.
Unknown
inv-random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The bear is green.[(triple1)] The mouse is young.[(triple2)] The mouse visits the bear.[(triple3 OR ((triple5) -> rule4))] The mouse visits the squirrel.[(triple4)] The rabbit visits the mouse.[(triple5)] The rabbit visits the squirrel.[(triple6)] The squirrel is green.[(triple7)] @1: The rabbit chases the bear.[(((triple5) -> rule3))] @2: The rabbit sees the squirrel.[(((((triple5) -> rule3)) -> rule2))]
The bear is green.
("bear" "is" "green" "+")
triple1
The mouse is young.
("mouse" "is" "young" "+")
triple2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple3
((triple5) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple4
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple5
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple5) -> (rule3 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2