The bald eagle needs the lion. The bald eagle needs the tiger. The lion is rough. The lion is round. The lion needs the tiger. The tiger eats the lion. The tiger is big. The tiger is nice. The tiger needs the bald eagle. The tiger visits the lion. If someone visits the lion then they visit the bald eagle. If someone is round then they need the tiger. If someone visits the bald eagle then they need the lion. If the lion is round then the lion needs the bald eagle. If someone eats the tiger then they eat the lion. If someone needs the lion and they eat the lion then the lion is big.
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone visits the lion then they visit the bald eagle.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone is round then they need the tiger.
((("someone" "is" "round" "+")) -> ("someone" "needs" "tiger" "+"))
If someone visits the bald eagle then they need the lion.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "needs" "lion" "+"))
If the lion is round then the lion needs the bald eagle.
((("lion" "is" "round" "+")) -> ("lion" "needs" "bald eagle" "+"))
If someone eats the tiger then they eat the lion.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "lion" "+"))
If someone needs the lion and they eat the lion then the lion is big.
((("someone" "needs" "lion" "+") ("someone" "eats" "lion" "+")) -> ("lion" "is" "big" "+"))
The lion is round.
True
1
proof
[(triple4)]
("lion" "is" "round" "+")
triple4
The tiger is not nice.
False
1
inv-proof
[(triple8)]
("tiger" "is" "nice" "-")
triple8
The tiger visits the bald eagle.
True
2
proof
[(((triple10) -> rule1))]
("tiger" "visits" "bald eagle" "+")
((triple10) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The lion does not need the bald eagle.
False
2
inv-proof
[(((triple4) -> rule4))]
("lion" "needs" "bald eagle" "-")
((triple4) -> (rule4 % int1))
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int1
The tiger needs the lion.
True
3
proof
[(((((triple10) -> rule1)) -> rule3))]
("tiger" "needs" "lion" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger does not need the lion.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule3))]
("tiger" "needs" "lion" "-")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The lion is big.
True
5
proof
[(((((((triple10) -> rule1)) -> rule3) triple6) -> rule6))]
("lion" "is" "big" "+")
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The lion is not big.
False
5
inv-proof
[(((((((triple10) -> rule1)) -> rule3) triple6) -> rule6))]
("lion" "is" "big" "-")
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The lion does not visit the bald eagle.
Unknown
inv-rconc
[@1: The lion visits the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "bald eagle" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The bald eagle does not eat the lion.
Unknown
inv-rconc
[@1: The bald eagle eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "eats" "lion" "-")
The lion needs the lion.
Unknown
rconc
[@2: The lion needs the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "needs" "lion" "+")
The bald eagle does not visit the tiger.
Unknown
inv-random
[@0: The bald eagle visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "tiger" "-")
The bald eagle visits the lion.
Unknown
random
[@0: The bald eagle visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "lion" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
@0: The bald eagle needs the lion.[(triple1)] The bald eagle needs the tiger.[(triple2)] The lion is rough.[(triple3)] The lion is round.[(triple4)] The lion needs the tiger.[(triple5 OR ((triple4) -> rule2))] The tiger eats the lion.[(triple6)] The tiger is big.[(triple7)] The tiger is nice.[(triple8)] The tiger needs the bald eagle.[(triple9)] The tiger visits the lion.[(triple10)] @1: The lion needs the bald eagle.[(((triple4) -> rule4))] The tiger visits the bald eagle.[(((triple10) -> rule1))] @2: The tiger needs the lion.[(((((triple10) -> rule1)) -> rule3))] @3: The lion is big.[(((((((triple10) -> rule1)) -> rule3) triple6) -> rule6))]
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple5
((triple4) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple9
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple10
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
((triple4) -> (rule4 % int1))
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
((triple10) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3