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