Bob is furry. Bob is white. Bob is young. Charlie is not furry. Charlie is kind. Charlie is smart. Charlie is white. Furry, cold things are nice. If something is nice and not smart then it is cold. Furry things are young. Kind, nice things are young. Smart, kind things are young. All nice, cold things are not kind. All smart, young things are kind. If something is smart and not nice then it is kind.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Furry, cold things are nice.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not smart then it is cold.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "cold" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Kind, nice things are young.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Smart, kind things are young.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All nice, cold things are not kind.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "-"))
All smart, young things are kind.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is smart and not nice then it is kind.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "kind" "+"))
Charlie is white.
True
1
proof
[(triple7)]
("Charlie" "is" "white" "+")
triple7
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Charlie is young.
True
3
proof
[(((triple6 triple5) -> rule5))]
("Charlie" "is" "young" "+")
((triple6 triple5) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
3
inv-proof
[(((triple6 triple5) -> rule5))]
("Charlie" "is" "young" "-")
((triple6 triple5) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is furry.[(triple1)] Bob is white.[(triple2)] Bob is young.[(triple3 OR ((triple1) -> rule3))] Charlie is kind.[(triple5)] Charlie is not furry.[(triple4)] Charlie is smart.[(triple6)] Charlie is white.[(triple7)] @1: Charlie is young.[(((triple6 triple5) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
((triple6 triple5) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1