The bear eats the mouse. The bear is blue. The bear does not visit the mouse. The bear visits the squirrel. The mouse eats the bear. The mouse is not red. The mouse sees the squirrel. The mouse visits the squirrel. The squirrel eats the mouse. The squirrel sees the mouse. If someone eats the squirrel then the squirrel is red. If someone is cold then they see the bear. If someone is blue then they eat the squirrel. If the mouse is red and the mouse is rough then the mouse eats the bear. If someone visits the bear then the bear visits the mouse. If someone is red then they eat the bear.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone eats the squirrel then the squirrel is red.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If someone is cold then they see the bear.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "bear" "+"))
If someone is blue then they eat the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "squirrel" "+"))
If the mouse is red and the mouse is rough then the mouse eats the bear.
((("mouse" "is" "red" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "eats" "bear" "+"))
If someone visits the bear then the bear visits the mouse.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If someone is red then they eat the bear.
((("someone" "is" "red" "+")) -> ("someone" "eats" "bear" "+"))
The bear eats the mouse.
True
1
proof
[(triple1)]
("bear" "eats" "mouse" "+")
triple1
The bear visits the mouse.
False
1
inv-proof
[(triple3)]
("bear" "visits" "mouse" "+")
triple3
The bear eats the squirrel.
True
2
proof
[(((triple2) -> rule3))]
("bear" "eats" "squirrel" "+")
((triple2) -> (rule3 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear does not eat the squirrel.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "eats" "squirrel" "-")
((triple2) -> (rule3 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("squirrel" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The squirrel is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("squirrel" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The squirrel eats the bear.
True
4
proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule6))]
("squirrel" "eats" "bear" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int3
The squirrel does not eat the bear.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule6))]
("squirrel" "eats" "bear" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "bear" "-")
The squirrel sees the bear.
Unknown
rconc
[@1: The squirrel sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "bear" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse sees the bear.
Unknown
rconc
[@1: The mouse sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "bear" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
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 does not visit the mouse.[(triple3)] The bear eats the mouse.[(triple1)] The bear is blue.[(triple2)] The bear visits the squirrel.[(triple4)] The mouse eats the bear.[(triple5)] The mouse is not red.[(triple6)] The mouse sees the squirrel.[(triple7)] The mouse visits the squirrel.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel sees the mouse.[(triple10)] @1: The bear eats the squirrel.[(((triple2) -> rule3))] @2: The squirrel is red.[(((((triple2) -> rule3)) -> rule1))] @3: The squirrel eats the bear.[(((((((triple2) -> rule3)) -> rule1)) -> rule6))]
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
triple3
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple4
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple5
The mouse is not red.
("mouse" "is" "red" "-")
triple6
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple10
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
((triple2) -> (rule3 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int3