The cat chases the lion. The cat eats the lion. The cat is cold. The cat is red. The cat likes the lion. The lion eats the cat. The lion is kind. The lion is red. The lion is young. The lion likes the cat. All kind things are nice. If something is kind then it eats the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it eats the cat.
((("something" "is" "kind" "+")) -> ("something" "eats" "cat" "+"))
The lion is young.
True
1
proof
[(triple9)]
("lion" "is" "young" "+")
triple9
The lion does not eat the cat.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule2))]
("lion" "eats" "cat" "-")
triple6
((triple7) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is nice.
True
2
proof
[(((triple7) -> rule1))]
("lion" "is" "nice" "+")
((triple7) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not nice.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "is" "nice" "-")
((triple7) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "cat" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat chases the lion.[(triple1)] The cat eats the lion.[(triple2)] The cat is cold.[(triple3)] The cat is red.[(triple4)] The cat likes the lion.[(triple5)] The lion eats the cat.[(triple6 OR ((triple7) -> rule2))] The lion is kind.[(triple7)] The lion is red.[(triple8)] The lion is young.[(triple9)] The lion likes the cat.[(triple10)] @1: The lion is nice.[(((triple7) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat likes the lion.
("cat" "likes" "lion" "+")
triple5
The lion eats the cat.
("lion" "eats" "cat" "+")
triple6
((triple7) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple7
The lion is red.
("lion" "is" "red" "+")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion likes the cat.
("lion" "likes" "cat" "+")
triple10
The lion is nice.
("lion" "is" "nice" "+")
((triple7) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1