Anne is cold. Anne is furry. Anne is nice. Anne is quiet. Anne is young. Fiona is kind. Fiona is quiet. Fiona is rough. Fiona is young. Harry is cold. Harry is furry. Harry is kind. Harry is nice. Harry is quiet. Harry is young. Cold, quiet people are kind. Kind, young people are rough. If someone is kind and quiet then they are nice. All nice, cold people are furry. If someone is young and nice then they are quiet. If Fiona is furry and Fiona is young then Fiona is kind. All quiet, kind people are cold. If someone is kind then they are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Cold, quiet people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Kind, young people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and quiet then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All nice, cold people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is young and nice then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is furry and Fiona is young then Fiona is kind.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "kind" "+"))
All quiet, kind people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple12 OR ((triple10 triple14) -> rule1) OR ((triple10 ((triple15 triple13) -> rule5)) -> rule1))]
("Harry" "is" "kind" "-")
triple12
((triple10 triple14) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple10 ((triple15 triple13) -> (rule5 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Fiona is cold.
True
2
proof
[(((triple6) -> rule8) OR ((triple7 triple6) -> rule7))]
("Fiona" "is" "cold" "+")
((triple6) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple7 triple6) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple6) -> rule8) OR ((triple7 triple6) -> rule7))]
("Fiona" "is" "cold" "-")
((triple6) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple7 triple6) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Anne is rough.
True
5
proof
[(((((triple1 triple4) -> rule1) triple5) -> rule2) OR ((((triple1 ((triple5 triple3) -> rule5)) -> rule1) triple5) -> rule2))]
("Anne" "is" "rough" "+")
((((triple1 triple4) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1 ((triple5 triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not rough.
False
5
inv-proof
[(((((triple1 triple4) -> rule1) triple5) -> rule2) OR ((((triple1 ((triple5 triple3) -> rule5)) -> rule1) triple5) -> rule2))]
("Anne" "is" "rough" "-")
((((triple1 triple4) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1 ((triple5 triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2 OR ((triple3 triple1) -> rule4) OR ((((((triple1 triple4) -> rule1) triple4) -> rule3) triple1) -> rule4))] Anne is nice.[(triple3 OR ((((triple1 triple4) -> rule1) triple4) -> rule3))] Anne is quiet.[(triple4 OR ((triple5 triple3) -> rule5))] Anne is young.[(triple5)] Fiona is kind.[(triple6)] Fiona is quiet.[(triple7)] Fiona is rough.[(triple8 OR ((triple6 triple9) -> rule2))] Fiona is young.[(triple9)] Harry is cold.[(triple10 OR ((triple12) -> rule8) OR ((triple14 triple12) -> rule7) OR ((((triple15 triple13) -> rule5) triple12) -> rule7))] Harry is furry.[(triple11 OR ((triple13 triple10) -> rule4) OR ((triple13 ((triple12) -> rule8)) -> rule4) OR ((triple13 ((triple14 triple12) -> rule7)) -> rule4) OR ((((triple12 triple14) -> rule3) triple10) -> rule4) OR ((((triple12 triple14) -> rule3) ((triple12) -> rule8)) -> rule4) OR ((((triple12 triple14) -> rule3) ((triple14 triple12) -> rule7)) -> rule4) OR ((triple13 ((((triple15 triple13) -> rule5) triple12) -> rule7)) -> rule4) OR ((((((triple10 triple14) -> rule1) triple14) -> rule3) triple10) -> rule4) OR ((((triple12 triple14) -> rule3) ((((triple15 triple13) -> rule5) triple12) -> rule7)) -> rule4) OR ((((((triple10 triple14) -> rule1) triple14) -> rule3) ((triple12) -> rule8)) -> rule4) OR ((((((triple10 triple14) -> rule1) triple14) -> rule3) ((triple14 triple12) -> rule7)) -> rule4) OR ((((((triple10 triple14) -> rule1) triple14) -> rule3) ((((triple15 triple13) -> rule5) triple12) -> rule7)) -> rule4))] Harry is kind.[(triple12 OR ((triple10 triple14) -> rule1) OR ((triple10 ((triple15 triple13) -> rule5)) -> rule1))] Harry is nice.[(triple13 OR ((triple12 triple14) -> rule3) OR ((((triple10 triple14) -> rule1) triple14) -> rule3))] Harry is quiet.[(triple14 OR ((triple15 triple13) -> rule5))] Harry is young.[(triple15)] @1: Anne is kind.[(((triple1 triple4) -> rule1) OR ((triple1 ((triple5 triple3) -> rule5)) -> rule1))] Fiona is cold.[(((triple6) -> rule8) OR ((triple7 triple6) -> rule7))] Fiona is nice.[(((triple6 triple7) -> rule3))] Harry is rough.[(((triple12 triple15) -> rule2) OR ((((triple10 triple14) -> rule1) triple15) -> rule2) OR ((((triple10 ((triple15 triple13) -> rule5)) -> rule1) triple15) -> rule2))] @2: Anne is rough.[(((((triple1 triple4) -> rule1) triple5) -> rule2) OR ((((triple1 ((triple5 triple3) -> rule5)) -> rule1) triple5) -> rule2))] Fiona is furry.[(((((triple6 triple7) -> rule3) ((triple6) -> rule8)) -> rule4) OR ((((triple6 triple7) -> rule3) ((triple7 triple6) -> rule7)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple3 triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((((triple1 triple4) -> (rule1 % int3)) triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((((triple1 triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple5 triple3) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
((triple6 triple9) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((triple12) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple14 triple12) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple15 triple13) -> (rule5 % int2)) triple12) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple13 triple10) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple13 ((triple12) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple13 ((triple14 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple12 triple14) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple12 triple14) -> (rule3 % int3)) ((triple12) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple12 triple14) -> (rule3 % int3)) ((triple14 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple13 ((((triple15 triple13) -> (rule5 % int3)) triple12) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple10 triple14) -> (rule1 % int3)) triple14) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple12 triple14) -> (rule3 % int4)) ((((triple15 triple13) -> (rule5 % int3)) triple12) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple10 triple14) -> (rule1 % int4)) triple14) -> (rule3 % int3)) ((triple12) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((((triple10 triple14) -> (rule1 % int4)) triple14) -> (rule3 % int3)) ((triple14 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((((triple10 triple14) -> (rule1 % int5)) triple14) -> (rule3 % int4)) ((((triple15 triple13) -> (rule5 % int3)) triple12) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5
Harry is kind.
("Harry" "is" "kind" "+")
triple12
((triple10 triple14) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple10 ((triple15 triple13) -> (rule5 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple13
((triple12 triple14) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple10 triple14) -> (rule1 % int2)) triple14) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((triple15 triple13) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple4) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple5 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple6) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple7 triple6) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple6 triple7) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple12 triple15) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10 triple14) -> (rule1 % int2)) triple15) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple10 ((triple15 triple13) -> (rule5 % int3))) -> (rule1 % int2)) triple15) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 triple4) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1 ((triple5 triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple6 triple7) -> (rule3 % int3)) ((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((triple6 triple7) -> (rule3 % int3)) ((triple7 triple6) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3