Bob is blue. Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is rough. Bob is smart. Erin is cold. Erin is furry. Erin is nice. Erin is smart. Harry is blue. Harry is cold. Harry is furry. Harry is nice. Harry is rough. If someone is cold then they are quiet. If someone is blue and smart then they are furry. If someone is quiet and cold then they are blue. If Harry is blue then Harry is furry. If Bob is furry then Bob is nice. Nice people are quiet. Blue people are rough. If Erin is rough and Erin is blue then Erin is quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and smart then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet and cold then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Harry is blue then Harry is furry.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "furry" "+"))
If Bob is furry then Bob is nice.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Erin is rough and Erin is blue then Erin is quiet.
((("Erin" "is" "rough" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "quiet" "+"))
Bob is nice.
True
1
proof
[(triple4 OR ((triple3) -> rule5) OR ((((triple1 triple7) -> rule2)) -> rule5) OR ((((((triple5 triple2) -> rule3) triple7) -> rule2)) -> rule5) OR ((((((((triple2) -> rule1) triple2) -> rule3) triple7) -> rule2)) -> rule5))]
("Bob" "is" "nice" "+")
triple4
((triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple5 triple2) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((((triple2) -> (rule1 % int4)) triple2) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Erin is not nice.
False
1
inv-proof
[(triple10)]
("Erin" "is" "nice" "-")
triple10
Erin is quiet.
True
2
proof
[(((triple10) -> rule6) OR ((triple8) -> rule1))]
("Erin" "is" "quiet" "+")
((triple10) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple8) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple10) -> rule6) OR ((triple8) -> rule1))]
("Erin" "is" "quiet" "-")
((triple10) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple8) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
True
4
proof
[(((((triple10) -> rule6) triple8) -> rule3) OR ((((triple8) -> rule1) triple8) -> rule3))]
("Erin" "is" "blue" "+")
((((triple10) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((((triple10) -> rule6) triple8) -> rule3) OR ((((triple8) -> rule1) triple8) -> rule3))]
("Erin" "is" "blue" "-")
((((triple10) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
@0: Bob is blue.[(triple1 OR ((triple5 triple2) -> rule3) OR ((((triple2) -> rule1) triple2) -> rule3) OR ((((triple4) -> rule6) triple2) -> rule3) OR ((((((triple3) -> rule5)) -> rule6) triple2) -> rule3))] Bob is cold.[(triple2)] Bob is furry.[(triple3 OR ((triple1 triple7) -> rule2) OR ((((triple5 triple2) -> rule3) triple7) -> rule2) OR ((((((triple2) -> rule1) triple2) -> rule3) triple7) -> rule2) OR ((((((triple4) -> rule6) triple2) -> rule3) triple7) -> rule2))] Bob is nice.[(triple4 OR ((triple3) -> rule5) OR ((((triple1 triple7) -> rule2)) -> rule5) OR ((((((triple5 triple2) -> rule3) triple7) -> rule2)) -> rule5) OR ((((((((triple2) -> rule1) triple2) -> rule3) triple7) -> rule2)) -> rule5))] Bob is quiet.[(triple5 OR ((triple2) -> rule1) OR ((triple4) -> rule6) OR ((((triple3) -> rule5)) -> rule6) OR ((((((triple1 triple7) -> rule2)) -> rule5)) -> rule6))] Bob is rough.[(triple6 OR ((triple1) -> rule7) OR ((((triple5 triple2) -> rule3)) -> rule7) OR ((((((triple2) -> rule1) triple2) -> rule3)) -> rule7) OR ((((((triple4) -> rule6) triple2) -> rule3)) -> rule7) OR ((((((((triple3) -> rule5)) -> rule6) triple2) -> rule3)) -> rule7))] Bob is smart.[(triple7)] Erin is cold.[(triple8)] Erin is furry.[(triple9 OR ((((((triple10) -> rule6) triple8) -> rule3) triple11) -> rule2) OR ((((((triple8) -> rule1) triple8) -> rule3) triple11) -> rule2))] Erin is nice.[(triple10)] Erin is smart.[(triple11)] Harry is blue.[(triple12 OR ((((triple13) -> rule1) triple13) -> rule3) OR ((((triple15) -> rule6) triple13) -> rule3))] Harry is cold.[(triple13)] Harry is furry.[(triple14 OR ((triple12) -> rule4) OR ((((((triple13) -> rule1) triple13) -> rule3)) -> rule4) OR ((((((triple15) -> rule6) triple13) -> rule3)) -> rule4))] Harry is nice.[(triple15)] Harry is rough.[(triple16 OR ((triple12) -> rule7) OR ((((((triple13) -> rule1) triple13) -> rule3)) -> rule7) OR ((((((triple15) -> rule6) triple13) -> rule3)) -> rule7))] @1: Erin is quiet.[(((triple10) -> rule6) OR ((triple8) -> rule1))] Harry is quiet.[(((triple13) -> rule1) OR ((triple15) -> rule6))] @2: Erin is blue.[(((((triple10) -> rule6) triple8) -> rule3) OR ((((triple8) -> rule1) triple8) -> rule3))] @3: Erin is rough.[(((((((triple10) -> rule6) triple8) -> rule3)) -> rule7) OR ((((((triple8) -> rule1) triple8) -> rule3)) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5 triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple4) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple1 triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5 triple2) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple4) -> (rule6 % int3)) triple2) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple5 triple2) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((((triple2) -> (rule1 % int4)) triple2) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple1 triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple1) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple5 triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple4) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((((((triple10) -> (rule6 % int3)) triple8) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple8) -> (rule1 % int3)) triple8) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
((((triple13) -> (rule1 % int2)) triple13) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple15) -> (rule6 % int2)) triple13) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
((triple12) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((((triple13) -> (rule1 % int3)) triple13) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple15) -> (rule6 % int3)) triple13) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
((triple12) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((triple13) -> (rule1 % int3)) triple13) -> (rule3 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple15) -> (rule6 % int3)) triple13) -> (rule3 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple10) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple8) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple13) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple15) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple10) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple10) -> (rule6 % int3)) triple8) -> (rule3 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple8) -> (rule1 % int3)) triple8) -> (rule3 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3