Bob is blue. Bob is red. Bob is white. Dave is quiet. Dave is white. Fiona is red. Gary is quiet. Furry, red things are cold. Rough, blue things are quiet. If something is cold then it is red. Quiet, white things are furry. If Gary is blue and Gary is furry then Gary is white. All cold, furry things are rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Furry, red things are cold.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Rough, blue things are quiet.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Quiet, white things are furry.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Gary is blue and Gary is furry then Gary is white.
((("Gary" "is" "blue" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "white" "+"))
All cold, furry things are rough.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Bob is white.
True
1
proof
[(triple3)]
("Bob" "is" "white" "+")
triple3
Gary is not quiet.
False
1
inv-proof
[(triple7)]
("Gary" "is" "quiet" "-")
triple7
Dave is furry.
True
3
proof
[(((triple4 triple5) -> rule4))]
("Dave" "is" "furry" "+")
((triple4 triple5) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
3
inv-proof
[(((triple4 triple5) -> rule4))]
("Dave" "is" "furry" "-")
((triple4 triple5) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "rough" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Bob is red.[(triple2)] Bob is white.[(triple3)] Dave is quiet.[(triple4)] Dave is white.[(triple5)] Fiona is red.[(triple6)] Gary is quiet.[(triple7)] @1: Dave is furry.[(((triple4 triple5) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
((triple4 triple5) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1