Erin is cold. Erin is not kind. Erin is quiet. Erin is white. Harry is cold. Harry is not kind. Harry is not quiet. Harry is round. Harry is smart. Harry is white. If Erin is white then Erin is round. All smart people are round. White people are smart. If Harry is white and Harry is not round then Harry is blue. If someone is cold and smart then they are blue. Kind, cold people are not blue. If someone is white and blue then they are cold. All white people are cold.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Erin is white then Erin is round.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "round" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Harry is white and Harry is not round then Harry is blue.
((("Harry" "is" "white" "+") ("Harry" "is" "round" "~")) -> ("Harry" "is" "blue" "+"))
If someone is cold and smart then they are blue.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Kind, cold people are not blue.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "-"))
If someone is white and blue then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple5 OR ((triple10) -> rule8))]
("Harry" "is" "cold" "+")
triple5
((triple10) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
1
inv-proof
[(triple5 OR ((triple10) -> rule8))]
("Harry" "is" "cold" "-")
triple5
((triple10) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is smart.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is not blue.
False
3
inv-proof
[(((triple5 triple9) -> rule5) OR ((triple5 ((triple10) -> rule3)) -> rule5) OR ((((triple10) -> rule8) triple9) -> rule5) OR ((((triple10) -> rule8) ((triple10) -> rule3)) -> rule5))]
("Harry" "is" "blue" "-")
((triple5 triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple5 ((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10) -> (rule8 % int2)) triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple10) -> (rule8 % int3)) ((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Erin is blue.
True
4
proof
[(((triple1 ((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule8) ((triple4) -> rule3)) -> rule5))]
("Erin" "is" "blue" "+")
((triple1 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not blue.
False
4
inv-proof
[(((triple1 ((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule8) ((triple4) -> rule3)) -> rule5))]
("Erin" "is" "blue" "-")
((triple1 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
@0: Erin is cold.[(triple1 OR ((triple4) -> rule8))] Erin is not kind.[(triple2)] Erin is quiet.[(triple3)] Erin is white.[(triple4)] Harry is cold.[(triple5 OR ((triple10) -> rule8))] Harry is not kind.[(triple6)] Harry is not quiet.[(triple7)] Harry is round.[(triple8 OR ((triple9) -> rule2) OR ((((triple10) -> rule3)) -> rule2))] Harry is smart.[(triple9 OR ((triple10) -> rule3))] Harry is white.[(triple10)] @1: Erin is round.[(((triple4) -> rule1) OR ((((triple4) -> rule3)) -> rule2))] Erin is smart.[(((triple4) -> rule3))] Harry is blue.[(((triple5 triple9) -> rule5) OR ((triple5 ((triple10) -> rule3)) -> rule5) OR ((((triple10) -> rule8) triple9) -> rule5) OR ((((triple10) -> rule8) ((triple10) -> rule3)) -> rule5))] @2: Erin is blue.[(((triple1 ((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule8) ((triple4) -> rule3)) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple4) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
((triple10) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
triple6
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple7
Harry is round.
("Harry" "is" "round" "+")
triple8
((triple9) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple9
((triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
((triple4) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple5 triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple5 ((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10) -> (rule8 % int2)) triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple10) -> (rule8 % int3)) ((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((triple1 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3