The bald eagle eats the lion. The lion eats the mouse. The mouse needs the bald eagle. The squirrel is blue. If someone is nice then they need the squirrel. If someone eats the squirrel then the squirrel is nice. If someone needs the bald eagle then they eat the squirrel.
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If someone is nice then they need the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone eats the squirrel then the squirrel is nice.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If someone needs the bald eagle then they eat the squirrel.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "eats" "squirrel" "+"))
The mouse needs the bald eagle.
True
1
proof
[(triple3)]
("mouse" "needs" "bald eagle" "+")
triple3
The bald eagle does not eat the lion.
False
1
inv-proof
[(triple1)]
("bald eagle" "eats" "lion" "-")
triple1
The mouse eats the squirrel.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "eats" "squirrel" "+")
((triple3) -> (rule3 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse does not eat the squirrel.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "eats" "squirrel" "-")
((triple3) -> (rule3 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("squirrel" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("squirrel" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel needs the squirrel.
True
4
proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3
The squirrel does not need the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The bald eagle does not eat the squirrel.
Unknown
inv-rconc
[@1: The bald eagle eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "eats" "squirrel" "-")
The lion needs the squirrel.
Unknown
rconc
[@1: The lion needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "squirrel" "+")
The mouse does not eat the lion.
Unknown
inv-random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "-")
The bald eagle eats the mouse.
Unknown
random
[@0: The bald eagle eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "mouse" "+")
The bald eagle is not blue.
Unknown
inv-random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "-")
The mouse chases the squirrel.
Unknown
random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "+")
@0: The bald eagle eats the lion.[(triple1)] The lion eats the mouse.[(triple2)] The mouse needs the bald eagle.[(triple3)] The squirrel is blue.[(triple4)] @1: The mouse eats the squirrel.[(((triple3) -> rule3))] @2: The squirrel is nice.[(((((triple3) -> rule3)) -> rule2))] @3: The squirrel needs the squirrel.[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
triple1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple2
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((triple3) -> (rule3 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3