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