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