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