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