Erin is big. Erin is cold. Erin is green. Erin is kind. Erin is nice. Erin is quiet. Erin is white. All green, quiet things are big. All nice, white things are quiet.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
All green, quiet things are big.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All nice, white things are quiet.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Erin is nice.
True
1
proof
[(triple5)]
("Erin" "is" "nice" "+")
triple5
Erin is not quiet.
False
1
inv-proof
[(triple6 OR ((triple5 triple7) -> rule2))]
("Erin" "is" "quiet" "-")
triple6
((triple5 triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
@0: Erin is big.[(triple1 OR ((triple3 triple6) -> rule1) OR ((triple3 ((triple5 triple7) -> rule2)) -> rule1))] Erin is cold.[(triple2)] Erin is green.[(triple3)] Erin is kind.[(triple4)] Erin is nice.[(triple5)] Erin is quiet.[(triple6 OR ((triple5 triple7) -> rule2))] Erin is white.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple3 triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
((triple5 triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple7