Charlie is big. Charlie is cold. Dave is big. Dave is cold. Dave is nice. Gary is big. Gary is not blue. Gary is cold. Gary is white. Harry is cold. If Gary is cold then Gary is rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Gary is cold then Gary is rough.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "rough" "+"))
Gary is white.
True
1
proof
[(triple9)]
("Gary" "is" "white" "+")
triple9
Gary is not white.
False
1
inv-proof
[(triple9)]
("Gary" "is" "white" "-")
triple9
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Dave is big.[(triple3)] Dave is cold.[(triple4)] Dave is nice.[(triple5)] Gary is big.[(triple6)] Gary is cold.[(triple8)] Gary is not blue.[(triple7)] Gary is white.[(triple9)] Harry is cold.[(triple10)] @1: Gary is rough.[(((triple8) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is not blue.
("Gary" "is" "blue" "-")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
((triple8) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1