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