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