The rabbit eats the tiger. The rabbit is big. The rabbit is cold. The rabbit is green. The rabbit is kind. The rabbit is round. The rabbit likes the tiger. The rabbit visits the tiger. The tiger eats the rabbit. The tiger is big. The tiger is cold. The tiger is green. The tiger is kind. The tiger is round. The tiger likes the rabbit. The tiger visits the rabbit. If something eats the tiger and it visits the rabbit then the rabbit eats the tiger. If something likes the rabbit and the rabbit is green then it visits the rabbit. If something is round then it eats the rabbit. If something is round then it eats the rabbit. If something visits the rabbit then it eats the rabbit. If something likes the tiger then it visits the rabbit.
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something eats the tiger and it visits the rabbit then the rabbit eats the tiger.
((("something" "eats" "tiger" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "eats" "tiger" "+"))
If something likes the rabbit and the rabbit is green then it visits the rabbit.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("something" "visits" "rabbit" "+"))
If something is round then it eats the rabbit.
((("something" "is" "round" "+")) -> ("something" "eats" "rabbit" "+"))
If something is round then it eats the rabbit.
((("something" "is" "round" "+")) -> ("something" "eats" "rabbit" "+"))
If something visits the rabbit then it eats the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "eats" "rabbit" "+"))
If something likes the tiger then it visits the rabbit.
((("something" "likes" "tiger" "+")) -> ("something" "visits" "rabbit" "+"))
The rabbit is big.
True
1
proof
[(triple2)]
("rabbit" "is" "big" "+")
triple2
The tiger does not like the rabbit.
False
1
inv-proof
[(triple15)]
("tiger" "likes" "rabbit" "-")
triple15
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The rabbit eats the tiger.[(triple1)] The rabbit is big.[(triple2)] The rabbit is cold.[(triple3)] The rabbit is green.[(triple4)] The rabbit is kind.[(triple5)] The rabbit is round.[(triple6)] The rabbit likes the tiger.[(triple7)] The rabbit visits the tiger.[(triple8)] The tiger eats the rabbit.[(triple9 OR ((triple14) -> rule3) OR ((triple14) -> rule4) OR ((triple16) -> rule5) OR ((((triple15 triple4) -> rule2)) -> rule5))] The tiger is big.[(triple10)] The tiger is cold.[(triple11)] The tiger is green.[(triple12)] The tiger is kind.[(triple13)] The tiger is round.[(triple14)] The tiger likes the rabbit.[(triple15)] The tiger visits the rabbit.[(triple16 OR ((triple15 triple4) -> rule2))] @1: The rabbit eats the rabbit.[(((triple6) -> rule3) OR ((triple6) -> rule4) OR ((((triple7) -> rule6)) -> rule5))] The rabbit visits the rabbit.[(((triple7) -> rule6))]
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple7
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple8
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple9
((triple14) -> (rule3 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
((triple14) -> (rule4 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
((triple16) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
((((triple15 triple4) -> (rule2 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple15
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple16
((triple15 triple4) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple6) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((triple6) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple7) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1