The bear chases the cow. The bear chases the dog. The bear does not chase the mouse. The bear is blue. The bear likes the dog. The cow chases the mouse. The cow needs the bear. The cow needs the mouse. The dog does not chase the bear. The dog chases the mouse. The dog is red. The mouse chases the bear. If someone chases the cow then the cow is kind. If someone likes the cow then they need the cow. If someone likes the cow then they need the cow. If the dog is green then the dog is kind. If someone likes the cow and they are green then they are kind. If someone is big then they like the cow. If someone needs the dog and the dog likes the cow then the dog does not like the bear. All kind people are big. If someone needs the cow then the cow chases the dog.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear does not chase the mouse.
("bear" "chases" "mouse" "-")
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog does not chase the bear.
("dog" "chases" "bear" "-")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
If someone chases the cow then the cow is kind.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "kind" "+"))
If someone likes the cow then they need the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the cow then they need the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If the dog is green then the dog is kind.
((("dog" "is" "green" "+")) -> ("dog" "is" "kind" "+"))
If someone likes the cow and they are green then they are kind.
((("someone" "likes" "cow" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is big then they like the cow.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cow" "+"))
If someone needs the dog and the dog likes the cow then the dog does not like the bear.
((("someone" "needs" "dog" "+") ("dog" "likes" "cow" "+")) -> ("dog" "likes" "bear" "-"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone needs the cow then the cow chases the dog.
((("someone" "needs" "cow" "+")) -> ("cow" "chases" "dog" "+"))
The bear chases the dog.
True
1
proof
[(triple2)]
("bear" "chases" "dog" "+")
triple2
The dog chases the bear.
False
1
inv-proof
[(triple9)]
("dog" "chases" "bear" "+")
triple9
The cow is kind.
True
2
proof
[(((triple1) -> rule1))]
("cow" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("cow" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("cow" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow likes the cow.
True
4
proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule6))]
("cow" "likes" "cow" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow does not like the cow.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule6))]
("cow" "likes" "cow" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow needs the cow.
True
5
proof
[(((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule3))]
("cow" "needs" "cow" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cow does not need the cow.
False
5
inv-proof
[(((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule3))]
("cow" "needs" "cow" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cow chases the dog.
True
6
proof
[(((((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule2)) -> rule9) OR ((((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule3)) -> rule9))]
("cow" "chases" "dog" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
The cow does not chase the dog.
False
6
inv-proof
[(((((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule2)) -> rule9) OR ((((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule3)) -> rule9))]
("cow" "chases" "dog" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
The bear does not need the cow.
Unknown
inv-rconc
[@4: The bear needs the cow.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule8 <- rule5 <- FAIL)]]
("bear" "needs" "cow" "-")
The mouse likes the cow.
Unknown
rconc
[@3: The mouse likes the cow.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule5 <- FAIL)]]
("mouse" "likes" "cow" "+")
The mouse is not big.
Unknown
inv-rconc
[@2: The mouse is big.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "kind" "+")
The dog does not need the cow.
Unknown
inv-rconc
[@4: The dog needs the cow.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule8 <- rule4 <- FAIL)]]
("dog" "needs" "cow" "-")
The dog is big.
Unknown
rconc
[@2: The dog is big.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("dog" "is" "big" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The mouse likes the dog.
Unknown
random
[@0: The mouse likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "dog" "+")
The cow does not like the dog.
Unknown
inv-random
[@0: The cow likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "dog" "-")
The cow chases the bear.
Unknown
random
[@0: The cow chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bear" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The bear chases the cow.[(triple1)] The bear chases the dog.[(triple2)] The bear does not chase the mouse.[(triple3)] The bear is blue.[(triple4)] The bear likes the dog.[(triple5)] The cow chases the mouse.[(triple6)] The cow needs the bear.[(triple7)] The cow needs the mouse.[(triple8)] The dog chases the mouse.[(triple10)] The dog does not chase the bear.[(triple9)] The dog is red.[(triple11)] The mouse chases the bear.[(triple12)] @1: The cow is kind.[(((triple1) -> rule1))] @2: The cow is big.[(((((triple1) -> rule1)) -> rule8))] @3: The cow likes the cow.[(((((((triple1) -> rule1)) -> rule8)) -> rule6))] @4: The cow needs the cow.[(((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule3))] @5: The cow chases the dog.[(((((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule2)) -> rule9) OR ((((((((((triple1) -> rule1)) -> rule8)) -> rule6)) -> rule3)) -> rule9))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear chases the dog.
("bear" "chases" "dog" "+")
triple2
The bear does not chase the mouse.
("bear" "chases" "mouse" "-")
triple3
The bear is blue.
("bear" "is" "blue" "+")
triple4
The bear likes the dog.
("bear" "likes" "dog" "+")
triple5
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple8
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple10
The dog does not chase the bear.
("dog" "chases" "bear" "-")
triple9
The dog is red.
("dog" "is" "red" "+")
triple11
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple12
The cow is kind.
("cow" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cow chases the dog.
("cow" "chases" "dog" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5