The bald eagle does not eat the lion. The bald eagle does not eat the rabbit. The bald eagle likes the rabbit. The bald eagle does not see the cat. The cat is nice. The cat is rough. The cat is young. The cat likes the bald eagle. The lion likes the bald eagle. The lion sees the bald eagle. The lion sees the cat. The rabbit sees the lion. If someone likes the bald eagle then they like the lion. If someone likes the lion then they see the rabbit. If someone eats the lion and the lion likes the bald eagle then they see the rabbit. If someone sees the rabbit then the rabbit likes the bald eagle. If someone eats the lion then they do not like the rabbit. If the cat is big and the cat is kind then the cat does not eat the rabbit. If the bald eagle is big then the bald eagle likes the lion.
The bald eagle does not eat the lion.
("bald eagle" "eats" "lion" "-")
The bald eagle does not eat the rabbit.
("bald eagle" "eats" "rabbit" "-")
The bald eagle likes the rabbit.
("bald eagle" "likes" "rabbit" "+")
The bald eagle does not see the cat.
("bald eagle" "sees" "cat" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone likes the bald eagle then they like the lion.
((("someone" "likes" "bald eagle" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the lion then they see the rabbit.
((("someone" "likes" "lion" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone eats the lion and the lion likes the bald eagle then they see the rabbit.
((("someone" "eats" "lion" "+") ("lion" "likes" "bald eagle" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone sees the rabbit then the rabbit likes the bald eagle.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "likes" "bald eagle" "+"))
If someone eats the lion then they do not like the rabbit.
((("someone" "eats" "lion" "+")) -> ("someone" "likes" "rabbit" "-"))
If the cat is big and the cat is kind then the cat does not eat the rabbit.
((("cat" "is" "big" "+") ("cat" "is" "kind" "+")) -> ("cat" "eats" "rabbit" "-"))
If the bald eagle is big then the bald eagle likes the lion.
((("bald eagle" "is" "big" "+")) -> ("bald eagle" "likes" "lion" "+"))
The bald eagle likes the rabbit.
True
1
proof
[(triple3)]
("bald eagle" "likes" "rabbit" "+")
triple3
The cat does not like the bald eagle.
False
1
inv-proof
[(triple8)]
("cat" "likes" "bald eagle" "-")
triple8
The cat likes the lion.
True
2
proof
[(((triple8) -> rule1))]
("cat" "likes" "lion" "+")
((triple8) -> (rule1 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat does not like the lion.
False
2
inv-proof
[(((triple8) -> rule1))]
("cat" "likes" "lion" "-")
((triple8) -> (rule1 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat sees the rabbit.
True
3
proof
[(((((triple8) -> rule1)) -> rule2))]
("cat" "sees" "rabbit" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The cat does not see the rabbit.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule2))]
("cat" "sees" "rabbit" "-")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
True
4
proof
[(((((((triple8) -> rule1)) -> rule2)) -> rule4) OR ((((((triple9) -> rule1)) -> rule2)) -> rule4))]
("rabbit" "likes" "bald eagle" "+")
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat likes the lion.
("cat" "likes" "lion" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The rabbit does not like the bald eagle.
False
4
inv-proof
[(((((((triple8) -> rule1)) -> rule2)) -> rule4) OR ((((((triple9) -> rule1)) -> rule2)) -> rule4))]
("rabbit" "likes" "bald eagle" "-")
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat likes the lion.
("cat" "likes" "lion" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The rabbit likes the lion.
True
5
proof
[(((((((((triple8) -> rule1)) -> rule2)) -> rule4)) -> rule1) OR ((((((((triple9) -> rule1)) -> rule2)) -> rule4)) -> rule1))]
("rabbit" "likes" "lion" "+")
((((((((triple8) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat likes the lion.
("cat" "likes" "lion" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The rabbit does not like the lion.
False
5
inv-proof
[(((((((((triple8) -> rule1)) -> rule2)) -> rule4)) -> rule1) OR ((((((((triple9) -> rule1)) -> rule2)) -> rule4)) -> rule1))]
("rabbit" "likes" "lion" "-")
((((((((triple8) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat likes the lion.
("cat" "likes" "lion" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The rabbit sees the rabbit.
True
6
proof
[(((((((((((triple8) -> rule1)) -> rule2)) -> rule4)) -> rule1)) -> rule2) OR ((((((((((triple9) -> rule1)) -> rule2)) -> rule4)) -> rule1)) -> rule2))]
("rabbit" "sees" "rabbit" "+")
((((((((((triple8) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat likes the lion.
("cat" "likes" "lion" "+")
int5
((((((((((triple9) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
int5
The rabbit does not see the rabbit.
False
6
inv-proof
[(((((((((((triple8) -> rule1)) -> rule2)) -> rule4)) -> rule1)) -> rule2) OR ((((((((((triple9) -> rule1)) -> rule2)) -> rule4)) -> rule1)) -> rule2))]
("rabbit" "sees" "rabbit" "-")
((((((((((triple8) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat likes the lion.
("cat" "likes" "lion" "+")
int5
((((((((((triple9) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
int5
The bald eagle does not like the lion.
Unknown
inv-rconc
[@1: The bald eagle likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "likes" "lion" "-")
The bald eagle sees the rabbit.
Unknown
rconc
[@2: The bald eagle sees the rabbit.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bald eagle" "sees" "rabbit" "+")
The bald eagle does not like the cat.
Unknown
inv-random
[@0: The bald eagle likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "cat" "-")
The cat eats the rabbit.
Unknown
random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "+")
The cat does not see the lion.
Unknown
inv-random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "-")
The rabbit eats the bald eagle.
Unknown
random
[@0: The rabbit eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bald eagle" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The cat likes the rabbit.
Unknown
random
[@0: The cat likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "rabbit" "+")
The rabbit does not see the cat.
Unknown
inv-random
[@0: The rabbit sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cat" "-")
The cat eats the lion.
Unknown
random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "+")
The bald eagle is not kind.
Unknown
inv-random
[@0: The bald eagle is kind.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "kind" "-")
The rabbit likes the cat.
Unknown
random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "+")
@0: The bald eagle does not eat the lion.[(triple1)] The bald eagle does not eat the rabbit.[(triple2)] The bald eagle does not see the cat.[(triple4)] The bald eagle likes the rabbit.[(triple3)] The cat is nice.[(triple5)] The cat is rough.[(triple6)] The cat is young.[(triple7)] The cat likes the bald eagle.[(triple8)] The lion likes the bald eagle.[(triple9)] The lion sees the bald eagle.[(triple10)] The lion sees the cat.[(triple11)] The rabbit sees the lion.[(triple12)] @1: The cat likes the lion.[(((triple8) -> rule1))] The lion likes the lion.[(((triple9) -> rule1))] @2: The cat sees the rabbit.[(((((triple8) -> rule1)) -> rule2))] The lion sees the rabbit.[(((((triple9) -> rule1)) -> rule2))] @3: The rabbit likes the bald eagle.[(((((((triple8) -> rule1)) -> rule2)) -> rule4) OR ((((((triple9) -> rule1)) -> rule2)) -> rule4))] @4: The rabbit likes the lion.[(((((((((triple8) -> rule1)) -> rule2)) -> rule4)) -> rule1) OR ((((((((triple9) -> rule1)) -> rule2)) -> rule4)) -> rule1))] @5: The rabbit sees the rabbit.[(((((((((((triple8) -> rule1)) -> rule2)) -> rule4)) -> rule1)) -> rule2) OR ((((((((((triple9) -> rule1)) -> rule2)) -> rule4)) -> rule1)) -> rule2))]
The bald eagle does not eat the lion.
("bald eagle" "eats" "lion" "-")
triple1
The bald eagle does not eat the rabbit.
("bald eagle" "eats" "rabbit" "-")
triple2
The bald eagle does not see the cat.
("bald eagle" "sees" "cat" "-")
triple4
The bald eagle likes the rabbit.
("bald eagle" "likes" "rabbit" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat is young.
("cat" "is" "young" "+")
triple7
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple8
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
triple9
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple10
The lion sees the cat.
("lion" "sees" "cat" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
The cat likes the lion.
("cat" "likes" "lion" "+")
((triple8) -> (rule1 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple9) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat likes the lion.
("cat" "likes" "lion" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((((((((triple8) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat likes the lion.
("cat" "likes" "lion" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((((triple8) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat likes the lion.
("cat" "likes" "lion" "+")
int5
((((((((((triple9) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
int5