Gary is quiet. Round things are blue. If something is quiet and blue then it is white. Green, white things are furry. If something is quiet then it is blue. If something is kind and white then it is quiet. Quiet, blue things are round. If Gary is round and Gary is green then Gary is furry. If something is kind and furry then it is white.
Gary is quiet.
("Gary" "is" "quiet" "+")
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is quiet and blue then it is white.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Green, white things are furry.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is kind and white then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Quiet, blue things are round.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Gary is round and Gary is green then Gary is furry.
((("Gary" "is" "round" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "furry" "+"))
If something is kind and furry then it is white.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Gary is quiet.
True
1
proof
[(triple1)]
("Gary" "is" "quiet" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple1)]
("Gary" "is" "quiet" "-")
triple1
Gary is blue.
True
2
proof
[(((triple1) -> rule4))]
("Gary" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("Gary" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Gary" "is" "round" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not white.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("Gary" "is" "white" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Gary is quiet.[(triple1)] @1: Gary is blue.[(((triple1) -> rule4))] @2: Gary is round.[(((triple1 ((triple1) -> rule4)) -> rule6))] Gary is white.[(((triple1 ((triple1) -> rule4)) -> rule2))]
Gary is quiet.
("Gary" "is" "quiet" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2