Erin is big. Erin is furry. Erin is quiet. Quiet, big things are kind. If something is quiet then it is furry. If Erin is rough and Erin is quiet then Erin is blue. All nice things are rough. If Erin is rough and Erin is big then Erin is quiet. Blue things are furry. All kind, furry things are rough. All furry, nice things are kind.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Quiet, big things are kind.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Erin is rough and Erin is quiet then Erin is blue.
((("Erin" "is" "rough" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "blue" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Erin is rough and Erin is big then Erin is quiet.
((("Erin" "is" "rough" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "quiet" "+"))
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All kind, furry things are rough.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All furry, nice things are kind.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Erin is kind.
True
3
proof
[(((triple3 triple1) -> rule1))]
("Erin" "is" "kind" "+")
((triple3 triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
3
inv-proof
[(((triple3 triple1) -> rule1))]
("Erin" "is" "kind" "-")
((triple3 triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
True
5
proof
[(((((triple3 triple1) -> rule1) triple2) -> rule7) OR ((((triple3 triple1) -> rule1) ((triple3) -> rule2)) -> rule7))]
("Erin" "is" "rough" "+")
((((triple3 triple1) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 triple1) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not rough.
False
5
inv-proof
[(((((triple3 triple1) -> rule1) triple2) -> rule7) OR ((((triple3 triple1) -> rule1) ((triple3) -> rule2)) -> rule7))]
("Erin" "is" "rough" "-")
((((triple3 triple1) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 triple1) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
True
7
proof
[(((((((triple3 triple1) -> rule1) triple2) -> rule7) triple3) -> rule3) OR ((((((triple3 triple1) -> rule1) ((triple3) -> rule2)) -> rule7) triple3) -> rule3))]
("Erin" "is" "blue" "+")
((((((triple3 triple1) -> (rule1 % int3)) triple2) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple3 triple1) -> (rule1 % int4)) ((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not blue.
False
7
inv-proof
[(((((((triple3 triple1) -> rule1) triple2) -> rule7) triple3) -> rule3) OR ((((((triple3 triple1) -> rule1) ((triple3) -> rule2)) -> rule7) triple3) -> rule3))]
("Erin" "is" "blue" "-")
((((((triple3 triple1) -> (rule1 % int3)) triple2) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple3 triple1) -> (rule1 % int4)) ((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
@0: Erin is big.[(triple1)] Erin is furry.[(triple2 OR ((triple3) -> rule2))] Erin is quiet.[(triple3)] @1: Erin is kind.[(((triple3 triple1) -> rule1))] @2: Erin is rough.[(((((triple3 triple1) -> rule1) triple2) -> rule7) OR ((((triple3 triple1) -> rule1) ((triple3) -> rule2)) -> rule7))] @3: Erin is blue.[(((((((triple3 triple1) -> rule1) triple2) -> rule7) triple3) -> rule3) OR ((((((triple3 triple1) -> rule1) ((triple3) -> rule2)) -> rule7) triple3) -> rule3))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple3) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
((triple3 triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3 triple1) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 triple1) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple3 triple1) -> (rule1 % int3)) triple2) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple3 triple1) -> (rule1 % int4)) ((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4