Erin is smart. All rough, smart things are nice. All rough things are blue. If something is red and rough then it is blue. Smart things are rough. If Erin is furry then Erin is smart. If something is blue then it is young.
Erin is smart.
("Erin" "is" "smart" "+")
All rough, smart things are nice.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is red and rough then it is blue.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Erin is furry then Erin is smart.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "smart" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
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) -> rule4))]
("Erin" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not young.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "young" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is smart.[(triple1)] @1: Erin is rough.[(((triple1) -> rule4))] @2: Erin is blue.[(((((triple1) -> rule4)) -> rule2))] Erin is nice.[(((((triple1) -> rule4) triple1) -> rule1))] @3: Erin is young.[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3