Dave is furry. Gary is white. Harry is round. If something is furry then it is round. Round, furry things are nice. If Gary is rough then Gary is quiet. If something is round then it is white. Nice, rough things are quiet. If something is white and rough then it is nice.
Dave is furry.
("Dave" "is" "furry" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Round, furry things are nice.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Gary is rough then Gary is quiet.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "quiet" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Nice, rough things are quiet.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is white and rough then it is nice.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Gary is white.
True
1
proof
[(triple2)]
("Gary" "is" "white" "+")
triple2
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Harry is white.
True
2
proof
[(((triple3) -> rule4))]
("Harry" "is" "white" "+")
((triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule4))]
("Harry" "is" "white" "-")
((triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Dave" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Dave" "is" "nice" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Dave is furry.[(triple1)] Gary is white.[(triple2)] Harry is round.[(triple3)] @1: Dave is round.[(((triple1) -> rule1))] Harry is white.[(((triple3) -> rule4))] @2: Dave is nice.[(((((triple1) -> rule1) triple1) -> rule2))] Dave is white.[(((((triple1) -> rule1)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2