The lion is cold. If the lion is rough then the lion is nice. If the lion is nice then the lion is blue. If the lion is not rough then the lion is young. If the lion is cold then the lion is young. If the lion is young and the lion is not nice then the lion is not cold. All cold people are young.
The lion is cold.
("lion" "is" "cold" "+")
If the lion is rough then the lion is nice.
((("lion" "is" "rough" "+")) -> ("lion" "is" "nice" "+"))
If the lion is nice then the lion is blue.
((("lion" "is" "nice" "+")) -> ("lion" "is" "blue" "+"))
If the lion is not rough then the lion is young.
((("lion" "is" "rough" "~")) -> ("lion" "is" "young" "+"))
If the lion is cold then the lion is young.
((("lion" "is" "cold" "+")) -> ("lion" "is" "young" "+"))
If the lion is young and the lion is not nice then the lion is not cold.
((("lion" "is" "young" "+") ("lion" "is" "nice" "~")) -> ("lion" "is" "cold" "-"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
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 young.
True
2
proof
[(((triple1) -> rule4) OR ((triple1) -> rule6))]
("lion" "is" "young" "+")
((triple1) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple1) -> rule6))]
("lion" "is" "young" "-")
((triple1) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "nice" "-")
The lion is blue.
Unknown
rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("lion" "is" "blue" "+")
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 eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion is cold.[(triple1)] @1: The lion is young.[(((triple1) -> rule4) OR ((triple1) -> rule6))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
((triple1) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1