The mouse eats the rabbit. The mouse is green. The mouse is kind. The mouse is rough. The mouse is round. The mouse is young. The mouse likes the rabbit. The mouse needs the rabbit. The rabbit eats the mouse. The rabbit is green. The rabbit is kind. The rabbit is rough. The rabbit is round. The rabbit is young. The rabbit likes the mouse. The rabbit needs the mouse. If someone needs the mouse then the mouse needs the rabbit. If someone likes the mouse then they need the rabbit. If someone is kind and green then they eat the rabbit.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If someone needs the mouse then the mouse needs the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone likes the mouse then they need the rabbit.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is kind and green then they eat the rabbit.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "rabbit" "+"))
The rabbit is rough.
True
1
proof
[(triple12)]
("rabbit" "is" "rough" "+")
triple12
The rabbit is not green.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "green" "-")
triple10
The rabbit needs the rabbit.
True
2
proof
[(((triple15) -> rule2))]
("rabbit" "needs" "rabbit" "+")
((triple15) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((triple11 triple10) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((triple11 triple10) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The mouse eats the rabbit.[(triple1 OR ((triple3 triple2) -> rule3))] The mouse is green.[(triple2)] The mouse is kind.[(triple3)] The mouse is rough.[(triple4)] The mouse is round.[(triple5)] The mouse is young.[(triple6)] The mouse likes the rabbit.[(triple7)] The mouse needs the rabbit.[(triple8 OR ((triple16) -> rule1))] The rabbit eats the mouse.[(triple9)] The rabbit is green.[(triple10)] The rabbit is kind.[(triple11)] The rabbit is rough.[(triple12)] The rabbit is round.[(triple13)] The rabbit is young.[(triple14)] The rabbit likes the mouse.[(triple15)] The rabbit needs the mouse.[(triple16)] @1: The rabbit eats the rabbit.[(((triple11 triple10) -> rule3))] The rabbit needs the rabbit.[(((triple15) -> rule2))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
((triple3 triple2) -> (rule3 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple7
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple8
((triple16) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple15
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple16
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple11 triple10) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple15) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1