The mouse is big. The mouse is kind. The mouse is rough. The mouse likes the rabbit. The mouse visits the rabbit. The rabbit chases the mouse. The rabbit is nice. The rabbit is rough. The rabbit likes the mouse. The rabbit visits the mouse. If something chases the mouse and it is nice then it does not visit the rabbit.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something chases the mouse and it is nice then it does not visit the rabbit.
((("something" "chases" "mouse" "+") ("something" "is" "nice" "+")) -> ("something" "visits" "rabbit" "-"))
The rabbit visits the mouse.
True
1
proof
[(triple10)]
("rabbit" "visits" "mouse" "+")
triple10
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "visits" "mouse" "-")
triple10
The rabbit does not visit the rabbit.
True
3
proof
[(((triple6 triple7) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((triple6 triple7) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit visits the rabbit.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((triple6 triple7) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
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 chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is kind.[(triple2)] The mouse is rough.[(triple3)] The mouse likes the rabbit.[(triple4)] The mouse visits the rabbit.[(triple5)] The rabbit chases the mouse.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is rough.[(triple8)] The rabbit likes the mouse.[(triple9)] The rabbit visits the mouse.[(triple10)] @1: The rabbit does not visit the rabbit.[(((triple6 triple7) -> rule1))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple9
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple10
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
((triple6 triple7) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1