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