Gary is big. Gary is kind. Gary is red. Gary is white. Gary is young. Harry is big. Harry is kind. Harry is red. Harry is not rough. Harry is smart. Harry is white. Harry is young. If someone is red and white then they are smart. If someone is smart and not young then they are rough.
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is red and white then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not young then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "+"))
Harry is smart.
True
1
proof
[(triple10 OR ((triple8 triple11) -> rule1))]
("Harry" "is" "smart" "+")
triple10
((triple8 triple11) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is smart.
True
3
proof
[(((triple3 triple4) -> rule1))]
("Gary" "is" "smart" "+")
((triple3 triple4) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
3
inv-proof
[(((triple3 triple4) -> rule1))]
("Gary" "is" "smart" "-")
((triple3 triple4) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
@0: Gary is big.[(triple1)] Gary is kind.[(triple2)] Gary is red.[(triple3)] Gary is white.[(triple4)] Gary is young.[(triple5)] Harry is big.[(triple6)] Harry is kind.[(triple7)] Harry is not rough.[(triple9)] Harry is red.[(triple8)] Harry is smart.[(triple10 OR ((triple8 triple11) -> rule1))] Harry is white.[(triple11)] Harry is young.[(triple12)] @1: Gary is smart.[(((triple3 triple4) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is not rough.
("Harry" "is" "rough" "-")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple8 triple11) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
((triple3 triple4) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1