The bear sees the tiger. The lion visits the tiger. The tiger likes the bear. If someone visits the tiger then they are round. If someone sees the lion then the lion is cold. If someone visits the tiger then they visit the lion. If someone likes the bear then they visit the tiger. Big people are nice. If someone sees the lion and they see the tiger then they are round. If someone sees the bear then they are big. If the tiger likes the lion then the tiger likes the bear.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
If someone visits the tiger then they are round.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "round" "+"))
If someone sees the lion then the lion is cold.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone visits the tiger then they visit the lion.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the bear then they visit the tiger.
((("someone" "likes" "bear" "+")) -> ("someone" "visits" "tiger" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the lion and they see the tiger then they are round.
((("someone" "sees" "lion" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "is" "round" "+"))
If someone sees the bear then they are big.
((("someone" "sees" "bear" "+")) -> ("someone" "is" "big" "+"))
If the tiger likes the lion then the tiger likes the bear.
((("tiger" "likes" "lion" "+")) -> ("tiger" "likes" "bear" "+"))
The tiger likes the bear.
True
1
proof
[(triple3)]
("tiger" "likes" "bear" "+")
triple3
The lion does not visit the tiger.
False
1
inv-proof
[(triple2)]
("lion" "visits" "tiger" "-")
triple2
The tiger visits the tiger.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "visits" "tiger" "+")
((triple3) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "is" "round" "-")
((triple2) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger visits the lion.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("tiger" "visits" "lion" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is not round.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("tiger" "is" "round" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "big" "-")
The bear visits the lion.
Unknown
rconc
[@2: The bear visits the lion.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("bear" "visits" "lion" "+")
The tiger is not nice.
Unknown
inv-rconc
[@2: The tiger is nice.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("tiger" "is" "nice" "-")
The tiger visits the bear.
Unknown
random
[@0: The tiger visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bear" "+")
The tiger does not see the lion.
Unknown
inv-random
[@0: The tiger sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "lion" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
@0: The bear sees the tiger.[(triple1)] The lion visits the tiger.[(triple2)] The tiger likes the bear.[(triple3)] @1: The lion is round.[(((triple2) -> rule1))] The lion visits the lion.[(((triple2) -> rule3))] The tiger visits the tiger.[(((triple3) -> rule4))] @2: The tiger is round.[(((((triple3) -> rule4)) -> rule1))] The tiger visits the lion.[(((((triple3) -> rule4)) -> rule3))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
((triple2) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple2) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple3) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2