The bear is green. The bear is not round. The bear likes the mouse. The bear sees the mouse. The mouse does not eat the bear. The mouse is green. The mouse is rough. If someone sees the mouse and they like the bear then they do not like the mouse. If someone is kind and rough then they do not see the bear. If someone likes the mouse then the mouse is green. If someone sees the mouse then the mouse likes the bear. If the mouse is green then the mouse is kind. If someone is green and not round then they eat the mouse. If someone likes the bear then they see the mouse. If the mouse eats the bear then the bear likes the mouse.
The bear is green.
("bear" "is" "green" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If someone sees the mouse and they like the bear then they do not like the mouse.
((("someone" "sees" "mouse" "+") ("someone" "likes" "bear" "+")) -> ("someone" "likes" "mouse" "-"))
If someone is kind and rough then they do not see the bear.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "sees" "bear" "-"))
If someone likes the mouse then the mouse is green.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If someone sees the mouse then the mouse likes the bear.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If the mouse is green then the mouse is kind.
((("mouse" "is" "green" "+")) -> ("mouse" "is" "kind" "+"))
If someone is green and not round then they eat the mouse.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "eats" "mouse" "+"))
If someone likes the bear then they see the mouse.
((("someone" "likes" "bear" "+")) -> ("someone" "sees" "mouse" "+"))
If the mouse eats the bear then the bear likes the mouse.
((("mouse" "eats" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
The mouse is rough.
True
1
proof
[(triple7)]
("mouse" "is" "rough" "+")
triple7
The bear is not green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The bear eats the mouse.
True
3
proof
[(((triple1 triple2) -> rule6))]
("bear" "eats" "mouse" "+")
((triple1 triple2) -> (rule6 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse does not like the bear.
False
2
inv-proof
[(((triple4) -> rule4))]
("mouse" "likes" "bear" "-")
((triple4) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse does not see the bear.
True
4
proof
[(((((triple6) -> rule5) triple7) -> rule2) OR ((((((triple3) -> rule3)) -> rule5) triple7) -> rule2))]
("mouse" "sees" "bear" "-")
((((triple6) -> (rule5 % int2)) triple7) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse sees the bear.
False
4
inv-proof
[(((((triple6) -> rule5) triple7) -> rule2) OR ((((((triple3) -> rule3)) -> rule5) triple7) -> rule2))]
("mouse" "sees" "bear" "+")
((((triple6) -> (rule5 % int2)) triple7) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse does not like the mouse.
True
6
proof
[(((((((triple4) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule1))]
("mouse" "likes" "mouse" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The mouse likes the mouse.
False
6
inv-proof
[(((((((triple4) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule1))]
("mouse" "likes" "mouse" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear is green.[(triple1)] The bear is not round.[(triple2)] The bear likes the mouse.[(triple3)] The bear sees the mouse.[(triple4)] The mouse does not eat the bear.[(triple5)] The mouse is green.[(triple6 OR ((triple3) -> rule3))] The mouse is rough.[(triple7)] @1: The bear eats the mouse.[(((triple1 triple2) -> rule6))] The mouse is kind.[(((triple6) -> rule5) OR ((((triple3) -> rule3)) -> rule5))] The mouse likes the bear.[(((triple4) -> rule4))] @2: The mouse does not see the bear.[(((((triple6) -> rule5) triple7) -> rule2) OR ((((((triple3) -> rule3)) -> rule5) triple7) -> rule2))] The mouse sees the mouse.[(((((triple4) -> rule4)) -> rule7))] @3: The mouse does not like the mouse.[(((((((triple4) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule1))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is not round.
("bear" "is" "round" "-")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
((triple3) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The bear eats the mouse.
("bear" "eats" "mouse" "+")
((triple1 triple2) -> (rule6 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple6) -> (rule5 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((triple4) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
((((triple6) -> (rule5 % int2)) triple7) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3