The bear eats the dog. The bear is kind. The bear is red. The bear likes the cow. The bear likes the lion. The bear sees the cow. The cow eats the dog. The cow sees the bear. The dog eats the bear. The dog eats the cow. The dog is nice. The dog sees the bear. The lion likes the bear. The lion likes the cow. The lion likes the dog. The lion sees the bear. If someone eats the cow and they are cold then the cow likes the dog. If someone likes the dog then the dog is cold. If someone eats the dog then they like the dog. If someone is kind then they are young. If someone is kind and young then they eat the cow. If the lion likes the bear and the bear sees the lion then the lion eats the cow. If someone eats the lion then they see the dog. If someone eats the cow then they see the lion. If the lion is young and the lion likes the bear then the bear sees the lion.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If someone eats the cow and they are cold then the cow likes the dog.
((("someone" "eats" "cow" "+") ("someone" "is" "cold" "+")) -> ("cow" "likes" "dog" "+"))
If someone likes the dog then the dog is cold.
((("someone" "likes" "dog" "+")) -> ("dog" "is" "cold" "+"))
If someone eats the dog then they like the dog.
((("someone" "eats" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and young then they eat the cow.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "eats" "cow" "+"))
If the lion likes the bear and the bear sees the lion then the lion eats the cow.
((("lion" "likes" "bear" "+") ("bear" "sees" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If someone eats the lion then they see the dog.
((("someone" "eats" "lion" "+")) -> ("someone" "sees" "dog" "+"))
If someone eats the cow then they see the lion.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "lion" "+"))
If the lion is young and the lion likes the bear then the bear sees the lion.
((("lion" "is" "young" "+") ("lion" "likes" "bear" "+")) -> ("bear" "sees" "lion" "+"))
The dog sees the bear.
True
1
proof
[(triple12)]
("dog" "sees" "bear" "+")
triple12
The bear does not see the cow.
False
1
inv-proof
[(triple6)]
("bear" "sees" "cow" "-")
triple6
The dog is cold.
True
2
proof
[(((triple15) -> rule2) OR ((((triple1) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("dog" "is" "cold" "+")
((triple15) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog does not see the lion.
False
2
inv-proof
[(((triple10) -> rule8))]
("dog" "sees" "lion" "-")
((triple10) -> (rule8 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The bear eats the cow.
True
4
proof
[(((triple2 ((triple2) -> rule4)) -> rule5))]
("bear" "eats" "cow" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear does not eat the cow.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule5))]
("bear" "eats" "cow" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear sees the lion.
True
5
proof
[(((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8))]
("bear" "sees" "lion" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear does not see the lion.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8))]
("bear" "sees" "lion" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The lion eats the cow.
True
7
proof
[(((triple13 ((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8)) -> rule6))]
("lion" "eats" "cow" "+")
((triple13 ((((triple2 ((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The bear is young.
("bear" "is" "young" "+")
int4
The lion does not eat the cow.
False
7
inv-proof
[(((triple13 ((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8)) -> rule6))]
("lion" "eats" "cow" "-")
((triple13 ((((triple2 ((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The bear is young.
("bear" "is" "young" "+")
int4
The lion sees the lion.
True
8
proof
[(((((triple13 ((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8)) -> rule6)) -> rule8))]
("lion" "sees" "lion" "+")
((((triple13 ((((triple2 ((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
The bear eats the cow.
("bear" "eats" "cow" "+")
int4
The bear is young.
("bear" "is" "young" "+")
int5
The lion does not see the lion.
False
8
inv-proof
[(((((triple13 ((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8)) -> rule6)) -> rule8))]
("lion" "sees" "lion" "-")
((((triple13 ((((triple2 ((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
The bear eats the cow.
("bear" "eats" "cow" "+")
int4
The bear is young.
("bear" "is" "young" "+")
int5
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion is young.
Unknown
rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "young" "+")
The cow does not see the lion.
Unknown
inv-rconc
[@2: The cow sees the lion.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("cow" "sees" "lion" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "sees" "dog" "+")
The bear does not see the dog.
Unknown
inv-rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "sees" "dog" "-")
The lion sees the dog.
Unknown
rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "dog" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The cow does not eat the bear.
Unknown
inv-random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "-")
The cow eats the lion.
Unknown
random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "+")
The dog does not eat the lion.
Unknown
inv-random
[@0: The dog eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "lion" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear eats the dog.[(triple1)] The bear is kind.[(triple2)] The bear is red.[(triple3)] The bear likes the cow.[(triple4)] The bear likes the lion.[(triple5)] The bear sees the cow.[(triple6)] The cow eats the dog.[(triple7)] The cow sees the bear.[(triple8)] The dog eats the bear.[(triple9)] The dog eats the cow.[(triple10)] The dog is nice.[(triple11)] The dog sees the bear.[(triple12)] The lion likes the bear.[(triple13)] The lion likes the cow.[(triple14)] The lion likes the dog.[(triple15)] The lion sees the bear.[(triple16)] @1: The bear is young.[(((triple2) -> rule4))] The bear likes the dog.[(((triple1) -> rule3))] The cow likes the dog.[(((triple7) -> rule3) OR ((triple10 ((triple15) -> rule2)) -> rule1) OR ((triple10 ((((triple1) -> rule3)) -> rule2)) -> rule1))] The dog is cold.[(((triple15) -> rule2) OR ((((triple1) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))] The dog sees the lion.[(((triple10) -> rule8))] @2: The bear eats the cow.[(((triple2 ((triple2) -> rule4)) -> rule5))] @3: The bear sees the lion.[(((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8))] @4: The lion eats the cow.[(((triple13 ((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8)) -> rule6))] @5: The lion sees the lion.[(((((triple13 ((((triple2 ((triple2) -> rule4)) -> rule5)) -> rule8)) -> rule6)) -> rule8))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear likes the cow.
("bear" "likes" "cow" "+")
triple4
The bear likes the lion.
("bear" "likes" "lion" "+")
triple5
The bear sees the cow.
("bear" "sees" "cow" "+")
triple6
The cow eats the dog.
("cow" "eats" "dog" "+")
triple7
The cow sees the bear.
("cow" "sees" "bear" "+")
triple8
The dog eats the bear.
("dog" "eats" "bear" "+")
triple9
The dog eats the cow.
("dog" "eats" "cow" "+")
triple10
The dog is nice.
("dog" "is" "nice" "+")
triple11
The dog sees the bear.
("dog" "sees" "bear" "+")
triple12
The lion likes the bear.
("lion" "likes" "bear" "+")
triple13
The lion likes the cow.
("lion" "likes" "cow" "+")
triple14
The lion likes the dog.
("lion" "likes" "dog" "+")
triple15
The lion sees the bear.
("lion" "sees" "bear" "+")
triple16
The bear is young.
("bear" "is" "young" "+")
((triple2) -> (rule4 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
((triple1) -> (rule3 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple7) -> (rule3 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
((triple10 ((triple15) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((triple10 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The dog is cold.
("dog" "is" "cold" "+")
((triple15) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
((triple10) -> (rule8 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple13 ((((triple2 ((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The bear is young.
("bear" "is" "young" "+")
int4
The lion sees the lion.
("lion" "sees" "lion" "+")
((((triple13 ((((triple2 ((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
The bear eats the cow.
("bear" "eats" "cow" "+")
int4
The bear is young.
("bear" "is" "young" "+")
int5