The bald eagle eats the squirrel. The mouse sees the squirrel. The rabbit is kind. The squirrel sees the mouse. If something is big then it sees the squirrel. If something eats the rabbit and it is big then the rabbit chases the mouse. If something eats the squirrel then the squirrel is big. If something is cold and it sees the mouse then the mouse is rough. If the squirrel chases the rabbit and the squirrel is rough then the squirrel eats the rabbit. If something sees the squirrel and it sees the mouse then it eats the bald eagle. If the bald eagle sees the rabbit and the rabbit chases the squirrel then the rabbit eats the squirrel. If something eats the rabbit then it is big.
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
If something eats the rabbit and it is big then the rabbit chases the mouse.
((("something" "eats" "rabbit" "+") ("something" "is" "big" "+")) -> ("rabbit" "chases" "mouse" "+"))
If something eats the squirrel then the squirrel is big.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If something is cold and it sees the mouse then the mouse is rough.
((("something" "is" "cold" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If the squirrel chases the rabbit and the squirrel is rough then the squirrel eats the rabbit.
((("squirrel" "chases" "rabbit" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If something sees the squirrel and it sees the mouse then it eats the bald eagle.
((("something" "sees" "squirrel" "+") ("something" "sees" "mouse" "+")) -> ("something" "eats" "bald eagle" "+"))
If the bald eagle sees the rabbit and the rabbit chases the squirrel then the rabbit eats the squirrel.
((("bald eagle" "sees" "rabbit" "+") ("rabbit" "chases" "squirrel" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If something eats the rabbit then it is big.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "big" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple4)]
("squirrel" "sees" "mouse" "+")
triple4
The bald eagle does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("bald eagle" "eats" "squirrel" "-")
triple1
The squirrel is big.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "is" "big" "+")
((triple1) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "is" "big" "-")
((triple1) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the squirrel.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel eats the bald eagle.
True
5
proof
[(((((((triple1) -> rule3)) -> rule1) triple4) -> rule6))]
("squirrel" "eats" "bald eagle" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel does not eat the bald eagle.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule1) triple4) -> rule6))]
("squirrel" "eats" "bald eagle" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "big" "-")
The rabbit eats the squirrel.
Unknown
rconc
[@1: The rabbit eats the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "eats" "squirrel" "+")
The rabbit does not eat the bald eagle.
Unknown
inv-rconc
[@1: The rabbit eats the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "bald eagle" "-")
The mouse eats the bald eagle.
Unknown
rconc
[@1: The mouse eats the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "bald eagle" "+")
The bald eagle does not see the mouse.
Unknown
inv-random
[@0: The bald eagle sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "mouse" "-")
The squirrel chases the rabbit.
Unknown
random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The bald eagle eats the squirrel.[(triple1)] The mouse sees the squirrel.[(triple2)] The rabbit is kind.[(triple3)] The squirrel sees the mouse.[(triple4)] @1: The squirrel is big.[(((triple1) -> rule3))] @2: The squirrel sees the squirrel.[(((((triple1) -> rule3)) -> rule1))] @3: The squirrel eats the bald eagle.[(((((((triple1) -> rule3)) -> rule1) triple4) -> rule6))]
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
((triple1) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3