The rabbit is big. The rabbit needs the tiger. The tiger eats the rabbit. If something needs the tiger and the tiger eats the rabbit then the rabbit is red. If something eats the rabbit and the rabbit likes the tiger then the tiger likes the rabbit. If something eats the tiger then the tiger is rough. If something is big then it is round. If something eats the rabbit and it is red then it likes the tiger. All rough things are big. If something likes the tiger and it needs the tiger then the tiger needs the rabbit. If something is rough and it needs the rabbit then the rabbit is big.
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If something needs the tiger and the tiger eats the rabbit then the rabbit is red.
((("something" "needs" "tiger" "+") ("tiger" "eats" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If something eats the rabbit and the rabbit likes the tiger then the tiger likes the rabbit.
((("something" "eats" "rabbit" "+") ("rabbit" "likes" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If something eats the tiger then the tiger is rough.
((("something" "eats" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something eats the rabbit and it is red then it likes the tiger.
((("something" "eats" "rabbit" "+") ("something" "is" "red" "+")) -> ("something" "likes" "tiger" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something likes the tiger and it needs the tiger then the tiger needs the rabbit.
((("something" "likes" "tiger" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "needs" "rabbit" "+"))
If something is rough and it needs the rabbit then the rabbit is big.
((("something" "is" "rough" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
The tiger eats the rabbit.
True
1
proof
[(triple3)]
("tiger" "eats" "rabbit" "+")
triple3
The tiger does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("tiger" "eats" "rabbit" "-")
triple3
The rabbit is round.
True
2
proof
[(((triple1) -> rule4))]
("rabbit" "is" "round" "+")
((triple1) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not red.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("rabbit" "is" "red" "-")
((triple2 triple3) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger is not big.
Unknown
inv-rconc
[@2: The tiger is big.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "is" "big" "-")
The tiger needs the rabbit.
Unknown
rconc
[@2: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("tiger" "needs" "rabbit" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is big.[(triple1)] The rabbit needs the tiger.[(triple2)] The tiger eats the rabbit.[(triple3)] @1: The rabbit is red.[(((triple2 triple3) -> rule1))] The rabbit is round.[(((triple1) -> rule4))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
((triple2 triple3) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1