Erin is big. If something is furry and not red then it is not smart. Green things are furry. If something is big then it is green. If something is smart then it is green. If Erin is smart then Erin is big. Big, furry things are cold.
Erin is big.
("Erin" "is" "big" "+")
If something is furry and not red then it is not smart.
((("something" "is" "furry" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "-"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Erin is smart then Erin is big.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "big" "+"))
Big, furry things are cold.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Erin is green.
True
2
proof
[(((triple1) -> rule3))]
("Erin" "is" "green" "+")
((triple1) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Erin" "is" "green" "-")
((triple1) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Erin" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Erin" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule6))]
("Erin" "is" "cold" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule6))]
("Erin" "is" "cold" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is big.[(triple1)] @1: Erin is green.[(((triple1) -> rule3))] @2: Erin is furry.[(((((triple1) -> rule3)) -> rule2))] @3: Erin is cold.[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
((triple1) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3