The mouse is kind. The mouse is nice. The mouse is red. The mouse is rough. The mouse likes the tiger. The mouse needs the rabbit. The rabbit chases the tiger. The rabbit is kind. The rabbit is rough. The rabbit needs the tiger. The tiger chases the mouse. The tiger is nice. The tiger is red. The tiger likes the mouse. The tiger likes the rabbit. The tiger needs the rabbit. If something is red then it likes the tiger.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something is red then it likes the tiger.
((("something" "is" "red" "+")) -> ("something" "likes" "tiger" "+"))
The tiger needs the rabbit.
True
1
proof
[(triple16)]
("tiger" "needs" "rabbit" "+")
triple16
The mouse does not like the tiger.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule1))]
("mouse" "likes" "tiger" "-")
triple5
((triple3) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The mouse likes the rabbit.
Unknown
random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "+")
@0: The mouse is kind.[(triple1)] The mouse is nice.[(triple2)] The mouse is red.[(triple3)] The mouse is rough.[(triple4)] The mouse likes the tiger.[(triple5 OR ((triple3) -> rule1))] The mouse needs the rabbit.[(triple6)] The rabbit chases the tiger.[(triple7)] The rabbit is kind.[(triple8)] The rabbit is rough.[(triple9)] The rabbit needs the tiger.[(triple10)] The tiger chases the mouse.[(triple11)] The tiger is nice.[(triple12)] The tiger is red.[(triple13)] The tiger likes the mouse.[(triple14)] The tiger likes the rabbit.[(triple15)] The tiger needs the rabbit.[(triple16)] @1: The tiger likes the tiger.[(((triple13) -> rule1))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
((triple3) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple6
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple10
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple15
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple16
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple13) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1