Anne is not big. Erin is furry. Erin is kind. Erin is not white. Gary is big. Gary is round. Gary is not white. All rough things are big. All white things are not big. All rough, round things are big. Kind, furry things are rough. If something is white then it is cold. If something is rough then it is not cold. If Gary is big then Gary is furry. Big things are round.
Anne is not big.
("Anne" "is" "big" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not white.
("Erin" "is" "white" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not white.
("Gary" "is" "white" "-")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All white things are not big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "-"))
All rough, round things are big.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Kind, furry things are rough.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is not cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
If Gary is big then Gary is furry.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "furry" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Gary is round.
True
1
proof
[(triple6 OR ((triple5) -> rule8))]
("Gary" "is" "round" "+")
triple6
((triple5) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Erin is rough.
True
3
proof
[(((triple3 triple2) -> rule4))]
("Erin" "is" "rough" "+")
((triple3 triple2) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple5) -> rule7))]
("Gary" "is" "furry" "-")
((triple5) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is not cold.
True
4
proof
[(((((triple3 triple2) -> rule4)) -> rule6))]
("Erin" "is" "cold" "-")
((((triple3 triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
False
4
inv-proof
[(((((triple3 triple2) -> rule4)) -> rule6))]
("Erin" "is" "cold" "+")
((((triple3 triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
True
5
proof
[(((((((triple3 triple2) -> rule4)) -> rule1)) -> rule8))]
("Erin" "is" "round" "+")
((((((triple3 triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not round.
False
5
inv-proof
[(((((((triple3 triple2) -> rule4)) -> rule1)) -> rule8))]
("Erin" "is" "round" "-")
((((((triple3 triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "cold" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is not big.[(triple1)] Erin is furry.[(triple2)] Erin is kind.[(triple3)] Erin is not white.[(triple4)] Gary is big.[(triple5)] Gary is not white.[(triple7)] Gary is round.[(triple6 OR ((triple5) -> rule8))] @1: Erin is rough.[(((triple3 triple2) -> rule4))] Gary is furry.[(((triple5) -> rule7))] @2: Erin is big.[(((((triple3 triple2) -> rule4)) -> rule1))] Erin is not cold.[(((((triple3 triple2) -> rule4)) -> rule6))] @3: Erin is round.[(((((((triple3 triple2) -> rule4)) -> rule1)) -> rule8))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is not white.
("Erin" "is" "white" "-")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is not white.
("Gary" "is" "white" "-")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple5) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3 triple2) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple5) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple3 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
((((triple3 triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple3 triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3