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