Erin is blue. Erin is quiet. Erin is red. Erin is rough. Erin is round. Erin is smart. Erin is young. All smart, quiet things are blue. Red, smart things are quiet. All smart things are round.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All smart, quiet things are blue.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Red, smart things are quiet.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Erin is not smart.
False
1
inv-proof
[(triple6)]
("Erin" "is" "smart" "-")
triple6
@0: Erin is blue.[(triple1 OR ((triple6 triple2) -> rule1) OR ((triple6 ((triple3 triple6) -> rule2)) -> rule1))] Erin is quiet.[(triple2 OR ((triple3 triple6) -> rule2))] Erin is red.[(triple3)] Erin is rough.[(triple4)] Erin is round.[(triple5 OR ((triple6) -> rule3))] Erin is smart.[(triple6)] Erin is young.[(triple7)]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple6 triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple6 ((triple3 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
((triple3 triple6) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple6) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7