Erin is big. Erin is nice. Erin is round. Young things are big. If Erin is round then Erin is young. All young things are blue. If something is round and not nice then it is not blue. If something is round and not young then it is smart. All blue things are smart.
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Erin is round then Erin is young.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "young" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is round and not nice then it is not blue.
((("something" "is" "round" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "-"))
If something is round and not young then it is smart.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "smart" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Erin is big.
True
1
proof
[(triple1 OR ((((triple3) -> rule2)) -> rule1))]
("Erin" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not round.
False
1
inv-proof
[(triple3)]
("Erin" "is" "round" "-")
triple3
Erin is young.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "young" "+")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "young" "-")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Erin" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Erin" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
True
4
proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule6))]
("Erin" "is" "smart" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not smart.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule6))]
("Erin" "is" "smart" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
@0: Erin is big.[(triple1 OR ((((triple3) -> rule2)) -> rule1))] Erin is nice.[(triple2)] Erin is round.[(triple3)] @1: Erin is young.[(((triple3) -> rule2))] @2: Erin is blue.[(((((triple3) -> rule2)) -> rule3))] @3: Erin is smart.[(((((((triple3) -> rule2)) -> rule3)) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3