Bob is white. Charlie is cold. Dave is smart. Fiona is not big. If something is nice and not smart then it is not white.
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
If something is nice and not smart then it is not white.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "white" "-"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is white.[(triple1)] Charlie is cold.[(triple2)] Dave is smart.[(triple3)] Fiona is not big.[(triple4)]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is not big.
("Fiona" "is" "big" "-")
triple4