The cat eats the lion. The lion likes the cat. If someone likes the cat then they see the cat. If the lion sees the cat then the lion eats the cat. If someone eats the lion and they like the cat then the cat eats the lion.
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
If someone likes the cat then they see the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If the lion sees the cat then the lion eats the cat.
((("lion" "sees" "cat" "+")) -> ("lion" "eats" "cat" "+"))
If someone eats the lion and they like the cat then the cat eats the lion.
((("someone" "eats" "lion" "+") ("someone" "likes" "cat" "+")) -> ("cat" "eats" "lion" "+"))
The cat eats the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The lion does not like the cat.
False
1
inv-proof
[(triple2)]
("lion" "likes" "cat" "-")
triple2
The lion sees the cat.
True
2
proof
[(((triple2) -> rule1))]
("lion" "sees" "cat" "+")
((triple2) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion does not see the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "sees" "cat" "-")
((triple2) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion eats the cat.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("lion" "eats" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion does not eat the cat.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("lion" "eats" "cat" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat eats the lion.[(triple1)] The lion likes the cat.[(triple2)] @1: The lion sees the cat.[(((triple2) -> rule1))] @2: The lion eats the cat.[(((((triple2) -> rule1)) -> rule2))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The lion likes the cat.
("lion" "likes" "cat" "+")
triple2
The lion sees the cat.
("lion" "sees" "cat" "+")
((triple2) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2