The bald eagle visits the squirrel. The rabbit visits the squirrel. The squirrel does not visit the bald eagle. If the squirrel does not visit the bald eagle then the bald eagle eats the squirrel. If the bald eagle eats the squirrel then the bald eagle visits the rabbit. If someone is big then they do not see the rabbit. If someone sees the bald eagle and they visit the rabbit then the rabbit eats the squirrel. If someone eats the bald eagle and the bald eagle sees the squirrel then they see the squirrel. If the rabbit sees the squirrel then the rabbit visits the squirrel. If someone is round then they do not eat the squirrel. If the bald eagle does not see the squirrel then the squirrel eats the rabbit.
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel does not visit the bald eagle.
("squirrel" "visits" "bald eagle" "-")
If the squirrel does not visit the bald eagle then the bald eagle eats the squirrel.
((("squirrel" "visits" "bald eagle" "~")) -> ("bald eagle" "eats" "squirrel" "+"))
If the bald eagle eats the squirrel then the bald eagle visits the rabbit.
((("bald eagle" "eats" "squirrel" "+")) -> ("bald eagle" "visits" "rabbit" "+"))
If someone is big then they do not see the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone sees the bald eagle and they visit the rabbit then the rabbit eats the squirrel.
((("someone" "sees" "bald eagle" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If someone eats the bald eagle and the bald eagle sees the squirrel then they see the squirrel.
((("someone" "eats" "bald eagle" "+") ("bald eagle" "sees" "squirrel" "+")) -> ("someone" "sees" "squirrel" "+"))
If the rabbit sees the squirrel then the rabbit visits the squirrel.
((("rabbit" "sees" "squirrel" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If someone is round then they do not eat the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "eats" "squirrel" "-"))
If the bald eagle does not see the squirrel then the squirrel eats the rabbit.
((("bald eagle" "sees" "squirrel" "~")) -> ("squirrel" "eats" "rabbit" "+"))
The rabbit visits the squirrel.
True
1
proof
[(triple2)]
("rabbit" "visits" "squirrel" "+")
triple2
The rabbit does not visit the squirrel.
False
1
inv-proof
[(triple2)]
("rabbit" "visits" "squirrel" "-")
triple2
The bald eagle eats the squirrel.
True
2
proof
[(((triple3) -> rule1))]
("bald eagle" "eats" "squirrel" "+")
((triple3) -> (rule1 % int1))
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int1
The bald eagle does not eat the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("bald eagle" "eats" "squirrel" "-")
((triple3) -> (rule1 % int1))
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int1
The bald eagle visits the rabbit.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("bald eagle" "visits" "rabbit" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int1
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int2
The bald eagle does not visit the rabbit.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("bald eagle" "visits" "rabbit" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int1
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int2
The rabbit does not eat the squirrel.
Unknown
inv-rconc
[@1: The rabbit eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "eats" "squirrel" "-")
The bald eagle sees the squirrel.
Unknown
rconc
[@1: The bald eagle sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "sees" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The bald eagle sees the rabbit.
Unknown
random
[@0: The bald eagle sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "rabbit" "+")
The bald eagle is not young.
Unknown
inv-random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
@0: The bald eagle visits the squirrel.[(triple1)] The rabbit visits the squirrel.[(triple2)] The squirrel does not visit the bald eagle.[(triple3)] @1: The bald eagle eats the squirrel.[(((triple3) -> rule1))] @2: The bald eagle visits the rabbit.[(((((triple3) -> rule1)) -> rule2))]
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple2
The squirrel does not visit the bald eagle.
("squirrel" "visits" "bald eagle" "-")
triple3
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
((triple3) -> (rule1 % int1))
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int1
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int1
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int2