The rabbit is rough. The tiger is nice. The tiger visits the rabbit. If the tiger sees the rabbit and the tiger visits the rabbit then the rabbit chases the tiger. If someone visits the rabbit then they see the rabbit.
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the tiger sees the rabbit and the tiger visits the rabbit then the rabbit chases the tiger.
((("tiger" "sees" "rabbit" "+") ("tiger" "visits" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "+"))
If someone visits the rabbit then they see the rabbit.
((("someone" "visits" "rabbit" "+")) -> ("someone" "sees" "rabbit" "+"))
The tiger visits the rabbit.
True
1
proof
[(triple3)]
("tiger" "visits" "rabbit" "+")
triple3
The tiger is not nice.
False
1
inv-proof
[(triple2)]
("tiger" "is" "nice" "-")
triple2
The tiger sees the rabbit.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "sees" "rabbit" "+")
((triple3) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger does not see the rabbit.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "sees" "rabbit" "-")
((triple3) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit chases the tiger.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("rabbit" "chases" "tiger" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit does not chase the tiger.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("rabbit" "chases" "tiger" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The rabbit is rough.[(triple1)] The tiger is nice.[(triple2)] The tiger visits the rabbit.[(triple3)] @1: The tiger sees the rabbit.[(((triple3) -> rule2))] @2: The rabbit chases the tiger.[(((((triple3) -> rule2) triple3) -> rule1))]
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple3) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2