Gary is cold. Gary is kind. Gary is nice. Gary is round. Gary is smart. Gary is white. Gary is young. All white things are young. All nice, kind things are smart. Cold things are kind. If something is white then it is smart. If Gary is nice and Gary is young then Gary is smart. All young, white things are smart.
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" "+")
Gary is young.
("Gary" "is" "young" "+")
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All nice, kind things are smart.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is white then it is smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Gary is nice and Gary is young then Gary is smart.
((("Gary" "is" "nice" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "smart" "+"))
All young, white things are smart.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple5 OR ((triple6) -> rule4) OR ((triple3 triple2) -> rule2) OR ((triple3 triple7) -> rule5) OR ((triple7 triple6) -> rule6) OR ((triple3 ((triple1) -> rule3)) -> rule2) OR ((triple3 ((triple6) -> rule1)) -> rule5) OR ((((triple6) -> rule1) triple6) -> rule6))]
("Gary" "is" "smart" "+")
triple5
((triple6) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 triple7) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple7 triple6) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple3 ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not young.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule1))]
("Gary" "is" "young" "-")
triple7
((triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
@0: Gary is cold.[(triple1)] Gary is kind.[(triple2 OR ((triple1) -> rule3))] Gary is nice.[(triple3)] Gary is round.[(triple4)] Gary is smart.[(triple5 OR ((triple6) -> rule4) OR ((triple3 triple2) -> rule2) OR ((triple3 triple7) -> rule5) OR ((triple7 triple6) -> rule6) OR ((triple3 ((triple1) -> rule3)) -> rule2) OR ((triple3 ((triple6) -> rule1)) -> rule5) OR ((((triple6) -> rule1) triple6) -> rule6))] Gary is white.[(triple6)] Gary is young.[(triple7 OR ((triple6) -> rule1))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
((triple1) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
((triple6) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 triple7) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple7 triple6) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple3 ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1