The lion is cold. If the lion is rough then the lion is not kind. If something is rough then it is nice. All kind things are nice. If something is nice then it is young. If the lion is cold then the lion is not rough. If something is young and nice then it is kind.
The lion is cold.
("lion" "is" "cold" "+")
If the lion is rough then the lion is not kind.
((("lion" "is" "rough" "+")) -> ("lion" "is" "kind" "-"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If the lion is cold then the lion is not rough.
((("lion" "is" "cold" "+")) -> ("lion" "is" "rough" "-"))
If something is young and nice then it is kind.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
The lion is cold.
True
1
proof
[(triple1)]
("lion" "is" "cold" "+")
triple1
The lion is not cold.
False
1
inv-proof
[(triple1)]
("lion" "is" "cold" "-")
triple1
The lion is not rough.
True
2
proof
[(((triple1) -> rule5))]
("lion" "is" "rough" "-")
((triple1) -> (rule5 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion is rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("lion" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion is not kind.
Unknown
inv-rconc
[@2: The lion is kind.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "is" "kind" "-")
The lion is nice.
Unknown
rconc
[@3: The lion is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule2 <- FAIL)]]
("lion" "is" "nice" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion is cold.[(triple1)] @1: The lion is not rough.[(((triple1) -> rule5))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is not rough.
("lion" "is" "rough" "-")
((triple1) -> (rule5 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1