Erin is big. Erin is blue. Erin is cold. Erin is nice. Erin is quiet. Erin is smart. Erin is young. If Erin is young and Erin is smart then Erin is quiet. All young things are quiet. If something is blue and cold then it is smart.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If Erin is young and Erin is smart then Erin is quiet.
((("Erin" "is" "young" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "quiet" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is blue and cold then it is smart.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Erin is quiet.
True
1
proof
[(triple5 OR ((triple7) -> rule2) OR ((triple7 triple6) -> rule1) OR ((triple7 ((triple2 triple3) -> rule3)) -> rule1))]
("Erin" "is" "quiet" "+")
triple5
((triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple2 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not blue.
False
1
inv-proof
[(triple2)]
("Erin" "is" "blue" "-")
triple2
@0: Erin is big.[(triple1)] Erin is blue.[(triple2)] Erin is cold.[(triple3)] Erin is nice.[(triple4)] Erin is quiet.[(triple5 OR ((triple7) -> rule2) OR ((triple7 triple6) -> rule1) OR ((triple7 ((triple2 triple3) -> rule3)) -> rule1))] Erin is smart.[(triple6 OR ((triple2 triple3) -> rule3))] Erin is young.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple2 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple2 triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7