Erin is cold. Erin is green. Erin is nice. All nice, rough people are quiet. If Erin is cold and Erin is green then Erin is big. Young, nice people are rough. If someone is cold then they are young. All nice people are green. Nice people are big.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All nice, rough people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is cold and Erin is green then Erin is big.
((("Erin" "is" "cold" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
Young, nice people are rough.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Erin is green.
True
1
proof
[(triple2 OR ((triple3) -> rule5))]
("Erin" "is" "green" "+")
triple2
((triple3) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not cold.
False
1
inv-proof
[(triple1)]
("Erin" "is" "cold" "-")
triple1
Erin is big.
True
2
proof
[(((triple3) -> rule6) OR ((triple1 triple2) -> rule2) OR ((triple1 ((triple3) -> rule5)) -> rule2))]
("Erin" "is" "big" "+")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple1 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule6) OR ((triple1 triple2) -> rule2) OR ((triple1 ((triple3) -> rule5)) -> rule2))]
("Erin" "is" "big" "-")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple1 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
True
4
proof
[(((((triple1) -> rule4) triple3) -> rule3))]
("Erin" "is" "rough" "+")
((((triple1) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple1) -> rule4) triple3) -> rule3))]
("Erin" "is" "rough" "-")
((((triple1) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
@0: Erin is cold.[(triple1)] Erin is green.[(triple2 OR ((triple3) -> rule5))] Erin is nice.[(triple3)] @1: Erin is big.[(((triple3) -> rule6) OR ((triple1 triple2) -> rule2) OR ((triple1 ((triple3) -> rule5)) -> rule2))] Erin is young.[(((triple1) -> rule4))] @2: Erin is rough.[(((((triple1) -> rule4) triple3) -> rule3))] @3: Erin is quiet.[(((triple3 ((((triple1) -> rule4) triple3) -> rule3)) -> rule1))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
((triple3) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple1 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple1) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3 ((((triple1) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3