The cat eats the lion. The cat is nice. The cat is red. The cat is rough. The cat likes the lion. The cat sees the lion. The lion is nice. If something sees the lion then it eats the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
If something sees the lion then it eats the cat.
((("something" "sees" "lion" "+")) -> ("something" "eats" "cat" "+"))
The cat is red.
True
1
proof
[(triple3)]
("cat" "is" "red" "+")
triple3
The lion is not nice.
False
1
inv-proof
[(triple7)]
("lion" "is" "nice" "-")
triple7
The lion does not eat the cat.
Unknown
inv-rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat eats the lion.[(triple1)] The cat is nice.[(triple2)] The cat is red.[(triple3)] The cat is rough.[(triple4)] The cat likes the lion.[(triple5)] The cat sees the lion.[(triple6)] The lion is nice.[(triple7)] @1: The cat eats the cat.[(((triple6) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat likes the lion.
("cat" "likes" "lion" "+")
triple5
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple6) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1