Charlie is blue. Dave is blue. Dave is quiet. If Dave is blue then Dave is furry. If something is furry then it is kind. Quiet, round things are smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If Dave is blue then Dave is furry.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "furry" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Quiet, round things are smart.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Dave is furry.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Dave is blue.[(triple2)] Dave is quiet.[(triple3)] @1: Dave is furry.[(((triple2) -> rule1))] @2: Dave is kind.[(((((triple2) -> rule1)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2