The bald eagle eats the lion. The bald eagle is big. The cow is nice. The cow likes the bald eagle. The cow needs the lion. The lion eats the bald eagle. The lion eats the rabbit. The lion is not nice. The lion is rough. The lion likes the cow. The lion needs the rabbit. The rabbit eats the lion. The rabbit is kind. The rabbit is nice. The rabbit does not like the cow. If something is rough and it eats the cow then it does not need the rabbit. If something is big and not red then it eats the lion. If something is nice then it eats the cow. If something likes the rabbit then it does not like the bald eagle. Red things are not big. If something is kind and it eats the rabbit then the rabbit does not eat the bald eagle. If something eats the cow then the cow is rough. If something likes the cow then it is not kind.
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
The bald eagle is big.
("bald eagle" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
If something is rough and it eats the cow then it does not need the rabbit.
((("something" "is" "rough" "+") ("something" "eats" "cow" "+")) -> ("something" "needs" "rabbit" "-"))
If something is big and not red then it eats the lion.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "eats" "lion" "+"))
If something is nice then it eats the cow.
((("something" "is" "nice" "+")) -> ("something" "eats" "cow" "+"))
If something likes the rabbit then it does not like the bald eagle.
((("something" "likes" "rabbit" "+")) -> ("something" "likes" "bald eagle" "-"))
Red things are not big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "-"))
If something is kind and it eats the rabbit then the rabbit does not eat the bald eagle.
((("something" "is" "kind" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "eats" "bald eagle" "-"))
If something eats the cow then the cow is rough.
((("something" "eats" "cow" "+")) -> ("cow" "is" "rough" "+"))
If something likes the cow then it is not kind.
((("something" "likes" "cow" "+")) -> ("something" "is" "kind" "-"))
The rabbit is nice.
True
1
proof
[(triple14)]
("rabbit" "is" "nice" "+")
triple14
The cow is not nice.
False
1
inv-proof
[(triple3)]
("cow" "is" "nice" "-")
triple3
The lion is not kind.
True
2
proof
[(((triple10) -> rule8))]
("lion" "is" "kind" "-")
((triple10) -> (rule8 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The rabbit does not eat the cow.
False
2
inv-proof
[(((triple14) -> rule3))]
("rabbit" "eats" "cow" "-")
((triple14) -> (rule3 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow is rough.
True
3
proof
[(((((triple14) -> rule3)) -> rule7) OR ((((triple3) -> rule3)) -> rule7))]
("cow" "is" "rough" "+")
((((triple14) -> (rule3 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is not rough.
False
3
inv-proof
[(((((triple14) -> rule3)) -> rule7) OR ((((triple3) -> rule3)) -> rule7))]
("cow" "is" "rough" "-")
((((triple14) -> (rule3 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not need the rabbit.
True
6
proof
[(((((((triple14) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule1) OR ((((((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule1))]
("cow" "needs" "rabbit" "-")
((((((triple14) -> (rule3 % int4))) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int4
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow needs the rabbit.
False
6
inv-proof
[(((((((triple14) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule1) OR ((((((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule1))]
("cow" "needs" "rabbit" "+")
((((((triple14) -> (rule3 % int4))) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int4
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The bald eagle does not eat the cow.
Unknown
inv-rconc
[@1: The bald eagle eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "eats" "cow" "-")
The lion eats the cow.
Unknown
rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "cow" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "lion" "-")
The cow eats the lion.
Unknown
rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "lion" "+")
The cow does not like the lion.
Unknown
inv-random
[@0: The cow likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "lion" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The lion does not like the rabbit.
Unknown
inv-random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "-")
The bald eagle likes the rabbit.
Unknown
random
[@0: The bald eagle likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "rabbit" "+")
@0: The bald eagle eats the lion.[(triple1)] The bald eagle is big.[(triple2)] The cow is nice.[(triple3)] The cow likes the bald eagle.[(triple4)] The cow needs the lion.[(triple5)] The lion eats the bald eagle.[(triple6)] The lion eats the rabbit.[(triple7)] The lion is not nice.[(triple8)] The lion is rough.[(triple9)] The lion likes the cow.[(triple10)] The lion needs the rabbit.[(triple11)] The rabbit does not like the cow.[(triple15)] The rabbit eats the lion.[(triple12)] The rabbit is kind.[(triple13)] The rabbit is nice.[(triple14)] @1: The cow eats the cow.[(((triple3) -> rule3))] The lion is not kind.[(((triple10) -> rule8))] The rabbit eats the cow.[(((triple14) -> rule3))] @2: The cow is rough.[(((((triple14) -> rule3)) -> rule7) OR ((((triple3) -> rule3)) -> rule7))] @3: The cow does not need the rabbit.[(((((((triple14) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule1) OR ((((((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule1))]
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
triple1
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
triple4
The cow needs the lion.
("cow" "needs" "lion" "+")
triple5
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
triple6
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple7
The lion is not nice.
("lion" "is" "nice" "-")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The lion likes the cow.
("lion" "likes" "cow" "+")
triple10
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple11
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
triple15
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple14
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple3) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The lion is not kind.
("lion" "is" "kind" "-")
((triple10) -> (rule8 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((triple14) -> (rule3 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple14) -> (rule3 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
((((((triple14) -> (rule3 % int4))) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int4
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3