The cat eats the lion. The lion eats the cat. The lion sees the cat. If something eats the cat then it likes the cat. If something is cold then it sees the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something eats the cat then it likes the cat.
((("something" "eats" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something is cold then it sees the cat.
((("something" "is" "cold" "+")) -> ("something" "sees" "cat" "+"))
The lion sees the cat.
True
1
proof
[(triple3)]
("lion" "sees" "cat" "+")
triple3
The cat does not eat the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The lion likes the cat.
True
2
proof
[(((triple2) -> rule1))]
("lion" "likes" "cat" "+")
((triple2) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion does not like the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "likes" "cat" "-")
((triple2) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "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 green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat eats the lion.[(triple1)] The lion eats the cat.[(triple2)] The lion sees the cat.[(triple3)] @1: The lion likes the cat.[(((triple2) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The lion eats the cat.
("lion" "eats" "cat" "+")
triple2
The lion sees the cat.
("lion" "sees" "cat" "+")
triple3
The lion likes the cat.
("lion" "likes" "cat" "+")
((triple2) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1