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