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