Erin is furry. Erin is kind. Erin is nice. Erin is red. Erin is rough. Erin is smart. Erin is white. Fiona is furry. Fiona is kind. Fiona is nice. Fiona is red. Fiona is rough. Fiona is white. Harry is kind. Harry is smart. Harry is white. All kind things are red. Kind, rough things are furry. If something is nice then it is white. If something is white then it is nice. If Harry is white and Harry is smart then Harry is kind. If something is kind and furry then it is rough. If Erin is smart then Erin is red. All red things are furry.
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Kind, rough things are furry.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If Harry is white and Harry is smart then Harry is kind.
((("Harry" "is" "white" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "kind" "+"))
If something is kind and furry then it is rough.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Erin is smart then Erin is red.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "red" "+"))
All red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Harry is white.
True
1
proof
[(triple16)]
("Harry" "is" "white" "+")
triple16
Fiona is not nice.
False
1
inv-proof
[(triple10 OR ((triple13) -> rule4))]
("Fiona" "is" "nice" "-")
triple10
((triple13) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is red.
True
2
proof
[(((triple14) -> rule1) OR ((((triple16 triple15) -> rule5)) -> rule1))]
("Harry" "is" "red" "+")
((triple14) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple16 triple15) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not nice.
False
2
inv-proof
[(((triple16) -> rule4))]
("Harry" "is" "nice" "-")
((triple16) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
True
3
proof
[(((((triple14) -> rule1)) -> rule8) OR ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8))]
("Harry" "is" "furry" "+")
((((triple14) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple16 triple15) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not furry.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule8) OR ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8))]
("Harry" "is" "furry" "-")
((((triple14) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple16 triple15) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is rough.
True
5
proof
[(((triple14 ((((triple14) -> rule1)) -> rule8)) -> rule6) OR ((((triple16 triple15) -> rule5) ((((triple14) -> rule1)) -> rule8)) -> rule6) OR ((triple14 ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8)) -> rule6) OR ((((triple16 triple15) -> rule5) ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8)) -> rule6))]
("Harry" "is" "rough" "+")
((triple14 ((((triple14) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple16 triple15) -> (rule5 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((triple14 ((((((triple16 triple15) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple16 triple15) -> (rule5 % int4)) ((((((triple16 triple15) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is not rough.
False
5
inv-proof
[(((triple14 ((((triple14) -> rule1)) -> rule8)) -> rule6) OR ((((triple16 triple15) -> rule5) ((((triple14) -> rule1)) -> rule8)) -> rule6) OR ((triple14 ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8)) -> rule6) OR ((((triple16 triple15) -> rule5) ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8)) -> rule6))]
("Harry" "is" "rough" "-")
((triple14 ((((triple14) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple16 triple15) -> (rule5 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((triple14 ((((((triple16 triple15) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple16 triple15) -> (rule5 % int4)) ((((((triple16 triple15) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
@0: Erin is furry.[(triple1 OR ((triple4) -> rule8) OR ((triple2 triple5) -> rule2) OR ((((triple2) -> rule1)) -> rule8) OR ((((triple6) -> rule7)) -> rule8))] Erin is kind.[(triple2)] Erin is nice.[(triple3 OR ((triple7) -> rule4))] Erin is red.[(triple4 OR ((triple2) -> rule1) OR ((triple6) -> rule7))] Erin is rough.[(triple5 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple4) -> rule8)) -> rule6) OR ((triple2 ((((triple2) -> rule1)) -> rule8)) -> rule6) OR ((triple2 ((((triple6) -> rule7)) -> rule8)) -> rule6))] Erin is smart.[(triple6)] Erin is white.[(triple7 OR ((triple3) -> rule3))] Fiona is furry.[(triple8 OR ((triple11) -> rule8) OR ((triple9 triple12) -> rule2) OR ((((triple9) -> rule1)) -> rule8))] Fiona is kind.[(triple9)] Fiona is nice.[(triple10 OR ((triple13) -> rule4))] Fiona is red.[(triple11 OR ((triple9) -> rule1))] Fiona is rough.[(triple12 OR ((triple9 triple8) -> rule6) OR ((triple9 ((triple11) -> rule8)) -> rule6) OR ((triple9 ((((triple9) -> rule1)) -> rule8)) -> rule6))] Fiona is white.[(triple13 OR ((triple10) -> rule3))] Harry is kind.[(triple14 OR ((triple16 triple15) -> rule5))] Harry is smart.[(triple15)] Harry is white.[(triple16)] @1: Harry is nice.[(((triple16) -> rule4))] Harry is red.[(((triple14) -> rule1) OR ((((triple16 triple15) -> rule5)) -> rule1))] @2: Harry is furry.[(((((triple14) -> rule1)) -> rule8) OR ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8))] @3: Harry is rough.[(((triple14 ((((triple14) -> rule1)) -> rule8)) -> rule6) OR ((((triple16 triple15) -> rule5) ((((triple14) -> rule1)) -> rule8)) -> rule6) OR ((triple14 ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8)) -> rule6) OR ((((triple16 triple15) -> rule5) ((((((triple16 triple15) -> rule5)) -> rule1)) -> rule8)) -> rule6))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
((triple4) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple2 triple5) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
((triple7) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple6) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple2 triple1) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple2 ((triple4) -> (rule8 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((triple2 ((((triple6) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((triple11) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 triple12) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple13) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple11
((triple9) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
((triple9 triple8) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple9 ((triple11) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple9 ((((triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple13
((triple10) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple16 triple15) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Harry is nice.
("Harry" "is" "nice" "+")
((triple16) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple14) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple16 triple15) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple14) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple16 triple15) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((triple14 ((((triple14) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple16 triple15) -> (rule5 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((triple14 ((((((triple16 triple15) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple16 triple15) -> (rule5 % int4)) ((((((triple16 triple15) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4