Erin is rough. If Erin is smart then Erin is furry. If something is rough then it is smart. If Erin is furry then Erin is smart. Furry things are cold. If something is young and furry then it is round. If Erin is furry then Erin is cold.
Erin is rough.
("Erin" "is" "rough" "+")
If Erin is smart then Erin is furry.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "furry" "+"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Erin is furry then Erin is smart.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "smart" "+"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is young and furry then it is round.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Erin is furry then Erin is cold.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "cold" "+"))
Erin is rough.
True
1
proof
[(triple1)]
("Erin" "is" "rough" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple1)]
("Erin" "is" "rough" "-")
triple1
Erin is smart.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Erin" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Erin" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule1)) -> rule6))]
("Erin" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule1)) -> rule6))]
("Erin" "is" "cold" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Erin is rough.[(triple1)] @1: Erin is smart.[(((triple1) -> rule2))] @2: Erin is furry.[(((((triple1) -> rule2)) -> rule1))] @3: Erin is cold.[(((((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule1)) -> rule6))]
Erin is rough.
("Erin" "is" "rough" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3