The cat visits the lion. The lion is cold. The tiger is young. If the tiger is cold and the tiger needs the lion then the lion likes the cat.
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is cold and the tiger needs the lion then the lion likes the cat.
((("tiger" "is" "cold" "+") ("tiger" "needs" "lion" "+")) -> ("lion" "likes" "cat" "+"))
The tiger is young.
True
1
proof
[(triple3)]
("tiger" "is" "young" "+")
triple3
The tiger is not young.
False
1
inv-proof
[(triple3)]
("tiger" "is" "young" "-")
triple3
The lion does not like the cat.
Unknown
inv-rconc
[@1: The lion likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "cat" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The cat visits the lion.[(triple1)] The lion is cold.[(triple2)] The tiger is young.[(triple3)]
The cat visits the lion.
("cat" "visits" "lion" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3