Charlie is kind. If Charlie is quiet then Charlie is furry. If something is furry and kind then it is smart. All quiet, furry things are young. If something is smart and young then it is red. If something is smart then it is white. All kind things are furry.
Charlie is kind.
("Charlie" "is" "kind" "+")
If Charlie is quiet then Charlie is furry.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
If something is furry and kind then it is smart.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All quiet, furry things are young.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is smart and young then it is red.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Charlie is furry.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule2))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not smart.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule2))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
True
5
proof
[(((((((triple1) -> rule6) triple1) -> rule2)) -> rule5))]
("Charlie" "is" "white" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not white.
False
5
inv-proof
[(((((((triple1) -> rule6) triple1) -> rule2)) -> rule5))]
("Charlie" "is" "white" "-")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is kind.[(triple1)] @1: Charlie is furry.[(((triple1) -> rule6))] @2: Charlie is smart.[(((((triple1) -> rule6) triple1) -> rule2))] @3: Charlie is white.[(((((((triple1) -> rule6) triple1) -> rule2)) -> rule5))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3