Dave is quiet. Erin is quiet. Gary is young. Harry is quiet. If Harry is furry and Harry is blue then Harry is big. All blue things are quiet. White, big things are round. All blue, round things are white. If Harry is quiet then Harry is white. If Gary is big then Gary is white.
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is furry and Harry is blue then Harry is big.
((("Harry" "is" "furry" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "big" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
White, big things are round.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All blue, round things are white.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Harry is quiet then Harry is white.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "white" "+"))
If Gary is big then Gary is white.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "white" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Harry is not quiet.
False
1
inv-proof
[(triple4)]
("Harry" "is" "quiet" "-")
triple4
Harry is white.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "white" "+")
((triple4) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "white" "-")
((triple4) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "white" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is quiet.[(triple1)] Erin is quiet.[(triple2)] Gary is young.[(triple3)] Harry is quiet.[(triple4)] @1: Harry is white.[(((triple4) -> rule5))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1