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