Erin is blue. Erin is kind. Erin is not nice. Erin is quiet. Erin is rough. Erin is round. Erin is smart. If Erin is smart then Erin is rough. If someone is rough and blue then they are round. If someone is smart then they are quiet.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is smart then Erin is rough.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "rough" "+"))
If someone is rough and blue then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Erin is rough.
True
1
proof
[(triple5 OR ((triple7) -> rule1))]
("Erin" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not round.
False
1
inv-proof
[(triple6 OR ((triple5 triple1) -> rule2) OR ((((triple7) -> rule1) triple1) -> rule2))]
("Erin" "is" "round" "-")
triple6
((triple5 triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple7) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
@0: Erin is blue.[(triple1)] Erin is kind.[(triple2)] Erin is not nice.[(triple3)] Erin is quiet.[(triple4 OR ((triple7) -> rule3))] Erin is rough.[(triple5 OR ((triple7) -> rule1))] Erin is round.[(triple6 OR ((triple5 triple1) -> rule2) OR ((((triple7) -> rule1) triple1) -> rule2))] Erin is smart.[(triple7)]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is not nice.
("Erin" "is" "nice" "-")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple5 triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple7) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple7