The bear is red. The cow likes the dog. The dog likes the bear. If someone is red and they do not like the bear then the bear is red. If someone sees the cow then they do not like the dog. If someone likes the cow and the cow needs the dog then the cow likes the dog. If someone needs the cow and the cow sees the dog then they need the dog. If someone needs the dog then the dog is not green. If someone is nice then they like the cow. If the bear is red and the bear is green then the bear needs the dog. If someone likes the bear then the bear is nice.
The bear is red.
("bear" "is" "red" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
If someone is red and they do not like the bear then the bear is red.
((("someone" "is" "red" "+") ("someone" "likes" "bear" "~")) -> ("bear" "is" "red" "+"))
If someone sees the cow then they do not like the dog.
((("someone" "sees" "cow" "+")) -> ("someone" "likes" "dog" "-"))
If someone likes the cow and the cow needs the dog then the cow likes the dog.
((("someone" "likes" "cow" "+") ("cow" "needs" "dog" "+")) -> ("cow" "likes" "dog" "+"))
If someone needs the cow and the cow sees the dog then they need the dog.
((("someone" "needs" "cow" "+") ("cow" "sees" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If someone needs the dog then the dog is not green.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "green" "-"))
If someone is nice then they like the cow.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "cow" "+"))
If the bear is red and the bear is green then the bear needs the dog.
((("bear" "is" "red" "+") ("bear" "is" "green" "+")) -> ("bear" "needs" "dog" "+"))
If someone likes the bear then the bear is nice.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "nice" "+"))
The cow likes the dog.
True
1
proof
[(triple2)]
("cow" "likes" "dog" "+")
triple2
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The bear is nice.
True
2
proof
[(((triple3) -> rule8))]
("bear" "is" "nice" "+")
((triple3) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple3) -> rule8))]
("bear" "is" "nice" "-")
((triple3) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the cow.
True
3
proof
[(((((triple3) -> rule8)) -> rule6))]
("bear" "likes" "cow" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not like the cow.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule6))]
("bear" "likes" "cow" "-")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The dog does not like the cow.
Unknown
inv-rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "cow" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "+")
The cow does not need the dog.
Unknown
inv-rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "dog" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The bear is red.[(triple1)] The cow likes the dog.[(triple2)] The dog likes the bear.[(triple3)] @1: The bear is nice.[(((triple3) -> rule8))] @2: The bear likes the cow.[(((((triple3) -> rule8)) -> rule6))]
The bear is red.
("bear" "is" "red" "+")
triple1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple2
The dog likes the bear.
("dog" "likes" "bear" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple3) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2