The mouse is green. The mouse is kind. The mouse is nice. The mouse is red. The mouse is rough. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit is green. The rabbit is nice. The rabbit is red. The rabbit is rough. The rabbit needs the mouse. The rabbit sees the mouse. The rabbit visits the mouse. If someone sees the mouse and they are red then they need the rabbit. If someone is red then they visit the mouse. If the rabbit visits the mouse and the rabbit sees the mouse then the mouse needs the rabbit. If someone needs the mouse then the mouse needs the rabbit. If someone is nice then they need the rabbit. If someone needs the mouse then they see the mouse.
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone sees the mouse and they are red then they need the rabbit.
((("someone" "sees" "mouse" "+") ("someone" "is" "red" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is red then they visit the mouse.
((("someone" "is" "red" "+")) -> ("someone" "visits" "mouse" "+"))
If the rabbit visits the mouse and the rabbit sees the mouse then the mouse needs the rabbit.
((("rabbit" "visits" "mouse" "+") ("rabbit" "sees" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone needs the mouse then the mouse needs the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone is nice then they need the rabbit.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the mouse then they see the mouse.
((("someone" "needs" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
The mouse is rough.
True
1
proof
[(triple5)]
("mouse" "is" "rough" "+")
triple5
The mouse is not nice.
False
1
inv-proof
[(triple3)]
("mouse" "is" "nice" "-")
triple3
The rabbit needs the rabbit.
True
2
proof
[(((triple10) -> rule5) OR ((triple14 triple11) -> rule1) OR ((((triple13) -> rule6) triple11) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((triple14 triple11) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple13) -> (rule6 % int2)) triple11) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple4) -> rule2))]
("mouse" "visits" "mouse" "-")
((triple4) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The mouse is green.[(triple1)] The mouse is kind.[(triple2)] The mouse is nice.[(triple3)] The mouse is red.[(triple4)] The mouse is rough.[(triple5)] The mouse needs the rabbit.[(triple6 OR ((triple13) -> rule4) OR ((triple3) -> rule5) OR ((triple15 triple14) -> rule3) OR ((triple15 ((triple13) -> rule6)) -> rule3) OR ((((triple11) -> rule2) triple14) -> rule3) OR ((((triple11) -> rule2) ((triple13) -> rule6)) -> rule3))] The mouse sees the rabbit.[(triple7)] The mouse visits the rabbit.[(triple8)] The rabbit is green.[(triple9)] The rabbit is nice.[(triple10)] The rabbit is red.[(triple11)] The rabbit is rough.[(triple12)] The rabbit needs the mouse.[(triple13)] The rabbit sees the mouse.[(triple14 OR ((triple13) -> rule6))] The rabbit visits the mouse.[(triple15 OR ((triple11) -> rule2))] @1: The mouse visits the mouse.[(((triple4) -> rule2))] The rabbit needs the rabbit.[(((triple10) -> rule5) OR ((triple14 triple11) -> rule1) OR ((((triple13) -> rule6) triple11) -> rule1))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple6
((triple13) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple3) -> (rule5 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple15 triple14) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple15 ((triple13) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
((((triple11) -> (rule2 % int2)) triple14) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple13) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple7
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple14
((triple13) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple15
((triple11) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple4) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((triple14 triple11) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple13) -> (rule6 % int2)) triple11) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2