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