The bear chases the squirrel. The bear is cold. The bear is not kind. The bear is red. The bear is not round. The bear needs the mouse. The bear needs the squirrel. The bear does not visit the mouse. The mouse is blue. The mouse is kind. The mouse is round. The mouse needs the bear. The squirrel is round. The squirrel does not need the bear. The squirrel needs the mouse. The squirrel does not visit the mouse. Cold, round things are kind. If something is cold and blue then it needs the bear. If something chases the mouse then the mouse does not visit the squirrel. If something is kind and it does not chase the squirrel then the squirrel chases the bear. If something is blue then it chases the mouse. If the mouse visits the bear and the mouse does not need the bear then the bear visits the mouse.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is not kind.
("bear" "is" "kind" "-")
The bear is red.
("bear" "is" "red" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel does not need the bear.
("squirrel" "needs" "bear" "-")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
Cold, round things are kind.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is cold and blue then it needs the bear.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "bear" "+"))
If something chases the mouse then the mouse does not visit the squirrel.
((("something" "chases" "mouse" "+")) -> ("mouse" "visits" "squirrel" "-"))
If something is kind and it does not chase the squirrel then the squirrel chases the bear.
((("something" "is" "kind" "+") ("something" "chases" "squirrel" "~")) -> ("squirrel" "chases" "bear" "+"))
If something is blue then it chases the mouse.
((("something" "is" "blue" "+")) -> ("something" "chases" "mouse" "+"))
If the mouse visits the bear and the mouse does not need the bear then the bear visits the mouse.
((("mouse" "visits" "bear" "+") ("mouse" "needs" "bear" "~")) -> ("bear" "visits" "mouse" "+"))
The bear is not round.
True
1
proof
[(triple5)]
("bear" "is" "round" "-")
triple5
The squirrel visits the mouse.
False
1
inv-proof
[(triple16)]
("squirrel" "visits" "mouse" "+")
triple16
The mouse chases the mouse.
True
2
proof
[(((triple9) -> rule5))]
("mouse" "chases" "mouse" "+")
((triple9) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple9) -> rule5))]
("mouse" "chases" "mouse" "-")
((triple9) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The bear does not chase the mouse.
Unknown
inv-rconc
[@1: The bear chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "chases" "mouse" "-")
The squirrel chases the mouse.
Unknown
rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear chases the squirrel.[(triple1)] The bear does not visit the mouse.[(triple8)] The bear is cold.[(triple2)] The bear is not kind.[(triple3)] The bear is not round.[(triple5)] The bear is red.[(triple4)] The bear needs the mouse.[(triple6)] The bear needs the squirrel.[(triple7)] The mouse is blue.[(triple9)] The mouse is kind.[(triple10)] The mouse is round.[(triple11)] The mouse needs the bear.[(triple12)] The squirrel does not need the bear.[(triple14)] The squirrel does not visit the mouse.[(triple16)] The squirrel is round.[(triple13)] The squirrel needs the mouse.[(triple15)] @1: The mouse chases the mouse.[(((triple9) -> rule5))] @2: The mouse does not visit the squirrel.[(((((triple9) -> rule5)) -> rule3))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
triple8
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is not kind.
("bear" "is" "kind" "-")
triple3
The bear is not round.
("bear" "is" "round" "-")
triple5
The bear is red.
("bear" "is" "red" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple6
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse is round.
("mouse" "is" "round" "+")
triple11
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple12
The squirrel does not need the bear.
("squirrel" "needs" "bear" "-")
triple14
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
triple16
The squirrel is round.
("squirrel" "is" "round" "+")
triple13
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple15
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple9) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2