Erin is blue. Erin is cold. Erin is green. Erin is round. Gary is blue. Gary is cold. Gary is not furry. Gary is green. Gary is kind. Gary is round. If someone is kind and cold then they are blue. If someone is kind then they are blue. If someone is blue then they are kind. If someone is furry and not green then they are not round. If someone is green and not kind then they are round. If someone is cold and kind then they are round. If someone is round and not blue then they are white. All round people are white.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is kind and cold then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry and not green then they are not round.
((("someone" "is" "furry" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "round" "-"))
If someone is green and not kind then they are round.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "round" "+"))
If someone is cold and kind then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not blue then they are white.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Gary is not furry.
True
1
proof
[(triple7)]
("Gary" "is" "furry" "-")
triple7
Gary is not cold.
False
1
inv-proof
[(triple6)]
("Gary" "is" "cold" "-")
triple6
@0: Erin is blue.[(triple1)] Erin is cold.[(triple2)] Erin is green.[(triple3)] Erin is round.[(triple4 OR ((triple2 ((triple1) -> rule3)) -> rule6))] Gary is blue.[(triple5 OR ((triple9) -> rule2) OR ((triple9 triple6) -> rule1))] Gary is cold.[(triple6)] Gary is green.[(triple8)] Gary is kind.[(triple9 OR ((triple5) -> rule3))] Gary is not furry.[(triple7)] Gary is round.[(triple10 OR ((triple6 triple9) -> rule6) OR ((triple6 ((triple5) -> rule3)) -> rule6))] @1: Erin is kind.[(((triple1) -> rule3))] Erin is white.[(((triple4) -> rule8) OR ((((triple2 ((triple1) -> rule3)) -> rule6)) -> rule8))] Gary is white.[(((triple10) -> rule8) OR ((((triple6 triple9) -> rule6)) -> rule8) OR ((((triple6 ((triple5) -> rule3)) -> rule6)) -> rule8))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple5
((triple9) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple9 triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
((triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple10
((triple6 triple9) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple10) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple6 triple9) -> (rule6 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple6 ((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3