The cat does not eat the lion. The lion chases the cat. If someone is rough then they eat the lion. If someone is cold and they eat the cat then they do not eat the lion. If someone chases the cat then the cat chases the lion. If someone chases the lion then they chase the cat. If someone chases the cat and they do not eat the lion then they do not need the lion. If the lion eats the cat and the cat does not eat the lion then the lion is round.
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The lion chases the cat.
("lion" "chases" "cat" "+")
If someone is rough then they eat the lion.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "lion" "+"))
If someone is cold and they eat the cat then they do not eat the lion.
((("someone" "is" "cold" "+") ("someone" "eats" "cat" "+")) -> ("someone" "eats" "lion" "-"))
If someone chases the cat then the cat chases the lion.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "lion" "+"))
If someone chases the lion then they chase the cat.
((("someone" "chases" "lion" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat and they do not eat the lion then they do not need the lion.
((("someone" "chases" "cat" "+") ("someone" "eats" "lion" "~")) -> ("someone" "needs" "lion" "-"))
If the lion eats the cat and the cat does not eat the lion then the lion is round.
((("lion" "eats" "cat" "+") ("cat" "eats" "lion" "~")) -> ("lion" "is" "round" "+"))
The cat does not eat the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The cat eats the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The cat chases the lion.
True
2
proof
[(((triple2) -> rule3))]
("cat" "chases" "lion" "+")
((triple2) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat does not chase the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "chases" "lion" "-")
((triple2) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat chases the cat.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("cat" "chases" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The cat does not chase the cat.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("cat" "chases" "cat" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The cat does not need the lion.
True
5
proof
[(((((((triple2) -> rule3)) -> rule4) triple1) -> rule5))]
("cat" "needs" "lion" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The cat does not need the lion.
("cat" "needs" "lion" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The cat needs the lion.
False
5
inv-proof
[(((((((triple2) -> rule3)) -> rule4) triple1) -> rule5))]
("cat" "needs" "lion" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The cat does not need the lion.
("cat" "needs" "lion" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "round" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The lion does not eat the cat.
Unknown
inv-random
[@0: The lion eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The cat does not eat the lion.[(triple1)] The lion chases the cat.[(triple2)] @1: The cat chases the lion.[(((triple2) -> rule3))] @2: The cat chases the cat.[(((((triple2) -> rule3)) -> rule4))] @3: The cat does not need the lion.[(((((((triple2) -> rule3)) -> rule4) triple1) -> rule5))]
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple1
The lion chases the cat.
("lion" "chases" "cat" "+")
triple2
The cat chases the lion.
("cat" "chases" "lion" "+")
((triple2) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The cat does not need the lion.
("cat" "needs" "lion" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The cat does not need the lion.
("cat" "needs" "lion" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3