Charlie is cold. Dave is round. Gary is kind. If something is cold then it is nice. If something is nice and round then it is furry. If something is round and not smart then it is not furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is nice and round then it is furry.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is round and not smart then it is not furry.
((("something" "is" "round" "+") ("something" "is" "smart" "~")) -> ("something" "is" "furry" "-"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
Charlie is nice.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Dave is furry.
Unknown
rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is cold.[(triple1)] Dave is round.[(triple2)] Gary is kind.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1