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