Gary is big. Gary is cold. Gary is furry. Gary is green. Gary is nice. Gary is quiet. Gary is white. Harry is big. Harry is cold. Harry is furry. Harry is green. Harry is nice. Harry is quiet. Harry is white. If someone is green and quiet then they are nice. All white, big people are quiet.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is green and quiet then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All white, big people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Gary is not big.
False
1
inv-proof
[(triple1)]
("Gary" "is" "big" "-")
triple1
@0: Gary is big.[(triple1)] Gary is cold.[(triple2)] Gary is furry.[(triple3)] Gary is green.[(triple4)] Gary is nice.[(triple5 OR ((triple4 triple6) -> rule1) OR ((triple4 ((triple7 triple1) -> rule2)) -> rule1))] Gary is quiet.[(triple6 OR ((triple7 triple1) -> rule2))] Gary is white.[(triple7)] Harry is big.[(triple8)] Harry is cold.[(triple9)] Harry is furry.[(triple10)] Harry is green.[(triple11)] Harry is nice.[(triple12 OR ((triple11 triple13) -> rule1) OR ((triple11 ((triple14 triple8) -> rule2)) -> rule1))] Harry is quiet.[(triple13 OR ((triple14 triple8) -> rule2))] Harry is white.[(triple14)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
((triple4 triple6) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple4 ((triple7 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
((triple7 triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((triple11 triple13) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple11 ((triple14 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple14 triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14