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