The bear visits the squirrel. The mouse chases the squirrel. The mouse is blue. The mouse does not see the squirrel. The mouse visits the squirrel. The squirrel chases the bear. The squirrel does not see the mouse. If something is blue then it chases the bear.
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
If something is blue then it chases the bear.
((("something" "is" "blue" "+")) -> ("something" "chases" "bear" "+"))
The mouse visits the squirrel.
True
1
proof
[(triple5)]
("mouse" "visits" "squirrel" "+")
triple5
The mouse sees the squirrel.
False
1
inv-proof
[(triple4)]
("mouse" "sees" "squirrel" "+")
triple4
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "bear" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bear visits the squirrel.[(triple1)] The mouse chases the squirrel.[(triple2)] The mouse does not see the squirrel.[(triple4)] The mouse is blue.[(triple3)] The mouse visits the squirrel.[(triple5)] The squirrel chases the bear.[(triple6)] The squirrel does not see the mouse.[(triple7)] @1: The mouse chases the bear.[(((triple3) -> rule1))]
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple2
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple5
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple6
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple7
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((triple3) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1