The cat chases the lion. The lion chases the cat. If something is green and it chases the lion then the lion eats the cat. If something chases the cat then it eats the lion. If the cat eats the lion and the lion chases the cat then the lion eats the cat. If something chases the cat then it visits the cat. If something eats the lion then it visits the lion. If something eats the lion and the lion is kind then it chases the cat. If something is kind then it chases the cat. If something visits the cat then the cat eats the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
If something is green and it chases the lion then the lion eats the cat.
((("something" "is" "green" "+") ("something" "chases" "lion" "+")) -> ("lion" "eats" "cat" "+"))
If something chases the cat then it eats the lion.
((("something" "chases" "cat" "+")) -> ("something" "eats" "lion" "+"))
If the cat eats the lion and the lion chases the cat then the lion eats the cat.
((("cat" "eats" "lion" "+") ("lion" "chases" "cat" "+")) -> ("lion" "eats" "cat" "+"))
If something chases the cat then it visits the cat.
((("something" "chases" "cat" "+")) -> ("something" "visits" "cat" "+"))
If something eats the lion then it visits the lion.
((("something" "eats" "lion" "+")) -> ("something" "visits" "lion" "+"))
If something eats the lion and the lion is kind then it chases the cat.
((("something" "eats" "lion" "+") ("lion" "is" "kind" "+")) -> ("something" "chases" "cat" "+"))
If something is kind then it chases the cat.
((("something" "is" "kind" "+")) -> ("something" "chases" "cat" "+"))
If something visits the cat then the cat eats the lion.
((("something" "visits" "cat" "+")) -> ("cat" "eats" "lion" "+"))
The lion chases the cat.
True
1
proof
[(triple2)]
("lion" "chases" "cat" "+")
triple2
The lion does not chase the cat.
False
1
inv-proof
[(triple2)]
("lion" "chases" "cat" "-")
triple2
The lion visits the cat.
True
2
proof
[(((triple2) -> rule4))]
("lion" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "visits" "cat" "-")
((triple2) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion visits the lion.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("lion" "visits" "lion" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("lion" "visits" "lion" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The cat visits the lion.
True
4
proof
[(((((((triple2) -> rule4)) -> rule8)) -> rule5))]
("cat" "visits" "lion" "+")
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The lion does not eat the cat.
False
5
inv-proof
[(((((((triple2) -> rule4)) -> rule8) triple2) -> rule3))]
("lion" "eats" "cat" "-")
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@2: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("cat" "visits" "cat" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "cat" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
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 chases the cat.[(triple2)] @1: The lion eats the lion.[(((triple2) -> rule2))] The lion visits the cat.[(((triple2) -> rule4))] @2: The cat eats the lion.[(((((triple2) -> rule4)) -> rule8))] The lion visits the lion.[(((((triple2) -> rule2)) -> rule5))] @3: The cat visits the lion.[(((((((triple2) -> rule4)) -> rule8)) -> rule5))] The lion eats the cat.[(((((((triple2) -> rule4)) -> rule8) triple2) -> rule3))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The lion chases the cat.
("lion" "chases" "cat" "+")
triple2
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple2) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The lion eats the cat.
("lion" "eats" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3