The cow is big. The cow is blue. The cow is not nice. The cow is round. The cow is young. If something is round and not young then it is big. If the cow is not nice and the cow is not big then the cow is blue.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
If something is round and not young then it is big.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
If the cow is not nice and the cow is not big then the cow is blue.
((("cow" "is" "nice" "~") ("cow" "is" "big" "~")) -> ("cow" "is" "blue" "+"))
The cow is young.
True
1
proof
[(triple5)]
("cow" "is" "young" "+")
triple5
The cow is not blue.
False
1
inv-proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is big.[(triple1)] The cow is blue.[(triple2)] The cow is not nice.[(triple3)] The cow is round.[(triple4)] The cow is young.[(triple5)]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is not nice.
("cow" "is" "nice" "-")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5