The lion is blue. The lion is cold. The lion is kind. The lion is red. The lion is young. If the lion is red then the lion is kind. All cold things are kind.
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
If the lion is red then the lion is kind.
((("lion" "is" "red" "+")) -> ("lion" "is" "kind" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
The lion is cold.
True
1
proof
[(triple2)]
("lion" "is" "cold" "+")
triple2
The lion is not kind.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule2) OR ((triple4) -> rule1))]
("lion" "is" "kind" "-")
triple3
((triple2) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
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 needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is blue.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple3 OR ((triple2) -> rule2) OR ((triple4) -> rule1))] The lion is red.[(triple4)] The lion is young.[(triple5)]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple2) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5