The bear does not eat the cow. The bear needs the dog. The cow does not eat the dog. The cow visits the dog. The dog is big. The dog is rough. The dog needs the cow. If something is big and kind then it visits the dog. If something eats the cow then it eats the bear. If something is green then it eats the bear. If something is big then it eats the cow. If the bear visits the cow and the bear is not green then the cow eats the dog. If something is rough and it does not visit the cow then the cow is green. If something eats the bear then the bear eats the dog. If something visits the dog and it does not eat the cow then the dog is cold.
The bear does not eat the cow.
("bear" "eats" "cow" "-")
The bear needs the dog.
("bear" "needs" "dog" "+")
The cow does not eat the dog.
("cow" "eats" "dog" "-")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
If something is big and kind then it visits the dog.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "visits" "dog" "+"))
If something eats the cow then it eats the bear.
((("something" "eats" "cow" "+")) -> ("something" "eats" "bear" "+"))
If something is green then it eats the bear.
((("something" "is" "green" "+")) -> ("something" "eats" "bear" "+"))
If something is big then it eats the cow.
((("something" "is" "big" "+")) -> ("something" "eats" "cow" "+"))
If the bear visits the cow and the bear is not green then the cow eats the dog.
((("bear" "visits" "cow" "+") ("bear" "is" "green" "~")) -> ("cow" "eats" "dog" "+"))
If something is rough and it does not visit the cow then the cow is green.
((("something" "is" "rough" "+") ("something" "visits" "cow" "~")) -> ("cow" "is" "green" "+"))
If something eats the bear then the bear eats the dog.
((("something" "eats" "bear" "+")) -> ("bear" "eats" "dog" "+"))
If something visits the dog and it does not eat the cow then the dog is cold.
((("something" "visits" "dog" "+") ("something" "eats" "cow" "~")) -> ("dog" "is" "cold" "+"))
The bear does not eat the cow.
True
1
proof
[(triple1)]
("bear" "eats" "cow" "-")
triple1
The cow eats the dog.
False
1
inv-proof
[(triple3)]
("cow" "eats" "dog" "+")
triple3
The dog eats the cow.
True
2
proof
[(((triple5) -> rule4))]
("dog" "eats" "cow" "+")
((triple5) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog does not eat the cow.
False
2
inv-proof
[(((triple5) -> rule4))]
("dog" "eats" "cow" "-")
((triple5) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the bear.
True
3
proof
[(((((triple5) -> rule4)) -> rule2))]
("dog" "eats" "bear" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog does not eat the bear.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule2))]
("dog" "eats" "bear" "-")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The bear eats the dog.
True
4
proof
[(((((((triple5) -> rule4)) -> rule2)) -> rule7))]
("bear" "eats" "dog" "+")
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
The bear does not eat the dog.
False
4
inv-proof
[(((((((triple5) -> rule4)) -> rule2)) -> rule7))]
("bear" "eats" "dog" "-")
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "-")
The bear visits the dog.
Unknown
rconc
[@1: The bear visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "dog" "+")
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 bear eats the bear.
Unknown
rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "bear" "+")
The bear does not need the cow.
Unknown
inv-random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not need the bear.
Unknown
inv-random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear does not eat the cow.[(triple1)] The bear needs the dog.[(triple2)] The cow does not eat the dog.[(triple3)] The cow visits the dog.[(triple4)] The dog is big.[(triple5)] The dog is rough.[(triple6)] The dog needs the cow.[(triple7)] @1: The dog eats the cow.[(((triple5) -> rule4))] @2: The dog eats the bear.[(((((triple5) -> rule4)) -> rule2))] @3: The bear eats the dog.[(((((((triple5) -> rule4)) -> rule2)) -> rule7))]
The bear does not eat the cow.
("bear" "eats" "cow" "-")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The cow does not eat the dog.
("cow" "eats" "dog" "-")
triple3
The cow visits the dog.
("cow" "visits" "dog" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog needs the cow.
("dog" "needs" "cow" "+")
triple7
The dog eats the cow.
("dog" "eats" "cow" "+")
((triple5) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The bear eats the dog.
("bear" "eats" "dog" "+")
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3