Charlie is not quiet. Gary is round. Smart people are round. Green people are blue. If someone is green and blue then they are cold. If Gary is round then Gary is blue. If someone is blue then they are quiet. If Charlie is green and Charlie is not blue then Charlie is quiet.
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Gary is round.
("Gary" "is" "round" "+")
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is green and blue then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If Gary is round then Gary is blue.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "blue" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is green and Charlie is not blue then Charlie is quiet.
((("Charlie" "is" "green" "+") ("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "quiet" "+"))
Gary is round.
True
1
proof
[(triple2)]
("Gary" "is" "round" "+")
triple2
Charlie is quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Gary is blue.
True
2
proof
[(((triple2) -> rule4))]
("Gary" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Gary" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Gary" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Gary" "is" "quiet" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is not quiet.[(triple1)] Gary is round.[(triple2)] @1: Gary is blue.[(((triple2) -> rule4))] @2: Gary is quiet.[(((((triple2) -> rule4)) -> rule5))]
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2