The cow is not big. The cow is cold. The cow is not green. The cow is red. The cow is round. If something is green and not cold then it is big. If something is round then it is red. All cold, big things are round.
The cow is not big.
("cow" "is" "big" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow is not green.
("cow" "is" "green" "-")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
If something is green and not cold then it is big.
((("something" "is" "green" "+") ("something" "is" "cold" "~")) -> ("something" "is" "big" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All cold, big things are round.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
The cow is not green.
True
1
proof
[(triple3)]
("cow" "is" "green" "-")
triple3
The cow is green.
False
1
inv-proof
[(triple3)]
("cow" "is" "green" "+")
triple3
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "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 cold.[(triple2)] The cow is not big.[(triple1)] The cow is not green.[(triple3)] The cow is red.[(triple4 OR ((triple5) -> rule2))] The cow is round.[(triple5)]
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is not big.
("cow" "is" "big" "-")
triple1
The cow is not green.
("cow" "is" "green" "-")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
((triple5) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple5