Erin is smart. All rough people are smart. Big, rough people are smart. If someone is quiet and rough then they are smart. If someone is rough then they are not young. If someone is blue then they are not young. All smart people are rough. Big, smart people are blue. If Erin is rough then Erin is big.
Erin is smart.
("Erin" "is" "smart" "+")
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Big, rough people are smart.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and rough then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are not young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "-"))
If someone is blue then they are not young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Big, smart people are blue.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Erin is rough then Erin is big.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "big" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Erin is not smart.
False
1
inv-proof
[(triple1)]
("Erin" "is" "smart" "-")
triple1
Erin is rough.
True
2
proof
[(((triple1) -> rule6))]
("Erin" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple1) -> rule6))]
("Erin" "is" "rough" "-")
((triple1) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule8))]
("Erin" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4) OR ((((((((triple1) -> rule6)) -> rule8) triple1) -> rule7)) -> rule5))]
("Erin" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((((triple1) -> (rule6 % int4))) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is blue.
True
5
proof
[(((((((triple1) -> rule6)) -> rule8) triple1) -> rule7))]
("Erin" "is" "blue" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((((((triple1) -> rule6)) -> rule8) triple1) -> rule7))]
("Erin" "is" "blue" "-")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Erin is smart.[(triple1)] @1: Erin is rough.[(((triple1) -> rule6))] @2: Erin is big.[(((((triple1) -> rule6)) -> rule8))] Erin is not young.[(((((triple1) -> rule6)) -> rule4) OR ((((((((triple1) -> rule6)) -> rule8) triple1) -> rule7)) -> rule5))] @3: Erin is blue.[(((((((triple1) -> rule6)) -> rule8) triple1) -> rule7))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((((triple1) -> (rule6 % int4))) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3