Anne is white. Charlie is blue. Gary is rough. If someone is quiet and rough then they are furry. All blue, furry people are white. All rough, blue people are furry. If someone is rough then they are quiet. If someone is quiet and kind then they are blue. If someone is kind and white then they are furry.
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is quiet and rough then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All blue, furry people are white.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All rough, blue people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and kind then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and white then they are furry.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule1))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
False
4
inv-proof
[(((((triple3) -> rule4) triple3) -> rule1))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is white.[(triple1)] Charlie is blue.[(triple2)] Gary is rough.[(triple3)] @1: Gary is quiet.[(((triple3) -> rule4))] @2: Gary is furry.[(((((triple3) -> rule4) triple3) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2