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