Charlie is not blue. Charlie is cold. Charlie is not smart. Charlie is not white. Dave is big. Dave is blue. Dave is not cold. If something is big and not cold then it is not white.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
If something is big and not cold then it is not white.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "-"))
Dave is big.
True
1
proof
[(triple5)]
("Dave" "is" "big" "+")
triple5
Dave is not big.
False
1
inv-proof
[(triple5)]
("Dave" "is" "big" "-")
triple5
Dave is not white.
True
3
proof
[(((triple5 triple7) -> rule1))]
("Dave" "is" "white" "-")
((triple5 triple7) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is white.
False
3
inv-proof
[(((triple5 triple7) -> rule1))]
("Dave" "is" "white" "+")
((triple5 triple7) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Charlie is cold.[(triple2)] Charlie is not blue.[(triple1)] Charlie is not smart.[(triple3)] Charlie is not white.[(triple4)] Dave is big.[(triple5)] Dave is blue.[(triple6)] Dave is not cold.[(triple7)] @1: Dave is not white.[(((triple5 triple7) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is not cold.
("Dave" "is" "cold" "-")
triple7
Dave is not white.
("Dave" "is" "white" "-")
((triple5 triple7) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1