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