The rabbit eats the tiger. The rabbit is young. The tiger eats the rabbit. If someone likes the rabbit then the rabbit sees the tiger. If someone eats the tiger then the tiger eats the rabbit. If someone is cold then they see the rabbit. If someone is cold and they like the rabbit then the rabbit eats the tiger. If the rabbit sees the tiger and the tiger is nice then the tiger likes the rabbit. If someone eats the rabbit then they are kind. If someone sees the tiger and they eat the tiger then they are nice. If the rabbit likes the tiger then the tiger sees the rabbit.
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If someone likes the rabbit then the rabbit sees the tiger.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone eats the tiger then the tiger eats the rabbit.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone is cold then they see the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is cold and they like the rabbit then the rabbit eats the tiger.
((("someone" "is" "cold" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "eats" "tiger" "+"))
If the rabbit sees the tiger and the tiger is nice then the tiger likes the rabbit.
((("rabbit" "sees" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "likes" "rabbit" "+"))
If someone eats the rabbit then they are kind.
((("someone" "eats" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If someone sees the tiger and they eat the tiger then they are nice.
((("someone" "sees" "tiger" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "is" "nice" "+"))
If the rabbit likes the tiger then the tiger sees the rabbit.
((("rabbit" "likes" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
The tiger eats the rabbit.
True
1
proof
[(triple3 OR ((triple1) -> rule2))]
("tiger" "eats" "rabbit" "+")
triple3
((triple1) -> (rule2 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit is not young.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "young" "-")
triple2
The tiger is kind.
True
2
proof
[(((triple3) -> rule6) OR ((((triple1) -> rule2)) -> rule6))]
("tiger" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger is not kind.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple1) -> rule2)) -> rule6))]
("tiger" "is" "kind" "-")
((triple3) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
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 = (rule7 <- FAIL)]]
("tiger" "is" "nice" "-")
The rabbit sees the tiger.
Unknown
rconc
[@2: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("rabbit" "sees" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The rabbit eats the tiger.[(triple1)] The rabbit is young.[(triple2)] The tiger eats the rabbit.[(triple3 OR ((triple1) -> rule2))] @1: The tiger is kind.[(((triple3) -> rule6) OR ((((triple1) -> rule2)) -> rule6))]
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple1
The rabbit is young.
("rabbit" "is" "young" "+")
triple2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple3
((triple1) -> (rule2 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2