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