The bear does not chase the dog. The bear likes the lion. The cow is round. The cow is young. The dog chases the bear. The dog does not like the bear. The dog visits the cow. The lion does not chase the cow. The lion is red. The lion likes the dog. The lion visits the bear. If someone likes the cow and they are round then they visit the dog. If someone visits the dog and they are not round then they are kind. If someone likes the dog then they visit the cow. If someone chases the cow and the cow visits the dog then the dog does not like the lion. If someone likes the cow then the cow likes the dog. If someone is red and they visit the cow then they do not chase the dog. If someone chases the lion then the lion is kind. If someone visits the cow then they like the cow. If someone visits the dog and the dog is young then the dog chases the bear.
The bear does not chase the dog.
("bear" "chases" "dog" "-")
The bear likes the lion.
("bear" "likes" "lion" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog does not like the bear.
("dog" "likes" "bear" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion does not chase the cow.
("lion" "chases" "cow" "-")
The lion is red.
("lion" "is" "red" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone likes the cow and they are round then they visit the dog.
((("someone" "likes" "cow" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog and they are not round then they are kind.
((("someone" "visits" "dog" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "kind" "+"))
If someone likes the dog then they visit the cow.
((("someone" "likes" "dog" "+")) -> ("someone" "visits" "cow" "+"))
If someone chases the cow and the cow visits the dog then the dog does not like the lion.
((("someone" "chases" "cow" "+") ("cow" "visits" "dog" "+")) -> ("dog" "likes" "lion" "-"))
If someone likes the cow then the cow likes the dog.
((("someone" "likes" "cow" "+")) -> ("cow" "likes" "dog" "+"))
If someone is red and they visit the cow then they do not chase the dog.
((("someone" "is" "red" "+") ("someone" "visits" "cow" "+")) -> ("someone" "chases" "dog" "-"))
If someone chases the lion then the lion is kind.
((("someone" "chases" "lion" "+")) -> ("lion" "is" "kind" "+"))
If someone visits the cow then they like the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the dog and the dog is young then the dog chases the bear.
((("someone" "visits" "dog" "+") ("dog" "is" "young" "+")) -> ("dog" "chases" "bear" "+"))
The dog visits the cow.
True
1
proof
[(triple7)]
("dog" "visits" "cow" "+")
triple7
The bear does not like the lion.
False
1
inv-proof
[(triple2)]
("bear" "likes" "lion" "-")
triple2
The dog likes the cow.
True
2
proof
[(((triple7) -> rule8))]
("dog" "likes" "cow" "+")
((triple7) -> (rule8 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The lion does not visit the cow.
False
2
inv-proof
[(((triple10) -> rule3))]
("lion" "visits" "cow" "-")
((triple10) -> (rule3 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion does not chase the dog.
True
4
proof
[(((triple9 ((triple10) -> rule3)) -> rule6))]
("lion" "chases" "dog" "-")
((triple9 ((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The lion does not chase the dog.
("lion" "chases" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion does not like the cow.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule8))]
("lion" "likes" "cow" "-")
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow visits the cow.
True
4
proof
[(((((((triple7) -> rule8)) -> rule5)) -> rule3) OR ((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3))]
("cow" "visits" "cow" "+")
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog likes the cow.
("dog" "likes" "cow" "+")
int3
((((((((triple10) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The cow does not visit the cow.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule5)) -> rule3) OR ((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3))]
("cow" "visits" "cow" "-")
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog likes the cow.
("dog" "likes" "cow" "+")
int3
((((((((triple10) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The cow likes the cow.
True
5
proof
[(((((((((triple7) -> rule8)) -> rule5)) -> rule3)) -> rule8) OR ((((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3)) -> rule8))]
("cow" "likes" "cow" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The dog likes the cow.
("dog" "likes" "cow" "+")
int4
((((((((((triple10) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The lion likes the cow.
("lion" "likes" "cow" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The cow does not like the cow.
False
5
inv-proof
[(((((((((triple7) -> rule8)) -> rule5)) -> rule3)) -> rule8) OR ((((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3)) -> rule8))]
("cow" "likes" "cow" "-")
((((((((triple7) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The dog likes the cow.
("dog" "likes" "cow" "+")
int4
((((((((((triple10) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The lion likes the cow.
("lion" "likes" "cow" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The cow visits the dog.
True
7
proof
[(((((((((((triple7) -> rule8)) -> rule5)) -> rule3)) -> rule8) triple3) -> rule1) OR ((((((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3)) -> rule8) triple3) -> rule1))]
("cow" "visits" "dog" "+")
((((((((((triple7) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The dog likes the cow.
("dog" "likes" "cow" "+")
int5
((((((((((((triple10) -> (rule3 % int6))) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The lion likes the cow.
("lion" "likes" "cow" "+")
int5
The lion visits the cow.
("lion" "visits" "cow" "+")
int6
The cow does not visit the dog.
False
7
inv-proof
[(((((((((((triple7) -> rule8)) -> rule5)) -> rule3)) -> rule8) triple3) -> rule1) OR ((((((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3)) -> rule8) triple3) -> rule1))]
("cow" "visits" "dog" "-")
((((((((((triple7) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The dog likes the cow.
("dog" "likes" "cow" "+")
int5
((((((((((((triple10) -> (rule3 % int6))) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The lion likes the cow.
("lion" "likes" "cow" "+")
int5
The lion visits the cow.
("lion" "visits" "cow" "+")
int6
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "kind" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "kind" "+")
The bear does not visit the cow.
Unknown
inv-rconc
[@1: The bear visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "cow" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "kind" "+")
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "dog" "-")
The lion visits the dog.
Unknown
rconc
[@1: The lion visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "dog" "+")
The cow does not like the lion.
Unknown
inv-random
[@0: The cow likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "lion" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The dog visits the bear.
Unknown
random
[@0: The dog visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bear" "+")
@0: The bear does not chase the dog.[(triple1)] The bear likes the lion.[(triple2)] The cow is round.[(triple3)] The cow is young.[(triple4)] The dog chases the bear.[(triple5)] The dog does not like the bear.[(triple6)] The dog visits the cow.[(triple7)] The lion does not chase the cow.[(triple8)] The lion is red.[(triple9)] The lion likes the dog.[(triple10)] The lion visits the bear.[(triple11)] @1: The dog likes the cow.[(((triple7) -> rule8))] The lion visits the cow.[(((triple10) -> rule3))] @2: The cow likes the dog.[(((((triple7) -> rule8)) -> rule5) OR ((((((triple10) -> rule3)) -> rule8)) -> rule5))] The lion does not chase the dog.[(((triple9 ((triple10) -> rule3)) -> rule6))] The lion likes the cow.[(((((triple10) -> rule3)) -> rule8))] @3: The cow visits the cow.[(((((((triple7) -> rule8)) -> rule5)) -> rule3) OR ((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3))] @4: The cow likes the cow.[(((((((((triple7) -> rule8)) -> rule5)) -> rule3)) -> rule8) OR ((((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3)) -> rule8))] @5: The cow visits the dog.[(((((((((((triple7) -> rule8)) -> rule5)) -> rule3)) -> rule8) triple3) -> rule1) OR ((((((((((((triple10) -> rule3)) -> rule8)) -> rule5)) -> rule3)) -> rule8) triple3) -> rule1))]
The bear does not chase the dog.
("bear" "chases" "dog" "-")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The dog chases the bear.
("dog" "chases" "bear" "+")
triple5
The dog does not like the bear.
("dog" "likes" "bear" "-")
triple6
The dog visits the cow.
("dog" "visits" "cow" "+")
triple7
The lion does not chase the cow.
("lion" "chases" "cow" "-")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion likes the dog.
("lion" "likes" "dog" "+")
triple10
The lion visits the bear.
("lion" "visits" "bear" "+")
triple11
The dog likes the cow.
("dog" "likes" "cow" "+")
((triple7) -> (rule8 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
((triple10) -> (rule3 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
((((triple7) -> (rule8 % int2))) -> (rule5 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The lion does not chase the dog.
("lion" "chases" "dog" "-")
((triple9 ((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The lion does not chase the dog.
("lion" "chases" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog likes the cow.
("dog" "likes" "cow" "+")
int3
((((((((triple10) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The dog likes the cow.
("dog" "likes" "cow" "+")
int4
((((((((((triple10) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The lion likes the cow.
("lion" "likes" "cow" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The cow visits the dog.
("cow" "visits" "dog" "+")
((((((((((triple7) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The dog likes the cow.
("dog" "likes" "cow" "+")
int5
((((((((((((triple10) -> (rule3 % int6))) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The lion likes the cow.
("lion" "likes" "cow" "+")
int5
The lion visits the cow.
("lion" "visits" "cow" "+")
int6