Anne is cold. Anne is quiet. Anne is not rough. Anne is not smart. Anne is not white. Anne is young. Charlie is cold. Charlie is not furry. Charlie is quiet. Charlie is white. Gary is cold. Gary is furry. Gary is quiet. Gary is rough. Gary is young. If something is rough and young then it is not smart. If Charlie is not white then Charlie is not cold. If something is smart then it is quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is not white.
("Anne" "is" "white" "-")
Anne is young.
("Anne" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is rough and young then it is not smart.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "-"))
If Charlie is not white then Charlie is not cold.
((("Charlie" "is" "white" "~")) -> ("Charlie" "is" "cold" "-"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Charlie is white.
True
1
proof
[(triple10)]
("Charlie" "is" "white" "+")
triple10
Anne is not young.
False
1
inv-proof
[(triple6)]
("Anne" "is" "young" "-")
triple6
Gary is not smart.
True
3
proof
[(((triple14 triple15) -> rule1))]
("Gary" "is" "smart" "-")
((triple14 triple15) -> (rule1 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is smart.
False
3
inv-proof
[(((triple14 triple15) -> rule1))]
("Gary" "is" "smart" "+")
((triple14 triple15) -> (rule1 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Anne is cold.[(triple1)] Anne is not rough.[(triple3)] Anne is not smart.[(triple4)] Anne is not white.[(triple5)] Anne is quiet.[(triple2)] Anne is young.[(triple6)] Charlie is cold.[(triple7)] Charlie is not furry.[(triple8)] Charlie is quiet.[(triple9)] Charlie is white.[(triple10)] Gary is cold.[(triple11)] Gary is furry.[(triple12)] Gary is quiet.[(triple13)] Gary is rough.[(triple14)] Gary is young.[(triple15)] @1: Gary is not smart.[(((triple14 triple15) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple3
Anne is not smart.
("Anne" "is" "smart" "-")
triple4
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
Gary is not smart.
("Gary" "is" "smart" "-")
((triple14 triple15) -> (rule1 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1