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