Dave is blue. Dave is furry. Dave is green. Dave is not kind. Dave is red. Dave is rough. Dave is white. Erin is not blue. Erin is furry. Erin is kind. Gary is furry. Gary is green. Gary is not kind. Gary is red. Gary is rough. Gary is white. If Gary is furry then Gary is rough. If something is blue and not furry then it is not white. Kind, blue things are red. If something is furry then it is red. If something is red and not blue then it is not rough. All blue, red things are green.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is furry then Gary is rough.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
If something is blue and not furry then it is not white.
((("something" "is" "blue" "+") ("something" "is" "furry" "~")) -> ("something" "is" "white" "-"))
Kind, blue things are red.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is red and not blue then it is not rough.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "-"))
All blue, red things are green.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Dave is white.
True
1
proof
[(triple7)]
("Dave" "is" "white" "+")
triple7
Gary is not white.
False
1
inv-proof
[(triple16)]
("Gary" "is" "white" "-")
triple16
Erin is red.
True
2
proof
[(((triple9) -> rule4))]
("Erin" "is" "red" "+")
((triple9) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple9) -> rule4))]
("Erin" "is" "red" "-")
((triple9) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not rough.
True
4
proof
[(((((triple9) -> rule4) triple8) -> rule5))]
("Erin" "is" "rough" "-")
((((triple9) -> (rule4 % int2)) triple8) -> (rule5 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is rough.
False
4
inv-proof
[(((((triple9) -> rule4) triple8) -> rule5))]
("Erin" "is" "rough" "+")
((((triple9) -> (rule4 % int2)) triple8) -> (rule5 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3 OR ((triple1 triple5) -> rule6) OR ((triple1 ((triple2) -> rule4)) -> rule6))] Dave is not kind.[(triple4)] Dave is red.[(triple5 OR ((triple2) -> rule4))] Dave is rough.[(triple6)] Dave is white.[(triple7)] Erin is furry.[(triple9)] Erin is kind.[(triple10)] Erin is not blue.[(triple8)] Gary is furry.[(triple11)] Gary is green.[(triple12)] Gary is not kind.[(triple13)] Gary is red.[(triple14 OR ((triple11) -> rule4))] Gary is rough.[(triple15 OR ((triple11) -> rule1))] Gary is white.[(triple16)] @1: Erin is red.[(((triple9) -> rule4))] @2: Erin is not rough.[(((((triple9) -> rule4) triple8) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple1 triple5) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple1 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not kind.
("Dave" "is" "kind" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple2) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is not blue.
("Erin" "is" "blue" "-")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple11
Gary is green.
("Gary" "is" "green" "+")
triple12
Gary is not kind.
("Gary" "is" "kind" "-")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple11) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple15
((triple11) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple16
Erin is red.
("Erin" "is" "red" "+")
((triple9) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple9) -> (rule4 % int2)) triple8) -> (rule5 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2