Erin is green. Erin is kind. Erin is nice. Erin is red. Erin is rough. Erin is smart. Erin is young. Gary is green. Gary is kind. Gary is nice. Gary is red. Gary is rough. Gary is smart. Gary is young. All rough, red people are green.
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
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 smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
All rough, red people are green.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Gary is green.
True
1
proof
[(triple8 OR ((triple12 triple11) -> rule1))]
("Gary" "is" "green" "+")
triple8
((triple12 triple11) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is not rough.
False
1
inv-proof
[(triple5)]
("Erin" "is" "rough" "-")
triple5
@0: Erin is green.[(triple1 OR ((triple5 triple4) -> rule1))] Erin is kind.[(triple2)] Erin is nice.[(triple3)] Erin is red.[(triple4)] Erin is rough.[(triple5)] Erin is smart.[(triple6)] Erin is young.[(triple7)] Gary is green.[(triple8 OR ((triple12 triple11) -> rule1))] Gary is kind.[(triple9)] Gary is nice.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] Gary is smart.[(triple13)] Gary is young.[(triple14)]
Erin is green.
("Erin" "is" "green" "+")
triple1
((triple5 triple4) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple12 triple11) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14