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