The bald eagle is round. The rabbit eats the squirrel. The squirrel eats the rabbit. If someone is round then they see the rabbit. If someone is nice and they like the squirrel then they see the squirrel. If someone likes the squirrel then they eat the bald eagle. If someone eats the rabbit then the rabbit likes the bald eagle. If someone likes the bald eagle and they like the rabbit then the rabbit eats the bald eagle. If someone likes the bald eagle then they eat the rabbit. If someone eats the squirrel and they eat the rabbit then the squirrel is red. If someone is nice then they eat the bald eagle.
The bald eagle is round.
("bald eagle" "is" "round" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
If someone is round then they see the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is nice and they like the squirrel then they see the squirrel.
((("someone" "is" "nice" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone likes the squirrel then they eat the bald eagle.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "bald eagle" "+"))
If someone eats the rabbit then the rabbit likes the bald eagle.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "likes" "bald eagle" "+"))
If someone likes the bald eagle and they like the rabbit then the rabbit eats the bald eagle.
((("someone" "likes" "bald eagle" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "eats" "bald eagle" "+"))
If someone likes the bald eagle then they eat the rabbit.
((("someone" "likes" "bald eagle" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone eats the squirrel and they eat the rabbit then the squirrel is red.
((("someone" "eats" "squirrel" "+") ("someone" "eats" "rabbit" "+")) -> ("squirrel" "is" "red" "+"))
If someone is nice then they eat the bald eagle.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "bald eagle" "+"))
The squirrel eats the rabbit.
True
1
proof
[(triple3)]
("squirrel" "eats" "rabbit" "+")
triple3
The squirrel does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "rabbit" "-")
triple3
The rabbit likes the bald eagle.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "likes" "bald eagle" "+")
((triple3) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The rabbit does not like the bald eagle.
False
2
inv-proof
[(((triple3) -> rule4))]
("rabbit" "likes" "bald eagle" "-")
((triple3) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("rabbit" "eats" "rabbit" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The squirrel is red.
True
5
proof
[(((triple2 ((((triple3) -> rule4)) -> rule6)) -> rule7))]
("squirrel" "is" "red" "+")
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The squirrel is not red.
False
5
inv-proof
[(((triple2 ((((triple3) -> rule4)) -> rule6)) -> rule7))]
("squirrel" "is" "red" "-")
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The bald eagle eats the bald eagle.
Unknown
rconc
[@1: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The rabbit eats the bald eagle.
Unknown
rconc
[@1: The rabbit eats the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "bald eagle" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The bald eagle does not eat the squirrel.
Unknown
inv-random
[@0: The bald eagle eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "squirrel" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
@0: The bald eagle is round.[(triple1)] The rabbit eats the squirrel.[(triple2)] The squirrel eats the rabbit.[(triple3)] @1: The bald eagle sees the rabbit.[(((triple1) -> rule1))] The rabbit likes the bald eagle.[(((triple3) -> rule4))] @2: The rabbit eats the rabbit.[(((((triple3) -> rule4)) -> rule6))] @3: The squirrel is red.[(((triple2 ((((triple3) -> rule4)) -> rule6)) -> rule7))]
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple3
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
((triple1) -> (rule1 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
((triple3) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3