Harry is big. Harry is cold. Harry is nice. Harry is red. Harry is rough. Harry is round. Harry is smart. If something is smart and rough then it is round. If something is nice then it is smart. If something is red and big then it is smart.
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and rough then it is round.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is red and big then it is smart.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple7 OR ((triple3) -> rule2) OR ((triple4 triple1) -> rule3))]
("Harry" "is" "smart" "+")
triple7
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple4 triple1) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not red.
False
1
inv-proof
[(triple4)]
("Harry" "is" "red" "-")
triple4
@0: Harry is big.[(triple1)] Harry is cold.[(triple2)] Harry is nice.[(triple3)] Harry is red.[(triple4)] Harry is rough.[(triple5)] Harry is round.[(triple6 OR ((triple7 triple5) -> rule1) OR ((((triple3) -> rule2) triple5) -> rule1) OR ((((triple4 triple1) -> rule3) triple5) -> rule1))] Harry is smart.[(triple7 OR ((triple3) -> rule2) OR ((triple4 triple1) -> rule3))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
((triple7 triple5) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple3) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple4 triple1) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple4 triple1) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1