The bald eagle is kind. The bald eagle is not nice. The bald eagle sees the rabbit. The bald eagle visits the cow. The bald eagle visits the lion. The cow does not chase the bald eagle. The cow is nice. The lion chases the rabbit. The rabbit chases the cow. The rabbit is kind. If someone sees the lion then the lion chases the cow. If someone sees the cow then the cow chases the bald eagle. If someone visits the rabbit then they chase the lion. If someone sees the lion then they visit the rabbit. If someone chases the cow then they see the lion. If someone sees the rabbit then the rabbit chases the bald eagle. If someone is round and blue then they do not chase the bald eagle. If someone is kind then they see the rabbit. If someone is kind and they do not chase the cow then the cow visits the bald eagle.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
The cow does not chase the bald eagle.
("cow" "chases" "bald eagle" "-")
The cow is nice.
("cow" "is" "nice" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If someone sees the lion then the lion chases the cow.
((("someone" "sees" "lion" "+")) -> ("lion" "chases" "cow" "+"))
If someone sees the cow then the cow chases the bald eagle.
((("someone" "sees" "cow" "+")) -> ("cow" "chases" "bald eagle" "+"))
If someone visits the rabbit then they chase the lion.
((("someone" "visits" "rabbit" "+")) -> ("someone" "chases" "lion" "+"))
If someone sees the lion then they visit the rabbit.
((("someone" "sees" "lion" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone chases the cow then they see the lion.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the rabbit then the rabbit chases the bald eagle.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "bald eagle" "+"))
If someone is round and blue then they do not chase the bald eagle.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "chases" "bald eagle" "-"))
If someone is kind then they see the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is kind and they do not chase the cow then the cow visits the bald eagle.
((("someone" "is" "kind" "+") ("someone" "chases" "cow" "~")) -> ("cow" "visits" "bald eagle" "+"))
The rabbit chases the cow.
True
1
proof
[(triple9)]
("rabbit" "chases" "cow" "+")
triple9
The bald eagle does not see the rabbit.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule8))]
("bald eagle" "sees" "rabbit" "-")
triple3
((triple1) -> (rule8 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The rabbit chases the bald eagle.
True
2
proof
[(((triple3) -> rule6) OR ((((triple1) -> rule8)) -> rule6) OR ((((triple10) -> rule8)) -> rule6))]
("rabbit" "chases" "bald eagle" "+")
((triple3) -> (rule6 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
((((triple10) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple10) -> rule8))]
("rabbit" "sees" "rabbit" "-")
((triple10) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the rabbit.
True
3
proof
[(((((triple9) -> rule5)) -> rule4))]
("rabbit" "visits" "rabbit" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule4))]
("rabbit" "visits" "rabbit" "-")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit chases the lion.
True
4
proof
[(((((((triple9) -> rule5)) -> rule4)) -> rule3))]
("rabbit" "chases" "lion" "+")
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion does not see the lion.
False
4
inv-proof
[(((((((triple9) -> rule5)) -> rule1)) -> rule5))]
("lion" "sees" "lion" "-")
((((((triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion visits the rabbit.
True
5
proof
[(((((((((triple9) -> rule5)) -> rule1)) -> rule5)) -> rule4))]
("lion" "visits" "rabbit" "+")
((((((((triple9) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int4
The lion does not visit the rabbit.
False
5
inv-proof
[(((((((((triple9) -> rule5)) -> rule1)) -> rule5)) -> rule4))]
("lion" "visits" "rabbit" "-")
((((((((triple9) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int4
The lion chases the lion.
True
6
proof
[(((((((((((triple9) -> rule5)) -> rule1)) -> rule5)) -> rule4)) -> rule3))]
("lion" "chases" "lion" "+")
((((((((((triple9) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
int4
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int5
The lion does not chase the lion.
False
6
inv-proof
[(((((((((((triple9) -> rule5)) -> rule1)) -> rule5)) -> rule4)) -> rule3))]
("lion" "chases" "lion" "-")
((((((((((triple9) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
int4
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int5
The bald eagle does not visit the rabbit.
Unknown
inv-rconc
[@2: The bald eagle visits the rabbit.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("bald eagle" "visits" "rabbit" "-")
The cow sees the rabbit.
Unknown
rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "rabbit" "+")
The cow does not visit the bald eagle.
Unknown
inv-rconc
[@1: The cow visits the bald eagle.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "visits" "bald eagle" "-")
The cow visits the rabbit.
Unknown
rconc
[@2: The cow visits the rabbit.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("cow" "visits" "rabbit" "+")
The cow does not see the lion.
Unknown
inv-rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "lion" "-")
The bald eagle chases the lion.
Unknown
rconc
[@3: The bald eagle chases the lion.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- FAIL)]]
("bald eagle" "chases" "lion" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The bald eagle is not round.
Unknown
inv-random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The rabbit does not see the bald eagle.
Unknown
inv-random
[@0: The rabbit sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bald eagle" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The bald eagle is kind.[(triple1)] The bald eagle is not nice.[(triple2)] The bald eagle sees the rabbit.[(triple3 OR ((triple1) -> rule8))] The bald eagle visits the cow.[(triple4)] The bald eagle visits the lion.[(triple5)] The cow does not chase the bald eagle.[(triple6)] The cow is nice.[(triple7)] The lion chases the rabbit.[(triple8)] The rabbit chases the cow.[(triple9)] The rabbit is kind.[(triple10)] @1: The rabbit chases the bald eagle.[(((triple3) -> rule6) OR ((((triple1) -> rule8)) -> rule6) OR ((((triple10) -> rule8)) -> rule6))] The rabbit sees the lion.[(((triple9) -> rule5))] The rabbit sees the rabbit.[(((triple10) -> rule8))] @2: The lion chases the cow.[(((((triple9) -> rule5)) -> rule1))] The rabbit visits the rabbit.[(((((triple9) -> rule5)) -> rule4))] @3: The lion sees the lion.[(((((((triple9) -> rule5)) -> rule1)) -> rule5))] The rabbit chases the lion.[(((((((triple9) -> rule5)) -> rule4)) -> rule3))] @4: The lion visits the rabbit.[(((((((((triple9) -> rule5)) -> rule1)) -> rule5)) -> rule4))] @5: The lion chases the lion.[(((((((((((triple9) -> rule5)) -> rule1)) -> rule5)) -> rule4)) -> rule3))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
triple2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
triple3
((triple1) -> (rule8 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
triple4
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
triple5
The cow does not chase the bald eagle.
("cow" "chases" "bald eagle" "-")
triple6
The cow is nice.
("cow" "is" "nice" "+")
triple7
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple8
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
((triple3) -> (rule6 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
((((triple10) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple9) -> (rule5 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple10) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((((((((triple9) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int4
The lion chases the lion.
("lion" "chases" "lion" "+")
((((((((((triple9) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
int4
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int5