The cow does not need the lion. The lion chases the cow. The rabbit needs the cow. If someone is young then they need the cow. If the lion needs the rabbit then the rabbit needs the lion. If someone chases the rabbit then the rabbit is nice. If someone is nice and they do not eat the lion then they are not red. If the rabbit chases the lion then the lion is red. If someone chases the cow then the cow is round. If someone is red and not nice then they chase the cow. If someone is round then they chase the lion.
The cow does not need the lion.
("cow" "needs" "lion" "-")
The lion chases the cow.
("lion" "chases" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If someone is young then they need the cow.
((("someone" "is" "young" "+")) -> ("someone" "needs" "cow" "+"))
If the lion needs the rabbit then the rabbit needs the lion.
((("lion" "needs" "rabbit" "+")) -> ("rabbit" "needs" "lion" "+"))
If someone chases the rabbit then the rabbit is nice.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If someone is nice and they do not eat the lion then they are not red.
((("someone" "is" "nice" "+") ("someone" "eats" "lion" "~")) -> ("someone" "is" "red" "-"))
If the rabbit chases the lion then the lion is red.
((("rabbit" "chases" "lion" "+")) -> ("lion" "is" "red" "+"))
If someone chases the cow then the cow is round.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "round" "+"))
If someone is red and not nice then they chase the cow.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "chases" "cow" "+"))
If someone is round then they chase the lion.
((("someone" "is" "round" "+")) -> ("someone" "chases" "lion" "+"))
The rabbit needs the cow.
True
1
proof
[(triple3)]
("rabbit" "needs" "cow" "+")
triple3
The lion does not chase the cow.
False
1
inv-proof
[(triple2)]
("lion" "chases" "cow" "-")
triple2
The cow is round.
True
2
proof
[(((triple2) -> rule6))]
("cow" "is" "round" "+")
((triple2) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple2) -> rule6))]
("cow" "is" "round" "-")
((triple2) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the lion.
True
3
proof
[(((((triple2) -> rule6)) -> rule8))]
("cow" "chases" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow does not chase the lion.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule8))]
("cow" "chases" "lion" "-")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "cow" "-")
The lion is red.
Unknown
rconc
[@2: The lion is red.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("lion" "is" "red" "+")
The rabbit does not need the lion.
Unknown
inv-rconc
[@1: The rabbit needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "lion" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cow does not need the lion.[(triple1)] The lion chases the cow.[(triple2)] The rabbit needs the cow.[(triple3)] @1: The cow is round.[(((triple2) -> rule6))] @2: The cow chases the lion.[(((((triple2) -> rule6)) -> rule8))]
The cow does not need the lion.
("cow" "needs" "lion" "-")
triple1
The lion chases the cow.
("lion" "chases" "cow" "+")
triple2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
((triple2) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the lion.
("cow" "chases" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2