Erin is big. Erin is cold. Erin is kind. Erin is nice. Erin is quiet. Erin is white. Gary is big. Gary is cold. Gary is kind. Gary is nice. Gary is quiet. Gary is rough. All cold people are big. All kind people are big. If Erin is not kind then Erin is cold. If Erin is quiet and Erin is cold then Erin is white. All quiet people are white. If Gary is white then Gary is rough. If someone is rough and not big then they are quiet. If someone is rough and not nice then they are quiet.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Erin is not kind then Erin is cold.
((("Erin" "is" "kind" "~")) -> ("Erin" "is" "cold" "+"))
If Erin is quiet and Erin is cold then Erin is white.
((("Erin" "is" "quiet" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Gary is white then Gary is rough.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "rough" "+"))
If someone is rough and not big then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "+"))
If someone is rough and not nice then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
Gary is nice.
True
1
proof
[(triple10)]
("Gary" "is" "nice" "+")
triple10
Gary is not quiet.
False
1
inv-proof
[(triple11)]
("Gary" "is" "quiet" "-")
triple11
Gary is white.
True
2
proof
[(((triple11) -> rule5))]
("Gary" "is" "white" "+")
((triple11) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple11) -> rule5))]
("Gary" "is" "white" "-")
((triple11) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
@0: Erin is big.[(triple1 OR ((triple2) -> rule1) OR ((triple3) -> rule2))] Erin is cold.[(triple2)] Erin is kind.[(triple3)] Erin is nice.[(triple4)] Erin is quiet.[(triple5)] Erin is white.[(triple6 OR ((triple5) -> rule5) OR ((triple5 triple2) -> rule4))] Gary is big.[(triple7 OR ((triple8) -> rule1) OR ((triple9) -> rule2))] Gary is cold.[(triple8)] Gary is kind.[(triple9)] Gary is nice.[(triple10)] Gary is quiet.[(triple11)] Gary is rough.[(triple12 OR ((((triple11) -> rule5)) -> rule6))] @1: Gary is white.[(((triple11) -> rule5))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5 triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((((triple11) -> (rule5 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple11) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1