Bob is nice. Charlie is nice. Dave is furry. All quiet, white things are furry. All cold things are red. Nice things are kind. All kind, red things are furry. If Charlie is quiet then Charlie is kind. All red things are cold.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
All quiet, white things are furry.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All kind, red things are furry.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Charlie is quiet then Charlie is kind.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "kind" "+"))
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is red.
Unknown
rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is nice.[(triple1)] Charlie is nice.[(triple2)] Dave is furry.[(triple3)] @1: Bob is kind.[(((triple1) -> rule3))] Charlie is kind.[(((triple2) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1