Erin is cold. Erin is kind. Erin is nice. Erin is quiet. Erin is red. Erin is rough. Erin is smart. If someone is quiet then they are kind. If Erin is quiet then Erin is smart. Cold, smart people are kind. All cold, rough people are kind. Kind, red people are smart. If someone is nice and kind then they are quiet.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Erin is quiet then Erin is smart.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "smart" "+"))
Cold, smart people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All cold, rough people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Kind, red people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice and kind then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Erin is quiet.
True
1
proof
[(triple4 OR ((triple3 triple2) -> rule6) OR ((triple3 ((triple1 triple6) -> rule4)) -> rule6) OR ((triple3 ((triple1 triple7) -> rule3)) -> rule6))]
("Erin" "is" "quiet" "+")
triple4
((triple3 triple2) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple3 ((triple1 triple6) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple3 ((triple1 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not kind.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule1) OR ((triple1 triple6) -> rule4) OR ((triple1 triple7) -> rule3) OR ((triple1 ((triple4) -> rule2)) -> rule3))]
("Erin" "is" "kind" "-")
triple2
((triple4) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 triple7) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
@0: Erin is cold.[(triple1)] Erin is kind.[(triple2 OR ((triple4) -> rule1) OR ((triple1 triple6) -> rule4) OR ((triple1 triple7) -> rule3) OR ((triple1 ((triple4) -> rule2)) -> rule3))] Erin is nice.[(triple3)] Erin is quiet.[(triple4 OR ((triple3 triple2) -> rule6) OR ((triple3 ((triple1 triple6) -> rule4)) -> rule6) OR ((triple3 ((triple1 triple7) -> rule3)) -> rule6))] Erin is red.[(triple5)] Erin is rough.[(triple6)] Erin is smart.[(triple7 OR ((triple4) -> rule2) OR ((triple2 triple5) -> rule5) OR ((((triple3 triple2) -> rule6)) -> rule2) OR ((((triple4) -> rule1) triple5) -> rule5) OR ((((triple1 triple6) -> rule4) triple5) -> rule5) OR ((((triple3 ((triple1 triple6) -> rule4)) -> rule6)) -> rule2))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
((triple4) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 triple7) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((triple3 triple2) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple3 ((triple1 triple6) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple3 ((triple1 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple4) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple2 triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple4) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple1 triple6) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 ((triple1 triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3