Erin is cold. Erin is furry. Erin is kind. Erin is quiet. Erin is round. Erin is smart. Erin is white. Furry people are quiet. If Erin is smart and Erin is furry then Erin is cold. If someone is cold and kind then they are round. If Erin is kind and Erin is white then Erin is quiet. If someone is white then they are quiet. If Erin is cold then Erin is white.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is smart and Erin is furry then Erin is cold.
((("Erin" "is" "smart" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "cold" "+"))
If someone is cold and kind then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Erin is kind and Erin is white then Erin is quiet.
((("Erin" "is" "kind" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "quiet" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is cold then Erin is white.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
Erin is round.
True
1
proof
[(triple5 OR ((triple1 triple3) -> rule3) OR ((((triple6 triple2) -> rule2) triple3) -> rule3))]
("Erin" "is" "round" "+")
triple5
((triple1 triple3) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple6 triple2) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
@0: Erin is cold.[(triple1 OR ((triple6 triple2) -> rule2))] Erin is furry.[(triple2)] Erin is kind.[(triple3)] Erin is quiet.[(triple4 OR ((triple2) -> rule1) OR ((triple7) -> rule5) OR ((triple3 triple7) -> rule4) OR ((((triple1) -> rule6)) -> rule5) OR ((triple3 ((triple1) -> rule6)) -> rule4) OR ((((((triple6 triple2) -> rule2)) -> rule6)) -> rule5) OR ((triple3 ((((triple6 triple2) -> rule2)) -> rule6)) -> rule4))] Erin is round.[(triple5 OR ((triple1 triple3) -> rule3) OR ((((triple6 triple2) -> rule2) triple3) -> rule3))] Erin is smart.[(triple6)] Erin is white.[(triple7 OR ((triple1) -> rule6) OR ((((triple6 triple2) -> rule2)) -> rule6))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple6 triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((triple2) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple3 triple7) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple3 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple6 triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((triple3 ((((triple6 triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple1 triple3) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple6 triple2) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple6 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2