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