The mouse is not blue. The mouse likes the rabbit. The mouse visits the tiger. The rabbit is green. The rabbit is red. The tiger is green. The tiger is rough. If something is green and it visits the tiger then the tiger chases the rabbit. If something visits the tiger then it is rough.
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If something is green and it visits the tiger then the tiger chases the rabbit.
((("something" "is" "green" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something visits the tiger then it is rough.
((("something" "visits" "tiger" "+")) -> ("something" "is" "rough" "+"))
The tiger is rough.
True
1
proof
[(triple7)]
("tiger" "is" "rough" "+")
triple7
The rabbit is not red.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "red" "-")
triple5
The mouse is rough.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "is" "rough" "+")
((triple3) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "is" "rough" "-")
((triple3) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "rough" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The mouse chases the rabbit.
Unknown
random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "+")
@0: The mouse is not blue.[(triple1)] The mouse likes the rabbit.[(triple2)] The mouse visits the tiger.[(triple3)] The rabbit is green.[(triple4)] The rabbit is red.[(triple5)] The tiger is green.[(triple6)] The tiger is rough.[(triple7)] @1: The mouse is rough.[(((triple3) -> rule2))]
The mouse is not blue.
("mouse" "is" "blue" "-")
triple1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1