Erin is not cold. Erin is quiet. Gary is not furry. If someone is red then they are blue. All quiet people are blue. If someone is blue and round then they are cold. If someone is quiet and red then they are kind. Blue people are kind. If Gary is quiet then Gary is kind. If Gary is furry and Gary is red then Gary is blue. If someone is quiet and kind then they are not red.
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and round then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and red then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Gary is quiet then Gary is kind.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "kind" "+"))
If Gary is furry and Gary is red then Gary is blue.
((("Gary" "is" "furry" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "blue" "+"))
If someone is quiet and kind then they are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
Erin is not cold.
True
1
proof
[(triple1)]
("Erin" "is" "cold" "-")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple2)]
("Erin" "is" "quiet" "-")
triple2
Erin is blue.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("Erin" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not red.
True
5
proof
[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule8))]
("Erin" "is" "red" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule8))]
("Erin" "is" "red" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Erin is not cold.[(triple1)] Erin is quiet.[(triple2)] Gary is not furry.[(triple3)] @1: Erin is blue.[(((triple2) -> rule2))] @2: Erin is kind.[(((((triple2) -> rule2)) -> rule5))] @3: Erin is not red.[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule8))]
Erin is not cold.
("Erin" "is" "cold" "-")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is not furry.
("Gary" "is" "furry" "-")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not red.
("Erin" "is" "red" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3