The lion is cold. The lion is green. The lion is nice. The lion is rough. The lion is young. Young, rough things are cold. If something is rough and nice then it is cold.
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
Young, rough things are cold.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is rough and nice then it is cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
The lion is rough.
True
1
proof
[(triple4)]
("lion" "is" "rough" "+")
triple4
The lion is not cold.
False
1
inv-proof
[(triple1 OR ((triple4 triple3) -> rule2) OR ((triple5 triple4) -> rule1))]
("lion" "is" "cold" "-")
triple1
((triple4 triple3) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple5 triple4) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion is cold.[(triple1 OR ((triple4 triple3) -> rule2) OR ((triple5 triple4) -> rule1))] The lion is green.[(triple2)] The lion is nice.[(triple3)] The lion is rough.[(triple4)] The lion is young.[(triple5)]
The lion is cold.
("lion" "is" "cold" "+")
triple1
((triple4 triple3) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple5 triple4) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5