Gary is big. Gary is cold. Gary is kind. Gary is nice. Gary is round. Gary is smart. Gary is white. If Gary is kind then Gary is white. Round things are cold. If something is white and cold then it is nice. If something is nice and cold then it is white. All round things are smart. All round, big things are kind. If Gary is nice then Gary is cold. All white things are big.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is kind then Gary is white.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "white" "+"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is white and cold then it is nice.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is nice and cold then it is white.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All round, big things are kind.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If Gary is nice then Gary is cold.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "cold" "+"))
All white things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Gary is kind.
True
1
proof
[(triple3 OR ((triple5 triple1) -> rule6) OR ((triple5 ((triple7) -> rule8)) -> rule6) OR ((triple5 ((((triple4 triple2) -> rule4)) -> rule8)) -> rule6) OR ((triple5 ((((triple4 ((triple4) -> rule7)) -> rule4)) -> rule8)) -> rule6) OR ((triple5 ((((triple4 ((triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6))]
("Gary" "is" "kind" "+")
triple3
((triple5 triple1) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple5 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple5 ((((triple4 triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple5 ((((triple4 ((triple4) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((triple5 ((((triple4 ((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not kind.
False
1
inv-proof
[(triple3 OR ((triple5 triple1) -> rule6) OR ((triple5 ((triple7) -> rule8)) -> rule6) OR ((triple5 ((((triple4 triple2) -> rule4)) -> rule8)) -> rule6) OR ((triple5 ((((triple4 ((triple4) -> rule7)) -> rule4)) -> rule8)) -> rule6) OR ((triple5 ((((triple4 ((triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6))]
("Gary" "is" "kind" "-")
triple3
((triple5 triple1) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple5 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple5 ((((triple4 triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple5 ((((triple4 ((triple4) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((triple5 ((((triple4 ((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
@0: Gary is big.[(triple1 OR ((triple7) -> rule8) OR ((((triple3) -> rule1)) -> rule8) OR ((((triple4 triple2) -> rule4)) -> rule8) OR ((((triple4 ((triple4) -> rule7)) -> rule4)) -> rule8) OR ((((triple4 ((triple5) -> rule2)) -> rule4)) -> rule8))] Gary is cold.[(triple2 OR ((triple4) -> rule7) OR ((triple5) -> rule2))] Gary is kind.[(triple3 OR ((triple5 triple1) -> rule6) OR ((triple5 ((triple7) -> rule8)) -> rule6) OR ((triple5 ((((triple4 triple2) -> rule4)) -> rule8)) -> rule6) OR ((triple5 ((((triple4 ((triple4) -> rule7)) -> rule4)) -> rule8)) -> rule6) OR ((triple5 ((((triple4 ((triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6))] Gary is nice.[(triple4 OR ((triple7 triple2) -> rule3) OR ((triple7 ((triple5) -> rule2)) -> rule3) OR ((((triple3) -> rule1) triple2) -> rule3) OR ((((triple3) -> rule1) ((triple5) -> rule2)) -> rule3) OR ((((((triple5 triple1) -> rule6)) -> rule1) triple2) -> rule3) OR ((((((triple5 triple1) -> rule6)) -> rule1) ((triple5) -> rule2)) -> rule3))] Gary is round.[(triple5)] Gary is smart.[(triple6 OR ((triple5) -> rule5))] Gary is white.[(triple7 OR ((triple3) -> rule1) OR ((triple4 triple2) -> rule4) OR ((((triple5 triple1) -> rule6)) -> rule1) OR ((triple4 ((triple4) -> rule7)) -> rule4) OR ((triple4 ((triple5) -> rule2)) -> rule4))]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple7) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple4 triple2) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple4 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple2
((triple4) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple5) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple5 triple1) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple5 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple5 ((((triple4 triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple5 ((((triple4 ((triple4) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((triple5 ((((triple4 ((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
triple4
((triple7 triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple7 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple3) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((((triple5 triple1) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple5 triple1) -> (rule6 % int4))) -> (rule1 % int3)) ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple5) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple5 triple1) -> (rule6 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple4 ((triple4) -> (rule7 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple4 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2