Harry is blue. Harry is nice. Harry is white. All nice, furry things are white. If something is nice then it is green. White things are nice. If something is kind and blue then it is nice. If something is white and green then it is big. If something is big then it is white. If something is green then it is furry. All nice things are blue.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
All nice, furry things are white.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is kind and blue then it is nice.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is white and green then it is big.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Harry is white.
True
1
proof
[(triple3 OR ((triple2 ((((triple2) -> rule2)) -> rule7)) -> rule1))]
("Harry" "is" "white" "+")
triple3
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not blue.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule8) OR ((((triple3) -> rule3)) -> rule8))]
("Harry" "is" "blue" "-")
triple1
((triple2) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
@0: Harry is blue.[(triple1 OR ((triple2) -> rule8) OR ((((triple3) -> rule3)) -> rule8))] Harry is nice.[(triple2 OR ((triple3) -> rule3))] Harry is white.[(triple3 OR ((triple2 ((((triple2) -> rule2)) -> rule7)) -> rule1))] @1: Harry is green.[(((triple2) -> rule2) OR ((((triple3) -> rule3)) -> rule2))] @2: Harry is big.[(((triple3 ((triple2) -> rule2)) -> rule5) OR ((triple3 ((((triple3) -> rule3)) -> rule2)) -> rule5) OR ((((triple2 ((((triple2) -> rule2)) -> rule7)) -> rule1) ((triple2) -> rule2)) -> rule5) OR ((((triple2 ((((triple2) -> rule2)) -> rule7)) -> rule1) ((((triple3) -> rule3)) -> rule2)) -> rule5))] Harry is furry.[(((((triple2) -> rule2)) -> rule7) OR ((((((triple3) -> rule3)) -> rule2)) -> rule7))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple2) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple2
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple3
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple2 ((((triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) ((triple2) -> (rule2 % int4))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((triple2 ((((triple2) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule3 % int2))) -> (rule2 % int5))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Harry is furry.
("Harry" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3