The mouse is big. The mouse is round. The mouse is young. The mouse likes the rabbit. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit is not kind. The rabbit does not like the mouse. The rabbit needs the mouse. The rabbit does not see the mouse. If someone likes the rabbit and they do not see the mouse then the mouse is not kind.
The mouse is big.
("mouse" "is" "big" "+")
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 mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
If someone likes the rabbit and they do not see the mouse then the mouse is not kind.
((("someone" "likes" "rabbit" "+") ("someone" "sees" "mouse" "~")) -> ("mouse" "is" "kind" "-"))
The mouse is big.
True
1
proof
[(triple1)]
("mouse" "is" "big" "+")
triple1
The mouse does not like the rabbit.
False
1
inv-proof
[(triple4)]
("mouse" "likes" "rabbit" "-")
triple4
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The mouse is big.[(triple1)] The mouse is round.[(triple2)] The mouse is young.[(triple3)] The mouse likes the rabbit.[(triple4)] The mouse needs the rabbit.[(triple5)] The mouse sees the rabbit.[(triple6)] The rabbit does not like the mouse.[(triple8)] The rabbit does not see the mouse.[(triple10)] The rabbit is not kind.[(triple7)] The rabbit needs the mouse.[(triple9)]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple5
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple6
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
triple8
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
triple10
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple7
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple9