The rabbit needs the tiger. The tiger does not like the rabbit. If something needs the rabbit and it likes the tiger then the rabbit needs the tiger. If something needs the tiger then it eats the tiger. If something eats the rabbit then it needs the rabbit. If something eats the tiger and it is kind then the tiger is not green. If something is red then it eats the rabbit. If something eats the tiger then it eats the rabbit. If something likes the rabbit and it is young then it is green. If the tiger is cold and the tiger needs the rabbit then the tiger eats the rabbit.
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger does not like the rabbit.
("tiger" "likes" "rabbit" "-")
If something needs the rabbit and it likes the tiger then the rabbit needs the tiger.
((("something" "needs" "rabbit" "+") ("something" "likes" "tiger" "+")) -> ("rabbit" "needs" "tiger" "+"))
If something needs the tiger then it eats the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the rabbit then it needs the rabbit.
((("something" "eats" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If something eats the tiger and it is kind then the tiger is not green.
((("something" "eats" "tiger" "+") ("something" "is" "kind" "+")) -> ("tiger" "is" "green" "-"))
If something is red then it eats the rabbit.
((("something" "is" "red" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the tiger then it eats the rabbit.
((("something" "eats" "tiger" "+")) -> ("something" "eats" "rabbit" "+"))
If something likes the rabbit and it is young then it is green.
((("something" "likes" "rabbit" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If the tiger is cold and the tiger needs the rabbit then the tiger eats the rabbit.
((("tiger" "is" "cold" "+") ("tiger" "needs" "rabbit" "+")) -> ("tiger" "eats" "rabbit" "+"))
The tiger does not like the rabbit.
True
1
proof
[(triple2)]
("tiger" "likes" "rabbit" "-")
triple2
The rabbit does not need the tiger.
False
1
inv-proof
[(triple1)]
("rabbit" "needs" "tiger" "-")
triple1
The rabbit eats the tiger.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "eats" "tiger" "+")
((triple1) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "eats" "tiger" "-")
((triple1) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("rabbit" "eats" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit needs the rabbit.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule3))]
("rabbit" "needs" "rabbit" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The rabbit does not need the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule3))]
("rabbit" "needs" "rabbit" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "green" "+")
The tiger does not eat the rabbit.
Unknown
inv-rconc
[@2: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("tiger" "eats" "rabbit" "-")
The tiger needs the rabbit.
Unknown
rconc
[@3: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule2 <- FAIL)]]
("tiger" "needs" "rabbit" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The rabbit needs the tiger.[(triple1)] The tiger does not like the rabbit.[(triple2)] @1: The rabbit eats the tiger.[(((triple1) -> rule2))] @2: The rabbit eats the rabbit.[(((((triple1) -> rule2)) -> rule6))] @3: The rabbit needs the rabbit.[(((((((triple1) -> rule2)) -> rule6)) -> rule3))]
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple1
The tiger does not like the rabbit.
("tiger" "likes" "rabbit" "-")
triple2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((triple1) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3