The bald eagle is rough. The bald eagle is young. The bald eagle sees the lion. The bald eagle sees the tiger. The bald eagle visits the cat. The cat likes the bald eagle. The cat sees the lion. The cat visits the tiger. The lion visits the cat. The tiger is kind. The tiger is nice. The tiger is rough. The tiger likes the cat. The tiger likes the lion. The tiger visits the cat. If someone is red then they like the tiger. If someone sees the tiger then they like the lion. If someone visits the cat then they are red. If the lion sees the cat then the cat visits the bald eagle. If someone is rough and nice then they like the cat. If someone is red then they see the tiger.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is red then they like the tiger.
((("someone" "is" "red" "+")) -> ("someone" "likes" "tiger" "+"))
If someone sees the tiger then they like the lion.
((("someone" "sees" "tiger" "+")) -> ("someone" "likes" "lion" "+"))
If someone visits the cat then they are red.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "red" "+"))
If the lion sees the cat then the cat visits the bald eagle.
((("lion" "sees" "cat" "+")) -> ("cat" "visits" "bald eagle" "+"))
If someone is rough and nice then they like the cat.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "likes" "cat" "+"))
If someone is red then they see the tiger.
((("someone" "is" "red" "+")) -> ("someone" "sees" "tiger" "+"))
The tiger is rough.
True
1
proof
[(triple12)]
("tiger" "is" "rough" "+")
triple12
The cat does not see the lion.
False
1
inv-proof
[(triple7)]
("cat" "sees" "lion" "-")
triple7
The tiger is red.
True
2
proof
[(((triple15) -> rule3))]
("tiger" "is" "red" "+")
((triple15) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple9) -> rule3))]
("lion" "is" "red" "-")
((triple9) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion likes the tiger.
True
3
proof
[(((((triple9) -> rule3)) -> rule1))]
("lion" "likes" "tiger" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The bald eagle does not like the tiger.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule1))]
("bald eagle" "likes" "tiger" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The lion likes the lion.
True
4
proof
[(((((((triple9) -> rule3)) -> rule6)) -> rule2))]
("lion" "likes" "lion" "+")
((((((triple9) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion does not like the lion.
False
4
inv-proof
[(((((((triple9) -> rule3)) -> rule6)) -> rule2))]
("lion" "likes" "lion" "-")
((((((triple9) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "red" "-")
The bald eagle likes the cat.
Unknown
rconc
[@1: The bald eagle likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "likes" "cat" "+")
The lion does not like the cat.
Unknown
inv-rconc
[@1: The lion likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "likes" "cat" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "cat" "+")
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 tiger sees the bald eagle.
Unknown
random
[@0: The tiger sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bald eagle" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The lion visits the tiger.
Unknown
random
[@0: The lion visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "tiger" "+")
@0: The bald eagle is rough.[(triple1)] The bald eagle is young.[(triple2)] The bald eagle sees the lion.[(triple3)] The bald eagle sees the tiger.[(triple4 OR ((((triple5) -> rule3)) -> rule6))] The bald eagle visits the cat.[(triple5)] The cat likes the bald eagle.[(triple6)] The cat sees the lion.[(triple7)] The cat visits the tiger.[(triple8)] The lion visits the cat.[(triple9)] The tiger is kind.[(triple10)] The tiger is nice.[(triple11)] The tiger is rough.[(triple12)] The tiger likes the cat.[(triple13 OR ((triple12 triple11) -> rule5))] The tiger likes the lion.[(triple14 OR ((((((triple15) -> rule3)) -> rule6)) -> rule2))] The tiger visits the cat.[(triple15)] @1: The bald eagle is red.[(((triple5) -> rule3))] The bald eagle likes the lion.[(((triple4) -> rule2) OR ((((((triple5) -> rule3)) -> rule6)) -> rule2))] The lion is red.[(((triple9) -> rule3))] The tiger is red.[(((triple15) -> rule3))] @2: The bald eagle likes the tiger.[(((((triple5) -> rule3)) -> rule1))] The lion likes the tiger.[(((((triple9) -> rule3)) -> rule1))] The lion sees the tiger.[(((((triple9) -> rule3)) -> rule6))] The tiger likes the tiger.[(((((triple15) -> rule3)) -> rule1))] The tiger sees the tiger.[(((((triple15) -> rule3)) -> rule6))] @3: The lion likes the lion.[(((((((triple9) -> rule3)) -> rule6)) -> rule2))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple3
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple4
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple5
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple6
The cat sees the lion.
("cat" "sees" "lion" "+")
triple7
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple8
The lion visits the cat.
("lion" "visits" "cat" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple13
((triple12 triple11) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
((((((triple15) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The bald eagle is red.
("bald eagle" "is" "red" "+")
((triple5) -> (rule3 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
((triple4) -> (rule2 % int1))
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
int1
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The lion is red.
("lion" "is" "red" "+")
((triple9) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple15) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple9) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple15) -> (rule3 % int2))) -> (rule6 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
((((((triple9) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3