Erin is big. Erin is cold. Erin is green. Erin is not kind. Erin is red. Erin is rough. Erin is smart. Cold things are green. If something is red then it is green. If something is big and green then it is red. If Erin is not kind and Erin is not big then Erin is cold. If something is green then it is smart. If Erin is rough and Erin is not red then Erin is not smart. If Erin is green and Erin is rough then Erin is smart. If Erin is kind then Erin is smart.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is big and green then it is red.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Erin is not kind and Erin is not big then Erin is cold.
((("Erin" "is" "kind" "~") ("Erin" "is" "big" "~")) -> ("Erin" "is" "cold" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Erin is rough and Erin is not red then Erin is not smart.
((("Erin" "is" "rough" "+") ("Erin" "is" "red" "~")) -> ("Erin" "is" "smart" "-"))
If Erin is green and Erin is rough then Erin is smart.
((("Erin" "is" "green" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
If Erin is kind then Erin is smart.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "smart" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple5 OR ((triple1 triple3) -> rule3) OR ((triple1 ((triple2) -> rule1)) -> rule3))]
("Erin" "is" "red" "-")
triple5
((triple1 triple3) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple1 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
@0: Erin is big.[(triple1)] Erin is cold.[(triple2)] Erin is green.[(triple3 OR ((triple2) -> rule1) OR ((triple5) -> rule2))] Erin is not kind.[(triple4)] Erin is red.[(triple5 OR ((triple1 triple3) -> rule3) OR ((triple1 ((triple2) -> rule1)) -> rule3))] Erin is rough.[(triple6)] Erin is smart.[(triple7 OR ((triple3) -> rule5) OR ((triple3 triple6) -> rule7) OR ((((triple2) -> rule1)) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((triple2) -> rule1) triple6) -> rule7) OR ((((triple5) -> rule2) triple6) -> rule7))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
((triple2) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple1 triple3) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple1 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple3) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple3 triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple2) -> (rule1 % int2)) triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple5) -> (rule2 % int2)) triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2