Erin is green. If something is blue and furry then it is young. All green, quiet things are furry. If Erin is green then Erin is big. If Erin is big and Erin is blue then Erin is quiet. If Erin is big then Erin is blue. Big things are rough.
Erin is green.
("Erin" "is" "green" "+")
If something is blue and furry then it is young.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All green, quiet things are furry.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Erin is green then Erin is big.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
If Erin is big and Erin is blue then Erin is quiet.
((("Erin" "is" "big" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "quiet" "+"))
If Erin is big then Erin is blue.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "blue" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Erin is green.
True
1
proof
[(triple1)]
("Erin" "is" "green" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple1)]
("Erin" "is" "green" "-")
triple1
Erin is big.
True
2
proof
[(((triple1) -> rule3))]
("Erin" "is" "big" "+")
((triple1) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Erin" "is" "big" "-")
((triple1) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
@0: Erin is green.[(triple1)] @1: Erin is big.[(((triple1) -> rule3))] @2: Erin is blue.[(((((triple1) -> rule3)) -> rule5))] Erin is rough.[(((((triple1) -> rule3)) -> rule6))] @3: Erin is quiet.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4))] @4: Erin is furry.[(((triple1 ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2))] @5: Erin is young.[(((((((triple1) -> rule3)) -> rule5) ((triple1 ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2)) -> rule1))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((triple1 ((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((((triple1) -> (rule3 % int5))) -> (rule5 % int4)) ((triple1 ((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5