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