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