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