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