The bear likes the dog. The cow needs the bear. The dog is blue. The rabbit is blue. If something is nice then it is young. If something needs the cow then it is blue. If something is nice and it needs the bear then the bear sees the rabbit.
The bear likes the dog.
("bear" "likes" "dog" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The dog is blue.
("dog" "is" "blue" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something needs the cow then it is blue.
((("something" "needs" "cow" "+")) -> ("something" "is" "blue" "+"))
If something is nice and it needs the bear then the bear sees the rabbit.
((("something" "is" "nice" "+") ("something" "needs" "bear" "+")) -> ("bear" "sees" "rabbit" "+"))
The rabbit is blue.
True
1
proof
[(triple4)]
("rabbit" "is" "blue" "+")
triple4
The rabbit is not blue.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "blue" "-")
triple4
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "blue" "-")
The rabbit sees the cow.
Unknown
random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "+")
@0: The bear likes the dog.[(triple1)] The cow needs the bear.[(triple2)] The dog is blue.[(triple3)] The rabbit is blue.[(triple4)]
The bear likes the dog.
("bear" "likes" "dog" "+")
triple1
The cow needs the bear.
("cow" "needs" "bear" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4