The bald eagle needs the lion. The lion visits the squirrel. The rabbit sees the lion. The squirrel needs the rabbit. If someone is round and they need the rabbit then the rabbit is round. If the lion needs the rabbit then the lion sees the bald eagle. If the rabbit is nice and the rabbit needs the lion then the rabbit is young. If someone sees the lion and the lion sees the squirrel then the lion visits the bald eagle. If someone sees the lion then they are big. If someone needs the bald eagle and they visit the squirrel then they visit the lion. If someone is young and rough then they see the squirrel. If the rabbit needs the bald eagle then the rabbit needs the lion.
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If someone is round and they need the rabbit then the rabbit is round.
((("someone" "is" "round" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If the lion needs the rabbit then the lion sees the bald eagle.
((("lion" "needs" "rabbit" "+")) -> ("lion" "sees" "bald eagle" "+"))
If the rabbit is nice and the rabbit needs the lion then the rabbit is young.
((("rabbit" "is" "nice" "+") ("rabbit" "needs" "lion" "+")) -> ("rabbit" "is" "young" "+"))
If someone sees the lion and the lion sees the squirrel then the lion visits the bald eagle.
((("someone" "sees" "lion" "+") ("lion" "sees" "squirrel" "+")) -> ("lion" "visits" "bald eagle" "+"))
If someone sees the lion then they are big.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone needs the bald eagle and they visit the squirrel then they visit the lion.
((("someone" "needs" "bald eagle" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "visits" "lion" "+"))
If someone is young and rough then they see the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "sees" "squirrel" "+"))
If the rabbit needs the bald eagle then the rabbit needs the lion.
((("rabbit" "needs" "bald eagle" "+")) -> ("rabbit" "needs" "lion" "+"))
The lion visits the squirrel.
True
1
proof
[(triple2)]
("lion" "visits" "squirrel" "+")
triple2
The lion does not visit the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "visits" "squirrel" "-")
triple2
The rabbit is big.
True
2
proof
[(((triple3) -> rule5))]
("rabbit" "is" "big" "+")
((triple3) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple3) -> rule5))]
("rabbit" "is" "big" "-")
((triple3) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The lion does not visit the bald eagle.
Unknown
inv-rconc
[@2: The lion visits the bald eagle.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("lion" "visits" "bald eagle" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The bald eagle needs the lion.[(triple1)] The lion visits the squirrel.[(triple2)] The rabbit sees the lion.[(triple3)] The squirrel needs the rabbit.[(triple4)] @1: The rabbit is big.[(((triple3) -> rule5))]
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
((triple3) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1