The cow is cold. The cow is nice. The cow is rough. All rough things are kind. If the cow is rough then the cow is nice.
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If the cow is rough then the cow is nice.
((("cow" "is" "rough" "+")) -> ("cow" "is" "nice" "+"))
The cow is rough.
True
1
proof
[(triple3)]
("cow" "is" "rough" "+")
triple3
The cow is not cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is cold.[(triple1)] The cow is nice.[(triple2 OR ((triple3) -> rule2))] The cow is rough.[(triple3)] @1: The cow is kind.[(((triple3) -> rule1))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
((triple3) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
((triple3) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1