Erin is not blue. Erin is furry. Erin is not green. Erin is nice. Erin is smart. Harry is not blue. Harry is not furry. Harry is green. Harry is nice. Harry is round. Harry is smart. Harry is white. Smart things are white.
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Erin is not blue.
True
1
proof
[(triple1)]
("Erin" "is" "blue" "-")
triple1
Erin is green.
False
1
inv-proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Erin is white.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "white" "+")
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "white" "-")
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
@0: Erin is furry.[(triple2)] Erin is nice.[(triple4)] Erin is not blue.[(triple1)] Erin is not green.[(triple3)] Erin is smart.[(triple5)] Harry is green.[(triple8)] Harry is nice.[(triple9)] Harry is not blue.[(triple6)] Harry is not furry.[(triple7)] Harry is round.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12 OR ((triple11) -> rule1))] @1: Erin is white.[(((triple5) -> rule1))]
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is not blue.
("Erin" "is" "blue" "-")
triple1
Erin is not green.
("Erin" "is" "green" "-")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is not blue.
("Harry" "is" "blue" "-")
triple6
Harry is not furry.
("Harry" "is" "furry" "-")
triple7
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple11) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1