Dave is blue. Erin is blue. Gary is big. Harry is cold. Green, round things are blue. Big, green things are not blue. If Gary is round and Gary is blue then Gary is green. Blue things are furry. If Dave is cold and Dave is not round then Dave is blue. If Gary is furry and Gary is big then Gary is blue. If something is furry then it is nice. If something is nice then it is not green.
Dave is blue.
("Dave" "is" "blue" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Green, round things are blue.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Big, green things are not blue.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "-"))
If Gary is round and Gary is blue then Gary is green.
((("Gary" "is" "round" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "green" "+"))
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If Dave is cold and Dave is not round then Dave is blue.
((("Dave" "is" "cold" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "blue" "+"))
If Gary is furry and Gary is big then Gary is blue.
((("Gary" "is" "furry" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "blue" "+"))
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is not green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
Erin is blue.
True
1
proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "-")
triple4
Erin is furry.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("Dave" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("Erin" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@3: Gary is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is nice.
Unknown
rconc
[@3: Harry is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "+")
Gary is not nice.
Unknown
inv-rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is blue.[(triple1)] Erin is blue.[(triple2)] Gary is big.[(triple3)] Harry is cold.[(triple4)] @1: Dave is furry.[(((triple1) -> rule4))] Erin is furry.[(((triple2) -> rule4))] @2: Dave is nice.[(((((triple1) -> rule4)) -> rule7))] Erin is nice.[(((((triple2) -> rule4)) -> rule7))] @3: Dave is not green.[(((((((triple1) -> rule4)) -> rule7)) -> rule8))] Erin is not green.[(((((((triple2) -> rule4)) -> rule7)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Dave is not green.
("Dave" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Erin is not green.
("Erin" "is" "green" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3