The rabbit chases the tiger. The rabbit eats the tiger. The rabbit is blue. The rabbit is nice. The rabbit is red. The rabbit is round. The rabbit needs the tiger. The tiger chases the rabbit. The tiger is blue. The tiger is red. The tiger is rough. The tiger needs the rabbit. If something eats the tiger then it needs the rabbit. If the tiger is red and the tiger eats the rabbit then the tiger needs the rabbit. If something needs the tiger and it needs the rabbit then the tiger needs the rabbit. If something eats the tiger then the tiger eats the rabbit. If something eats the tiger and the tiger is rough then the tiger needs the rabbit. All rough things are nice.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something eats the tiger then it needs the rabbit.
((("something" "eats" "tiger" "+")) -> ("something" "needs" "rabbit" "+"))
If the tiger is red and the tiger eats the rabbit then the tiger needs the rabbit.
((("tiger" "is" "red" "+") ("tiger" "eats" "rabbit" "+")) -> ("tiger" "needs" "rabbit" "+"))
If something needs the tiger and it needs the rabbit then the tiger needs the rabbit.
((("something" "needs" "tiger" "+") ("something" "needs" "rabbit" "+")) -> ("tiger" "needs" "rabbit" "+"))
If something eats the tiger then the tiger eats the rabbit.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If something eats the tiger and the tiger is rough then the tiger needs the rabbit.
((("something" "eats" "tiger" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "needs" "rabbit" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
The rabbit is blue.
True
1
proof
[(triple3)]
("rabbit" "is" "blue" "+")
triple3
The rabbit is not round.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "round" "-")
triple6
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit eats the tiger.[(triple2)] The rabbit is blue.[(triple3)] The rabbit is nice.[(triple4)] The rabbit is red.[(triple5)] The rabbit is round.[(triple6)] The rabbit needs the tiger.[(triple7)] The tiger chases the rabbit.[(triple8)] The tiger is blue.[(triple9)] The tiger is red.[(triple10)] The tiger is rough.[(triple11)] The tiger needs the rabbit.[(triple12 OR ((triple2 triple11) -> rule5) OR ((triple10 ((triple2) -> rule4)) -> rule2) OR ((triple7 ((triple2) -> rule1)) -> rule3))] @1: The rabbit needs the rabbit.[(((triple2) -> rule1))] The tiger eats the rabbit.[(((triple2) -> rule4))] The tiger is nice.[(((triple11) -> rule6))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple7
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple12
((triple2 triple11) -> (rule5 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
((triple10 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
((triple7 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple2) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple2) -> (rule4 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple11) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1