Erin is blue. Erin is cold. Erin is kind. If something is blue and cold then it is rough. Nice things are cold. If something is cold then it is nice. Rough things are kind. All quiet, kind things are not young. If something is cold and not rough then it is quiet. Rough, blue things are quiet. If something is rough then it is quiet.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If something is blue and cold then it is rough.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All quiet, kind things are not young.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "-"))
If something is cold and not rough then it is quiet.
((("something" "is" "cold" "+") ("something" "is" "rough" "~")) -> ("something" "is" "quiet" "+"))
Rough, blue things are quiet.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Erin is not blue.
False
1
inv-proof
[(triple1)]
("Erin" "is" "blue" "-")
triple1
Erin is nice.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not rough.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("Erin" "is" "rough" "-")
((triple1 triple2) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
True
4
proof
[(((((triple1 triple2) -> rule1)) -> rule8) OR ((((triple1 triple2) -> rule1) triple1) -> rule7))]
("Erin" "is" "quiet" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple1 triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple1 triple2) -> rule1)) -> rule8) OR ((((triple1 triple2) -> rule1) triple1) -> rule7))]
("Erin" "is" "quiet" "-")
((((triple1 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple1 triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not young.
True
6
proof
[(((((((triple1 triple2) -> rule1)) -> rule8) triple3) -> rule5) OR ((((((triple1 triple2) -> rule1) triple1) -> rule7) triple3) -> rule5) OR ((((((triple1 triple2) -> rule1)) -> rule8) ((((triple1 triple2) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1 triple2) -> rule1) triple1) -> rule7) ((((triple1 triple2) -> rule1)) -> rule4)) -> rule5))]
("Erin" "is" "young" "-")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1 triple2) -> (rule1 % int3)) triple1) -> (rule7 % int2)) triple3) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1 triple2) -> (rule1 % int4))) -> (rule8 % int3)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple1 triple2) -> (rule1 % int4)) triple1) -> (rule7 % int3)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
False
6
inv-proof
[(((((((triple1 triple2) -> rule1)) -> rule8) triple3) -> rule5) OR ((((((triple1 triple2) -> rule1) triple1) -> rule7) triple3) -> rule5) OR ((((((triple1 triple2) -> rule1)) -> rule8) ((((triple1 triple2) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1 triple2) -> rule1) triple1) -> rule7) ((((triple1 triple2) -> rule1)) -> rule4)) -> rule5))]
("Erin" "is" "young" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1 triple2) -> (rule1 % int3)) triple1) -> (rule7 % int2)) triple3) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1 triple2) -> (rule1 % int4))) -> (rule8 % int3)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple1 triple2) -> (rule1 % int4)) triple1) -> (rule7 % int3)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
@0: Erin is blue.[(triple1)] Erin is cold.[(triple2)] Erin is kind.[(triple3 OR ((((triple1 triple2) -> rule1)) -> rule4))] @1: Erin is nice.[(((triple2) -> rule3))] Erin is rough.[(((triple1 triple2) -> rule1))] @2: Erin is quiet.[(((((triple1 triple2) -> rule1)) -> rule8) OR ((((triple1 triple2) -> rule1) triple1) -> rule7))] @3: Erin is not young.[(((((((triple1 triple2) -> rule1)) -> rule8) triple3) -> rule5) OR ((((((triple1 triple2) -> rule1) triple1) -> rule7) triple3) -> rule5) OR ((((((triple1 triple2) -> rule1)) -> rule8) ((((triple1 triple2) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1 triple2) -> rule1) triple1) -> rule7) ((((triple1 triple2) -> rule1)) -> rule4)) -> rule5))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((((triple1 triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1 triple2) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple1 triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1 triple2) -> (rule1 % int3)) triple1) -> (rule7 % int2)) triple3) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1 triple2) -> (rule1 % int4))) -> (rule8 % int3)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple1 triple2) -> (rule1 % int4)) triple1) -> (rule7 % int3)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4