The bald eagle chases the lion. The bald eagle is rough. The bald eagle needs the rabbit. The cow chases the bald eagle. The lion is big. The lion needs the cow. The lion visits the cow. The rabbit chases the bald eagle. The rabbit is green. The rabbit is round. The rabbit needs the bald eagle. If something is rough then it visits the lion. If something is green and it visits the cow then the cow visits the lion. If something visits the cow then it is rough. If something needs the lion and the lion chases the rabbit then the lion chases the cow. If something visits the lion then the lion chases the rabbit. If something needs the cow then the cow visits the rabbit. If something chases the rabbit and the rabbit is green then the rabbit visits the cow. If the cow visits the rabbit then the cow chases the bald eagle. If something needs the cow and the cow visits the bald eagle then the bald eagle chases the lion.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
The lion is big.
("lion" "is" "big" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
If something is rough then it visits the lion.
((("something" "is" "rough" "+")) -> ("something" "visits" "lion" "+"))
If something is green and it visits the cow then the cow visits the lion.
((("something" "is" "green" "+") ("something" "visits" "cow" "+")) -> ("cow" "visits" "lion" "+"))
If something visits the cow then it is rough.
((("something" "visits" "cow" "+")) -> ("something" "is" "rough" "+"))
If something needs the lion and the lion chases the rabbit then the lion chases the cow.
((("something" "needs" "lion" "+") ("lion" "chases" "rabbit" "+")) -> ("lion" "chases" "cow" "+"))
If something visits the lion then the lion chases the rabbit.
((("something" "visits" "lion" "+")) -> ("lion" "chases" "rabbit" "+"))
If something needs the cow then the cow visits the rabbit.
((("something" "needs" "cow" "+")) -> ("cow" "visits" "rabbit" "+"))
If something chases the rabbit and the rabbit is green then the rabbit visits the cow.
((("something" "chases" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "visits" "cow" "+"))
If the cow visits the rabbit then the cow chases the bald eagle.
((("cow" "visits" "rabbit" "+")) -> ("cow" "chases" "bald eagle" "+"))
If something needs the cow and the cow visits the bald eagle then the bald eagle chases the lion.
((("something" "needs" "cow" "+") ("cow" "visits" "bald eagle" "+")) -> ("bald eagle" "chases" "lion" "+"))
The lion visits the cow.
True
1
proof
[(triple7)]
("lion" "visits" "cow" "+")
triple7
The bald eagle does not chase the lion.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "lion" "-")
triple1
The bald eagle visits the lion.
True
2
proof
[(((triple2) -> rule1))]
("bald eagle" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple7) -> rule3))]
("lion" "is" "rough" "-")
((triple7) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the rabbit.
True
3
proof
[(((((triple2) -> rule1)) -> rule5) OR ((((((triple7) -> rule3)) -> rule1)) -> rule5))]
("lion" "chases" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion does not visit the lion.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("lion" "visits" "lion" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The rabbit visits the cow.
True
5
proof
[(((((((triple2) -> rule1)) -> rule5) triple9) -> rule7) OR ((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7))]
("rabbit" "visits" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule7 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int3
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule7 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The rabbit does not visit the cow.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule5) triple9) -> rule7) OR ((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7))]
("rabbit" "visits" "cow" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule7 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int3
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule7 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The cow visits the lion.
True
7
proof
[(((triple9 ((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule2) OR ((triple9 ((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule2))]
("cow" "visits" "lion" "+")
((triple9 ((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int4
((triple9 ((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The rabbit is not rough.
False
6
inv-proof
[(((((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3) OR ((((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3))]
("rabbit" "is" "rough" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int4
((((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The rabbit visits the lion.
True
7
proof
[(((((((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3)) -> rule1) OR ((((((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3)) -> rule1))]
("rabbit" "visits" "lion" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int4
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int5
((((((((((((triple7) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule5 % int4)) triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int4
The lion visits the lion.
("lion" "visits" "lion" "+")
int5
The lion is rough.
("lion" "is" "rough" "+")
int6
The rabbit does not visit the lion.
False
7
inv-proof
[(((((((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3)) -> rule1) OR ((((((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3)) -> rule1))]
("rabbit" "visits" "lion" "-")
((((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int4
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int5
((((((((((((triple7) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule5 % int4)) triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int4
The lion visits the lion.
("lion" "visits" "lion" "+")
int5
The lion is rough.
("lion" "is" "rough" "+")
int6
The lion does not chase the cow.
Unknown
inv-rconc
[@1: The lion chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "cow" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "rough" "+")
The bald eagle does not need the lion.
Unknown
inv-random
[@0: The bald eagle needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "lion" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
The bald eagle does not visit the rabbit.
Unknown
inv-random
[@0: The bald eagle visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "rabbit" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cow visits the bald eagle.
Unknown
random
[@0: The cow visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "bald eagle" "+")
The rabbit does not visit the bald eagle.
Unknown
inv-random
[@0: The rabbit visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bald eagle" "-")
The rabbit needs the cow.
Unknown
random
[@0: The rabbit needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cow" "+")
The bald eagle does not visit the bald eagle.
Unknown
inv-random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "-")
The lion visits the bald eagle.
Unknown
random
[@0: The lion visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bald eagle" "+")
@0: The bald eagle chases the lion.[(triple1)] The bald eagle is rough.[(triple2)] The bald eagle needs the rabbit.[(triple3)] The cow chases the bald eagle.[(triple4 OR ((((triple6) -> rule6)) -> rule8))] The lion is big.[(triple5)] The lion needs the cow.[(triple6)] The lion visits the cow.[(triple7)] The rabbit chases the bald eagle.[(triple8)] The rabbit is green.[(triple9)] The rabbit is round.[(triple10)] The rabbit needs the bald eagle.[(triple11)] @1: The bald eagle visits the lion.[(((triple2) -> rule1))] The cow visits the rabbit.[(((triple6) -> rule6))] The lion is rough.[(((triple7) -> rule3))] @2: The lion chases the rabbit.[(((((triple2) -> rule1)) -> rule5) OR ((((((triple7) -> rule3)) -> rule1)) -> rule5))] The lion visits the lion.[(((((triple7) -> rule3)) -> rule1))] @3: The rabbit visits the cow.[(((((((triple2) -> rule1)) -> rule5) triple9) -> rule7) OR ((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7))] @4: The cow visits the lion.[(((triple9 ((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule2) OR ((triple9 ((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule2))] The rabbit is rough.[(((((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3) OR ((((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3))] @5: The rabbit visits the lion.[(((((((((((triple2) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3)) -> rule1) OR ((((((((((((triple7) -> rule3)) -> rule1)) -> rule5) triple9) -> rule7)) -> rule3)) -> rule1))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple2
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple3
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
triple4
((((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The lion is big.
("lion" "is" "big" "+")
triple5
The lion needs the cow.
("lion" "needs" "cow" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple11
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
((triple6) -> (rule6 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple7) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule7 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int3
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule7 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple9 ((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int4
((triple9 ((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int4
((((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int4
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int5
((((((((((((triple7) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule5 % int4)) triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int4
The lion visits the lion.
("lion" "visits" "lion" "+")
int5
The lion is rough.
("lion" "is" "rough" "+")
int6