Harry is blue. Harry is cold. Harry is furry. Harry is kind. Harry is nice. Harry is red. Harry is round. Red, furry people are cold. All furry, nice people are round. Kind, furry people are red. If someone is kind then they are round. If someone is cold and round then they are furry. If someone is furry and cold then they are blue.
Harry is blue.
("Harry" "is" "blue" "+")
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 red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Red, furry people are cold.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All furry, nice people are round.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Kind, furry people are red.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and round then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and cold then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Harry is not nice.
False
1
inv-proof
[(triple5)]
("Harry" "is" "nice" "-")
triple5
@0: Harry is blue.[(triple1 OR ((triple3 triple2) -> rule6) OR ((triple3 ((triple6 triple3) -> rule1)) -> rule6) OR ((((triple2 triple7) -> rule5) triple2) -> rule6) OR ((((triple2 triple7) -> rule5) ((triple6 triple3) -> rule1)) -> rule6) OR ((triple3 ((((triple4 triple3) -> rule3) triple3) -> rule1)) -> rule6) OR ((((triple2 ((triple4) -> rule4)) -> rule5) triple2) -> rule6) OR ((((triple2 triple7) -> rule5) ((((triple4 triple3) -> rule3) triple3) -> rule1)) -> rule6) OR ((((triple2 ((triple4) -> rule4)) -> rule5) ((triple6 triple3) -> rule1)) -> rule6) OR ((((triple2 ((triple4) -> rule4)) -> rule5) ((((triple4 triple3) -> rule3) triple3) -> rule1)) -> rule6))] Harry is cold.[(triple2 OR ((triple6 triple3) -> rule1) OR ((((triple4 triple3) -> rule3) triple3) -> rule1))] Harry is furry.[(triple3 OR ((triple2 triple7) -> rule5) OR ((triple2 ((triple4) -> rule4)) -> rule5))] Harry is kind.[(triple4)] Harry is nice.[(triple5)] Harry is red.[(triple6 OR ((triple4 triple3) -> rule3) OR ((triple4 ((triple2 triple7) -> rule5)) -> rule3) OR ((triple4 ((triple2 ((triple4) -> rule4)) -> rule5)) -> rule3))] Harry is round.[(triple7 OR ((triple4) -> rule4) OR ((triple3 triple5) -> rule2))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple3 triple2) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple3 ((triple6 triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple2 triple7) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple2 triple7) -> (rule5 % int3)) ((triple6 triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((triple3 ((((triple4 triple3) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple2 ((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple2 triple7) -> (rule5 % int4)) ((((triple4 triple3) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
((((triple2 ((triple4) -> (rule4 % int4))) -> (rule5 % int3)) ((triple6 triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((triple2 ((triple4) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple4 triple3) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5
Harry is cold.
("Harry" "is" "cold" "+")
triple2
((triple6 triple3) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple4 triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
((triple2 triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple2 ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
((triple4 triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple4 ((triple2 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple4 ((triple2 ((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple7
((triple4) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple3 triple5) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1