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