The bald eagle chases the lion. The bald eagle eats the lion. The bald eagle is kind. The bald eagle sees the lion. The lion chases the bald eagle. The lion is kind. The lion sees the bald eagle. If something sees the lion then the lion chases the bald eagle. If something eats the lion and the lion eats the bald eagle then it chases the lion. If the bald eagle chases the lion then the bald eagle is kind. If something sees the lion then the lion eats the bald eagle. If the bald eagle sees the lion then the bald eagle chases the lion. Red things are nice. If something eats the bald eagle then it eats the lion. If the lion sees the bald eagle and the bald eagle chases the lion then the bald eagle sees the lion.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
If something sees the lion then the lion chases the bald eagle.
((("something" "sees" "lion" "+")) -> ("lion" "chases" "bald eagle" "+"))
If something eats the lion and the lion eats the bald eagle then it chases the lion.
((("something" "eats" "lion" "+") ("lion" "eats" "bald eagle" "+")) -> ("something" "chases" "lion" "+"))
If the bald eagle chases the lion then the bald eagle is kind.
((("bald eagle" "chases" "lion" "+")) -> ("bald eagle" "is" "kind" "+"))
If something sees the lion then the lion eats the bald eagle.
((("something" "sees" "lion" "+")) -> ("lion" "eats" "bald eagle" "+"))
If the bald eagle sees the lion then the bald eagle chases the lion.
((("bald eagle" "sees" "lion" "+")) -> ("bald eagle" "chases" "lion" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something eats the bald eagle then it eats the lion.
((("something" "eats" "bald eagle" "+")) -> ("something" "eats" "lion" "+"))
If the lion sees the bald eagle and the bald eagle chases the lion then the bald eagle sees the lion.
((("lion" "sees" "bald eagle" "+") ("bald eagle" "chases" "lion" "+")) -> ("bald eagle" "sees" "lion" "+"))
The lion chases the bald eagle.
True
1
proof
[(triple5 OR ((triple4) -> rule1) OR ((((triple7 triple1) -> rule8)) -> rule1))]
("lion" "chases" "bald eagle" "+")
triple5
((triple4) -> (rule1 % int1))
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int1
((((triple7 triple1) -> (rule8 % int2))) -> (rule1 % int1))
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle does not see the lion.
False
1
inv-proof
[(triple4 OR ((triple7 triple1) -> rule8))]
("bald eagle" "sees" "lion" "-")
triple4
((triple7 triple1) -> (rule8 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The lion eats the bald eagle.
True
2
proof
[(((triple4) -> rule4) OR ((((triple7 triple1) -> rule8)) -> rule4))]
("lion" "eats" "bald eagle" "+")
((triple4) -> (rule4 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
((((triple7 triple1) -> (rule8 % int2))) -> (rule4 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion does not eat the bald eagle.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple7 triple1) -> rule8)) -> rule4))]
("lion" "eats" "bald eagle" "-")
((triple4) -> (rule4 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
((((triple7 triple1) -> (rule8 % int2))) -> (rule4 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion eats the lion.
True
3
proof
[(((((triple4) -> rule4)) -> rule7) OR ((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7))]
("lion" "eats" "lion" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
((((((triple7 triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The lion does not eat the lion.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule7) OR ((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7))]
("lion" "eats" "lion" "-")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
((((((triple7 triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The lion chases the lion.
True
6
proof
[(((((((triple4) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule2) OR ((((((triple4) -> rule4)) -> rule7) ((((triple7 triple1) -> rule8)) -> rule4)) -> rule2) OR ((((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule2) OR ((((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7) ((((triple7 triple1) -> rule8)) -> rule4)) -> rule2))]
("lion" "chases" "lion" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
((((((triple4) -> (rule4 % int4))) -> (rule7 % int3)) ((((triple7 triple1) -> (rule8 % int2))) -> (rule4 % int4))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int4
((((((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
((((((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The lion does not chase the lion.
False
6
inv-proof
[(((((((triple4) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule2) OR ((((((triple4) -> rule4)) -> rule7) ((((triple7 triple1) -> rule8)) -> rule4)) -> rule2) OR ((((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule2) OR ((((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7) ((((triple7 triple1) -> rule8)) -> rule4)) -> rule2))]
("lion" "chases" "lion" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
((((((triple4) -> (rule4 % int4))) -> (rule7 % int3)) ((((triple7 triple1) -> (rule8 % int2))) -> (rule4 % int4))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int4
((((((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
((((((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "-")
The bald eagle is nice.
Unknown
rconc
[@1: The bald eagle is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "nice" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The bald eagle is young.
Unknown
random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "+")
The bald eagle is not green.
Unknown
inv-random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The bald eagle chases the lion.[(triple1 OR ((triple4) -> rule5) OR ((triple2 ((triple4) -> rule4)) -> rule2))] The bald eagle eats the lion.[(triple2)] The bald eagle is kind.[(triple3 OR ((triple1) -> rule3) OR ((((triple4) -> rule5)) -> rule3) OR ((((triple2 ((triple4) -> rule4)) -> rule2)) -> rule3))] The bald eagle sees the lion.[(triple4 OR ((triple7 triple1) -> rule8))] The lion chases the bald eagle.[(triple5 OR ((triple4) -> rule1) OR ((((triple7 triple1) -> rule8)) -> rule1))] The lion is kind.[(triple6)] The lion sees the bald eagle.[(triple7)] @1: The lion eats the bald eagle.[(((triple4) -> rule4) OR ((((triple7 triple1) -> rule8)) -> rule4))] @2: The lion eats the lion.[(((((triple4) -> rule4)) -> rule7) OR ((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7))] @3: The lion chases the lion.[(((((((triple4) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule2) OR ((((((triple4) -> rule4)) -> rule7) ((((triple7 triple1) -> rule8)) -> rule4)) -> rule2) OR ((((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7) ((triple4) -> rule4)) -> rule2) OR ((((((((triple7 triple1) -> rule8)) -> rule4)) -> rule7) ((((triple7 triple1) -> rule8)) -> rule4)) -> rule2))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
((triple4) -> (rule5 % int1))
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int1
((triple2 ((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
triple2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple3
((triple1) -> (rule3 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int2
((((triple2 ((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple4
((triple7 triple1) -> (rule8 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple5
((triple4) -> (rule1 % int1))
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int1
((((triple7 triple1) -> (rule8 % int2))) -> (rule1 % int1))
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple7
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
((triple4) -> (rule4 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
((((triple7 triple1) -> (rule8 % int2))) -> (rule4 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
((((((triple7 triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
((((((triple4) -> (rule4 % int4))) -> (rule7 % int3)) ((((triple7 triple1) -> (rule8 % int2))) -> (rule4 % int4))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int4
((((((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
((((((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple7 triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4