Erin is blue. Erin is cold. Erin is green. Erin is quiet. Erin is smart. Erin is white. Gary is cold. Gary is green. Gary is quiet. Gary is round. Gary is smart. Gary is white. Quiet, green things are blue. All smart, quiet things are cold.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Quiet, green things are blue.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All smart, quiet things are cold.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Erin is cold.
True
1
proof
[(triple2 OR ((triple5 triple4) -> rule2))]
("Erin" "is" "cold" "+")
triple2
((triple5 triple4) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not white.
False
1
inv-proof
[(triple6)]
("Erin" "is" "white" "-")
triple6
Gary is blue.
True
3
proof
[(((triple9 triple8) -> rule1))]
("Gary" "is" "blue" "+")
((triple9 triple8) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
3
inv-proof
[(((triple9 triple8) -> rule1))]
("Gary" "is" "blue" "-")
((triple9 triple8) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
@0: Erin is blue.[(triple1 OR ((triple4 triple3) -> rule1))] Erin is cold.[(triple2 OR ((triple5 triple4) -> rule2))] Erin is green.[(triple3)] Erin is quiet.[(triple4)] Erin is smart.[(triple5)] Erin is white.[(triple6)] Gary is cold.[(triple7 OR ((triple11 triple9) -> rule2))] Gary is green.[(triple8)] Gary is quiet.[(triple9)] Gary is round.[(triple10)] Gary is smart.[(triple11)] Gary is white.[(triple12)] @1: Gary is blue.[(((triple9 triple8) -> rule1))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple4 triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple5 triple4) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((triple11 triple9) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
((triple9 triple8) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1