The cat chases the lion. The lion is round. If someone chases the lion then they need the lion. If someone needs the lion and they are round then the lion chases the cat. If someone needs the lion then the lion eats the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
If someone chases the lion then they need the lion.
((("someone" "chases" "lion" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the lion and they are round then the lion chases the cat.
((("someone" "needs" "lion" "+") ("someone" "is" "round" "+")) -> ("lion" "chases" "cat" "+"))
If someone needs the lion then the lion eats the cat.
((("someone" "needs" "lion" "+")) -> ("lion" "eats" "cat" "+"))
The lion is round.
True
1
proof
[(triple2)]
("lion" "is" "round" "+")
triple2
The lion is not round.
False
1
inv-proof
[(triple2)]
("lion" "is" "round" "-")
triple2
The cat needs the lion.
True
2
proof
[(((triple1) -> rule1))]
("cat" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat does not need the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "needs" "lion" "-")
((triple1) -> (rule1 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("lion" "eats" "cat" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion does not eat the cat.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("lion" "eats" "cat" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion chases the cat.
Unknown
rconc
[@2: The lion chases the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("lion" "chases" "cat" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
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 big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat chases the lion.[(triple1)] The lion is round.[(triple2)] @1: The cat needs the lion.[(((triple1) -> rule1))] @2: The lion eats the cat.[(((((triple1) -> rule1)) -> rule3))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2