Charlie is white. Dave is quiet. Gary is quiet. Harry is rough. If someone is rough then they are furry. If Dave is blue then Dave is round. If Harry is rough and Harry is furry then Harry is quiet.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Dave is blue then Dave is round.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "round" "+"))
If Harry is rough and Harry is furry then Harry is quiet.
((("Harry" "is" "rough" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "-")
triple2
Harry is furry.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "furry" "-")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule3))]
("Harry" "is" "quiet" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule3))]
("Harry" "is" "quiet" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Charlie is white.[(triple1)] Dave is quiet.[(triple2)] Gary is quiet.[(triple3)] Harry is rough.[(triple4)] @1: Harry is furry.[(((triple4) -> rule1))] @2: Harry is quiet.[(((triple4 ((triple4) -> rule1)) -> rule3))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2