The rabbit chases the tiger. The rabbit eats the tiger. The rabbit is big. The rabbit is green. The rabbit is red. The rabbit is not round. The rabbit is young. The rabbit likes the tiger. The tiger chases the rabbit. The tiger does not eat the rabbit. The tiger is big. The tiger is not green. The tiger is red. The tiger is young. The tiger likes the rabbit. If someone is young and they eat the tiger then they eat the rabbit. If the rabbit likes the tiger and the tiger does not chase the rabbit then the tiger does not eat the rabbit.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If someone is young and they eat the tiger then they eat the rabbit.
((("someone" "is" "young" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "eats" "rabbit" "+"))
If the rabbit likes the tiger and the tiger does not chase the rabbit then the tiger does not eat the rabbit.
((("rabbit" "likes" "tiger" "+") ("tiger" "chases" "rabbit" "~")) -> ("tiger" "eats" "rabbit" "-"))
The tiger is big.
True
1
proof
[(triple11)]
("tiger" "is" "big" "+")
triple11
The rabbit does not eat the tiger.
False
1
inv-proof
[(triple2)]
("rabbit" "eats" "tiger" "-")
triple2
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 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 big.[(triple3)] The rabbit is green.[(triple4)] The rabbit is not round.[(triple6)] The rabbit is red.[(triple5)] The rabbit is young.[(triple7)] The rabbit likes the tiger.[(triple8)] The tiger chases the rabbit.[(triple9)] The tiger does not eat the rabbit.[(triple10)] The tiger is big.[(triple11)] The tiger is not green.[(triple12)] The tiger is red.[(triple13)] The tiger is young.[(triple14)] The tiger likes the rabbit.[(triple15)] @1: The rabbit eats the rabbit.[(((triple7 triple2) -> rule1))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple4
The rabbit is not round.
("rabbit" "is" "round" "-")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple8
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple9
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is not green.
("tiger" "is" "green" "-")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple15
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple7 triple2) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1