Gary is big. Gary is blue. Gary is furry. Gary is not quiet. Gary is red. Gary is round. Gary is smart. Harry is not big. Harry is blue. Harry is furry. Harry is quiet. Harry is red. Harry is round. Harry is smart. If Gary is red then Gary is smart. If someone is quiet then they are red. All big people are smart. If someone is smart and not blue then they are furry. If someone is smart and not red then they are furry. All furry people are round.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Gary is red then Gary is smart.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "smart" "+"))
If someone is quiet then they are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not blue then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "furry" "+"))
If someone is smart and not red then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "furry" "+"))
All furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Gary is not quiet.
True
1
proof
[(triple4)]
("Gary" "is" "quiet" "-")
triple4
Harry is not smart.
False
1
inv-proof
[(triple14)]
("Harry" "is" "smart" "-")
triple14
@0: Gary is big.[(triple1)] Gary is blue.[(triple2)] Gary is furry.[(triple3)] Gary is not quiet.[(triple4)] Gary is red.[(triple5)] Gary is round.[(triple6 OR ((triple3) -> rule6))] Gary is smart.[(triple7 OR ((triple1) -> rule3) OR ((triple5) -> rule1))] Harry is blue.[(triple9)] Harry is furry.[(triple10)] Harry is not big.[(triple8)] Harry is quiet.[(triple11)] Harry is red.[(triple12 OR ((triple11) -> rule2))] Harry is round.[(triple13 OR ((triple10) -> rule6))] Harry is smart.[(triple14)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((triple1) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is not big.
("Harry" "is" "big" "-")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((triple11) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple14