The cow is big. The cow is not blue. The cow is green. The cow is nice. The cow is red. If something is green and nice then it is red. If something is blue then it is not red.
The cow is big.
("cow" "is" "big" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
If something is green and nice then it is red.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is blue then it is not red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "-"))
The cow is green.
True
1
proof
[(triple3)]
("cow" "is" "green" "+")
triple3
The cow is not nice.
False
1
inv-proof
[(triple4)]
("cow" "is" "nice" "-")
triple4
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "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 big.[(triple1)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is not blue.[(triple2)] The cow is red.[(triple5 OR ((triple3 triple4) -> rule1))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is not blue.
("cow" "is" "blue" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple5
((triple3 triple4) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1