The cow needs the lion. The lion needs the cow. The rabbit visits the cow. If something needs the lion then the lion eats the rabbit. If something is green and it needs the rabbit then the rabbit is big. If something eats the rabbit then it is big.
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If something needs the lion then the lion eats the rabbit.
((("something" "needs" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If something is green and it needs the rabbit then the rabbit is big.
((("something" "is" "green" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If something eats the rabbit then it is big.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "big" "+"))
The cow needs the lion.
True
1
proof
[(triple1)]
("cow" "needs" "lion" "+")
triple1
The lion does not need the cow.
False
1
inv-proof
[(triple2)]
("lion" "needs" "cow" "-")
triple2
The lion eats the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("lion" "eats" "rabbit" "+")
((triple1) -> (rule1 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion does not eat the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "eats" "rabbit" "-")
((triple1) -> (rule1 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("lion" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "big" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "big" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit eats the cow.
Unknown
random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "+")
The lion does not visit the rabbit.
Unknown
inv-random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The cow needs the lion.[(triple1)] The lion needs the cow.[(triple2)] The rabbit visits the cow.[(triple3)] @1: The lion eats the rabbit.[(((triple1) -> rule1))] @2: The lion is big.[(((((triple1) -> rule1)) -> rule3))]
The cow needs the lion.
("cow" "needs" "lion" "+")
triple1
The lion needs the cow.
("lion" "needs" "cow" "+")
triple2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple1) -> (rule1 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2