Erin is big. Erin is cold. Erin is green. Erin is kind. Erin is quiet. Erin is smart. Erin is white. If Erin is green and Erin is big then Erin is kind. If someone is green then they are cold. All smart people are white. If Erin is smart then Erin is big. Cold people are smart. All kind people are cold.
Erin is big.
("Erin" "is" "big" "+")
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 smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If Erin is green and Erin is big then Erin is kind.
((("Erin" "is" "green" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "kind" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If Erin is smart then Erin is big.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "big" "+"))
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Erin is smart.
True
1
proof
[(triple6 OR ((triple2) -> rule5) OR ((((triple3) -> rule2)) -> rule5) OR ((((triple4) -> rule6)) -> rule5) OR ((((((triple3 triple1) -> rule1)) -> rule6)) -> rule5))]
("Erin" "is" "smart" "+")
triple6
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple3 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not cold.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule2) OR ((triple4) -> rule6) OR ((((triple3 triple1) -> rule1)) -> rule6) OR ((((triple3 ((triple6) -> rule4)) -> rule1)) -> rule6))]
("Erin" "is" "cold" "-")
triple2
((triple3) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple3 triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 ((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
@0: Erin is big.[(triple1 OR ((triple6) -> rule4) OR ((((triple2) -> rule5)) -> rule4) OR ((((((triple3) -> rule2)) -> rule5)) -> rule4) OR ((((((triple4) -> rule6)) -> rule5)) -> rule4))] Erin is cold.[(triple2 OR ((triple3) -> rule2) OR ((triple4) -> rule6) OR ((((triple3 triple1) -> rule1)) -> rule6) OR ((((triple3 ((triple6) -> rule4)) -> rule1)) -> rule6))] Erin is green.[(triple3)] Erin is kind.[(triple4 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple6) -> rule4)) -> rule1) OR ((triple3 ((((triple2) -> rule5)) -> rule4)) -> rule1) OR ((triple3 ((((((triple3) -> rule2)) -> rule5)) -> rule4)) -> rule1))] Erin is quiet.[(triple5)] Erin is smart.[(triple6 OR ((triple2) -> rule5) OR ((((triple3) -> rule2)) -> rule5) OR ((((triple4) -> rule6)) -> rule5) OR ((((((triple3 triple1) -> rule1)) -> rule6)) -> rule5))] Erin is white.[(triple7 OR ((triple6) -> rule3) OR ((((triple2) -> rule5)) -> rule3) OR ((((((triple3) -> rule2)) -> rule5)) -> rule3) OR ((((((triple4) -> rule6)) -> rule5)) -> rule3) OR ((((((((triple3 triple1) -> rule1)) -> rule6)) -> rule5)) -> rule3))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple6) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple3) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple3 triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 ((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple3 triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple3 ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple3 ((((((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple3 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple6) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple3 triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4