Erin is big. Erin is cold. Erin is nice. Erin is quiet. Erin is red. Erin is rough. Erin is smart. Gary is big. Gary is cold. Gary is nice. Gary is quiet. Gary is red. Gary is rough. Gary is smart. If something is rough then it is big. If Erin is smart then Erin is nice. Big, red things are rough.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Erin is smart then Erin is nice.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "nice" "+"))
Big, red things are rough.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Gary is smart.
True
1
proof
[(triple14)]
("Gary" "is" "smart" "+")
triple14
Gary is not red.
False
1
inv-proof
[(triple12)]
("Gary" "is" "red" "-")
triple12
@0: Erin is big.[(triple1 OR ((triple6) -> rule1))] Erin is cold.[(triple2)] Erin is nice.[(triple3 OR ((triple7) -> rule2))] Erin is quiet.[(triple4)] Erin is red.[(triple5)] Erin is rough.[(triple6 OR ((triple1 triple5) -> rule3))] Erin is smart.[(triple7)] Gary is big.[(triple8 OR ((triple13) -> rule1))] Gary is cold.[(triple9)] Gary is nice.[(triple10)] Gary is quiet.[(triple11)] Gary is red.[(triple12)] Gary is rough.[(triple13 OR ((triple8 triple12) -> rule3))] Gary is smart.[(triple14)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
((triple7) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple1 triple5) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple13) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple13
((triple8 triple12) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple14