The cat does not eat the lion. The lion eats the cat. The rabbit eats the lion. If something visits the lion and the lion does not see the rabbit then it is not green. If something visits the cat then the cat is rough. If the rabbit eats the lion then the lion eats the rabbit. If the lion is rough then the lion visits the cat. If the rabbit eats the cat and the rabbit is not round then the cat sees the lion. If the cat eats the lion and the lion visits the cat then the lion is green. If something eats the rabbit then it visits the cat. If something is rough and it does not eat the rabbit then it is young.
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The lion eats the cat.
("lion" "eats" "cat" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
If something visits the lion and the lion does not see the rabbit then it is not green.
((("something" "visits" "lion" "+") ("lion" "sees" "rabbit" "~")) -> ("something" "is" "green" "-"))
If something visits the cat then the cat is rough.
((("something" "visits" "cat" "+")) -> ("cat" "is" "rough" "+"))
If the rabbit eats the lion then the lion eats the rabbit.
((("rabbit" "eats" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If the lion is rough then the lion visits the cat.
((("lion" "is" "rough" "+")) -> ("lion" "visits" "cat" "+"))
If the rabbit eats the cat and the rabbit is not round then the cat sees the lion.
((("rabbit" "eats" "cat" "+") ("rabbit" "is" "round" "~")) -> ("cat" "sees" "lion" "+"))
If the cat eats the lion and the lion visits the cat then the lion is green.
((("cat" "eats" "lion" "+") ("lion" "visits" "cat" "+")) -> ("lion" "is" "green" "+"))
If something eats the rabbit then it visits the cat.
((("something" "eats" "rabbit" "+")) -> ("something" "visits" "cat" "+"))
If something is rough and it does not eat the rabbit then it is young.
((("something" "is" "rough" "+") ("something" "eats" "rabbit" "~")) -> ("something" "is" "young" "+"))
The cat does not eat the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The rabbit does not eat the lion.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "lion" "-")
triple3
The lion eats the rabbit.
True
2
proof
[(((triple3) -> rule3))]
("lion" "eats" "rabbit" "+")
((triple3) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion does not eat the rabbit.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "eats" "rabbit" "-")
((triple3) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion visits the cat.
True
3
proof
[(((((triple3) -> rule3)) -> rule7))]
("lion" "visits" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The lion does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule7))]
("lion" "visits" "cat" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The cat is rough.
True
4
proof
[(((((((triple3) -> rule3)) -> rule7)) -> rule2))]
("cat" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
The cat is not rough.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule7)) -> rule2))]
("cat" "is" "rough" "-")
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "green" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "young" "+")
The rabbit does not visit the cat.
Unknown
inv-rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "visits" "cat" "-")
The cat sees the lion.
Unknown
rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "lion" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The lion does not see the cat.
Unknown
inv-random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cat does not eat the lion.[(triple1)] The lion eats the cat.[(triple2)] The rabbit eats the lion.[(triple3)] @1: The lion eats the rabbit.[(((triple3) -> rule3))] @2: The lion visits the cat.[(((((triple3) -> rule3)) -> rule7))] @3: The cat is rough.[(((((((triple3) -> rule3)) -> rule7)) -> rule2))]
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple1
The lion eats the cat.
("lion" "eats" "cat" "+")
triple2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple3) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3