The bear is rough. The cow eats the dog. The dog needs the cow. If someone is rough then they need the bear. If someone needs the dog then the dog is young. If someone is cold and they do not eat the dog then the dog sees the bear. If the cow does not eat the bear and the bear does not need the dog then the bear sees the dog. If someone needs the cow then they are nice. If someone needs the cow and the cow is nice then the cow needs the dog.
The bear is rough.
("bear" "is" "rough" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
If someone is rough then they need the bear.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the dog then the dog is young.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "young" "+"))
If someone is cold and they do not eat the dog then the dog sees the bear.
((("someone" "is" "cold" "+") ("someone" "eats" "dog" "~")) -> ("dog" "sees" "bear" "+"))
If the cow does not eat the bear and the bear does not need the dog then the bear sees the dog.
((("cow" "eats" "bear" "~") ("bear" "needs" "dog" "~")) -> ("bear" "sees" "dog" "+"))
If someone needs the cow then they are nice.
((("someone" "needs" "cow" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the cow and the cow is nice then the cow needs the dog.
((("someone" "needs" "cow" "+") ("cow" "is" "nice" "+")) -> ("cow" "needs" "dog" "+"))
The cow eats the dog.
True
1
proof
[(triple2)]
("cow" "eats" "dog" "+")
triple2
The cow does not eat the dog.
False
1
inv-proof
[(triple2)]
("cow" "eats" "dog" "-")
triple2
The bear needs the bear.
True
2
proof
[(((triple1) -> rule1))]
("bear" "needs" "bear" "+")
((triple1) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("dog" "is" "nice" "-")
((triple3) -> (rule5 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "nice" "-")
The cow needs the dog.
Unknown
rconc
[@2: The cow needs the dog.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("cow" "needs" "dog" "+")
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 is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The bear is rough.[(triple1)] The cow eats the dog.[(triple2)] The dog needs the cow.[(triple3)] @1: The bear needs the bear.[(((triple1) -> rule1))] The dog is nice.[(((triple3) -> rule5))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The cow eats the dog.
("cow" "eats" "dog" "+")
triple2
The dog needs the cow.
("dog" "needs" "cow" "+")
triple3
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple3) -> (rule5 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1