The cow chases the dog. The cow is blue. The dog eats the cow. The dog eats the rabbit. The lion chases the dog. The lion eats the cow. The lion eats the rabbit. The lion is blue. The lion is kind. The lion is rough. The lion visits the dog. The rabbit chases the cow. The rabbit eats the lion. The rabbit is blue. The rabbit is cold. If something eats the rabbit then it eats the cow. If something chases the dog and the dog is rough then it chases the rabbit. If something visits the cow then it eats the rabbit. If something is cold then it visits the cow. If something is kind and it visits the dog then the dog visits the cow. If something visits the dog and the dog eats the cow then it chases the cow.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is blue.
("cow" "is" "blue" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
If something eats the rabbit then it eats the cow.
((("something" "eats" "rabbit" "+")) -> ("something" "eats" "cow" "+"))
If something chases the dog and the dog is rough then it chases the rabbit.
((("something" "chases" "dog" "+") ("dog" "is" "rough" "+")) -> ("something" "chases" "rabbit" "+"))
If something visits the cow then it eats the rabbit.
((("something" "visits" "cow" "+")) -> ("something" "eats" "rabbit" "+"))
If something is cold then it visits the cow.
((("something" "is" "cold" "+")) -> ("something" "visits" "cow" "+"))
If something is kind and it visits the dog then the dog visits the cow.
((("something" "is" "kind" "+") ("something" "visits" "dog" "+")) -> ("dog" "visits" "cow" "+"))
If something visits the dog and the dog eats the cow then it chases the cow.
((("something" "visits" "dog" "+") ("dog" "eats" "cow" "+")) -> ("something" "chases" "cow" "+"))
The lion is kind.
True
1
proof
[(triple9)]
("lion" "is" "kind" "+")
triple9
The dog does not eat the cow.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule1) OR ((((((triple9 triple11) -> rule5)) -> rule3)) -> rule1))]
("dog" "eats" "cow" "-")
triple3
((triple4) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
((((((triple9 triple11) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The dog visits the cow.
True
3
proof
[(((triple9 triple11) -> rule5))]
("dog" "visits" "cow" "+")
((triple9 triple11) -> (rule5 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog does not visit the cow.
False
3
inv-proof
[(((triple9 triple11) -> rule5))]
("dog" "visits" "cow" "-")
((triple9 triple11) -> (rule5 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple15) -> rule4)) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((((triple15) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple15) -> rule4)) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((((triple15) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit eats the cow.
True
4
proof
[(((((((triple15) -> rule4)) -> rule3)) -> rule1))]
("rabbit" "eats" "cow" "+")
((((((triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The rabbit does not eat the cow.
False
4
inv-proof
[(((((((triple15) -> rule4)) -> rule3)) -> rule1))]
("rabbit" "eats" "cow" "-")
((((((triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The cow does not eat the rabbit.
Unknown
inv-rconc
[@2: The cow eats the rabbit.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("cow" "eats" "rabbit" "-")
The cow eats the cow.
Unknown
rconc
[@3: The cow eats the cow.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule4 <- FAIL)]]
("cow" "eats" "cow" "+")
The dog does not chase the cow.
Unknown
inv-rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "cow" "-")
The lion chases the rabbit.
Unknown
rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "rabbit" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The cow chases the dog.[(triple1)] The cow is blue.[(triple2)] The dog eats the cow.[(triple3 OR ((triple4) -> rule1) OR ((((((triple9 triple11) -> rule5)) -> rule3)) -> rule1))] The dog eats the rabbit.[(triple4 OR ((((triple9 triple11) -> rule5)) -> rule3))] The lion chases the dog.[(triple5)] The lion eats the cow.[(triple6 OR ((triple7) -> rule1))] The lion eats the rabbit.[(triple7)] The lion is blue.[(triple8)] The lion is kind.[(triple9)] The lion is rough.[(triple10)] The lion visits the dog.[(triple11)] The rabbit chases the cow.[(triple12)] The rabbit eats the lion.[(triple13)] The rabbit is blue.[(triple14)] The rabbit is cold.[(triple15)] @1: The dog visits the cow.[(((triple9 triple11) -> rule5))] The lion chases the cow.[(((triple11 triple3) -> rule6) OR ((triple11 ((triple4) -> rule1)) -> rule6) OR ((triple11 ((((((triple9 triple11) -> rule5)) -> rule3)) -> rule1)) -> rule6))] The rabbit visits the cow.[(((triple15) -> rule4))] @2: The rabbit eats the rabbit.[(((((triple15) -> rule4)) -> rule3))] @3: The rabbit eats the cow.[(((((((triple15) -> rule4)) -> rule3)) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The dog eats the cow.
("dog" "eats" "cow" "+")
triple3
((triple4) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
((((((triple9 triple11) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple4
((((triple9 triple11) -> (rule5 % int2))) -> (rule3 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
The lion eats the cow.
("lion" "eats" "cow" "+")
triple6
((triple7) -> (rule1 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
triple8
The lion is kind.
("lion" "is" "kind" "+")
triple9
The lion is rough.
("lion" "is" "rough" "+")
triple10
The lion visits the dog.
("lion" "visits" "dog" "+")
triple11
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple12
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple13
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple14
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple15
The dog visits the cow.
("dog" "visits" "cow" "+")
((triple9 triple11) -> (rule5 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple11 triple3) -> (rule6 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
((triple11 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
((triple11 ((((((triple9 triple11) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
((triple15) -> (rule4 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple15) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((((((triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3