Charlie is kind. All red, furry things are green. Kind things are furry. All nice things are red. If something is nice then it is red. Furry things are red. Red, cold things are furry. If something is cold then it is nice. All cold, kind things are young.
Charlie is kind.
("Charlie" "is" "kind" "+")
All red, furry things are green.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Red, cold things are furry.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All cold, kind things are young.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
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) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is kind.[(triple1)] @1: Charlie is furry.[(((triple1) -> rule2))] @2: Charlie is red.[(((((triple1) -> rule2)) -> rule5))] @3: Charlie is green.[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3