Gary is big. Gary is blue. Gary is kind. Gary is red. Gary is smart. Gary is white. Gary is young. Harry is kind. Harry is red. Harry is smart. Harry is white. Harry is young. If something is smart then it is kind. Young, smart things are big. All smart, big things are blue.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Young, smart things are big.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All smart, big things are blue.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Harry is not white.
False
1
inv-proof
[(triple11)]
("Harry" "is" "white" "-")
triple11
Harry is big.
True
3
proof
[(((triple12 triple10) -> rule2))]
("Harry" "is" "big" "+")
((triple12 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
3
inv-proof
[(((triple12 triple10) -> rule2))]
("Harry" "is" "big" "-")
((triple12 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
True
5
proof
[(((triple10 ((triple12 triple10) -> rule2)) -> rule3))]
("Harry" "is" "blue" "+")
((triple10 ((triple12 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not blue.
False
5
inv-proof
[(((triple10 ((triple12 triple10) -> rule2)) -> rule3))]
("Harry" "is" "blue" "-")
((triple10 ((triple12 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
@0: Gary is big.[(triple1 OR ((triple7 triple5) -> rule2))] Gary is blue.[(triple2 OR ((triple5 triple1) -> rule3) OR ((triple5 ((triple7 triple5) -> rule2)) -> rule3))] Gary is kind.[(triple3 OR ((triple5) -> rule1))] Gary is red.[(triple4)] Gary is smart.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7)] Harry is kind.[(triple8 OR ((triple10) -> rule1))] Harry is red.[(triple9)] Harry is smart.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12)] @1: Harry is big.[(((triple12 triple10) -> rule2))] @2: Harry is blue.[(((triple10 ((triple12 triple10) -> rule2)) -> rule3))]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple7 triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
((triple5 triple1) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple5 ((triple7 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple5) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple10) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
((triple12 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple10 ((triple12 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2