The bear needs the lion. The lion does not eat the bear. The lion is blue. The lion is kind. The lion is rough. The lion needs the bear. The lion visits the bear. If someone is rough then they do not visit the lion.
The bear needs the lion.
("bear" "needs" "lion" "+")
The lion does not eat the bear.
("lion" "eats" "bear" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone is rough then they do not visit the lion.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "lion" "-"))
The lion is rough.
True
1
proof
[(triple5)]
("lion" "is" "rough" "+")
triple5
The bear does not need the lion.
False
1
inv-proof
[(triple1)]
("bear" "needs" "lion" "-")
triple1
The lion does not visit the lion.
True
2
proof
[(((triple5) -> rule1))]
("lion" "visits" "lion" "-")
((triple5) -> (rule1 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion visits the lion.
False
2
inv-proof
[(((triple5) -> rule1))]
("lion" "visits" "lion" "+")
((triple5) -> (rule1 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The bear eats the lion.
Unknown
random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "+")
@0: The bear needs the lion.[(triple1)] The lion does not eat the bear.[(triple2)] The lion is blue.[(triple3)] The lion is kind.[(triple4)] The lion is rough.[(triple5)] The lion needs the bear.[(triple6)] The lion visits the bear.[(triple7)] @1: The lion does not visit the lion.[(((triple5) -> rule1))]
The bear needs the lion.
("bear" "needs" "lion" "+")
triple1
The lion does not eat the bear.
("lion" "eats" "bear" "-")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion needs the bear.
("lion" "needs" "bear" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The lion does not visit the lion.
("lion" "visits" "lion" "-")
((triple5) -> (rule1 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1