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