The lion does not need the rabbit. The rabbit chases the lion. The squirrel needs the lion. If someone chases the squirrel and the squirrel is green then the squirrel chases the lion. If someone needs the rabbit and they need the lion then the lion needs the squirrel. If someone is young then they need the squirrel. If someone chases the lion then they like the rabbit. If someone is rough and they do not chase the squirrel then the squirrel needs the lion. If the lion does not chase the squirrel and the squirrel does not chase the lion then the squirrel likes the rabbit. If someone likes the lion then they are not round. If someone likes the rabbit and they chase the lion then the rabbit likes the lion.
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If someone chases the squirrel and the squirrel is green then the squirrel chases the lion.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("squirrel" "chases" "lion" "+"))
If someone needs the rabbit and they need the lion then the lion needs the squirrel.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
If someone is young then they need the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone chases the lion then they like the rabbit.
((("someone" "chases" "lion" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone is rough and they do not chase the squirrel then the squirrel needs the lion.
((("someone" "is" "rough" "+") ("someone" "chases" "squirrel" "~")) -> ("squirrel" "needs" "lion" "+"))
If the lion does not chase the squirrel and the squirrel does not chase the lion then the squirrel likes the rabbit.
((("lion" "chases" "squirrel" "~") ("squirrel" "chases" "lion" "~")) -> ("squirrel" "likes" "rabbit" "+"))
If someone likes the lion then they are not round.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "round" "-"))
If someone likes the rabbit and they chase the lion then the rabbit likes the lion.
((("someone" "likes" "rabbit" "+") ("someone" "chases" "lion" "+")) -> ("rabbit" "likes" "lion" "+"))
The squirrel needs the lion.
True
1
proof
[(triple3)]
("squirrel" "needs" "lion" "+")
triple3
The rabbit does not chase the lion.
False
1
inv-proof
[(triple2)]
("rabbit" "chases" "lion" "-")
triple2
The rabbit likes the rabbit.
True
2
proof
[(((triple2) -> rule4))]
("rabbit" "likes" "rabbit" "+")
((triple2) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple2) -> rule4))]
("rabbit" "likes" "rabbit" "-")
((triple2) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the lion.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule8))]
("rabbit" "likes" "lion" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit does not like the lion.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule8))]
("rabbit" "likes" "lion" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is not round.
True
5
proof
[(((((((triple2) -> rule4) triple2) -> rule8)) -> rule7))]
("rabbit" "is" "round" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The rabbit is round.
False
5
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule8)) -> rule7))]
("rabbit" "is" "round" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The lion needs the squirrel.
Unknown
rconc
[@1: The lion needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "squirrel" "+")
The squirrel does not chase the lion.
Unknown
inv-rconc
[@1: The squirrel chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "lion" "-")
The squirrel likes the rabbit.
Unknown
rconc
[@2: The squirrel likes the rabbit.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "likes" "rabbit" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion does not need the rabbit.[(triple1)] The rabbit chases the lion.[(triple2)] The squirrel needs the lion.[(triple3)] @1: The rabbit likes the rabbit.[(((triple2) -> rule4))] @2: The rabbit likes the lion.[(((((triple2) -> rule4) triple2) -> rule8))] @3: The rabbit is not round.[(((((((triple2) -> rule4) triple2) -> rule8)) -> rule7))]
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
triple1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple2) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is not round.
("rabbit" "is" "round" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3