The cow is blue. The cow is kind. The cow is nice. The cow is red. The cow is rough. If the cow is nice and the cow is not red then the cow is kind. If the cow is blue and the cow is nice then the cow is rough.
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
If the cow is nice and the cow is not red then the cow is kind.
((("cow" "is" "nice" "+") ("cow" "is" "red" "~")) -> ("cow" "is" "kind" "+"))
If the cow is blue and the cow is nice then the cow is rough.
((("cow" "is" "blue" "+") ("cow" "is" "nice" "+")) -> ("cow" "is" "rough" "+"))
The cow is nice.
True
1
proof
[(triple3)]
("cow" "is" "nice" "+")
triple3
The cow is not rough.
False
1
inv-proof
[(triple5 OR ((triple1 triple3) -> rule2))]
("cow" "is" "rough" "-")
triple5
((triple1 triple3) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
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 blue.[(triple1)] The cow is kind.[(triple2)] The cow is nice.[(triple3)] The cow is red.[(triple4)] The cow is rough.[(triple5 OR ((triple1 triple3) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
((triple1 triple3) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1