The rabbit eats the tiger. The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is red. The rabbit is young. The rabbit likes the tiger. The rabbit does not visit the tiger. The tiger eats the rabbit. The tiger is not big. The tiger is blue. The tiger is cold. The tiger is red. The tiger is young. The tiger likes the rabbit. The tiger visits the rabbit. If the tiger visits the rabbit and the tiger is not big then the rabbit eats the tiger. If the tiger visits the rabbit and the tiger is blue then the rabbit is cold. If someone is young and not red then they are cold. If someone is big and not blue then they do not visit the rabbit. If someone is red then they visit the rabbit. If someone likes the rabbit and the rabbit is red then they do not visit the tiger. If someone visits the tiger and they are cold then the tiger eats the rabbit. If someone is red and big then they do not eat the rabbit.
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the tiger visits the rabbit and the tiger is not big then the rabbit eats the tiger.
((("tiger" "visits" "rabbit" "+") ("tiger" "is" "big" "~")) -> ("rabbit" "eats" "tiger" "+"))
If the tiger visits the rabbit and the tiger is blue then the rabbit is cold.
((("tiger" "visits" "rabbit" "+") ("tiger" "is" "blue" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is young and not red then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
If someone is big and not blue then they do not visit the rabbit.
((("someone" "is" "big" "+") ("someone" "is" "blue" "~")) -> ("someone" "visits" "rabbit" "-"))
If someone is red then they visit the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone likes the rabbit and the rabbit is red then they do not visit the tiger.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("someone" "visits" "tiger" "-"))
If someone visits the tiger and they are cold then the tiger eats the rabbit.
((("someone" "visits" "tiger" "+") ("someone" "is" "cold" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone is red and big then they do not eat the rabbit.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "eats" "rabbit" "-"))
The tiger is red.
True
1
proof
[(triple13)]
("tiger" "is" "red" "+")
triple13
The tiger is not red.
False
1
inv-proof
[(triple13)]
("tiger" "is" "red" "-")
triple13
The rabbit visits the rabbit.
True
2
proof
[(((triple5) -> rule5))]
("rabbit" "visits" "rabbit" "+")
((triple5) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the rabbit.
False
3
inv-proof
[(((triple5 triple2) -> rule8))]
("rabbit" "eats" "rabbit" "+")
((triple5 triple2) -> (rule8 % int1))
The rabbit does not eat the rabbit.
("rabbit" "eats" "rabbit" "-")
int1
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The rabbit does not visit the tiger.[(triple8)] The rabbit eats the tiger.[(triple1 OR ((triple16 triple10) -> rule1) OR ((((triple13) -> rule5) triple10) -> rule1))] The rabbit is big.[(triple2)] The rabbit is blue.[(triple3)] The rabbit is cold.[(triple4 OR ((triple16 triple11) -> rule2) OR ((((triple13) -> rule5) triple11) -> rule2))] The rabbit is red.[(triple5)] The rabbit is young.[(triple6)] The rabbit likes the tiger.[(triple7)] The tiger eats the rabbit.[(triple9)] The tiger is blue.[(triple11)] The tiger is cold.[(triple12)] The tiger is not big.[(triple10)] The tiger is red.[(triple13)] The tiger is young.[(triple14)] The tiger likes the rabbit.[(triple15)] The tiger visits the rabbit.[(triple16 OR ((triple13) -> rule5))] @1: The rabbit does not eat the rabbit.[(((triple5 triple2) -> rule8))] The rabbit visits the rabbit.[(((triple5) -> rule5))] The tiger does not visit the tiger.[(((triple15 triple5) -> rule6))]
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
triple8
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple1
((triple16 triple10) -> (rule1 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
((((triple13) -> (rule5 % int2)) triple10) -> (rule1 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
((triple16 triple11) -> (rule2 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((((triple13) -> (rule5 % int2)) triple11) -> (rule2 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is not big.
("tiger" "is" "big" "-")
triple10
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 tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple16
((triple13) -> (rule5 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
("rabbit" "eats" "rabbit" "-")
((triple5 triple2) -> (rule8 % int1))
The rabbit does not eat the rabbit.
("rabbit" "eats" "rabbit" "-")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple5) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
((triple15 triple5) -> (rule6 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1