Gary is blue. Gary is furry. Gary is green. Gary is quiet. Gary is round. Harry is big. Harry is blue. Harry is furry. Harry is green. Harry is kind. Harry is quiet. Harry is round. If Gary is kind and Gary is blue then Gary is green. Round things are blue. All furry, kind things are blue. If Gary is blue then Gary is big. If something is round then it is furry. If something is round and not furry then it is not quiet.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is kind and Gary is blue then Gary is green.
((("Gary" "is" "kind" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "green" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All furry, kind things are blue.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Gary is blue then Gary is big.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "big" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is round and not furry then it is not quiet.
((("something" "is" "round" "+") ("something" "is" "furry" "~")) -> ("something" "is" "quiet" "-"))
Harry is kind.
True
1
proof
[(triple10)]
("Harry" "is" "kind" "+")
triple10
Gary is not furry.
False
1
inv-proof
[(triple2 OR ((triple5) -> rule5))]
("Gary" "is" "furry" "-")
triple2
((triple5) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
True
2
proof
[(((triple1) -> rule4) OR ((((triple5) -> rule2)) -> rule4))]
("Gary" "is" "big" "+")
((triple1) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not big.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple5) -> rule2)) -> rule4))]
("Gary" "is" "big" "-")
((triple1) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
@0: Gary is blue.[(triple1 OR ((triple5) -> rule2))] Gary is furry.[(triple2 OR ((triple5) -> rule5))] Gary is green.[(triple3)] Gary is quiet.[(triple4)] Gary is round.[(triple5)] Harry is big.[(triple6)] Harry is blue.[(triple7 OR ((triple12) -> rule2) OR ((triple8 triple10) -> rule3) OR ((((triple12) -> rule5) triple10) -> rule3))] Harry is furry.[(triple8 OR ((triple12) -> rule5))] Harry is green.[(triple9)] Harry is kind.[(triple10)] Harry is quiet.[(triple11)] Harry is round.[(triple12)] @1: Gary is big.[(((triple1) -> rule4) OR ((((triple5) -> rule2)) -> rule4))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
((triple5) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple12) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple8 triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple12) -> (rule5 % int2)) triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple12) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Gary is big.
("Gary" "is" "big" "+")
((triple1) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2