The cat is kind. The cat needs the lion. The cat sees the lion. The cat visits the lion. The lion is big. The lion is young. The lion needs the cat. If something is green and it visits the lion then it sees the lion.
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If something is green and it visits the lion then it sees the lion.
((("something" "is" "green" "+") ("something" "visits" "lion" "+")) -> ("something" "sees" "lion" "+"))
The cat needs the lion.
True
1
proof
[(triple2)]
("cat" "needs" "lion" "+")
triple2
The cat does not visit the lion.
False
1
inv-proof
[(triple4)]
("cat" "visits" "lion" "-")
triple4
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The cat is kind.[(triple1)] The cat needs the lion.[(triple2)] The cat sees the lion.[(triple3)] The cat visits the lion.[(triple4)] The lion is big.[(triple5)] The lion is young.[(triple6)] The lion needs the cat.[(triple7)]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The cat visits the lion.
("cat" "visits" "lion" "+")
triple4
The lion is big.
("lion" "is" "big" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7