Erin is cold. Gary is rough. If someone is rough and smart then they are round. If Erin is furry then Erin is rough. If Gary is smart then Gary is cold. All cold people are furry. If someone is cold and furry then they are round. If someone is quiet and smart then they are cold. If someone is smart and nice then they are cold. If someone is furry then they are rough.
Erin is cold.
("Erin" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is rough and smart then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Erin is furry then Erin is rough.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "rough" "+"))
If Gary is smart then Gary is cold.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "cold" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and furry then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet and smart then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and nice then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Erin is cold.
True
1
proof
[(triple1)]
("Erin" "is" "cold" "+")
triple1
Gary is not rough.
False
1
inv-proof
[(triple2)]
("Gary" "is" "rough" "-")
triple2
Erin is furry.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is furry.
Unknown
rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Erin is cold.[(triple1)] Gary is rough.[(triple2)] @1: Erin is furry.[(((triple1) -> rule4))] @2: Erin is rough.[(((((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule4)) -> rule8))] Erin is round.[(((triple1 ((triple1) -> rule4)) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2