The bear visits the lion. The lion is kind. The lion visits the bear. If the lion is kind then the lion visits the bear. If someone chases the bear and they visit the bear then they chase the lion. If someone is nice and they chase the bear then the bear is young. If someone visits the lion then the lion is rough. If the lion sees the bear and the bear is nice then the bear sees the lion. If someone chases the bear then they see the bear. If someone sees the bear then the bear visits the lion. If someone is cold and they see the lion then they see the bear.
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If the lion is kind then the lion visits the bear.
((("lion" "is" "kind" "+")) -> ("lion" "visits" "bear" "+"))
If someone chases the bear and they visit the bear then they chase the lion.
((("someone" "chases" "bear" "+") ("someone" "visits" "bear" "+")) -> ("someone" "chases" "lion" "+"))
If someone is nice and they chase the bear then the bear is young.
((("someone" "is" "nice" "+") ("someone" "chases" "bear" "+")) -> ("bear" "is" "young" "+"))
If someone visits the lion then the lion is rough.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "rough" "+"))
If the lion sees the bear and the bear is nice then the bear sees the lion.
((("lion" "sees" "bear" "+") ("bear" "is" "nice" "+")) -> ("bear" "sees" "lion" "+"))
If someone chases the bear then they see the bear.
((("someone" "chases" "bear" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the bear then the bear visits the lion.
((("someone" "sees" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If someone is cold and they see the lion then they see the bear.
((("someone" "is" "cold" "+") ("someone" "sees" "lion" "+")) -> ("someone" "sees" "bear" "+"))
The bear visits the lion.
True
1
proof
[(triple1)]
("bear" "visits" "lion" "+")
triple1
The bear does not visit the lion.
False
1
inv-proof
[(triple1)]
("bear" "visits" "lion" "-")
triple1
The lion is rough.
True
2
proof
[(((triple1) -> rule4))]
("lion" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "is" "rough" "-")
((triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "bear" "-")
The bear sees the lion.
Unknown
rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
@0: The bear visits the lion.[(triple1)] The lion is kind.[(triple2)] The lion visits the bear.[(triple3 OR ((triple2) -> rule1))] @1: The lion is rough.[(((triple1) -> rule4))]
The bear visits the lion.
("bear" "visits" "lion" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion visits the bear.
("lion" "visits" "bear" "+")
triple3
((triple2) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1