Charlie is big. Charlie is furry. Charlie is kind. Charlie is red. Charlie is smart. Charlie is white. Charlie is young. Gary is big. Gary is furry. Gary is red. Gary is smart. Gary is white. All furry people are kind. All kind people are young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Gary is smart.
True
1
proof
[(triple11)]
("Gary" "is" "smart" "+")
triple11
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Gary is kind.
True
2
proof
[(((triple9) -> rule1))]
("Gary" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple9) -> rule1))]
("Gary" "is" "kind" "-")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("Gary" "is" "young" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("Gary" "is" "young" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is kind.[(triple3 OR ((triple2) -> rule1))] Charlie is red.[(triple4)] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple3) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] Gary is big.[(triple8)] Gary is furry.[(triple9)] Gary is red.[(triple10)] Gary is smart.[(triple11)] Gary is white.[(triple12)] @1: Gary is kind.[(((triple9) -> rule1))] @2: Gary is young.[(((((triple9) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2