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