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