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