Bob is cold. Dave is blue. Erin is kind. Gary is not blue. If someone is kind then they are furry. Green people are furry. If Dave is furry then Dave is green. If Gary is round and Gary is kind then Gary is smart. If someone is smart then they are green. Cold, blue people are not green.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Dave is furry then Dave is green.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "green" "+"))
If Gary is round and Gary is kind then Gary is smart.
((("Gary" "is" "round" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Cold, blue people are not green.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "-"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is cold.[(triple1)] Dave is blue.[(triple2)] Erin is kind.[(triple3)] Gary is not blue.[(triple4)] @1: Erin is furry.[(((triple3) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Gary is not blue.
("Gary" "is" "blue" "-")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1