Bob is rough. Dave is furry. Harry is kind. White, cold things are rough. If Dave is cold then Dave is nice. Kind things are white.
Bob is rough.
("Bob" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
White, cold things are rough.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Dave is cold then Dave is nice.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "-")
triple2
Harry is white.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "+")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "-")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is rough.[(triple1)] Dave is furry.[(triple2)] Harry is kind.[(triple3)] @1: Harry is white.[(((triple3) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1