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