The cat needs the tiger. The cow needs the cat. The lion is blue. The tiger likes the cow. If something likes the cow then it is blue. If the cow chases the cat then the cow likes the cat. If something needs the cat then it likes the tiger. If something is kind and it needs the lion then the lion is kind. If something is blue and it chases the lion then it likes the cow. If the cow chases the tiger then the tiger is green.
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If something likes the cow then it is blue.
((("something" "likes" "cow" "+")) -> ("something" "is" "blue" "+"))
If the cow chases the cat then the cow likes the cat.
((("cow" "chases" "cat" "+")) -> ("cow" "likes" "cat" "+"))
If something needs the cat then it likes the tiger.
((("something" "needs" "cat" "+")) -> ("something" "likes" "tiger" "+"))
If something is kind and it needs the lion then the lion is kind.
((("something" "is" "kind" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something is blue and it chases the lion then it likes the cow.
((("something" "is" "blue" "+") ("something" "chases" "lion" "+")) -> ("something" "likes" "cow" "+"))
If the cow chases the tiger then the tiger is green.
((("cow" "chases" "tiger" "+")) -> ("tiger" "is" "green" "+"))
The cat needs the tiger.
True
1
proof
[(triple1)]
("cat" "needs" "tiger" "+")
triple1
The cat does not need the tiger.
False
1
inv-proof
[(triple1)]
("cat" "needs" "tiger" "-")
triple1
The cat does not like the tiger.
Unknown
inv-rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "tiger" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat needs the tiger.[(triple1)] The cow needs the cat.[(triple2)] The lion is blue.[(triple3)] The tiger likes the cow.[(triple4)] @1: The cow likes the tiger.[(((triple2) -> rule3))] The tiger is blue.[(((triple4) -> rule1))]
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple4
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple2) -> (rule3 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple4) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1