Bob is furry. Bob is nice. Dave is cold. Dave is furry. Dave is rough. Dave is smart. Dave is white. Harry is furry. Harry is green. Harry is nice. If Dave is white then Dave is furry. If someone is green then they are cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Dave is white then Dave is furry.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "furry" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Harry is furry.
True
1
proof
[(triple8)]
("Harry" "is" "furry" "+")
triple8
Dave is not furry.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule1))]
("Dave" "is" "furry" "-")
triple4
((triple7) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is furry.[(triple1)] Bob is nice.[(triple2)] Dave is cold.[(triple3)] Dave is furry.[(triple4 OR ((triple7) -> rule1))] Dave is rough.[(triple5)] Dave is smart.[(triple6)] Dave is white.[(triple7)] Harry is furry.[(triple8)] Harry is green.[(triple9)] Harry is nice.[(triple10)] @1: Harry is cold.[(((triple9) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple7) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
((triple9) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1