Gary is big. Gary is cold. Gary is furry. Gary is green. Gary is red. Gary is smart. Gary is white. Harry is big. Harry is cold. Harry is furry. Harry is green. Harry is red. Harry is smart. Harry is white. Green things are cold. All furry, green things are smart.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All furry, green things are smart.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple13 OR ((triple10 triple11) -> rule2))]
("Harry" "is" "smart" "+")
triple13
((triple10 triple11) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not cold.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule1))]
("Harry" "is" "cold" "-")
triple9
((triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
@0: Gary is big.[(triple1)] Gary is cold.[(triple2 OR ((triple4) -> rule1))] Gary is furry.[(triple3)] Gary is green.[(triple4)] Gary is red.[(triple5)] Gary is smart.[(triple6 OR ((triple3 triple4) -> rule2))] Gary is white.[(triple7)] Harry is big.[(triple8)] Harry is cold.[(triple9 OR ((triple11) -> rule1))] Harry is furry.[(triple10)] Harry is green.[(triple11)] Harry is red.[(triple12)] Harry is smart.[(triple13 OR ((triple10 triple11) -> rule2))] Harry is white.[(triple14)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
((triple4) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple3 triple4) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
((triple10 triple11) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14