Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is red. Gary is round. Gary is smart. Smart, big people are red. All blue people are red. If someone is kind then they are cold. Cold people are big. All smart people are cold. If someone is cold and kind then they are big. Red people are big. If Gary is blue and Gary is red then Gary is cold.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Smart, big people are red.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and kind then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Gary is blue and Gary is red then Gary is cold.
((("Gary" "is" "blue" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "cold" "+"))
Gary is cold.
True
1
proof
[(triple3 OR ((triple4) -> rule3) OR ((triple7) -> rule5) OR ((triple2 triple5) -> rule8) OR ((triple2 ((triple2) -> rule2)) -> rule8) OR ((triple2 ((triple7 triple1) -> rule1)) -> rule8))]
("Gary" "is" "cold" "+")
triple3
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple7) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple2 triple5) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple2 ((triple7 triple1) -> (rule1 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not red.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule2) OR ((triple7 triple1) -> rule1) OR ((triple7 ((triple3) -> rule4)) -> rule1) OR ((triple7 ((triple3 triple4) -> rule6)) -> rule1) OR ((triple7 ((((triple4) -> rule3)) -> rule4)) -> rule1) OR ((triple7 ((((triple7) -> rule5)) -> rule4)) -> rule1) OR ((triple7 ((((triple4) -> rule3) triple4) -> rule6)) -> rule1) OR ((triple7 ((((triple7) -> rule5) triple4) -> rule6)) -> rule1))]
("Gary" "is" "red" "-")
triple5
((triple2) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple7 triple1) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple7 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple7 ((triple3 triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple7 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple4) -> (rule3 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple7) -> (rule5 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
@0: Gary is big.[(triple1 OR ((triple3) -> rule4) OR ((triple5) -> rule7) OR ((triple3 triple4) -> rule6) OR ((((triple2) -> rule2)) -> rule7) OR ((((triple4) -> rule3)) -> rule4) OR ((((triple7) -> rule5)) -> rule4) OR ((((triple2 triple5) -> rule8)) -> rule4) OR ((((triple4) -> rule3) triple4) -> rule6) OR ((((triple7) -> rule5) triple4) -> rule6) OR ((((triple2 triple5) -> rule8) triple4) -> rule6) OR ((((triple2 ((triple2) -> rule2)) -> rule8)) -> rule4) OR ((((triple2 ((triple2) -> rule2)) -> rule8) triple4) -> rule6))] Gary is blue.[(triple2)] Gary is cold.[(triple3 OR ((triple4) -> rule3) OR ((triple7) -> rule5) OR ((triple2 triple5) -> rule8) OR ((triple2 ((triple2) -> rule2)) -> rule8) OR ((triple2 ((triple7 triple1) -> rule1)) -> rule8))] Gary is kind.[(triple4)] Gary is red.[(triple5 OR ((triple2) -> rule2) OR ((triple7 triple1) -> rule1) OR ((triple7 ((triple3) -> rule4)) -> rule1) OR ((triple7 ((triple3 triple4) -> rule6)) -> rule1) OR ((triple7 ((((triple4) -> rule3)) -> rule4)) -> rule1) OR ((triple7 ((((triple7) -> rule5)) -> rule4)) -> rule1) OR ((triple7 ((((triple4) -> rule3) triple4) -> rule6)) -> rule1) OR ((triple7 ((((triple7) -> rule5) triple4) -> rule6)) -> rule1))] Gary is round.[(triple6)] Gary is smart.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple5) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple3 triple4) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple2 triple5) -> (rule8 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple7) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple2 triple5) -> (rule8 % int2)) triple4) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule8 % int2)) triple4) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple7) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple2 triple5) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple2 ((triple7 triple1) -> (rule1 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple2) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple7 triple1) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple7 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple7 ((triple3 triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple7 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple4) -> (rule3 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple7) -> (rule5 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7