Erin is big. Erin is smart. Erin is white. Rough things are green. Round things are furry. All furry things are round. If Erin is big then Erin is green. Round things are furry. If Erin is green then Erin is rough.
Erin is big.
("Erin" "is" "big" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Erin is big then Erin is green.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "green" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If Erin is green then Erin is rough.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "rough" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Erin is green.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "green" "+")
((triple1) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "green" "-")
((triple1) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Erin" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("Erin" "is" "rough" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is furry.
Unknown
rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule5 <- FAIL)]]
("Erin" "is" "furry" "+")
@0: Erin is big.[(triple1)] Erin is smart.[(triple2)] Erin is white.[(triple3)] @1: Erin is green.[(((triple1) -> rule4))] @2: Erin is rough.[(((((triple1) -> rule4)) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
((triple1) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2