Gary is big. Gary is blue. Gary is cold. Gary is not quiet. Gary is red. Gary is smart. Gary is not young. Big people are red. All big people are red. If someone is red and not cold then they are smart. If Gary is red then Gary is blue. Quiet, red people are not big. All smart people are big. All smart, quiet people are blue. If someone is red and not cold then they are not blue.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not young.
("Gary" "is" "young" "-")
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is red and not cold then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "smart" "+"))
If Gary is red then Gary is blue.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "blue" "+"))
Quiet, red people are not big.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "-"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All smart, quiet people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and not cold then they are not blue.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "blue" "-"))
Gary is blue.
True
1
proof
[(triple2 OR ((triple5) -> rule4) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple6) -> rule6)) -> rule1)) -> rule4) OR ((((((triple6) -> rule6)) -> rule2)) -> rule4))]
("Gary" "is" "blue" "+")
triple2
((triple5) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not big.
False
1
inv-proof
[(triple1 OR ((triple6) -> rule6))]
("Gary" "is" "big" "-")
triple1
((triple6) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
@0: Gary is big.[(triple1 OR ((triple6) -> rule6))] Gary is blue.[(triple2 OR ((triple5) -> rule4) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple6) -> rule6)) -> rule1)) -> rule4) OR ((((((triple6) -> rule6)) -> rule2)) -> rule4))] Gary is cold.[(triple3)] Gary is not quiet.[(triple4)] Gary is not young.[(triple7)] Gary is red.[(triple5 OR ((triple1) -> rule1) OR ((triple1) -> rule2) OR ((((triple6) -> rule6)) -> rule1) OR ((((triple6) -> rule6)) -> rule2))] Gary is smart.[(triple6)]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple6) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
((triple5) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple4
Gary is not young.
("Gary" "is" "young" "-")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple1) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple1) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple6