The bald eagle needs the squirrel. The mouse is round. The rabbit eats the squirrel. The squirrel does not eat the mouse. If something is big then it eats the rabbit. If something needs the rabbit and the rabbit does not eat the bald eagle then the bald eagle needs the mouse. If something is round and it chases the mouse then the mouse eats the bald eagle. If the squirrel does not chase the rabbit then the squirrel does not eat the bald eagle. If something eats the rabbit then it does not chase the mouse. If something eats the squirrel then it is big. If something chases the bald eagle and the bald eagle eats the squirrel then it is nice. If something needs the squirrel and it is young then the squirrel needs the rabbit.
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel does not eat the mouse.
("squirrel" "eats" "mouse" "-")
If something is big then it eats the rabbit.
((("something" "is" "big" "+")) -> ("something" "eats" "rabbit" "+"))
If something needs the rabbit and the rabbit does not eat the bald eagle then the bald eagle needs the mouse.
((("something" "needs" "rabbit" "+") ("rabbit" "eats" "bald eagle" "~")) -> ("bald eagle" "needs" "mouse" "+"))
If something is round and it chases the mouse then the mouse eats the bald eagle.
((("something" "is" "round" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "eats" "bald eagle" "+"))
If the squirrel does not chase the rabbit then the squirrel does not eat the bald eagle.
((("squirrel" "chases" "rabbit" "~")) -> ("squirrel" "eats" "bald eagle" "-"))
If something eats the rabbit then it does not chase the mouse.
((("something" "eats" "rabbit" "+")) -> ("something" "chases" "mouse" "-"))
If something eats the squirrel then it is big.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "big" "+"))
If something chases the bald eagle and the bald eagle eats the squirrel then it is nice.
((("something" "chases" "bald eagle" "+") ("bald eagle" "eats" "squirrel" "+")) -> ("something" "is" "nice" "+"))
If something needs the squirrel and it is young then the squirrel needs the rabbit.
((("something" "needs" "squirrel" "+") ("something" "is" "young" "+")) -> ("squirrel" "needs" "rabbit" "+"))
The mouse is round.
True
1
proof
[(triple2)]
("mouse" "is" "round" "+")
triple2
The rabbit does not eat the squirrel.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "squirrel" "-")
triple3
The rabbit is big.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "is" "big" "+")
((triple3) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "is" "big" "-")
((triple3) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("rabbit" "eats" "rabbit" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("rabbit" "eats" "rabbit" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not chase the mouse.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule5))]
("rabbit" "chases" "mouse" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit chases the mouse.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule5))]
("rabbit" "chases" "mouse" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The squirrel does not need the rabbit.
Unknown
inv-rconc
[@1: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "rabbit" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "nice" "+")
The bald eagle does not need the mouse.
Unknown
inv-rconc
[@1: The bald eagle needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "needs" "mouse" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "nice" "+")
The bald eagle does not need the rabbit.
Unknown
inv-random
[@0: The bald eagle needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "rabbit" "-")
The mouse chases the squirrel.
Unknown
random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "+")
The mouse does not chase the bald eagle.
Unknown
inv-random
[@0: The mouse chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bald eagle" "-")
The rabbit needs the bald eagle.
Unknown
random
[@0: The rabbit needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bald eagle" "+")
@0: The bald eagle needs the squirrel.[(triple1)] The mouse is round.[(triple2)] The rabbit eats the squirrel.[(triple3)] The squirrel does not eat the mouse.[(triple4)] @1: The rabbit is big.[(((triple3) -> rule6))] @2: The rabbit eats the rabbit.[(((((triple3) -> rule6)) -> rule1))] @3: The rabbit does not chase the mouse.[(((((((triple3) -> rule6)) -> rule1)) -> rule5))]
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple3
The squirrel does not eat the mouse.
("squirrel" "eats" "mouse" "-")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
((triple3) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3