The cat is cold. The lion needs the rabbit. The rabbit chases the lion. If someone chases the lion then the lion chases the rabbit. If someone visits the rabbit and the rabbit needs the lion then they visit the cat. If the lion is round then the lion chases the rabbit. If the lion is kind and the lion visits the cat then the lion visits the rabbit. If someone needs the cat then they chase the rabbit. If someone chases the rabbit then the rabbit visits the cat.
The cat is cold.
("cat" "is" "cold" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
If someone chases the lion then the lion chases the rabbit.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "rabbit" "+"))
If someone visits the rabbit and the rabbit needs the lion then they visit the cat.
((("someone" "visits" "rabbit" "+") ("rabbit" "needs" "lion" "+")) -> ("someone" "visits" "cat" "+"))
If the lion is round then the lion chases the rabbit.
((("lion" "is" "round" "+")) -> ("lion" "chases" "rabbit" "+"))
If the lion is kind and the lion visits the cat then the lion visits the rabbit.
((("lion" "is" "kind" "+") ("lion" "visits" "cat" "+")) -> ("lion" "visits" "rabbit" "+"))
If someone needs the cat then they chase the rabbit.
((("someone" "needs" "cat" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the rabbit then the rabbit visits the cat.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "visits" "cat" "+"))
The lion needs the rabbit.
True
1
proof
[(triple2)]
("lion" "needs" "rabbit" "+")
triple2
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The lion chases the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("lion" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion does not chase the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "chases" "rabbit" "-")
((triple3) -> (rule1 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The rabbit visits the cat.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("rabbit" "visits" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The rabbit does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("rabbit" "visits" "cat" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "-")
The lion visits the rabbit.
Unknown
rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The cat does not chase the rabbit.
Unknown
inv-rconc
[@1: The cat chases the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "rabbit" "-")
The cat chases the lion.
Unknown
random
[@0: The cat chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "lion" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat is cold.[(triple1)] The lion needs the rabbit.[(triple2)] The rabbit chases the lion.[(triple3)] @1: The lion chases the rabbit.[(((triple3) -> rule1))] @2: The rabbit visits the cat.[(((((triple3) -> rule1)) -> rule6))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2