Gary is big. Gary is not blue. Gary is red. If Gary is green then Gary is furry. If Gary is big then Gary is green. If something is green and blue then it is cold. If Gary is furry and Gary is blue then Gary is round. If something is furry and not green then it is blue. All blue things are furry. If something is blue and not furry then it is not red. If something is furry and not red then it is not round.
Gary is big.
("Gary" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is red.
("Gary" "is" "red" "+")
If Gary is green then Gary is furry.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "furry" "+"))
If Gary is big then Gary is green.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "green" "+"))
If something is green and blue then it is cold.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If Gary is furry and Gary is blue then Gary is round.
((("Gary" "is" "furry" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "round" "+"))
If something is furry and not green then it is blue.
((("something" "is" "furry" "+") ("something" "is" "green" "~")) -> ("something" "is" "blue" "+"))
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is blue and not furry then it is not red.
((("something" "is" "blue" "+") ("something" "is" "furry" "~")) -> ("something" "is" "red" "-"))
If something is furry and not red then it is not round.
((("something" "is" "furry" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "-"))
Gary is big.
True
1
proof
[(triple1)]
("Gary" "is" "big" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple3)]
("Gary" "is" "red" "-")
triple3
Gary is green.
True
2
proof
[(((triple1) -> rule2))]
("Gary" "is" "green" "+")
((triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Gary" "is" "green" "-")
((triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Gary" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "+")
@0: Gary is big.[(triple1)] Gary is not blue.[(triple2)] Gary is red.[(triple3)] @1: Gary is green.[(((triple1) -> rule2))] @2: Gary is furry.[(((((triple1) -> rule2)) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is not blue.
("Gary" "is" "blue" "-")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2