Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is kind. Harry is red. Harry is round. If Harry is furry then Harry is blue. If Harry is furry then Harry is kind. All blue, furry people are kind. Cold, furry people are blue. If someone is blue and round then they are furry. If someone is furry and green then they are kind. All round people are blue. All red, blue people are kind.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is furry then Harry is blue.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is furry then Harry is kind.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "kind" "+"))
All blue, furry people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Cold, furry people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and round then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and green then they are kind.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All red, blue people are kind.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Harry is blue.
True
1
proof
[(triple1 OR ((triple3) -> rule1) OR ((triple7) -> rule7) OR ((triple2 triple3) -> rule4))]
("Harry" "is" "blue" "+")
triple1
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple7) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple2 triple3) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not furry.
False
1
inv-proof
[(triple3 OR ((triple1 triple7) -> rule5) OR ((((triple7) -> rule7) triple7) -> rule5))]
("Harry" "is" "furry" "-")
triple3
((triple1 triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple7) -> (rule7 % int2)) triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
@0: Harry is blue.[(triple1 OR ((triple3) -> rule1) OR ((triple7) -> rule7) OR ((triple2 triple3) -> rule4))] Harry is cold.[(triple2)] Harry is furry.[(triple3 OR ((triple1 triple7) -> rule5) OR ((((triple7) -> rule7) triple7) -> rule5))] Harry is green.[(triple4)] Harry is kind.[(triple5 OR ((triple3) -> rule2) OR ((triple1 triple3) -> rule3) OR ((triple3 triple4) -> rule6) OR ((triple6 triple1) -> rule8) OR ((((triple1 triple7) -> rule5)) -> rule2) OR ((triple1 ((triple1 triple7) -> rule5)) -> rule3) OR ((triple6 ((triple3) -> rule1)) -> rule8) OR ((triple6 ((triple7) -> rule7)) -> rule8) OR ((triple6 ((triple2 triple3) -> rule4)) -> rule8) OR ((((triple3) -> rule1) triple3) -> rule3) OR ((((triple7) -> rule7) triple3) -> rule3) OR ((((triple1 triple7) -> rule5) triple4) -> rule6) OR ((((triple2 triple3) -> rule4) triple3) -> rule3) OR ((((triple3) -> rule1) ((triple1 triple7) -> rule5)) -> rule3) OR ((((triple7) -> rule7) ((triple1 triple7) -> rule5)) -> rule3) OR ((((triple2 triple3) -> rule4) ((triple1 triple7) -> rule5)) -> rule3) OR ((((((triple7) -> rule7) triple7) -> rule5)) -> rule2) OR ((triple1 ((((triple7) -> rule7) triple7) -> rule5)) -> rule3) OR ((((((triple7) -> rule7) triple7) -> rule5) triple4) -> rule6) OR ((((triple3) -> rule1) ((((triple7) -> rule7) triple7) -> rule5)) -> rule3) OR ((((triple7) -> rule7) ((((triple7) -> rule7) triple7) -> rule5)) -> rule3) OR ((((triple2 triple3) -> rule4) ((((triple7) -> rule7) triple7) -> rule5)) -> rule3))] Harry is red.[(triple6)] Harry is round.[(triple7)]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple7) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple2 triple3) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
((triple1 triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple7) -> (rule7 % int2)) triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
((triple3) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple1 triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple3 triple4) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple6 triple1) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple1 triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple1 ((triple1 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple6 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple6 ((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple6 ((triple2 triple3) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple7) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple1 triple7) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple1 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple7) -> (rule7 % int3)) ((triple1 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple2 triple3) -> (rule4 % int3)) ((triple1 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple7) -> (rule7 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple1 ((((triple7) -> (rule7 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple7) -> (rule7 % int3)) triple7) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple3) -> (rule1 % int3)) ((((triple7) -> (rule7 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple7) -> (rule7 % int3)) ((((triple7) -> (rule7 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple2 triple3) -> (rule4 % int3)) ((((triple7) -> (rule7 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7