Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is quiet. Gary is young. Harry is big. Harry is not cold. Harry is kind. Harry is nice. Harry is not quiet. Harry is young. If something is young and big then it is kind. If something is cold and not blue then it is quiet. If something is blue then it is quiet. If something is blue then it is cold. All kind, young things are big. If something is young and not kind then it is not nice.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is young.
("Harry" "is" "young" "+")
If something is young and big then it is kind.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is cold and not blue then it is quiet.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All kind, young things are big.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is young and not kind then it is not nice.
((("something" "is" "young" "+") ("something" "is" "kind" "~")) -> ("something" "is" "nice" "-"))
Harry is nice.
True
1
proof
[(triple10)]
("Harry" "is" "nice" "+")
triple10
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
Gary is big.
True
3
proof
[(((triple3 triple6) -> rule5))]
("Gary" "is" "big" "+")
((triple3 triple6) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
3
inv-proof
[(((triple3 triple6) -> rule5))]
("Gary" "is" "big" "-")
((triple3 triple6) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
@0: Gary is blue.[(triple1)] Gary is cold.[(triple2 OR ((triple1) -> rule4))] Gary is kind.[(triple3)] Gary is nice.[(triple4)] Gary is quiet.[(triple5 OR ((triple1) -> rule3))] Gary is young.[(triple6)] Harry is big.[(triple7 OR ((triple9 triple12) -> rule5))] Harry is kind.[(triple9 OR ((triple12 triple7) -> rule1))] Harry is nice.[(triple10)] Harry is not cold.[(triple8)] Harry is not quiet.[(triple11)] Harry is young.[(triple12)] @1: Gary is big.[(((triple3 triple6) -> rule5))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
((triple1) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
((triple1) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple9 triple12) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple12 triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not cold.
("Harry" "is" "cold" "-")
triple8
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Gary is big.
("Gary" "is" "big" "+")
((triple3 triple6) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1