The bear visits the tiger. The lion is not cold. The tiger visits the lion. If something sees the bear then the bear is nice. If something is kind and not round then it sees the tiger. If something sees the tiger then the tiger chases the lion. If something visits the lion then the lion sees the bear. If something chases the lion and it does not see the bear then the lion is cold. If something is kind and cold then it does not see the lion.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something sees the bear then the bear is nice.
((("something" "sees" "bear" "+")) -> ("bear" "is" "nice" "+"))
If something is kind and not round then it sees the tiger.
((("something" "is" "kind" "+") ("something" "is" "round" "~")) -> ("something" "sees" "tiger" "+"))
If something sees the tiger then the tiger chases the lion.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If something visits the lion then the lion sees the bear.
((("something" "visits" "lion" "+")) -> ("lion" "sees" "bear" "+"))
If something chases the lion and it does not see the bear then the lion is cold.
((("something" "chases" "lion" "+") ("something" "sees" "bear" "~")) -> ("lion" "is" "cold" "+"))
If something is kind and cold then it does not see the lion.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "sees" "lion" "-"))
The tiger visits the lion.
True
1
proof
[(triple3)]
("tiger" "visits" "lion" "+")
triple3
The lion is cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "+")
triple2
The lion sees the bear.
True
2
proof
[(((triple3) -> rule4))]
("lion" "sees" "bear" "+")
((triple3) -> (rule4 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion does not see the bear.
False
2
inv-proof
[(((triple3) -> rule4))]
("lion" "sees" "bear" "-")
((triple3) -> (rule4 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The bear is nice.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("bear" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The bear is not nice.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("bear" "is" "nice" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "tiger" "-")
The lion sees the tiger.
Unknown
rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The bear chases the lion.
Unknown
random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "+")
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The tiger sees the bear.
Unknown
random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "+")
@0: The bear visits the tiger.[(triple1)] The lion is not cold.[(triple2)] The tiger visits the lion.[(triple3)] @1: The lion sees the bear.[(((triple3) -> rule4))] @2: The bear is nice.[(((((triple3) -> rule4)) -> rule1))]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The lion is not cold.
("lion" "is" "cold" "-")
triple2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple3
The lion sees the bear.
("lion" "sees" "bear" "+")
((triple3) -> (rule4 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2