Anne is kind. Anne is smart. Charlie is quiet. Charlie is not smart. Gary is furry. Gary is kind. Gary is young. Kind things are young. If something is white and not young then it is furry. Round things are quiet. Young, kind things are quiet. If something is round then it is smart. If something is smart and not furry then it is round.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is white and not young then it is furry.
((("something" "is" "white" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "+"))
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Young, kind things are quiet.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not furry then it is round.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "round" "+"))
Gary is kind.
True
1
proof
[(triple6)]
("Gary" "is" "kind" "+")
triple6
Charlie is smart.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "smart" "+")
triple4
Anne is young.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Gary is not quiet.
False
3
inv-proof
[(((triple7 triple6) -> rule4) OR ((((triple6) -> rule1) triple6) -> rule4))]
("Gary" "is" "quiet" "-")
((triple7 triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Anne is quiet.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule4))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not quiet.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule4))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is smart.[(triple2)] Charlie is not smart.[(triple4)] Charlie is quiet.[(triple3)] Gary is furry.[(triple5)] Gary is kind.[(triple6)] Gary is young.[(triple7 OR ((triple6) -> rule1))] @1: Anne is young.[(((triple1) -> rule1))] Gary is quiet.[(((triple7 triple6) -> rule4) OR ((((triple6) -> rule1) triple6) -> rule4))] @2: Anne is quiet.[(((((triple1) -> rule1) triple1) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7 triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2