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