Bob is cold. Bob is kind. Bob is not quiet. Bob is rough. Bob is not smart. Charlie is cold. Charlie is not kind. Charlie is not quiet. Charlie is red. Charlie is rough. Charlie is round. Charlie is smart. Gary is cold. Gary is kind. Gary is quiet. Gary is smart. If Charlie is quiet then Charlie is not red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Charlie is quiet then Charlie is not red.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "red" "-"))
Bob is not smart.
True
1
proof
[(triple5)]
("Bob" "is" "smart" "-")
triple5
Charlie is not round.
False
1
inv-proof
[(triple11)]
("Charlie" "is" "round" "-")
triple11
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Bob is not quiet.[(triple3)] Bob is not smart.[(triple5)] Bob is rough.[(triple4)] Charlie is cold.[(triple6)] Charlie is not kind.[(triple7)] Charlie is not quiet.[(triple8)] Charlie is red.[(triple9)] Charlie is rough.[(triple10)] Charlie is round.[(triple11)] Charlie is smart.[(triple12)] Gary is cold.[(triple13)] Gary is kind.[(triple14)] Gary is quiet.[(triple15)] Gary is smart.[(triple16)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple7
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
triple11
Charlie is smart.
("Charlie" "is" "smart" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple16