The bear eats the mouse. The bear is blue. The bear is cold. The bear is rough. The bear sees the mouse. The cat likes the mouse. The mouse is blue. The mouse likes the bear. The mouse sees the cat. The squirrel is blue. If someone eats the squirrel then the squirrel eats the mouse. If someone sees the bear then the bear is round. If someone is rough then they see the squirrel. If someone likes the squirrel and they like the bear then the squirrel likes the cat. Round people are kind. If the mouse likes the bear then the mouse sees the bear.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If someone eats the squirrel then the squirrel eats the mouse.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "+"))
If someone sees the bear then the bear is round.
((("someone" "sees" "bear" "+")) -> ("bear" "is" "round" "+"))
If someone is rough then they see the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone likes the squirrel and they like the bear then the squirrel likes the cat.
((("someone" "likes" "squirrel" "+") ("someone" "likes" "bear" "+")) -> ("squirrel" "likes" "cat" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If the mouse likes the bear then the mouse sees the bear.
((("mouse" "likes" "bear" "+")) -> ("mouse" "sees" "bear" "+"))
The mouse likes the bear.
True
1
proof
[(triple8)]
("mouse" "likes" "bear" "+")
triple8
The bear does not eat the mouse.
False
1
inv-proof
[(triple1)]
("bear" "eats" "mouse" "-")
triple1
The mouse sees the bear.
True
2
proof
[(((triple8) -> rule6))]
("mouse" "sees" "bear" "+")
((triple8) -> (rule6 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear does not see the squirrel.
False
2
inv-proof
[(((triple4) -> rule3))]
("bear" "sees" "squirrel" "-")
((triple4) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is round.
True
3
proof
[(((((triple8) -> rule6)) -> rule2))]
("bear" "is" "round" "+")
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear is not round.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule2))]
("bear" "is" "round" "-")
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear is kind.
True
4
proof
[(((((((triple8) -> rule6)) -> rule2)) -> rule5))]
("bear" "is" "kind" "+")
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3
The bear is not kind.
False
4
inv-proof
[(((((((triple8) -> rule6)) -> rule2)) -> rule5))]
("bear" "is" "kind" "-")
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3
The squirrel does not like the cat.
Unknown
inv-rconc
[@1: The squirrel likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "cat" "-")
The mouse sees the squirrel.
Unknown
rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "kind" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The cat does not see the mouse.
Unknown
inv-random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear eats the mouse.[(triple1)] The bear is blue.[(triple2)] The bear is cold.[(triple3)] The bear is rough.[(triple4)] The bear sees the mouse.[(triple5)] The cat likes the mouse.[(triple6)] The mouse is blue.[(triple7)] The mouse likes the bear.[(triple8)] The mouse sees the cat.[(triple9)] The squirrel is blue.[(triple10)] @1: The bear sees the squirrel.[(((triple4) -> rule3))] The mouse sees the bear.[(((triple8) -> rule6))] @2: The bear is round.[(((((triple8) -> rule6)) -> rule2))] @3: The bear is kind.[(((((((triple8) -> rule6)) -> rule2)) -> rule5))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple4) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
((triple8) -> (rule6 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3