The bear eats the mouse. The bear eats the rabbit. The bear is nice. The bear needs the mouse. The bear sees the mouse. The mouse eats the bear. The mouse is big. The mouse is kind. The mouse sees the bear. The rabbit is kind. If the bear eats the rabbit and the bear needs the mouse then the bear sees the rabbit. If the bear sees the rabbit then the rabbit needs the mouse. If something eats the bear and it sees the mouse then the mouse needs the bear. If something sees the mouse and it needs the rabbit then the mouse sees the bear. If something sees the rabbit and the rabbit sees the bear then it eats the bear. If something needs the bear and the bear sees the mouse then the bear needs the mouse. If something eats the bear and it is big then the bear is young. If the rabbit eats the mouse and the rabbit needs the bear then the bear is kind.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If the bear eats the rabbit and the bear needs the mouse then the bear sees the rabbit.
((("bear" "eats" "rabbit" "+") ("bear" "needs" "mouse" "+")) -> ("bear" "sees" "rabbit" "+"))
If the bear sees the rabbit then the rabbit needs the mouse.
((("bear" "sees" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something eats the bear and it sees the mouse then the mouse needs the bear.
((("something" "eats" "bear" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If something sees the mouse and it needs the rabbit then the mouse sees the bear.
((("something" "sees" "mouse" "+") ("something" "needs" "rabbit" "+")) -> ("mouse" "sees" "bear" "+"))
If something sees the rabbit and the rabbit sees the bear then it eats the bear.
((("something" "sees" "rabbit" "+") ("rabbit" "sees" "bear" "+")) -> ("something" "eats" "bear" "+"))
If something needs the bear and the bear sees the mouse then the bear needs the mouse.
((("something" "needs" "bear" "+") ("bear" "sees" "mouse" "+")) -> ("bear" "needs" "mouse" "+"))
If something eats the bear and it is big then the bear is young.
((("something" "eats" "bear" "+") ("something" "is" "big" "+")) -> ("bear" "is" "young" "+"))
If the rabbit eats the mouse and the rabbit needs the bear then the bear is kind.
((("rabbit" "eats" "mouse" "+") ("rabbit" "needs" "bear" "+")) -> ("bear" "is" "kind" "+"))
The bear is nice.
True
1
proof
[(triple3)]
("bear" "is" "nice" "+")
triple3
The bear does not see the mouse.
False
1
inv-proof
[(triple5)]
("bear" "sees" "mouse" "-")
triple5
The bear is young.
True
3
proof
[(((triple6 triple7) -> rule7))]
("bear" "is" "young" "+")
((triple6 triple7) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear does not see the rabbit.
False
3
inv-proof
[(((triple2 triple4) -> rule1))]
("bear" "sees" "rabbit" "-")
((triple2 triple4) -> (rule1 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The rabbit needs the mouse.
True
4
proof
[(((((triple2 triple4) -> rule1)) -> rule2))]
("rabbit" "needs" "mouse" "+")
((((triple2 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The rabbit does not need the mouse.
False
4
inv-proof
[(((((triple2 triple4) -> rule1)) -> rule2))]
("rabbit" "needs" "mouse" "-")
((((triple2 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The rabbit does not eat the bear.
Unknown
inv-rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "bear" "-")
The bear eats the bear.
Unknown
rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "+")
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "kind" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear eats the mouse.[(triple1)] The bear eats the rabbit.[(triple2)] The bear is nice.[(triple3)] The bear needs the mouse.[(triple4)] The bear sees the mouse.[(triple5)] The mouse eats the bear.[(triple6)] The mouse is big.[(triple7)] The mouse is kind.[(triple8)] The mouse sees the bear.[(triple9)] The rabbit is kind.[(triple10)] @1: The bear is young.[(((triple6 triple7) -> rule7))] The bear sees the rabbit.[(((triple2 triple4) -> rule1))] @2: The rabbit needs the mouse.[(((((triple2 triple4) -> rule1)) -> rule2))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple5
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The bear is young.
("bear" "is" "young" "+")
((triple6 triple7) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((triple2 triple4) -> (rule1 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((((triple2 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2