Erin is cold. Erin is green. Erin is kind. Erin is quiet. Erin is red. Erin is smart. Erin is young. Quiet, kind people are red. If Erin is young and Erin is kind then Erin is quiet. If someone is red and cold then they are kind.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Erin is young and Erin is kind then Erin is quiet.
((("Erin" "is" "young" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
If someone is red and cold then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Erin is red.
True
1
proof
[(triple5 OR ((triple4 triple3) -> rule1) OR ((((triple7 triple3) -> rule2) triple3) -> rule1))]
("Erin" "is" "red" "+")
triple5
((triple4 triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple7 triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not young.
False
1
inv-proof
[(triple7)]
("Erin" "is" "young" "-")
triple7
@0: Erin is cold.[(triple1)] Erin is green.[(triple2)] Erin is kind.[(triple3 OR ((triple5 triple1) -> rule3))] Erin is quiet.[(triple4 OR ((triple7 triple3) -> rule2) OR ((triple7 ((triple5 triple1) -> rule3)) -> rule2))] Erin is red.[(triple5 OR ((triple4 triple3) -> rule1) OR ((((triple7 triple3) -> rule2) triple3) -> rule1))] Erin is smart.[(triple6)] Erin is young.[(triple7)]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple5 triple1) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((triple7 triple3) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple5 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple4 triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple7 triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7