Anne is furry. Dave is kind. Erin is cold. Gary is quiet. If Erin is cold then Erin is furry. Quiet people are kind. If someone is quiet and kind then they are white.
Anne is furry.
("Anne" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Erin is cold then Erin is furry.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and kind then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Gary is kind.
True
2
proof
[(((triple4) -> rule2))]
("Gary" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is white.
True
4
proof
[(((triple4 ((triple4) -> rule2)) -> rule3))]
("Gary" "is" "white" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not white.
False
4
inv-proof
[(((triple4 ((triple4) -> rule2)) -> rule3))]
("Gary" "is" "white" "-")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Dave is kind.[(triple2)] Erin is cold.[(triple3)] Gary is quiet.[(triple4)] @1: Erin is furry.[(((triple3) -> rule1))] Gary is kind.[(((triple4) -> rule2))] @2: Gary is white.[(((triple4 ((triple4) -> rule2)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2