Gary is big. Gary is cold. Gary is furry. Gary is nice. Gary is red. Gary is round. Gary is white. All white people are nice. Furry, nice people are round. If Gary is cold then Gary is big. If Gary is big then Gary is furry. If someone is white then they are round. White people are furry.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Furry, nice people are round.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If Gary is cold then Gary is big.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "big" "+"))
If Gary is big then Gary is furry.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "furry" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
White people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Gary is big.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("Gary" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule1))]
("Gary" "is" "nice" "-")
triple4
((triple7) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
@0: Gary is big.[(triple1 OR ((triple2) -> rule3))] Gary is cold.[(triple2)] Gary is furry.[(triple3 OR ((triple1) -> rule4) OR ((triple7) -> rule6) OR ((((triple2) -> rule3)) -> rule4))] Gary is nice.[(triple4 OR ((triple7) -> rule1))] Gary is red.[(triple5)] Gary is round.[(triple6 OR ((triple7) -> rule5) OR ((triple3 triple4) -> rule2) OR ((triple3 ((triple7) -> rule1)) -> rule2) OR ((((triple1) -> rule4) triple4) -> rule2) OR ((((triple7) -> rule6) triple4) -> rule2) OR ((((triple1) -> rule4) ((triple7) -> rule1)) -> rule2) OR ((((triple7) -> rule6) ((triple7) -> rule1)) -> rule2) OR ((((((triple2) -> rule3)) -> rule4) triple4) -> rule2) OR ((((((triple2) -> rule3)) -> rule4) ((triple7) -> rule1)) -> rule2))] Gary is white.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
((triple1) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple7) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple4
((triple7) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple7) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple3 triple4) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple3 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple7) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple7) -> (rule6 % int3)) ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple2) -> (rule3 % int4))) -> (rule4 % int3)) ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
triple7