Gary is big. Gary is blue. Gary is not furry. Gary is nice. Gary is quiet. Gary is smart. Gary is white. If something is white and not furry then it is nice. All nice things are big. If something is furry then it is big. If something is furry and not smart then it is not white. If something is big then it is white. If Gary is furry and Gary is big then Gary is white.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is white and not furry then it is nice.
((("something" "is" "white" "+") ("something" "is" "furry" "~")) -> ("something" "is" "nice" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is furry and not smart then it is not white.
((("something" "is" "furry" "+") ("something" "is" "smart" "~")) -> ("something" "is" "white" "-"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Gary is furry and Gary is big then Gary is white.
((("Gary" "is" "furry" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "white" "+"))
Gary is nice.
True
1
proof
[(triple4 OR ((triple7 triple3) -> rule1) OR ((((triple1) -> rule5) triple3) -> rule1))]
("Gary" "is" "nice" "+")
triple4
((triple7 triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
False
1
inv-proof
[(triple3)]
("Gary" "is" "furry" "+")
triple3
@0: Gary is big.[(triple1 OR ((triple4) -> rule2) OR ((((triple7 triple3) -> rule1)) -> rule2))] Gary is blue.[(triple2)] Gary is nice.[(triple4 OR ((triple7 triple3) -> rule1) OR ((((triple1) -> rule5) triple3) -> rule1))] Gary is not furry.[(triple3)] Gary is quiet.[(triple5)] Gary is smart.[(triple6)] Gary is white.[(triple7 OR ((triple1) -> rule5) OR ((((triple4) -> rule2)) -> rule5))]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple7 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple4
((triple7 triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple1) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2