The dog chases the rabbit. The dog eats the rabbit. The dog is big. The dog is cold. The dog is green. The dog is red. The dog is young. The dog likes the rabbit. The rabbit chases the dog. The rabbit eats the dog. The rabbit is big. The rabbit is cold. The rabbit is green. The rabbit is red. The rabbit is young. The rabbit likes the dog. If someone likes the dog then they eat the rabbit. If someone eats the rabbit and the rabbit likes the dog then they like the rabbit. If the rabbit is big and the rabbit likes the dog then the rabbit is cold. If someone is cold and they chase the dog then they eat the rabbit. If the dog chases the rabbit then the rabbit eats the dog. If someone likes the rabbit then the rabbit eats the dog.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
If someone likes the dog then they eat the rabbit.
((("someone" "likes" "dog" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone eats the rabbit and the rabbit likes the dog then they like the rabbit.
((("someone" "eats" "rabbit" "+") ("rabbit" "likes" "dog" "+")) -> ("someone" "likes" "rabbit" "+"))
If the rabbit is big and the rabbit likes the dog then the rabbit is cold.
((("rabbit" "is" "big" "+") ("rabbit" "likes" "dog" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is cold and they chase the dog then they eat the rabbit.
((("someone" "is" "cold" "+") ("someone" "chases" "dog" "+")) -> ("someone" "eats" "rabbit" "+"))
If the dog chases the rabbit then the rabbit eats the dog.
((("dog" "chases" "rabbit" "+")) -> ("rabbit" "eats" "dog" "+"))
If someone likes the rabbit then the rabbit eats the dog.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "eats" "dog" "+"))
The rabbit is green.
True
1
proof
[(triple13)]
("rabbit" "is" "green" "+")
triple13
The dog is not cold.
False
1
inv-proof
[(triple4)]
("dog" "is" "cold" "-")
triple4
The rabbit eats the rabbit.
True
2
proof
[(((triple16) -> rule1) OR ((triple12 triple9) -> rule4) OR ((((triple11 triple16) -> rule3) triple9) -> rule4))]
("rabbit" "eats" "rabbit" "+")
((triple16) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((triple12 triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple11 triple16) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple16) -> rule1) OR ((triple12 triple9) -> rule4) OR ((((triple11 triple16) -> rule3) triple9) -> rule4))]
("rabbit" "eats" "rabbit" "-")
((triple16) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((triple12 triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple11 triple16) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit likes the rabbit.
True
4
proof
[(((((triple16) -> rule1) triple16) -> rule2) OR ((((triple12 triple9) -> rule4) triple16) -> rule2) OR ((((((triple11 triple16) -> rule3) triple9) -> rule4) triple16) -> rule2))]
("rabbit" "likes" "rabbit" "+")
((((triple16) -> (rule1 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((triple12 triple9) -> (rule4 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((triple11 triple16) -> (rule3 % int3)) triple9) -> (rule4 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit does not like the rabbit.
False
4
inv-proof
[(((((triple16) -> rule1) triple16) -> rule2) OR ((((triple12 triple9) -> rule4) triple16) -> rule2) OR ((((((triple11 triple16) -> rule3) triple9) -> rule4) triple16) -> rule2))]
("rabbit" "likes" "rabbit" "-")
((((triple16) -> (rule1 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((triple12 triple9) -> (rule4 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((triple11 triple16) -> (rule3 % int3)) triple9) -> (rule4 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog chases the rabbit.[(triple1)] The dog eats the rabbit.[(triple2)] The dog is big.[(triple3)] The dog is cold.[(triple4)] The dog is green.[(triple5)] The dog is red.[(triple6)] The dog is young.[(triple7)] The dog likes the rabbit.[(triple8 OR ((triple2 triple16) -> rule2))] The rabbit chases the dog.[(triple9)] The rabbit eats the dog.[(triple10 OR ((triple1) -> rule5) OR ((triple8) -> rule6) OR ((((triple2 triple16) -> rule2)) -> rule6) OR ((((((triple16) -> rule1) triple16) -> rule2)) -> rule6) OR ((((((triple12 triple9) -> rule4) triple16) -> rule2)) -> rule6) OR ((((((((triple11 triple16) -> rule3) triple9) -> rule4) triple16) -> rule2)) -> rule6))] The rabbit is big.[(triple11)] The rabbit is cold.[(triple12 OR ((triple11 triple16) -> rule3))] The rabbit is green.[(triple13)] The rabbit is red.[(triple14)] The rabbit is young.[(triple15)] The rabbit likes the dog.[(triple16)] @1: The rabbit eats the rabbit.[(((triple16) -> rule1) OR ((triple12 triple9) -> rule4) OR ((((triple11 triple16) -> rule3) triple9) -> rule4))] @2: The rabbit likes the rabbit.[(((((triple16) -> rule1) triple16) -> rule2) OR ((((triple12 triple9) -> rule4) triple16) -> rule2) OR ((((((triple11 triple16) -> rule3) triple9) -> rule4) triple16) -> rule2))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple8
((triple2 triple16) -> (rule2 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple9
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple10
((triple1) -> (rule5 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
((triple8) -> (rule6 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
((((triple2 triple16) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
((((((triple16) -> (rule1 % int3)) triple16) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
((((((triple12 triple9) -> (rule4 % int3)) triple16) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
((((((((triple11 triple16) -> (rule3 % int4)) triple9) -> (rule4 % int3)) triple16) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
((triple11 triple16) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple13
The rabbit is red.
("rabbit" "is" "red" "+")
triple14
The rabbit is young.
("rabbit" "is" "young" "+")
triple15
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple16
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple16) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((triple12 triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple11 triple16) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple16) -> (rule1 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((triple12 triple9) -> (rule4 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((triple11 triple16) -> (rule3 % int3)) triple9) -> (rule4 % int2)) triple16) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3