Erin is furry. Round things are nice. Cold, round things are big. All young, furry things are nice. If something is furry then it is young. Furry things are round. If something is young then it is nice. If Erin is blue then Erin is big. Nice things are big.
Erin is furry.
("Erin" "is" "furry" "+")
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Cold, round things are big.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All young, furry things are nice.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Erin is blue then Erin is big.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "big" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Erin is furry.
True
1
proof
[(triple1)]
("Erin" "is" "furry" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple1)]
("Erin" "is" "furry" "-")
triple1
Erin is young.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "young" "+")
((triple1) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Erin" "is" "round" "-")
((triple1) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule6) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) triple1) -> rule3))]
("Erin" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) triple1) -> rule3))]
("Erin" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule8) OR ((((((triple1) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule4) triple1) -> rule3)) -> rule8))]
("Erin" "is" "big" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not big.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule8) OR ((((((triple1) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule4) triple1) -> rule3)) -> rule8))]
("Erin" "is" "big" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Erin is furry.[(triple1)] @1: Erin is round.[(((triple1) -> rule5))] Erin is young.[(((triple1) -> rule4))] @2: Erin is nice.[(((((triple1) -> rule4)) -> rule6) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) triple1) -> rule3))] @3: Erin is big.[(((((((triple1) -> rule4)) -> rule6)) -> rule8) OR ((((((triple1) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule4) triple1) -> rule3)) -> rule8))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
((triple1) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple1) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3