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