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