The mouse is round. The mouse likes the tiger. The mouse needs the tiger. The mouse sees the tiger. The tiger is not kind. The tiger likes the mouse. The tiger needs the mouse. If something likes the mouse and it does not see the mouse then the mouse does not need the tiger. If something is round then it is not red.
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something likes the mouse and it does not see the mouse then the mouse does not need the tiger.
((("something" "likes" "mouse" "+") ("something" "sees" "mouse" "~")) -> ("mouse" "needs" "tiger" "-"))
If something is round then it is not red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
The mouse sees the tiger.
True
1
proof
[(triple4)]
("mouse" "sees" "tiger" "+")
triple4
The mouse does not see the tiger.
False
1
inv-proof
[(triple4)]
("mouse" "sees" "tiger" "-")
triple4
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse is round.[(triple1)] The mouse likes the tiger.[(triple2)] The mouse needs the tiger.[(triple3)] The mouse sees the tiger.[(triple4)] The tiger is not kind.[(triple5)] The tiger likes the mouse.[(triple6)] The tiger needs the mouse.[(triple7)] @1: The mouse is not red.[(((triple1) -> rule2))]
The mouse is round.
("mouse" "is" "round" "+")
triple1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The tiger is not kind.
("tiger" "is" "kind" "-")
triple5
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple6
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple7
The mouse is not red.
("mouse" "is" "red" "-")
((triple1) -> (rule2 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1