Gary is blue. Gary is kind. Gary is quiet. Gary is rough. Gary is round. Gary is white. Harry is blue. Blue things are kind. If something is rough and round then it is quiet. If Harry is furry then Harry is round. If something is white and furry then it is quiet. Kind, quiet things are round. All white, rough things are kind.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is rough and round then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If Harry is furry then Harry is round.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "round" "+"))
If something is white and furry then it is quiet.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Kind, quiet things are round.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All white, rough things are kind.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Gary is white.
True
1
proof
[(triple6)]
("Gary" "is" "white" "+")
triple6
Gary is not kind.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule1) OR ((triple6 triple4) -> rule6))]
("Gary" "is" "kind" "-")
triple2
((triple1) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple6 triple4) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Gary is blue.[(triple1)] Gary is kind.[(triple2 OR ((triple1) -> rule1) OR ((triple6 triple4) -> rule6))] Gary is quiet.[(triple3 OR ((triple4 triple5) -> rule2))] Gary is rough.[(triple4)] Gary is round.[(triple5 OR ((triple2 triple3) -> rule5) OR ((((triple1) -> rule1) triple3) -> rule5) OR ((((triple6 triple4) -> rule6) triple3) -> rule5))] Gary is white.[(triple6)] Harry is blue.[(triple7)] @1: Harry is kind.[(((triple7) -> rule1))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple6 triple4) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
((triple4 triple5) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
((triple2 triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple6 triple4) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1