The rabbit is kind. The rabbit visits the tiger. The tiger chases the rabbit. If someone chases the tiger and the tiger chases the rabbit then the rabbit is kind. If the rabbit eats the tiger then the tiger is red. If someone visits the rabbit then they are nice. If someone eats the rabbit and the rabbit visits the tiger then the rabbit eats the tiger. If someone visits the rabbit and they are kind then the rabbit eats the tiger. If the tiger is blue then the tiger chases the rabbit. If the rabbit visits the tiger and the rabbit is kind then the tiger eats the rabbit. If someone eats the tiger then they chase the tiger.
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
If someone chases the tiger and the tiger chases the rabbit then the rabbit is kind.
((("someone" "chases" "tiger" "+") ("tiger" "chases" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If the rabbit eats the tiger then the tiger is red.
((("rabbit" "eats" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone visits the rabbit then they are nice.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the rabbit and the rabbit visits the tiger then the rabbit eats the tiger.
((("someone" "eats" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("rabbit" "eats" "tiger" "+"))
If someone visits the rabbit and they are kind then the rabbit eats the tiger.
((("someone" "visits" "rabbit" "+") ("someone" "is" "kind" "+")) -> ("rabbit" "eats" "tiger" "+"))
If the tiger is blue then the tiger chases the rabbit.
((("tiger" "is" "blue" "+")) -> ("tiger" "chases" "rabbit" "+"))
If the rabbit visits the tiger and the rabbit is kind then the tiger eats the rabbit.
((("rabbit" "visits" "tiger" "+") ("rabbit" "is" "kind" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone eats the tiger then they chase the tiger.
((("someone" "eats" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
The rabbit is kind.
True
1
proof
[(triple1)]
("rabbit" "is" "kind" "+")
triple1
The rabbit does not visit the tiger.
False
1
inv-proof
[(triple2)]
("rabbit" "visits" "tiger" "-")
triple2
The tiger eats the rabbit.
True
3
proof
[(((triple2 triple1) -> rule7))]
("tiger" "eats" "rabbit" "+")
((triple2 triple1) -> (rule7 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger does not eat the rabbit.
False
3
inv-proof
[(((triple2 triple1) -> rule7))]
("tiger" "eats" "rabbit" "-")
((triple2 triple1) -> (rule7 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit eats the tiger.
True
5
proof
[(((((triple2 triple1) -> rule7) triple2) -> rule4))]
("rabbit" "eats" "tiger" "+")
((((triple2 triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit does not eat the tiger.
False
5
inv-proof
[(((((triple2 triple1) -> rule7) triple2) -> rule4))]
("rabbit" "eats" "tiger" "-")
((((triple2 triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "nice" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "nice" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The rabbit is kind.[(triple1)] The rabbit visits the tiger.[(triple2)] The tiger chases the rabbit.[(triple3)] @1: The tiger eats the rabbit.[(((triple2 triple1) -> rule7))] @2: The rabbit eats the tiger.[(((((triple2 triple1) -> rule7) triple2) -> rule4))] @3: The rabbit chases the tiger.[(((((((triple2 triple1) -> rule7) triple2) -> rule4)) -> rule8))] The tiger is red.[(((((((triple2 triple1) -> rule7) triple2) -> rule4)) -> rule2))]
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple3
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple2 triple1) -> (rule7 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((((triple2 triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((((((triple2 triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
((((((triple2 triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3