Charlie is big. Charlie is furry. Charlie is green. Charlie is not red. Gary is big. Gary is cold. Gary is furry. Gary is not green. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is nice. Harry is red. If Harry is big and Harry is not furry then Harry is not green.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
If Harry is big and Harry is not furry then Harry is not green.
((("Harry" "is" "big" "+") ("Harry" "is" "furry" "~")) -> ("Harry" "is" "green" "-"))
Harry is furry.
True
1
proof
[(triple12)]
("Harry" "is" "furry" "+")
triple12
Gary is green.
False
1
inv-proof
[(triple8)]
("Gary" "is" "green" "+")
triple8
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is not red.[(triple4)] Gary is big.[(triple5)] Gary is cold.[(triple6)] Gary is furry.[(triple7)] Gary is not green.[(triple8)] Harry is big.[(triple9)] Harry is blue.[(triple10)] Harry is cold.[(triple11)] Harry is furry.[(triple12)] Harry is green.[(triple13)] Harry is nice.[(triple14)] Harry is red.[(triple15)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is not green.
("Gary" "is" "green" "-")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple15