Charlie is cold. Dave is white. Erin is quiet. Gary is green. If Dave is round and Dave is cold then Dave is kind. Cold people are kind. If someone is cold and white then they are kind. If someone is green then they are cold. Kind, cold people are furry. If Erin is furry and Erin is round then Erin is green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
If Dave is round and Dave is cold then Dave is kind.
((("Dave" "is" "round" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "kind" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and white then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Kind, cold people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If Erin is furry and Erin is round then Erin is green.
((("Erin" "is" "furry" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "green" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Gary is cold.
True
2
proof
[(((triple4) -> rule4))]
("Gary" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple4) -> rule4))]
("Gary" "is" "cold" "-")
((triple4) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is furry.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Dave" "is" "kind" "+")
Erin is not furry.
Unknown
inv-rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is cold.[(triple1)] Dave is white.[(triple2)] Erin is quiet.[(triple3)] Gary is green.[(triple4)] @1: Charlie is kind.[(((triple1) -> rule2))] Gary is cold.[(((triple4) -> rule4))] @2: Charlie is furry.[(((((triple1) -> rule2) triple1) -> rule5))] Gary is kind.[(((((triple4) -> rule4)) -> rule2))] @3: Gary is furry.[(((((((triple4) -> rule4)) -> rule2) ((triple4) -> rule4)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2)) ((triple4) -> (rule4 % int3))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3