Gary is big. Gary is blue. Gary is kind. Gary is nice. Gary is rough. Gary is smart. Gary is white. If someone is blue and nice then they are big.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is blue and nice then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Gary is nice.
True
1
proof
[(triple4)]
("Gary" "is" "nice" "+")
triple4
Gary is not rough.
False
1
inv-proof
[(triple5)]
("Gary" "is" "rough" "-")
triple5
@0: Gary is big.[(triple1 OR ((triple2 triple4) -> rule1))] Gary is blue.[(triple2)] Gary is kind.[(triple3)] Gary is nice.[(triple4)] Gary is rough.[(triple5)] Gary is smart.[(triple6)] Gary is white.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple2 triple4) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7