The bald eagle is big. The lion is rough. The rabbit needs the squirrel. The squirrel is young. If someone is young then they eat the lion. If someone is nice then they do not need the bald eagle. If someone eats the lion then they see the bald eagle. If someone sees the bald eagle then the bald eagle eats the lion. If someone needs the rabbit then they need the lion. If the rabbit eats the bald eagle and the rabbit needs the bald eagle then the rabbit needs the squirrel.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The lion is rough.
("lion" "is" "rough" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If someone is young then they eat the lion.
((("someone" "is" "young" "+")) -> ("someone" "eats" "lion" "+"))
If someone is nice then they do not need the bald eagle.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "bald eagle" "-"))
If someone eats the lion then they see the bald eagle.
((("someone" "eats" "lion" "+")) -> ("someone" "sees" "bald eagle" "+"))
If someone sees the bald eagle then the bald eagle eats the lion.
((("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "eats" "lion" "+"))
If someone needs the rabbit then they need the lion.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "lion" "+"))
If the rabbit eats the bald eagle and the rabbit needs the bald eagle then the rabbit needs the squirrel.
((("rabbit" "eats" "bald eagle" "+") ("rabbit" "needs" "bald eagle" "+")) -> ("rabbit" "needs" "squirrel" "+"))
The bald eagle is big.
True
1
proof
[(triple1)]
("bald eagle" "is" "big" "+")
triple1
The lion is not rough.
False
1
inv-proof
[(triple2)]
("lion" "is" "rough" "-")
triple2
The squirrel eats the lion.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "eats" "lion" "+")
((triple4) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel does not eat the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("squirrel" "eats" "lion" "-")
((triple4) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel sees the bald eagle.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("squirrel" "sees" "bald eagle" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The squirrel does not see the bald eagle.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("squirrel" "sees" "bald eagle" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The bald eagle eats the lion.
True
4
proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule4))]
("bald eagle" "eats" "lion" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int3
The bald eagle does not eat the lion.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule4))]
("bald eagle" "eats" "lion" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int3
The squirrel does not need the lion.
Unknown
inv-rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "lion" "-")
The bald eagle needs the lion.
Unknown
rconc
[@1: The bald eagle needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "needs" "lion" "+")
The lion does not see the bald eagle.
Unknown
inv-rconc
[@2: The lion sees the bald eagle.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "sees" "bald eagle" "-")
The rabbit sees the bald eagle.
Unknown
rconc
[@2: The rabbit sees the bald eagle.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("rabbit" "sees" "bald eagle" "+")
The bald eagle does not need the squirrel.
Unknown
inv-random
[@0: The bald eagle needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "squirrel" "-")
The bald eagle is rough.
Unknown
random
[@0: The bald eagle is rough.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "rough" "+")
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 squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The bald eagle is big.[(triple1)] The lion is rough.[(triple2)] The rabbit needs the squirrel.[(triple3)] The squirrel is young.[(triple4)] @1: The squirrel eats the lion.[(((triple4) -> rule1))] @2: The squirrel sees the bald eagle.[(((((triple4) -> rule1)) -> rule3))] @3: The bald eagle eats the lion.[(((((((triple4) -> rule1)) -> rule3)) -> rule4))] @4: The bald eagle sees the bald eagle.[(((((((((triple4) -> rule1)) -> rule3)) -> rule4)) -> rule3))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
((triple4) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
((((((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int2
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int4