The lion is cold. The lion is kind. The lion is rough. If something is rough and not cold then it is kind. If something is cold then it is round.
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
If something is rough and not cold then it is kind.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "is" "kind" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
The lion is kind.
True
1
proof
[(triple2)]
("lion" "is" "kind" "+")
triple2
The lion is not kind.
False
1
inv-proof
[(triple2)]
("lion" "is" "kind" "-")
triple2
The lion is round.
True
2
proof
[(((triple1) -> rule2))]
("lion" "is" "round" "+")
((triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("lion" "is" "round" "-")
((triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion is cold.[(triple1)] The lion is kind.[(triple2)] The lion is rough.[(triple3)] @1: The lion is round.[(((triple1) -> rule2))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1