The cow is not cold. The cow is green. The cow is not kind. The cow is red. The cow is young. If someone is red then they are green. If someone is green and kind then they are red.
The cow is not cold.
("cow" "is" "cold" "-")
The cow is green.
("cow" "is" "green" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is green and kind then they are red.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
The cow is green.
True
1
proof
[(triple2 OR ((triple4) -> rule1))]
("cow" "is" "green" "+")
triple2
((triple4) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule1))]
("cow" "is" "green" "-")
triple2
((triple4) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is green.[(triple2 OR ((triple4) -> rule1))] The cow is not cold.[(triple1)] The cow is not kind.[(triple3)] The cow is red.[(triple4)] The cow is young.[(triple5)]
The cow is green.
("cow" "is" "green" "+")
triple2
((triple4) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not cold.
("cow" "is" "cold" "-")
triple1
The cow is not kind.
("cow" "is" "kind" "-")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5